-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Improve reporting of related locations #4929
Merged
keyboardDrummer
merged 11 commits into
dafny-lang:master
from
keyboardDrummer:reportingRefactoring
Jan 10, 2024
Merged
Changes from all commits
Commits
Show all changes
11 commits
Select commit
Hold shift + click to select a range
ee045e4
Refactor reporting code
keyboardDrummer 77b85b2
Update expect file
keyboardDrummer 4d3e527
Fix expect files
keyboardDrummer 09f3db3
Extract classes into separate files
keyboardDrummer 86513c4
Extract Util into a separate file and rename to DiagnosticUtil
keyboardDrummer 247baa0
Merge remote-tracking branch 'origin/master' into reportingRefactoring
keyboardDrummer cc4002a
Update expect file
keyboardDrummer c46a475
Fix warning
keyboardDrummer 2af5260
Merge branch 'master' into reportingRefactoring
keyboardDrummer 946aa41
Merge branch 'master' into reportingRefactoring
keyboardDrummer bb25495
Merge branch 'master' into reportingRefactoring
keyboardDrummer File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,76 @@ | ||
using System.Collections.Generic; | ||
using System.Diagnostics.Contracts; | ||
|
||
namespace Microsoft.Dafny; | ||
|
||
public class MapType : CollectionType { | ||
public bool Finite { | ||
get { return finite; } | ||
set { finite = value; } | ||
} | ||
private bool finite; | ||
public Type Range { | ||
get { return range; } | ||
} | ||
private Type range; | ||
public override void SetTypeArgs(Type domain, Type range) { | ||
base.SetTypeArgs(domain, range); | ||
Contract.Assume(this.range == null); // Can only set once. This is really a precondition. | ||
this.range = range; | ||
} | ||
public MapType(bool finite, Type domain, Type range) : base(domain, range) { | ||
Contract.Requires((domain == null && range == null) || (domain != null && range != null)); | ||
this.finite = finite; | ||
this.range = range; | ||
} | ||
public Type Domain { | ||
get { return Arg; } | ||
} | ||
public override string CollectionTypeName { get { return finite ? "map" : "imap"; } } | ||
[System.Diagnostics.Contracts.Pure] | ||
public override string TypeName(DafnyOptions options, ModuleDefinition context, bool parseAble) { | ||
Contract.Ensures(Contract.Result<string>() != null); | ||
var targs = HasTypeArg() ? this.TypeArgsToString(options, context, parseAble) : ""; | ||
return CollectionTypeName + targs; | ||
} | ||
public override bool Equals(Type that, bool keepConstraints = false) { | ||
var t = that.NormalizeExpand(keepConstraints) as MapType; | ||
return t != null && Finite == t.Finite && Arg.Equals(t.Arg, keepConstraints) && Range.Equals(t.Range, keepConstraints); | ||
} | ||
|
||
public override Type Subst(IDictionary<TypeParameter, Type> subst) { | ||
var dom = Domain.Subst(subst); | ||
if (dom is InferredTypeProxy) { | ||
((InferredTypeProxy)dom).KeepConstraints = true; | ||
} | ||
var ran = Range.Subst(subst); | ||
if (ran is InferredTypeProxy) { | ||
((InferredTypeProxy)ran).KeepConstraints = true; | ||
} | ||
if (dom == Domain && ran == Range) { | ||
return this; | ||
} else { | ||
return new MapType(Finite, dom, ran); | ||
} | ||
} | ||
|
||
public override Type ReplaceTypeArguments(List<Type> arguments) { | ||
return new MapType(Finite, arguments[0], arguments[1]); | ||
} | ||
|
||
public override bool SupportsEquality { | ||
get { | ||
// A map type supports equality if both its Keys type and Values type does. It is checked | ||
// that the Keys type always supports equality, so we only need to check the Values type here. | ||
return range.SupportsEquality; | ||
} | ||
} | ||
public override bool ComputeMayInvolveReferences(ISet<DatatypeDecl> visitedDatatypes) { | ||
return Domain.ComputeMayInvolveReferences(visitedDatatypes) || Range.ComputeMayInvolveReferences(visitedDatatypes); | ||
} | ||
|
||
public override BinaryExpr.ResolvedOpcode ResolvedOpcodeForIn => BinaryExpr.ResolvedOpcode.InMap; | ||
public override ComprehensionExpr.CollectionBoundedPool GetBoundedPool(Expression source) { | ||
return new ComprehensionExpr.MapBoundedPool(source, Domain, Domain, Finite); | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -61,9 +61,10 @@ private static JsonObject SerializeRelated(Boogie.IToken tok, string? category, | |
} | ||
|
||
private static IEnumerable<JsonNode> SerializeInnerTokens(Boogie.IToken tok) { | ||
while (tok is NestedToken ntok) { | ||
tok = ntok.Inner; | ||
yield return SerializeRelated(tok, null, "Related location"); | ||
while (tok is NestedToken nestedToken) { | ||
tok = nestedToken.Inner; | ||
var message = nestedToken.Message != null ? "Related location: " + nestedToken.Message : "Related location"; | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Good job updating this! I don't think it is tested, is it? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It is, in |
||
yield return SerializeRelated(tok, null, message); | ||
} | ||
} | ||
|
||
|
@@ -112,7 +113,7 @@ public DafnyJsonConsolePrinter(DafnyOptions options) : base(options) { | |
public class JsonConsoleErrorReporter : BatchErrorReporter { | ||
protected override bool MessageCore(MessageSource source, ErrorLevel level, string errorID, Dafny.IToken tok, string msg) { | ||
if (base.MessageCore(source, level, errorID, tok, msg) && (Options is { PrintTooltips: true } || level != ErrorLevel.Info)) { | ||
new DiagnosticMessageData(source, level, tok, null, msg, null).WriteJsonTo(Options.OutputWriter); | ||
new DiagnosticMessageData(source, level, tok, level == ErrorLevel.Error ? "Error" : null, msg, null).WriteJsonTo(Options.OutputWriter); | ||
return true; | ||
} | ||
|
||
|
@@ -121,4 +122,4 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri | |
|
||
public JsonConsoleErrorReporter(DafnyOptions options) : base(options) { | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Makes sense, thanks for doing that!