diff --git a/Source/DafnyCore.Test/ClonerTest.cs b/Source/DafnyCore.Test/ClonerTest.cs index 8baed8026fc..457719ae009 100644 --- a/Source/DafnyCore.Test/ClonerTest.cs +++ b/Source/DafnyCore.Test/ClonerTest.cs @@ -11,7 +11,7 @@ class DummyDecl : Declaration { public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) { } - public DummyDecl(RangeToken rangeOrigin, Name name, Attributes attributes, bool isRefining) : base(rangeOrigin, name, + public DummyDecl(IOrigin rangeOrigin, Name name, Attributes attributes, bool isRefining) : base(rangeOrigin, name, attributes, isRefining) { } diff --git a/Source/DafnyCore.Test/NodeTests.cs b/Source/DafnyCore.Test/NodeTests.cs index b3ec1b1754c..300a40770cb 100644 --- a/Source/DafnyCore.Test/NodeTests.cs +++ b/Source/DafnyCore.Test/NodeTests.cs @@ -6,12 +6,12 @@ namespace DafnyCore.Test; public class NodeTests { class ConcreteNode : Node { - public ConcreteNode(RangeToken rangeOrigin, IEnumerable? children = null) { + public ConcreteNode(IOrigin rangeOrigin, IEnumerable? children = null) { Origin = rangeOrigin; Children = children ?? Enumerable.Empty(); } - public override RangeToken Origin { get; set; } + public override IOrigin Origin { get; set; } public override IOrigin Tok => Origin.StartToken; public override IEnumerable Children { get; } public override IEnumerable PreResolveChildren => Children; diff --git a/Source/DafnyCore/AST/Cloner.cs b/Source/DafnyCore/AST/Cloner.cs index d5f7a2ea8af..80cd709a85d 100644 --- a/Source/DafnyCore/AST/Cloner.cs +++ b/Source/DafnyCore/AST/Cloner.cs @@ -269,7 +269,7 @@ public virtual Type CloneType(Type t) { public virtual Formal CloneFormal(Formal formal, bool isReference) { return (Formal)clones.GetOrCreate(formal, () => isReference ? formal - : new Formal(Origin(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost, + : new Formal(Origin(formal.tok), new Name(this, formal.NameNode), CloneType(formal.Type), formal.InParam, formal.IsGhost, CloneExpr(formal.DefaultValue), CloneAttributes(formal.Attributes), formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) { Origin = formal.Origin, @@ -283,7 +283,7 @@ public virtual BoundVar CloneBoundVar(BoundVar bv, bool isReference) { return bv; } - var bvNew = new BoundVar(Origin(bv.tok), bv.Name, CloneType(bv.SyntacticType)); + var bvNew = new BoundVar(Origin(bv.tok), new Name(this, bv.NameNode), CloneType(bv.SyntacticType)); bvNew.IsGhost = bv.IsGhost; return bvNew; }); @@ -596,14 +596,11 @@ public virtual BlockStmt CloneMethodBody(Method m) { } } - public virtual RangeToken Origin(RangeToken range) { - if (range == null) { + public virtual IOrigin Origin(IOrigin tok) { + if (tok == null) { return null; } - return new RangeToken(Origin(range.StartToken), Origin(range.EndToken)); - } - public virtual IOrigin Origin(IOrigin tok) { Contract.Requires(tok != null); return tok; } diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs index 0d26b29540f..e1a9f3c481d 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplyExpr.cs @@ -18,15 +18,15 @@ public override IEnumerable SubExpressions { } } - public IOrigin CloseParen; + public Token CloseParen; public ApplyExpr(Cloner cloner, ApplyExpr original) : base(cloner, original) { Function = cloner.CloneExpr(original.Function); Args = original.Args.ConvertAll(cloner.CloneExpr); - CloseParen = cloner.Origin(original.CloseParen); + CloseParen = original.CloseParen; } - public ApplyExpr(IOrigin tok, Expression fn, List args, IOrigin closeParen) + public ApplyExpr(IOrigin tok, Expression fn, List args, Token closeParen) : base(tok) { Function = fn; Args = args; diff --git a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs index 30324b52573..d4ffd7f61a8 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/ApplySuffix.cs @@ -9,7 +9,7 @@ namespace Microsoft.Dafny; /// public class ApplySuffix : SuffixExpr, ICloneable, ICanFormat { public readonly IOrigin/*?*/ AtTok; - public readonly IOrigin CloseParen; + public readonly Token CloseParen; public readonly ActualBindings Bindings; public List Args => Bindings.Arguments; [FilledInDuringResolution] public MethodCallInformation MethodCallInfo = null; // resolution will set to a non-null value if ApplySuffix makes a method call @@ -30,12 +30,12 @@ public ApplySuffix Clone(Cloner cloner) { public ApplySuffix(Cloner cloner, ApplySuffix original) : base(cloner, original) { AtTok = original.AtTok == null ? null : cloner.Origin(original.AtTok); - CloseParen = cloner.Origin(original.CloseParen); + CloseParen = original.CloseParen; FormatTokens = original.FormatTokens; Bindings = new ActualBindings(cloner, original.Bindings); } - public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List args, IOrigin closeParen) + public ApplySuffix(IOrigin tok, IOrigin/*?*/ atLabel, Expression lhs, List args, Token closeParen) : base(tok, lhs) { Contract.Requires(tok != null); Contract.Requires(lhs != null); @@ -69,7 +69,7 @@ public override IEnumerable PreResolveSubExpressions { public static Expression MakeRawApplySuffix(IOrigin tok, string name, List args) { var nameExpr = new NameSegment(tok, name, null); var argBindings = args.ConvertAll(arg => new ActualBinding(null, arg)); - return new ApplySuffix(tok, null, nameExpr, argBindings, tok); + return new ApplySuffix(tok, null, nameExpr, argBindings, Token.NoToken); } public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) { diff --git a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs index fd7726d5260..7afdea881e3 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/FunctionCallExpr.cs @@ -8,7 +8,7 @@ public class FunctionCallExpr : Expression, IHasReferences, ICloneable Args => Bindings.Arguments; @@ -74,7 +74,7 @@ void ObjectInvariant() { [FilledInDuringResolution] public Function Function; - public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] List args, Label/*?*/ atLabel = null) + public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List args, Label/*?*/ atLabel = null) : this(tok, fn, receiver, openParen, closeParen, new ActualBindings(args), atLabel) { Contract.Requires(tok != null); Contract.Requires(fn != null); @@ -84,7 +84,7 @@ public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin ope Contract.Ensures(type == null); } - public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null) + public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] ActualBindings bindings, Label/*?*/ atLabel = null) : base(tok) { Contract.Requires(tok != null); Contract.Requires(fn != null); @@ -106,7 +106,7 @@ public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin ope /// This constructor is intended to be used when constructing a resolved FunctionCallExpr. The "args" are expected /// to be already resolved, and are all given positionally. /// - public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, IOrigin closeParen, [Captured] List args, + public FunctionCallExpr(IOrigin tok, string fn, Expression receiver, IOrigin openParen, Token closeParen, [Captured] List args, Label /*?*/ atLabel = null) : this(tok, fn, receiver, openParen, closeParen, args.ConvertAll(e => new ActualBinding(null, e)), atLabel) { Bindings.AcceptArgumentExpressionsAsExactParameterList(); @@ -120,7 +120,7 @@ public FunctionCallExpr(Cloner cloner, FunctionCallExpr original) : base(cloner, Name = original.Name; Receiver = cloner.CloneExpr(original.Receiver); OpenParen = original.OpenParen == null ? null : cloner.Origin(original.OpenParen); - CloseParen = original.CloseParen == null ? null : cloner.Origin(original.CloseParen); + CloseParen = original.CloseParen; Bindings = new ActualBindings(cloner, original.Bindings); AtLabel = original.AtLabel; diff --git a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs b/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs index ca12f2f62db..434ebbd70ae 100644 --- a/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Applications/SeqSelectExpr.cs @@ -8,14 +8,14 @@ public class SeqSelectExpr : Expression, ICloneable { public readonly Expression Seq; public readonly Expression E0; public readonly Expression E1; - public readonly IOrigin CloseParen; + public readonly Token CloseParen; public SeqSelectExpr(Cloner cloner, SeqSelectExpr original) : base(cloner, original) { SelectOne = original.SelectOne; Seq = cloner.CloneExpr(original.Seq); E0 = cloner.CloneExpr(original.E0); E1 = cloner.CloneExpr(original.E1); - CloseParen = cloner.Origin(original.CloseParen); + CloseParen = original.CloseParen; } [ContractInvariantMethod] @@ -24,7 +24,7 @@ void ObjectInvariant() { Contract.Invariant(!SelectOne || E1 == null); } - public SeqSelectExpr(IOrigin tok, bool selectOne, Expression seq, Expression e0, Expression e1, IOrigin closeParen) + public SeqSelectExpr(IOrigin tok, bool selectOne, Expression seq, Expression e0, Expression e1, Token closeParen) : base(tok) { Contract.Requires(tok != null); Contract.Requires(seq != null); diff --git a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs index 8912d17197c..8cbb234e922 100644 --- a/Source/DafnyCore/AST/Expressions/AttributedExpression.cs +++ b/Source/DafnyCore/AST/Expressions/AttributedExpression.cs @@ -25,7 +25,7 @@ public Attributes Attributes { string IAttributeBearingDeclaration.WhatKind => "expression"; - public override RangeToken Origin => E.Origin; + public override IOrigin Origin => E.Origin; public bool HasAttributes() { return Attributes != null; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs index f78c26cc0a5..461939ffa5a 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs @@ -54,7 +54,7 @@ public List UncompilableBoundVars() { return BoundedPool.MissingBounds(BoundVars, Bounds, v); } - public ComprehensionExpr(IOrigin tok, RangeToken rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) + public ComprehensionExpr(IOrigin tok, IOrigin rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) : base(tok) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs index 9fb0ba0c018..307b22b1e68 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ExistsExpr.cs @@ -7,7 +7,7 @@ public class ExistsExpr : QuantifierExpr, ICloneable { public override string WhatKind => "exists expression"; protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } } - public ExistsExpr(IOrigin tok, RangeToken rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) + public ExistsExpr(IOrigin tok, IOrigin rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeOrigin, bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs index 4c040c44b93..e36bcb303cf 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/ForallExpr.cs @@ -7,7 +7,7 @@ public class ForallExpr : QuantifierExpr, ICloneable { public override string WhatKind => "forall expression"; protected override BinaryExpr.ResolvedOpcode SplitResolvedOp => BinaryExpr.ResolvedOpcode.And; - public ForallExpr(IOrigin tok, RangeToken rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) + public ForallExpr(IOrigin tok, IOrigin rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeOrigin, bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); Contract.Requires(tok != null); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs index d1c58294906..c6cc6e875a1 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs @@ -10,7 +10,7 @@ public class LambdaExpr : ComprehensionExpr, ICloneable, IFrameScope public readonly Specification Reads; - public LambdaExpr(IOrigin tok, RangeToken rangeOrigin, List bvars, Expression requires, Specification reads, Expression body) + public LambdaExpr(IOrigin tok, IOrigin rangeOrigin, List bvars, Expression requires, Specification reads, Expression body) : base(tok, rangeOrigin, bvars, requires, body, null) { Contract.Requires(reads != null); Reads = reads; diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs index e01bb64a6a0..5a69e6caa68 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/MapComprehension.cs @@ -20,7 +20,7 @@ public MapComprehension(Cloner cloner, MapComprehension original) : base(cloner, Finite = original.Finite; } - public MapComprehension(IOrigin tok, RangeToken rangeOrigin, bool finite, List bvars, Expression range, Expression/*?*/ termLeft, Expression termRight, Attributes attrs) + public MapComprehension(IOrigin tok, IOrigin rangeOrigin, bool finite, List bvars, Expression range, Expression/*?*/ termLeft, Expression termRight, Attributes attrs) : base(tok, rangeOrigin, bvars, range, termRight, attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs index b9b9f84efb9..268ab6a9687 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/QuantifierExpr.cs @@ -50,7 +50,7 @@ public String Refresh(string prefix, FreshIdGenerator idGen) { return idGen.FreshId(prefix); } - public QuantifierExpr(IOrigin tok, RangeToken rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) + public QuantifierExpr(IOrigin tok, IOrigin rangeOrigin, List bvars, Expression range, Expression term, Attributes attrs) : base(tok, rangeOrigin, bvars, range, term, attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs b/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs index 2482dd95347..4ca975a8c8c 100644 --- a/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs +++ b/Source/DafnyCore/AST/Expressions/Comprehensions/SetComprehension.cs @@ -27,7 +27,7 @@ public SetComprehension(Cloner cloner, SetComprehension original) : base(cloner, Finite = original.Finite; } - public SetComprehension(IOrigin tok, RangeToken rangeOrigin, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) + public SetComprehension(IOrigin tok, IOrigin rangeOrigin, bool finite, List bvars, Expression range, Expression/*?*/ term, Attributes attrs) : base(tok, rangeOrigin, bvars, range, term ?? new IdentifierExpr(tok, bvars[0].Name), attrs) { Contract.Requires(tok != null); Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs index dce1716e9e9..e54309eac13 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchCaseStmt.cs @@ -9,7 +9,7 @@ public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration public readonly List Body; public Attributes Attributes { get; set; } string IAttributeBearingDeclaration.WhatKind => "match statement case"; - public NestedMatchCaseStmt(RangeToken rangeOrigin, ExtendedPattern pat, List body) : base(rangeOrigin.StartToken, pat) { + public NestedMatchCaseStmt(IOrigin rangeOrigin, ExtendedPattern pat, List body) : base(rangeOrigin.StartToken, pat) { Origin = rangeOrigin; Contract.Requires(body != null); this.Body = body; diff --git a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs index ab5b56ed30b..d10229e4bed 100644 --- a/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs +++ b/Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs @@ -72,7 +72,7 @@ public override IEnumerable NonSpecificationSubExpressions { } } - public NestedMatchStmt(RangeToken rangeOrigin, Expression source, [Captured] List cases, bool usesOptionalBraces, Attributes attrs = null) + public NestedMatchStmt(IOrigin rangeOrigin, Expression source, [Captured] List cases, bool usesOptionalBraces, Attributes attrs = null) : base(rangeOrigin, attrs) { Contract.Requires(source != null); Contract.Requires(cce.NonNullElements(cases)); diff --git a/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs b/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs index b0956de94fb..6720e00687a 100644 --- a/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs +++ b/Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs @@ -41,7 +41,6 @@ protected DefaultValueExpression(IOrigin tok, Formal formal, Expression/*?*/ rec this.formal = formal; this.receiver = receiver; this.substMap = substMap; - Origin = new RangeToken(tok, tok); } protected DefaultValueExpression(Cloner cloner, DefaultValueExpression original) : base(cloner, original) { diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 7b86f553930..f4fa31316f4 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -752,7 +752,7 @@ public static Expression CreateResolvedCall(IOrigin tok, Expression receiver, Fu Contract.Requires(function.Ins.Count == arguments.Count); Contract.Requires(function.TypeArgs.Count == typeArguments.Count); - var call = new FunctionCallExpr(tok, function.Name, receiver, tok, tok, arguments) { + var call = new FunctionCallExpr(tok, function.Name, receiver, tok, Token.NoToken, arguments) { Function = function, Type = function.ResultType, TypeApplication_AtEnclosingClass = receiver.Type.TypeArgs, @@ -775,7 +775,7 @@ public static Expression WrapResolvedCall(FunctionCallExpr call, SystemModuleMan }; subst = TypeParameter.SubstitutionMap(call.Function.TypeArgs, call.TypeApplication_JustFunction); - return new ApplySuffix(call.tok, null, exprDotName, new ActualBindings(call.Args).ArgumentBindings, call.tok) { + return new ApplySuffix(call.tok, null, exprDotName, new ActualBindings(call.Args).ArgumentBindings, call.CloseParen) { ResolvedExpression = call, Type = call.Function.ResultType.Subst(subst) }; diff --git a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs index eadfd884f82..9b2067389a6 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/BoundVar.cs @@ -8,7 +8,11 @@ namespace Microsoft.Dafny; [DebuggerDisplay("Bound<{name}>")] public class BoundVar : NonglobalVariable { public override bool IsMutable => false; - public BoundVar(IOrigin tok, string name, Type type) + + public BoundVar(string name, Type type) : this(Token.NoToken, new Name(Token.NoToken, name), type) { } + public BoundVar(IOrigin origin, string name, Type type) : this(origin, new Name(origin.StartToken, name), type) { } + + public BoundVar(IOrigin tok, Name name, Type type) : base(tok, name, type, false) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -86,6 +90,10 @@ class QuantifiedVariableDomainCloner : Cloner { public static readonly QuantifiedVariableDomainCloner Instance = new QuantifiedVariableDomainCloner(); private QuantifiedVariableDomainCloner() { } public override IOrigin Origin(IOrigin tok) { + if (tok == null) { + return null; + } + return new QuantifiedVariableDomainOrigin(tok); } } @@ -94,6 +102,10 @@ class QuantifiedVariableRangeCloner : Cloner { public static readonly QuantifiedVariableRangeCloner Instance = new QuantifiedVariableRangeCloner(); private QuantifiedVariableRangeCloner() { } public override IOrigin Origin(IOrigin tok) { + if (tok == null) { + return null; + } + return new QuantifiedVariableRangeOrigin(tok); } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs index 2789a45a715..fe8318ac4f4 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/Formal.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/Formal.cs @@ -18,19 +18,26 @@ public class Formal : NonglobalVariable { public Formal(IOrigin tok, string name, Type type, bool inParam, bool isGhost, Expression defaultValue, Attributes attributes = null, bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null) - : base(tok, name, type, isGhost) { + : this(tok, new Name(tok.StartToken, name), type, inParam, isGhost, defaultValue, attributes, + isOld, isNameOnly, isOlder, nameForCompilation) { + } + + public Formal(IOrigin tok, Name nameNode, Type type, bool inParam, bool isGhost, Expression defaultValue, + Attributes attributes = null, + bool isOld = false, bool isNameOnly = false, bool isOlder = false, string nameForCompilation = null) + : base(tok, nameNode, type, isGhost) { Contract.Requires(tok != null); - Contract.Requires(name != null); + Contract.Requires(nameNode != null); Contract.Requires(type != null); Contract.Requires(inParam || defaultValue == null); - Contract.Requires(!isNameOnly || (inParam && !name.StartsWith("#"))); + Contract.Requires(!isNameOnly || (inParam && !nameNode.Value.StartsWith("#"))); InParam = inParam; IsOld = isOld; DefaultValue = defaultValue; Attributes = attributes; IsNameOnly = isNameOnly; IsOlder = isOlder; - NameForCompilation = nameForCompilation ?? name; + NameForCompilation = nameForCompilation ?? nameNode.Value; } public bool HasName => !Name.StartsWith("#"); diff --git a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs index 88207d183c5..be707672d5f 100644 --- a/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs +++ b/Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs @@ -6,14 +6,14 @@ namespace Microsoft.Dafny; public abstract class NonglobalVariable : TokenNode, IVariable { - readonly string name; + public Name NameNode { get; } - protected NonglobalVariable(IOrigin tok, string name, Type type, bool isGhost) { + protected NonglobalVariable(IOrigin tok, Name nameNode, Type type, bool isGhost) { Contract.Requires(tok != null); - Contract.Requires(name != null); + Contract.Requires(nameNode != null); Contract.Requires(type != null); this.tok = tok; - this.name = name; + this.NameNode = nameNode; IsTypeExplicit = type != null; this.type = type ?? new InferredTypeProxy(); this.isGhost = isGhost; @@ -21,14 +21,13 @@ protected NonglobalVariable(IOrigin tok, string name, Type type, bool isGhost) { [ContractInvariantMethod] void ObjectInvariant() { - Contract.Invariant(name != null); Contract.Invariant(type != null); } public string Name { get { Contract.Ensures(Contract.Result() != null); - return name; + return NameNode.Value; } } public string DafnyName => Origin == null || tok.line == 0 ? Name : Origin.PrintOriginal(); @@ -136,7 +135,7 @@ public void MakeGhost() { IsGhost = true; } - public IOrigin NavigationToken => tok; + public IOrigin NavigationToken => NameNode.Origin; public override IEnumerable Children => IsTypeExplicit ? new List { Type } : Enumerable.Empty(); public override IEnumerable PreResolveChildren => IsTypeExplicit ? new List() { Type } : Enumerable.Empty(); public SymbolKind? Kind => SymbolKind.Variable; diff --git a/Source/DafnyCore/AST/ExtremeCloner.cs b/Source/DafnyCore/AST/ExtremeCloner.cs index e5ed30d3f1f..b6d119f2ec5 100644 --- a/Source/DafnyCore/AST/ExtremeCloner.cs +++ b/Source/DafnyCore/AST/ExtremeCloner.cs @@ -42,7 +42,7 @@ protected Expression CloneCallAndAddK(ApplySuffix e) { foreach (var arg in e.Bindings.ArgumentBindings) { args.Add(CloneActualBinding(arg)); } - var apply = new ApplySuffix(Origin(e.tok), e.AtTok == null ? null : Origin(e.AtTok), lhs, args, Origin(e.CloseParen)); + var apply = new ApplySuffix(Origin(e.tok), e.AtTok == null ? null : Origin(e.AtTok), lhs, args, e.CloseParen); reporter.Info(MessageSource.Cloner, e.tok, name + suffix); return apply; } diff --git a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs index 6cdb232f19f..98824b613a2 100644 --- a/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs +++ b/Source/DafnyCore/AST/ExtremeLemmaBodyCloner.cs @@ -76,7 +76,7 @@ public override AssignmentRhs CloneRHS(AssignmentRhs rhs) { args.Add(new ActualBinding(null, k)); apply.Bindings.ArgumentBindings.ForEach(arg => args.Add(CloneActualBinding(arg))); var applyClone = new ApplySuffix(Origin(apply.tok), apply.AtTok == null ? null : Origin(apply.AtTok), - lhsClone, args, Origin(apply.CloseParen)); + lhsClone, args, apply.CloseParen); var c = new ExprRhs(applyClone, CloneAttributes(rhs.Attributes)); reporter.Info(MessageSource.Cloner, apply.Lhs.tok, extremeLemma.Name + suffix); return c; diff --git a/Source/DafnyCore/AST/Grammar/ParseErrors.cs b/Source/DafnyCore/AST/Grammar/ParseErrors.cs index ecebdd4dbc6..b65a0818d49 100644 --- a/Source/DafnyCore/AST/Grammar/ParseErrors.cs +++ b/Source/DafnyCore/AST/Grammar/ParseErrors.cs @@ -457,7 +457,7 @@ state properties of the otherwise uninterpreted or abstract type. ".TrimStart(), range => range.Prev.val == "," ? new List { - OneAction("remove comma", range.Prev.ToRange(), ""), + OneAction("remove comma", range.Prev, ""), OneAction("insert '=='", range, "==" + range.PrintOriginal()), OneAction("insert '0'", range, "0" + range.PrintOriginal()), OneAction("insert '00'", range, "00" + range.PrintOriginal()), diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 3b8fa32f0fd..d301fff3918 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -17,9 +17,9 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca dummyExpr = new LiteralExpr(Token.NoToken); dummyRhs = new ExprRhs(dummyExpr); dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null); - dummyStmt = new ReturnStmt(Token.NoToken.ToRange(), null); - var dummyBlockStmt = new BlockStmt(Token.NoToken.ToRange(), new List()); - dummyIfStmt = new IfStmt(Token.NoToken.ToRange(), false, null, dummyBlockStmt, null); + dummyStmt = new ReturnStmt(Token.NoToken, null); + var dummyBlockStmt = new BlockStmt(Token.NoToken, new List()); + dummyIfStmt = new IfStmt(Token.NoToken, false, null, dummyBlockStmt, null); theOptions = new DafnyOptions(options); theModule = new FileModuleDefinition(scanner.FirstToken); @@ -669,12 +669,12 @@ class DeclModifierData { public IOrigin StaticToken; public bool IsOpaque; public IOrigin OpaqueToken; - public IOrigin FirstTokenExceptAttributes; + public Token FirstTokenExceptAttributes; public Attributes Attributes = null; - public IOrigin FirstToken { + public Token FirstToken { get { - IOrigin result = FirstTokenExceptAttributes; + Token result = FirstTokenExceptAttributes; foreach (var attr in Attributes.AsEnumerable()) { if (result == null || result.pos > attr.tok.pos) { result = attr.StartToken; @@ -720,7 +720,7 @@ public void CheckAndSetToken(ref IOrigin token) { } // Check that token has not been set, then set it, but just ignores if it was set already - public void CheckAndSetTokenOnce(ref IOrigin token) { + public void CheckAndSetTokenOnce(ref Token token) { if (token == null) { token = t; } diff --git a/Source/DafnyCore/AST/IOrigin.cs b/Source/DafnyCore/AST/IOrigin.cs index 271189a53c8..4f9758f55e3 100644 --- a/Source/DafnyCore/AST/IOrigin.cs +++ b/Source/DafnyCore/AST/IOrigin.cs @@ -4,8 +4,11 @@ namespace Microsoft.Dafny; public interface IOrigin : Microsoft.Boogie.IToken, IComparable { - public RangeToken To(IOrigin end) => new RangeToken(this, end); + bool IsInherited(ModuleDefinition m); + + bool InclusiveEnd { get; } + bool IncludesRange { get; } /* int kind { get; set; } int pos { get; set; } @@ -23,6 +26,9 @@ string Boogie.IToken.filename { Uri Uri { get; set; } + Token StartToken { get; } + Token EndToken { get; } + /// /// TrailingTrivia contains everything after the token, /// until and including two newlines between which there is no commment diff --git a/Source/DafnyCore/AST/Members/ConstantField.cs b/Source/DafnyCore/AST/Members/ConstantField.cs index 8506590ef68..afe41fd4d78 100644 --- a/Source/DafnyCore/AST/Members/ConstantField.cs +++ b/Source/DafnyCore/AST/Members/ConstantField.cs @@ -12,7 +12,7 @@ public class ConstantField : SpecialField, ICallable, ICanAutoRevealDependencies public override bool IsOpaque { get; } - public ConstantField(RangeToken rangeOrigin, Name name, Expression/*?*/ rhs, bool hasStaticKeyword, bool isGhost, bool isOpaque, Type type, Attributes attributes) + public ConstantField(IOrigin rangeOrigin, Name name, Expression/*?*/ rhs, bool hasStaticKeyword, bool isGhost, bool isOpaque, Type type, Attributes attributes) : base(rangeOrigin, name, ID.UseIdParam, NonglobalVariable.SanitizeName(name.Value), hasStaticKeyword, isGhost, false, false, type, attributes) { Contract.Requires(tok != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/Members/Constructor.cs b/Source/DafnyCore/AST/Members/Constructor.cs index fcdefd4b986..626951606fc 100644 --- a/Source/DafnyCore/AST/Members/Constructor.cs +++ b/Source/DafnyCore/AST/Members/Constructor.cs @@ -34,7 +34,7 @@ public List BodyProper { // second part of Body's statements } } } - public Constructor(RangeToken rangeOrigin, Name name, + public Constructor(IOrigin rangeOrigin, Name name, bool isGhost, List typeArgs, List ins, diff --git a/Source/DafnyCore/AST/Members/ExtremeLemma.cs b/Source/DafnyCore/AST/Members/ExtremeLemma.cs index 22bddc75f4d..6f51880e5ee 100644 --- a/Source/DafnyCore/AST/Members/ExtremeLemma.cs +++ b/Source/DafnyCore/AST/Members/ExtremeLemma.cs @@ -18,7 +18,7 @@ public ExtremeLemma(Cloner cloner, ExtremeLemma lemma) : base(cloner, lemma) { TypeOfK = lemma.TypeOfK; } - public ExtremeLemma(RangeToken rangeOrigin, Name name, + public ExtremeLemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, @@ -48,7 +48,7 @@ public ExtremeLemma(RangeToken rangeOrigin, Name name, public class LeastLemma : ExtremeLemma { public override string WhatKind => "least lemma"; - public LeastLemma(RangeToken rangeOrigin, Name name, + public LeastLemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, @@ -78,7 +78,7 @@ public LeastLemma(Cloner cloner, LeastLemma leastLemma) : base(cloner, leastLemm public class GreatestLemma : ExtremeLemma { public override string WhatKind => "greatest lemma"; - public GreatestLemma(RangeToken rangeOrigin, Name name, + public GreatestLemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, ExtremePredicate.KType typeOfK, List typeArgs, List ins, [Captured] List outs, diff --git a/Source/DafnyCore/AST/Members/ExtremePredicate.cs b/Source/DafnyCore/AST/Members/ExtremePredicate.cs index 680be99e74a..dc9b37952f5 100644 --- a/Source/DafnyCore/AST/Members/ExtremePredicate.cs +++ b/Source/DafnyCore/AST/Members/ExtremePredicate.cs @@ -19,7 +19,7 @@ public bool KNat { public override IEnumerable Children => base.Children.Concat(new[] { PrefixPredicate }); public override IEnumerable PreResolveChildren => base.Children; - public ExtremePredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, + public ExtremePredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, List typeArgs, List ins, Formal result, List req, Specification reads, List ens, Expression body, Attributes attributes, IOrigin signatureEllipsis) @@ -52,7 +52,7 @@ public FunctionCallExpr CreatePrefixPredicateCall(FunctionCallExpr fexp, Express public class GreatestPredicate : ExtremePredicate { public override string WhatKind => "greatest predicate"; - public GreatestPredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, + public GreatestPredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, List typeArgs, List ins, Formal result, List req, Specification reads, List ens, Expression body, Attributes attributes, IOrigin signatureEllipsis) @@ -63,7 +63,7 @@ public GreatestPredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeywor public class LeastPredicate : ExtremePredicate { public override string WhatKind => "least predicate"; - public LeastPredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, + public LeastPredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK, List typeArgs, List ins, Formal result, List req, Specification reads, List ens, Expression body, Attributes attributes, IOrigin signatureEllipsis) diff --git a/Source/DafnyCore/AST/Members/Field.cs b/Source/DafnyCore/AST/Members/Field.cs index ab302a10208..9656497b136 100644 --- a/Source/DafnyCore/AST/Members/Field.cs +++ b/Source/DafnyCore/AST/Members/Field.cs @@ -21,14 +21,14 @@ void ObjectInvariant() { public override IEnumerable Children => (Type?.Nodes ?? Enumerable.Empty()).Concat(this.Attributes.AsEnumerable()); - public Field(RangeToken rangeOrigin, Name name, bool isGhost, Type type, Attributes attributes) + public Field(IOrigin rangeOrigin, Name name, bool isGhost, Type type, Attributes attributes) : this(rangeOrigin, name, false, isGhost, true, true, type, attributes) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); Contract.Requires(type != null); } - public Field(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) + public Field(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) : base(rangeOrigin, name, hasStaticKeyword, isGhost, attributes, false) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index dcf4ba2a92a..0c533b6d025 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -227,7 +227,7 @@ void ObjectInvariant() { Contract.Invariant(Decreases != null); } - public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque, + public Function(IOrigin range, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque, List typeArgs, List ins, Formal result, Type resultType, List req, Specification reads, List ens, Specification decreases, Expression/*?*/ body, IOrigin/*?*/ byMethodTok, BlockStmt/*?*/ byMethodBody, diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index b4baa72f9db..17af48faba0 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -104,7 +104,7 @@ public bool InferredDecreases { public bool SingleFileToken => CwInner.SingleFileToken; public IEnumerable OwnedTokens => CwInner.OwnedTokens; - public RangeToken Origin => CwInner.Origin; + public IOrigin Origin => CwInner.Origin; public IOrigin NavigationToken => CwInner.NavigationToken; public SymbolKind? Kind => CwInner.Kind; public string GetDescription(DafnyOptions options) { diff --git a/Source/DafnyCore/AST/Members/Lemma.cs b/Source/DafnyCore/AST/Members/Lemma.cs index f0907852c60..df4d2aa3a73 100644 --- a/Source/DafnyCore/AST/Members/Lemma.cs +++ b/Source/DafnyCore/AST/Members/Lemma.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class Lemma : Method { public override string WhatKind => "lemma"; public override string WhatKindMentionGhost => WhatKind; - public Lemma(RangeToken rangeOrigin, Name name, + public Lemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, @@ -30,7 +30,7 @@ public class TwoStateLemma : Method { public override string WhatKind => "twostate lemma"; public override string WhatKindMentionGhost => WhatKind; - public TwoStateLemma(RangeToken rangeOrigin, Name name, + public TwoStateLemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, diff --git a/Source/DafnyCore/AST/Members/MemberDecl.cs b/Source/DafnyCore/AST/Members/MemberDecl.cs index a8c93fe879b..fbea09c09c6 100644 --- a/Source/DafnyCore/AST/Members/MemberDecl.cs +++ b/Source/DafnyCore/AST/Members/MemberDecl.cs @@ -67,7 +67,7 @@ protected MemberDecl(Cloner cloner, MemberDecl original) : base(cloner, original this.isGhost = original.isGhost; } - protected MemberDecl(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) + protected MemberDecl(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining) : base(rangeOrigin, name, attributes, isRefining) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index 75704e519ba..787bb76526f 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -131,7 +131,7 @@ public Method(Cloner cloner, Method original) : base(cloner, original) { this.IsByMethod = original.IsByMethod; } - public Method(RangeToken rangeOrigin, Name name, + public Method(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, [Captured] List typeArgs, [Captured] List ins, [Captured] List outs, diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index b54ed62afba..4c8013dd075 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs @@ -22,7 +22,7 @@ static MethodOrFunction() { public readonly Specification Decreases; public readonly List Ins; - protected MethodOrFunction(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, + protected MethodOrFunction(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining, List typeArgs, List ins, List req, List ens, diff --git a/Source/DafnyCore/AST/Members/Predicate.cs b/Source/DafnyCore/AST/Members/Predicate.cs index 69c272ce2c3..7a3cb993ce4 100644 --- a/Source/DafnyCore/AST/Members/Predicate.cs +++ b/Source/DafnyCore/AST/Members/Predicate.cs @@ -11,7 +11,7 @@ public enum BodyOriginKind { Extension // this predicate extends the definition of a predicate with a body in a module being refined } public readonly BodyOriginKind BodyOrigin; - public Predicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque, + public Predicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque, List typeArgs, List ins, Formal result, List req, Specification reads, List ens, Specification decreases, diff --git a/Source/DafnyCore/AST/Members/PrefixLemma.cs b/Source/DafnyCore/AST/Members/PrefixLemma.cs index 77bb526c5e9..c3a415b0fb2 100644 --- a/Source/DafnyCore/AST/Members/PrefixLemma.cs +++ b/Source/DafnyCore/AST/Members/PrefixLemma.cs @@ -12,7 +12,7 @@ public class PrefixLemma : Method { public readonly Formal K; public readonly ExtremeLemma ExtremeLemma; - public PrefixLemma(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, + public PrefixLemma(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, List typeArgs, Formal k, List ins, List outs, List req, [Captured] Specification reads, Specification mod, List ens, Specification decreases, diff --git a/Source/DafnyCore/AST/Members/PrefixPredicate.cs b/Source/DafnyCore/AST/Members/PrefixPredicate.cs index 9ad247bd19b..704aa2daa10 100644 --- a/Source/DafnyCore/AST/Members/PrefixPredicate.cs +++ b/Source/DafnyCore/AST/Members/PrefixPredicate.cs @@ -11,7 +11,7 @@ public class PrefixPredicate : Function { public override string WhatKindMentionGhost => WhatKind; public readonly Formal K; public readonly ExtremePredicate ExtremePred; - public PrefixPredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, + public PrefixPredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, List typeArgs, Formal k, List ins, List req, Specification reads, List ens, Specification decreases, Expression body, Attributes attributes, ExtremePredicate extremePred) diff --git a/Source/DafnyCore/AST/Members/SpecialField.cs b/Source/DafnyCore/AST/Members/SpecialField.cs index d16232edc7f..c9124d4dd28 100644 --- a/Source/DafnyCore/AST/Members/SpecialField.cs +++ b/Source/DafnyCore/AST/Members/SpecialField.cs @@ -23,12 +23,12 @@ public enum ID { public readonly ID SpecialId; public readonly object IdParam; - public SpecialField(RangeToken rangeOrigin, string name, ID specialId, object idParam, + public SpecialField(IOrigin rangeOrigin, string name, ID specialId, object idParam, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) : this(rangeOrigin, new Name(name), specialId, idParam, false, isGhost, isMutable, isUserMutable, type, attributes) { } - public SpecialField(RangeToken rangeOrigin, Name name, ID specialId, object idParam, + public SpecialField(IOrigin rangeOrigin, Name name, ID specialId, object idParam, bool hasStaticKeyword, bool isGhost, bool isMutable, bool isUserMutable, Type type, Attributes attributes) : base(rangeOrigin, name, hasStaticKeyword, isGhost, isMutable, isUserMutable, type, attributes) { Contract.Requires(rangeOrigin != null); @@ -65,7 +65,7 @@ public override string WhatKind { get { return "discriminator"; } } - public DatatypeDiscriminator(RangeToken rangeOrigin, Name name, ID specialId, object idParam, bool isGhost, Type type, Attributes attributes) + public DatatypeDiscriminator(IOrigin rangeOrigin, Name name, ID specialId, object idParam, bool isGhost, Type type, Attributes attributes) : base(rangeOrigin, name, specialId, idParam, false, isGhost, false, false, type, attributes) { } } @@ -81,7 +81,7 @@ void ObjectInvariant() { Contract.Invariant(EnclosingCtors.Count == CorrespondingFormals.Count); } - public DatatypeDestructor(RangeToken rangeOrigin, DatatypeCtor enclosingCtor, Formal correspondingFormal, Name name, string compiledName, bool isGhost, Type type, Attributes attributes) + public DatatypeDestructor(IOrigin rangeOrigin, DatatypeCtor enclosingCtor, Formal correspondingFormal, Name name, string compiledName, bool isGhost, Type type, Attributes attributes) : base(rangeOrigin, name, SpecialField.ID.UseIdParam, compiledName, false, isGhost, false, false, type, attributes) { Contract.Requires(rangeOrigin != null); Contract.Requires(enclosingCtor != null); diff --git a/Source/DafnyCore/AST/Members/SpecialFunction.cs b/Source/DafnyCore/AST/Members/SpecialFunction.cs index 8e3cf4229a7..bfa7bd6ba3a 100644 --- a/Source/DafnyCore/AST/Members/SpecialFunction.cs +++ b/Source/DafnyCore/AST/Members/SpecialFunction.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; public class SpecialFunction : Function, ICallable { readonly ModuleDefinition Module; - public SpecialFunction(RangeToken rangeOrigin, string name, ModuleDefinition module, bool hasStaticKeyword, bool isGhost, + public SpecialFunction(IOrigin rangeOrigin, string name, ModuleDefinition module, bool hasStaticKeyword, bool isGhost, List typeArgs, List ins, Type resultType, List req, Specification reads, List ens, Specification decreases, Expression body, Attributes attributes, IOrigin signatureEllipsis) diff --git a/Source/DafnyCore/AST/Members/TwoStateFunction.cs b/Source/DafnyCore/AST/Members/TwoStateFunction.cs index c2f9896d07b..0a09fafc15b 100644 --- a/Source/DafnyCore/AST/Members/TwoStateFunction.cs +++ b/Source/DafnyCore/AST/Members/TwoStateFunction.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class TwoStateFunction : Function { public override string WhatKind => "twostate function"; public override string WhatKindMentionGhost => WhatKind; - public TwoStateFunction(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, + public TwoStateFunction(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, List typeArgs, List ins, Formal result, Type resultType, List req, Specification reads, List ens, Specification decreases, Expression body, Attributes attributes, IOrigin signatureEllipsis) @@ -26,7 +26,7 @@ public TwoStateFunction(RangeToken rangeOrigin, Name name, bool hasStaticKeyword public class TwoStatePredicate : TwoStateFunction { public override string WhatKind => "twostate predicate"; - public TwoStatePredicate(RangeToken rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, + public TwoStatePredicate(IOrigin rangeOrigin, Name name, bool hasStaticKeyword, bool isOpaque, List typeArgs, List ins, Formal result, List req, Specification reads, List ens, Specification decreases, Expression body, Attributes attributes, IOrigin signatureEllipsis) diff --git a/Source/DafnyCore/AST/Modules/AbstractModuleDecl.cs b/Source/DafnyCore/AST/Modules/AbstractModuleDecl.cs index acc9ca3b5bd..ead5e3e3ad4 100644 --- a/Source/DafnyCore/AST/Modules/AbstractModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/AbstractModuleDecl.cs @@ -20,7 +20,7 @@ public AbstractModuleDecl(Cloner cloner, AbstractModuleDecl original, ModuleDefi QId = new ModuleQualifiedId(cloner, original.QId); } - public AbstractModuleDecl(DafnyOptions options, RangeToken rangeOrigin, ModuleQualifiedId qid, Name name, + public AbstractModuleDecl(DafnyOptions options, IOrigin rangeOrigin, ModuleQualifiedId qid, Name name, ModuleDefinition parent, bool opened, List exports, Guid cloneId) : base(options, rangeOrigin, name, parent, opened, false, cloneId) { Contract.Requires(qid != null && qid.Path.Count > 0); diff --git a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs index aef47ef20b1..e0cbe4db640 100644 --- a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs @@ -13,7 +13,7 @@ public class FileModuleDefinition : ModuleDefinition { public List Includes { get; } = new(); public FileModuleDefinition(IOrigin token) : - base(token.ToRange(), new Name("_module"), new List(), + base(token, new Name("_module"), new List(), ModuleKindEnum.Concrete, false, null, null, null) { { } diff --git a/Source/DafnyCore/AST/Modules/ModuleDecl.cs b/Source/DafnyCore/AST/Modules/ModuleDecl.cs index 0b6d878369d..c8a27148405 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDecl.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDecl.cs @@ -45,7 +45,7 @@ protected ModuleDecl(Cloner cloner, ModuleDecl original, ModuleDefinition parent CloneId = original.CloneId; } - protected ModuleDecl(DafnyOptions options, RangeToken rangeOrigin, Name name, ModuleDefinition parent, bool opened, bool isRefining, Guid cloneId) + protected ModuleDecl(DafnyOptions options, IOrigin rangeOrigin, Name name, ModuleDefinition parent, bool opened, bool isRefining, Guid cloneId) : base(rangeOrigin, name, parent, new List(), null, isRefining) { Options = options; Height = -1; diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index 6a241de59b3..d1ba5ca09a1 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs @@ -157,7 +157,7 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original) : base(cloner, } } - public ModuleDefinition(RangeToken tok, Name name, List prefixIds, ModuleKindEnum moduleKind, bool isFacade, + public ModuleDefinition(IOrigin tok, Name name, List prefixIds, ModuleKindEnum moduleKind, bool isFacade, Implements implements, ModuleDefinition parent, Attributes attributes) : base(tok) { Contract.Requires(tok != null); Contract.Requires(name != null); @@ -633,7 +633,7 @@ public void ProcessPrefixNamedModules() { foreach (var (name, prefixNamedModules) in prefixModulesByFirstPart) { var prefixNameModule = prefixNamedModules.First(); var firstPartToken = prefixNameModule.Parts[0]; - var modDef = new ModuleDefinition(RangeToken.NoToken, new Name(firstPartToken.ToRange(), name), new List(), ModuleKindEnum.Concrete, + var modDef = new ModuleDefinition(RangeToken.NoToken, new Name(firstPartToken, name), new List(), ModuleKindEnum.Concrete, false, null, this, null); // Add the new module to the top-level declarations of its parent and then bind its names as usual @@ -896,7 +896,7 @@ public ModuleSignature RegisterTopLevelDecls(ModuleResolver resolver, bool useIm dtor.AddAnotherEnclosingCtor(ctor, formal); } else { // either the destructor has no explicit name, or this constructor declared another destructor with this name, or no previous destructor had this name - dtor = new DatatypeDestructor(formal.Origin, ctor, formal, new Name(formal.Origin, formal.Name), "dtor_" + formal.CompileName, + dtor = new DatatypeDestructor(formal.Origin, ctor, formal, formal.NameNode, "dtor_" + formal.CompileName, formal.IsGhost, formal.Type, null); dtor.InheritVisibility(dt); dtor.EnclosingClass = dt; // resolve here diff --git a/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs b/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs index bc2d6bbc739..cc1845f498f 100644 --- a/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs +++ b/Source/DafnyCore/AST/Modules/ModuleExportDecl.cs @@ -35,7 +35,7 @@ public ModuleExportDecl(Cloner cloner, ModuleExportDecl original, ModuleDefiniti SetupDefaultSignature(); } - public ModuleExportDecl(DafnyOptions options, RangeToken rangeOrigin, Name name, ModuleDefinition parent, + public ModuleExportDecl(DafnyOptions options, IOrigin rangeOrigin, Name name, ModuleDefinition parent, List exports, List extends, bool provideAll, bool revealAll, bool isDefault, bool isRefining, Guid cloneId) : base(options, rangeOrigin, name, parent, false, isRefining, cloneId) { diff --git a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs index 020707012e9..38cd17760c7 100644 --- a/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs +++ b/Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs @@ -66,8 +66,8 @@ public void SetTarget(ModuleDecl m) { public override IEnumerable Children => Enumerable.Empty(); public override IEnumerable PreResolveChildren => Children; - public override RangeToken Origin { - get => new(Path.First().StartToken, Path.Last().EndToken); + public override IOrigin Origin { + get => new RangeToken(Path.First().StartToken, Path.Last().EndToken); set => throw new NotSupportedException(); } diff --git a/Source/DafnyCore/AST/OriginWrapper.cs b/Source/DafnyCore/AST/OriginWrapper.cs index c0bcf1b661f..c2bdd3a8c3c 100644 --- a/Source/DafnyCore/AST/OriginWrapper.cs +++ b/Source/DafnyCore/AST/OriginWrapper.cs @@ -19,6 +19,12 @@ public virtual int col { set { WrappedToken.col = value; } } + public virtual bool IsInherited(ModuleDefinition m) { + return WrappedToken.IsInherited(m); + } + + public virtual bool InclusiveEnd => WrappedToken.InclusiveEnd; + public virtual bool IncludesRange => WrappedToken.IncludesRange; public string ActualFilename => WrappedToken.ActualFilename; public virtual string Filepath => WrappedToken.Filepath; @@ -28,6 +34,9 @@ public Uri Uri { set => WrappedToken.Uri = value; } + public virtual Token StartToken => WrappedToken.StartToken; + public virtual Token EndToken => WrappedToken.EndToken; + public bool IsValid { get { return WrappedToken.IsValid; } } @@ -75,20 +84,4 @@ public int CompareTo(IOrigin other) { public int CompareTo(Boogie.IToken other) { return WrappedToken.CompareTo(other); } - - /// - /// Removes token wrappings from a given token, so that it returns the bare token - /// - public static IOrigin Unwrap(IOrigin token, bool includeRanges = false) { - if (token is OriginWrapper wrapper - && (includeRanges || token is not RangeToken)) { - return Unwrap(wrapper.WrappedToken); - } - - if (token is RangeToken rangeToken) { - return new RangeToken(Unwrap(rangeToken.StartToken), Unwrap(rangeToken.EndToken)); - } - - return token; - } } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Program.cs b/Source/DafnyCore/AST/Program.cs index 33f7fc85991..23af4c467c2 100644 --- a/Source/DafnyCore/AST/Program.cs +++ b/Source/DafnyCore/AST/Program.cs @@ -110,12 +110,12 @@ public string Name { /// Get the first token that is in the same file as the DefaultModule.RootToken.FileName /// (skips included tokens) - public IOrigin GetStartOfFirstFileToken() { + public Token GetStartOfFirstFileToken() { return GetFirstTokenForUri(Compilation.RootSourceUris[0]); } public Token GetFirstTokenForUri(Uri uri) { - return (Token)OriginWrapper.Unwrap(this.FindNodesInUris(uri).MinBy(n => n.Origin.StartToken.pos)?.StartToken); + return this.FindNodesInUris(uri).MinBy(n => n.Origin.StartToken.pos)?.StartToken; } public override IEnumerable Children => new[] { DefaultModule }; diff --git a/Source/DafnyCore/AST/RangeToken.cs b/Source/DafnyCore/AST/RangeToken.cs index 9cd02f70ba1..5499ac02b31 100644 --- a/Source/DafnyCore/AST/RangeToken.cs +++ b/Source/DafnyCore/AST/RangeToken.cs @@ -4,11 +4,12 @@ namespace Microsoft.Dafny; public class RangeToken : OriginWrapper { - public IOrigin StartToken => WrappedToken; + public override Token StartToken => (Token)WrappedToken; - public IOrigin EndToken => endToken ?? StartToken; + public override Token EndToken => endToken ?? StartToken; - public bool InclusiveEnd => endToken != null; + public override bool InclusiveEnd => endToken != null; + public override bool IncludesRange => true; public override bool Equals(object obj) { if (obj is RangeToken other) { @@ -21,26 +22,7 @@ public override int GetHashCode() { return HashCode.Combine(StartToken.GetHashCode(), EndToken.GetHashCode()); } - public DafnyRange ToDafnyRange(bool includeTrailingWhitespace = false) { - var startLine = StartToken.line - 1; - var startColumn = StartToken.col - 1; - var endLine = EndToken.line - 1; - int whitespaceOffset = 0; - if (includeTrailingWhitespace) { - string trivia = EndToken.TrailingTrivia; - // Don't want to remove newlines or comments -- just spaces and tabs - while (whitespaceOffset < trivia.Length && (trivia[whitespaceOffset] == ' ' || trivia[whitespaceOffset] == '\t')) { - whitespaceOffset++; - } - } - - var endColumn = EndToken.col + (InclusiveEnd ? EndToken.val.Length : 0) + whitespaceOffset - 1; - return new DafnyRange( - new DafnyPosition(startLine, startColumn), - new DafnyPosition(endLine, endColumn)); - } - - public RangeToken(IOrigin startToken, IOrigin endToken) : base(startToken) { + public RangeToken(Token startToken, Token endToken) : base(startToken) { this.endToken = endToken; } @@ -62,36 +44,13 @@ public int Length() { return EndToken.pos - StartToken.pos; } - public RangeToken MakeAutoGenerated() { - return new RangeToken(new AutoGeneratedOrigin(StartToken), EndToken); - } - - public RangeToken MakeRefined(ModuleDefinition module) { - return new RangeToken(new RefinementOrigin(StartToken, module), EndToken); - } - // TODO rename to Generated, and Token.NoToken to Token.Generated, and remove AutoGeneratedToken. - public static RangeToken NoToken = new(Token.NoToken, Token.NoToken); - private readonly IOrigin endToken; + public static IOrigin NoToken => Token.NoToken; + private readonly Token endToken; public override IOrigin WithVal(string newVal) { throw new NotImplementedException(); } - public override bool IsSourceToken => this != NoToken; - - public BoogieRangeOrigin ToToken() { - return new BoogieRangeOrigin(StartToken, EndToken, null); - } - - public bool Contains(IOrigin otherToken) { - return StartToken.Uri == otherToken.Uri && - StartToken.pos <= otherToken.pos && - (EndToken == null || otherToken.pos <= EndToken.pos); - } - - public bool Intersects(RangeToken other) { - return !(other.EndToken.pos + other.EndToken.val.Length <= StartToken.pos - || EndToken.pos + EndToken.val.Length <= other.StartToken.pos); - } + public override bool IsSourceToken => !ReferenceEquals(this, NoToken); } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs index 38d5537d023..9c5cfff7abf 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignOrReturnStmt.cs @@ -53,7 +53,7 @@ public AssignOrReturnStmt(Cloner cloner, AssignOrReturnStmt original) : base(clo } } - public AssignOrReturnStmt(RangeToken rangeOrigin, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss) + public AssignOrReturnStmt(IOrigin rangeOrigin, List lhss, ExprRhs rhs, AttributedToken keywordToken, List rhss) : base(rangeOrigin, lhss) { Contract.Requires(rangeOrigin != null); Contract.Requires(lhss != null); @@ -296,18 +296,18 @@ private void DesugarElephantStatement(bool expectExtract, Expression lhsExtract, ResolvedStatements.Add(up); if (KeywordToken != null) { - var token = KeywordToken.Token; - var notFailureExpr = new UnaryOpExpr(token, UnaryOpExpr.Opcode.Not, resolver.VarDotMethod(Tok, temp, "IsFailure")); + var keyword = KeywordToken.Token; + var notFailureExpr = new UnaryOpExpr(keyword, UnaryOpExpr.Opcode.Not, resolver.VarDotMethod(Tok, temp, "IsFailure")); Statement ss = null; - if (token.val == "expect") { + if (keyword.val == "expect") { // "expect !temp.IsFailure(), temp" - ss = new ExpectStmt(new RangeToken(token, EndToken), notFailureExpr, new IdentifierExpr(Tok, temp), KeywordToken.Attrs); - } else if (token.val == "assume") { - ss = new AssumeStmt(new RangeToken(token, EndToken), notFailureExpr, SystemModuleManager.AxiomAttribute(KeywordToken.Attrs)); - } else if (token.val == "assert") { - ss = new AssertStmt(new RangeToken(token, EndToken), notFailureExpr, null, KeywordToken.Attrs); + ss = new ExpectStmt(new RangeToken(keyword.StartToken, EndToken), notFailureExpr, new IdentifierExpr(Tok, temp), KeywordToken.Attrs); + } else if (keyword.val == "assume") { + ss = new AssumeStmt(new RangeToken(keyword.StartToken, EndToken), notFailureExpr, SystemModuleManager.AxiomAttribute(KeywordToken.Attrs)); + } else if (keyword.val == "assert") { + ss = new AssertStmt(new RangeToken(keyword.StartToken, EndToken), notFailureExpr, null, KeywordToken.Attrs); } else { - Contract.Assert(false, $"Invalid token in :- statement: {token.val}"); + Contract.Assert(false, $"Invalid token in :- statement: {keyword.val}"); } ResolvedStatements.Add(ss); } else { diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs index 49572c105aa..e2585f65b8a 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignStatement.cs @@ -53,7 +53,7 @@ public AssignStatement(Cloner cloner, AssignStatement original) : base(cloner, o } } - public AssignStatement(RangeToken rangeOrigin, List lhss, List rhss) + public AssignStatement(IOrigin rangeOrigin, List lhss, List rhss) : base(rangeOrigin, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); @@ -61,7 +61,7 @@ public AssignStatement(RangeToken rangeOrigin, List lhss, List lhss, List rhss, bool mutate) + public AssignStatement(IOrigin rangeOrigin, List lhss, List rhss, bool mutate) : base(rangeOrigin, lhss) { Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(cce.NonNullElements(rhss)); diff --git a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs index c9bf69b45d5..e18509cc412 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/AssignSuchThatStmt.cs @@ -58,7 +58,7 @@ public AssignSuchThatStmt(Cloner cloner, AssignSuchThatStmt original) : base(clo /// "assumeToken" is allowed to be "null", in which case the verifier will check that a RHS value exists. /// If "assumeToken" is non-null, then it should denote the "assume" keyword used in the statement. /// - public AssignSuchThatStmt(RangeToken rangeOrigin, List lhss, Expression expr, AttributedToken assumeToken, Attributes attrs) + public AssignSuchThatStmt(IOrigin rangeOrigin, List lhss, Expression expr, AttributedToken assumeToken, Attributes attrs) : base(rangeOrigin, lhss, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(lhss)); diff --git a/Source/DafnyCore/AST/Statements/Assignment/ConcreteAssignStatement.cs b/Source/DafnyCore/AST/Statements/Assignment/ConcreteAssignStatement.cs index 657d4b95507..d7058b0bebf 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/ConcreteAssignStatement.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/ConcreteAssignStatement.cs @@ -14,7 +14,7 @@ protected ConcreteAssignStatement(Cloner cloner, ConcreteAssignStatement origina Lhss = original.Lhss.Select(cloner.CloneExpr).ToList(); } - public ConcreteAssignStatement(RangeToken rangeOrigin, List lhss, Attributes attrs = null) + public ConcreteAssignStatement(IOrigin rangeOrigin, List lhss, Attributes attrs = null) : base(rangeOrigin, attrs) { Contract.Requires(cce.NonNullElements(lhss)); Lhss = lhss; diff --git a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs index c6a25d99df9..21a18cb6089 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs @@ -22,7 +22,7 @@ void ObjectInvariant() { Contract.Invariant(SyntacticType != null); } - public override IOrigin Tok => Origin.StartToken; + public override IOrigin Tok => Origin; public LocalVariable(Cloner cloner, LocalVariable original) : base(cloner, original) { @@ -36,7 +36,7 @@ public LocalVariable(Cloner cloner, LocalVariable original) } } - public LocalVariable(RangeToken rangeOrigin, string name, Type type, bool isGhost) + public LocalVariable(IOrigin rangeOrigin, string name, Type type, bool isGhost) : base(rangeOrigin) { Contract.Requires(name != null); Contract.Requires(type != null); // can be a proxy, though diff --git a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs index 561b682afda..38c5559164a 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/SingleAssignStmt.cs @@ -45,7 +45,7 @@ public SingleAssignStmt(Cloner cloner, SingleAssignStmt original) : base(cloner, Rhs = cloner.CloneRHS(original.Rhs); } - public SingleAssignStmt(RangeToken rangeOrigin, Expression lhs, AssignmentRhs rhs) + public SingleAssignStmt(IOrigin rangeOrigin, Expression lhs, AssignmentRhs rhs) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(lhs != null); diff --git a/Source/DafnyCore/AST/Statements/Assignment/VarDeclPattern.cs b/Source/DafnyCore/AST/Statements/Assignment/VarDeclPattern.cs index 0f3fa4d9e02..dd7f5b5c8e9 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/VarDeclPattern.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/VarDeclPattern.cs @@ -18,7 +18,7 @@ public VarDeclPattern(Cloner cloner, VarDeclPattern original) : base(cloner, ori HasGhostModifier = original.HasGhostModifier; } - public VarDeclPattern(RangeToken rangeOrigin, CasePattern lhs, Expression rhs, bool hasGhostModifier) + public VarDeclPattern(IOrigin rangeOrigin, CasePattern lhs, Expression rhs, bool hasGhostModifier) : base(rangeOrigin) { LHS = lhs; RHS = rhs; diff --git a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs index fa66707919c..9cea53053c1 100644 --- a/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs +++ b/Source/DafnyCore/AST/Statements/Assignment/VarDeclStmt.cs @@ -22,7 +22,7 @@ public VarDeclStmt(Cloner cloner, VarDeclStmt original) : base(cloner, original) Assign = (ConcreteAssignStatement)cloner.CloneStmt(original.Assign, false); } - public VarDeclStmt(RangeToken rangeOrigin, List locals, ConcreteAssignStatement assign) + public VarDeclStmt(IOrigin rangeOrigin, List locals, ConcreteAssignStatement assign) : base(rangeOrigin) { Contract.Requires(locals != null); Contract.Requires(locals.Count != 0); diff --git a/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs b/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs index 09f0489dce3..ebade64175a 100644 --- a/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs +++ b/Source/DafnyCore/AST/Statements/BlockByProofStmt.cs @@ -9,7 +9,7 @@ public class BlockByProofStmt : Statement, ICanResolveNewAndOld, ICanPrint, public Statement Body { get; } public BlockStmt Proof { get; } - public BlockByProofStmt(RangeToken range, BlockStmt proof, Statement body) : base(range) { + public BlockByProofStmt(IOrigin range, BlockStmt proof, Statement body) : base(range) { Proof = proof; Body = body; } diff --git a/Source/DafnyCore/AST/Statements/BlockStmt.cs b/Source/DafnyCore/AST/Statements/BlockStmt.cs index 7ddef002368..ccc4f293734 100644 --- a/Source/DafnyCore/AST/Statements/BlockStmt.cs +++ b/Source/DafnyCore/AST/Statements/BlockStmt.cs @@ -15,7 +15,7 @@ protected BlockStmt(Cloner cloner, BlockStmt original) : base(cloner, original) Body = original.Body.Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); } - public BlockStmt(RangeToken rangeOrigin, [Captured] List body) + public BlockStmt(IOrigin rangeOrigin, [Captured] List body) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(body)); diff --git a/Source/DafnyCore/AST/Statements/CalcStmt.cs b/Source/DafnyCore/AST/Statements/CalcStmt.cs index b28d3e3e6de..36312ea1c06 100644 --- a/Source/DafnyCore/AST/Statements/CalcStmt.cs +++ b/Source/DafnyCore/AST/Statements/CalcStmt.cs @@ -223,7 +223,7 @@ void ObjectInvariant() { Contract.Invariant(StepOps.Count == Hints.Count); } - public CalcStmt(RangeToken rangeOrigin, CalcOp userSuppliedOp, List lines, List hints, List stepOps, Attributes attrs) + public CalcStmt(IOrigin rangeOrigin, CalcOp userSuppliedOp, List lines, List hints, List stepOps, Attributes attrs) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(lines != null); diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeLoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeLoopStmt.cs index fc88b91929d..fcbf6fb60b9 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeLoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeLoopStmt.cs @@ -21,7 +21,7 @@ public AlternativeLoopStmt(Cloner cloner, AlternativeLoopStmt original) : base(c UsesOptionalBraces = original.UsesOptionalBraces; } - public AlternativeLoopStmt(RangeToken rangeOrigin, + public AlternativeLoopStmt(IOrigin rangeOrigin, List invariants, Specification decreases, Specification mod, List alternatives, bool usesOptionalBraces) : base(rangeOrigin, invariants, decreases, mod) { @@ -29,7 +29,7 @@ public AlternativeLoopStmt(RangeToken rangeOrigin, this.Alternatives = alternatives; this.UsesOptionalBraces = usesOptionalBraces; } - public AlternativeLoopStmt(RangeToken rangeOrigin, + public AlternativeLoopStmt(IOrigin rangeOrigin, List invariants, Specification decreases, Specification mod, List alternatives, bool usesOptionalBraces, Attributes attrs) : base(rangeOrigin, invariants, decreases, mod, attrs) { diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs index d26e6dcb867..5526e075870 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/AlternativeStmt.cs @@ -21,13 +21,13 @@ public AlternativeStmt(Cloner cloner, AlternativeStmt original) : base(cloner, o UsesOptionalBraces = original.UsesOptionalBraces; } - public AlternativeStmt(RangeToken rangeOrigin, List alternatives, bool usesOptionalBraces) + public AlternativeStmt(IOrigin rangeOrigin, List alternatives, bool usesOptionalBraces) : base(rangeOrigin) { Contract.Requires(alternatives != null); Alternatives = alternatives; UsesOptionalBraces = usesOptionalBraces; } - public AlternativeStmt(RangeToken rangeOrigin, List alternatives, bool usesOptionalBraces, Attributes attrs) + public AlternativeStmt(IOrigin rangeOrigin, List alternatives, bool usesOptionalBraces, Attributes attrs) : base(rangeOrigin, attrs) { Contract.Requires(alternatives != null); Alternatives = alternatives; diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/BreakOrContinueStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/BreakOrContinueStmt.cs index 931a618e7e4..5f2a031d41c 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/BreakOrContinueStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/BreakOrContinueStmt.cs @@ -31,7 +31,7 @@ public BreakOrContinueStmt(Cloner cloner, BreakOrContinueStmt original) : base(c } } - public BreakOrContinueStmt(RangeToken rangeOrigin, IOrigin targetLabel, bool isContinue, Attributes attributes = null) + public BreakOrContinueStmt(IOrigin rangeOrigin, IOrigin targetLabel, bool isContinue, Attributes attributes = null) : base(rangeOrigin, attributes) { Contract.Requires(rangeOrigin != null); Contract.Requires(targetLabel != null); @@ -43,7 +43,7 @@ public BreakOrContinueStmt(RangeToken rangeOrigin, IOrigin targetLabel, bool isC /// For "isContinue == false", represents the statement "break ^breakAndContinueCount ;". /// For "isContinue == true", represents the statement "break ^(breakAndContinueCount - 1) continue;". /// - public BreakOrContinueStmt(RangeToken rangeOrigin, int breakAndContinueCount, bool isContinue, Attributes attributes = null) + public BreakOrContinueStmt(IOrigin rangeOrigin, int breakAndContinueCount, bool isContinue, Attributes attributes = null) : base(rangeOrigin, attributes) { Contract.Requires(rangeOrigin != null); Contract.Requires(1 <= breakAndContinueCount); diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/ForLoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/ForLoopStmt.cs index 0581daa34c9..cd1d06d2c08 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/ForLoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/ForLoopStmt.cs @@ -20,7 +20,7 @@ public ForLoopStmt(Cloner cloner, ForLoopStmt original) : base(cloner, original) GoingUp = original.GoingUp; } - public ForLoopStmt(RangeToken rangeOrigin, BoundVar loopIndexVariable, Expression start, Expression/*?*/ end, bool goingUp, + public ForLoopStmt(IOrigin rangeOrigin, BoundVar loopIndexVariable, Expression start, Expression/*?*/ end, bool goingUp, List invariants, Specification decreases, Specification mod, BlockStmt /*?*/ body, Attributes attrs) : base(rangeOrigin, invariants, decreases, mod, body, attrs) { diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs index 651af155f8d..c050c40163e 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/ForallStmt.cs @@ -63,7 +63,7 @@ public ForallStmt(Cloner cloner, ForallStmt original) : base(cloner, original) { } } - public ForallStmt(RangeToken rangeOrigin, List boundVars, Attributes attrs, Expression range, List ens, Statement body) + public ForallStmt(IOrigin rangeOrigin, List boundVars, Attributes attrs, Expression range, List ens, Statement body) : base(rangeOrigin, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(boundVars)); diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs index d3eddc5274e..6476299dcec 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/IfStmt.cs @@ -26,7 +26,7 @@ public IfStmt(Cloner cloner, IfStmt original) : base(cloner, original) { Els = cloner.CloneStmt(original.Els, false); } - public IfStmt(RangeToken rangeOrigin, bool isBindingGuard, Expression guard, BlockStmt thn, Statement els) + public IfStmt(IOrigin rangeOrigin, bool isBindingGuard, Expression guard, BlockStmt thn, Statement els) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(!isBindingGuard || (guard is ExistsExpr && ((ExistsExpr)guard).Range == null)); @@ -37,7 +37,7 @@ public IfStmt(RangeToken rangeOrigin, bool isBindingGuard, Expression guard, Blo Thn = thn; Els = els; } - public IfStmt(RangeToken rangeOrigin, bool isBindingGuard, Expression guard, BlockStmt thn, Statement els, Attributes attrs) + public IfStmt(IOrigin rangeOrigin, bool isBindingGuard, Expression guard, BlockStmt thn, Statement els, Attributes attrs) : base(rangeOrigin, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(!isBindingGuard || (guard is ExistsExpr && ((ExistsExpr)guard).Range == null)); diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs index 87ed107ad3c..9c7c8c8cfdf 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs @@ -26,7 +26,7 @@ protected LoopStmt(Cloner cloner, LoopStmt original) : base(cloner, original) { } } - public LoopStmt(RangeToken rangeOrigin, List invariants, Specification decreases, Specification mod) + public LoopStmt(IOrigin rangeOrigin, List invariants, Specification decreases, Specification mod) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(invariants)); @@ -37,7 +37,7 @@ public LoopStmt(RangeToken rangeOrigin, List invariants, S this.Decreases = decreases; this.Mod = mod; } - public LoopStmt(RangeToken rangeOrigin, List invariants, Specification decreases, Specification mod, Attributes attrs) + public LoopStmt(IOrigin rangeOrigin, List invariants, Specification decreases, Specification mod, Attributes attrs) : base(rangeOrigin, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(invariants)); @@ -85,5 +85,5 @@ public override IEnumerable SpecificationSubExpressions { } } - public IOrigin NavigationToken => Tok; + public IOrigin NavigationToken => StartToken; } \ No newline at end of file diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs index 41995a926a8..9d15140f315 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/OneBodyLoopStmt.cs @@ -21,7 +21,7 @@ protected OneBodyLoopStmt(Cloner cloner, OneBodyLoopStmt original) : base(cloner } } - protected OneBodyLoopStmt(RangeToken rangeOrigin, + protected OneBodyLoopStmt(IOrigin rangeOrigin, List invariants, Specification decreases, Specification mod, BlockStmt /*?*/ body, Attributes/*?*/ attrs) : base(rangeOrigin, invariants, decreases, mod, attrs) { diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/RefinedWhileStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/RefinedWhileStmt.cs index 6f06497e28c..d8a4127bcf9 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/RefinedWhileStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/RefinedWhileStmt.cs @@ -8,7 +8,7 @@ namespace Microsoft.Dafny; /// merge. /// public class RefinedWhileStmt : WhileStmt { - public RefinedWhileStmt(RangeToken rangeOrigin, Expression guard, + public RefinedWhileStmt(IOrigin rangeOrigin, Expression guard, List invariants, Specification decreases, Specification mod, BlockStmt body) : base(rangeOrigin, guard, invariants, decreases, mod, body) { diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs index 3a8a0693896..4c6b68abf82 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/WhileStmt.cs @@ -23,14 +23,14 @@ public WhileStmt(Cloner cloner, WhileStmt original) : base(cloner, original) { Guard = cloner.CloneExpr(original.Guard); } - public WhileStmt(RangeToken rangeOrigin, Expression guard, + public WhileStmt(IOrigin rangeOrigin, Expression guard, List invariants, Specification decreases, Specification mod, BlockStmt body) : base(rangeOrigin, invariants, decreases, mod, body, null) { Guard = guard; } - public WhileStmt(RangeToken rangeOrigin, Expression guard, + public WhileStmt(IOrigin rangeOrigin, Expression guard, List invariants, Specification decreases, Specification mod, BlockStmt body, Attributes attrs) : base(rangeOrigin, invariants, decreases, mod, body, attrs) { diff --git a/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs b/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs index 3d7b3b3f815..6f643a1ce25 100644 --- a/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs +++ b/Source/DafnyCore/AST/Statements/DividedBlockStmt.cs @@ -22,7 +22,7 @@ public DividedBlockStmt(Cloner cloner, DividedBlockStmt original) : base(cloner, SeparatorTok = original.SeparatorTok; } - public DividedBlockStmt(RangeToken rangeOrigin, List bodyInit, IOrigin/*?*/ separatorTok, List bodyProper) + public DividedBlockStmt(IOrigin rangeOrigin, List bodyInit, IOrigin/*?*/ separatorTok, List bodyProper) : base(rangeOrigin, Util.Concat(bodyInit, bodyProper)) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(bodyInit)); diff --git a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs index f8b0952ec1e..8c29b026e55 100644 --- a/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/CallStmt.cs @@ -33,7 +33,7 @@ public override IEnumerable GetAssignedLocals() { public Expression Receiver => MethodSelect.Obj; public Method Method => (Method)MethodSelect.Member; - public CallStmt(RangeToken rangeOrigin, List lhs, MemberSelectExpr memSel, List args, IOrigin overrideToken = null) + public CallStmt(IOrigin rangeOrigin, List lhs, MemberSelectExpr memSel, List args, IOrigin overrideToken = null) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(lhs)); @@ -62,7 +62,7 @@ public CallStmt(Cloner cloner, CallStmt original) : base(cloner, original) { /// This constructor is intended to be used when constructing a resolved CallStmt. The "args" are expected /// to be already resolved, and are all given positionally. /// - public CallStmt(RangeToken rangeOrigin, List lhs, MemberSelectExpr memSel, List args) + public CallStmt(IOrigin rangeOrigin, List lhs, MemberSelectExpr memSel, List args) : this(rangeOrigin, lhs, memSel, args.ConvertAll(e => new ActualBinding(null, e))) { Bindings.AcceptArgumentExpressionsAsExactParameterList(); } diff --git a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs index 5ac850414c7..15f92816a13 100644 --- a/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/PrintStmt.cs @@ -33,7 +33,7 @@ public PrintStmt(Cloner cloner, PrintStmt original) : base(cloner, original) { Args = original.Args.Select(cloner.CloneExpr).ToList(); } - public PrintStmt(RangeToken rangeOrigin, List args) + public PrintStmt(IOrigin rangeOrigin, List args) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(cce.NonNullElements(args)); diff --git a/Source/DafnyCore/AST/Statements/Methods/ProduceStmt.cs b/Source/DafnyCore/AST/Statements/Methods/ProduceStmt.cs index 4a05e91e1d4..28e012f2b11 100644 --- a/Source/DafnyCore/AST/Statements/Methods/ProduceStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/ProduceStmt.cs @@ -19,7 +19,7 @@ protected ProduceStmt(Cloner cloner, ProduceStmt original) : base(cloner, origin } } - protected ProduceStmt(RangeToken rangeOrigin, List rhss, Attributes attributes) + protected ProduceStmt(IOrigin rangeOrigin, List rhss, Attributes attributes) : base(rangeOrigin, attributes) { this.Rhss = rhss; HiddenUpdate = null; diff --git a/Source/DafnyCore/AST/Statements/Methods/ReturnStmt.cs b/Source/DafnyCore/AST/Statements/Methods/ReturnStmt.cs index d188c10d3ce..e6eb0612921 100644 --- a/Source/DafnyCore/AST/Statements/Methods/ReturnStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/ReturnStmt.cs @@ -14,7 +14,7 @@ public ReturnStmt(Cloner cloner, ReturnStmt original) : base(cloner, original) { ReverifyPost = original.ReverifyPost; } - public ReturnStmt(RangeToken rangeOrigin, List rhss, Attributes attributes = null) + public ReturnStmt(IOrigin rangeOrigin, List rhss, Attributes attributes = null) : base(rangeOrigin, rhss, attributes) { Contract.Requires(rangeOrigin != null); } diff --git a/Source/DafnyCore/AST/Statements/Methods/YieldStmt.cs b/Source/DafnyCore/AST/Statements/Methods/YieldStmt.cs index dd6a3b38e59..cd3d566111a 100644 --- a/Source/DafnyCore/AST/Statements/Methods/YieldStmt.cs +++ b/Source/DafnyCore/AST/Statements/Methods/YieldStmt.cs @@ -10,7 +10,7 @@ public YieldStmt Clone(Cloner cloner) { public YieldStmt(Cloner cloner, YieldStmt original) : base(cloner, original) { } - public YieldStmt(RangeToken rangeOrigin, List rhss) + public YieldStmt(IOrigin rangeOrigin, List rhss) : base(rangeOrigin, rhss, null) { } diff --git a/Source/DafnyCore/AST/Statements/OpaqueBlock.cs b/Source/DafnyCore/AST/Statements/OpaqueBlock.cs index 3d7ac1206fa..46d56a043db 100644 --- a/Source/DafnyCore/AST/Statements/OpaqueBlock.cs +++ b/Source/DafnyCore/AST/Statements/OpaqueBlock.cs @@ -23,7 +23,7 @@ public override IEnumerable SpecificationSubExpressions { } } - public OpaqueBlock(RangeToken rangeOrigin, List body, + public OpaqueBlock(IOrigin rangeOrigin, List body, List ensures, Specification modifies) : base(rangeOrigin, body) { Ensures = ensures; diff --git a/Source/DafnyCore/AST/Statements/SkeletonStatement.cs b/Source/DafnyCore/AST/Statements/SkeletonStatement.cs index eb7d99baa0b..8bedf479486 100644 --- a/Source/DafnyCore/AST/Statements/SkeletonStatement.cs +++ b/Source/DafnyCore/AST/Statements/SkeletonStatement.cs @@ -42,7 +42,7 @@ public SkeletonStatement(Cloner cloner, SkeletonStatement original) : base(clone BodyEllipsis = original.BodyEllipsis; } - public SkeletonStatement(RangeToken rangeOrigin) + public SkeletonStatement(IOrigin rangeOrigin) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); S = null; diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index d2d24383395..cd37b2c36e0 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public abstract class Statement : RangeNode, IAttributeBearingDeclaration { - public override IOrigin Tok => PostLabelToken ?? StartToken; + public override IOrigin Tok => PostLabelToken ?? Origin; public IOrigin PostLabelToken { get; set; } public int ScopeDepth { get; set; } @@ -36,11 +36,11 @@ protected Statement(Cloner cloner, Statement original) : base(cloner.Origin(orig } } - protected Statement(RangeToken rangeOrigin, Attributes attrs) : base(rangeOrigin) { + protected Statement(IOrigin rangeOrigin, Attributes attrs) : base(rangeOrigin) { this.Attributes = attrs; } - protected Statement(RangeToken rangeOrigin) + protected Statement(IOrigin rangeOrigin) : this(rangeOrigin, null) { Contract.Requires(rangeOrigin != null); } @@ -142,9 +142,9 @@ public static VarDeclStmt CreateLocalVariable(IOrigin tok, string name, Type typ Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(type != null); - var variable = new LocalVariable(tok.ToRange(), name, type, false); + var variable = new LocalVariable(tok, name, type, false); variable.type = type; - return new VarDeclStmt(tok.ToRange(), Util.Singleton(variable), null); + return new VarDeclStmt(tok, Util.Singleton(variable), null); } /// @@ -154,20 +154,18 @@ public static VarDeclStmt CreateLocalVariable(IOrigin tok, string name, Expressi Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(value != null); - var rangeToken = new RangeToken(tok, tok); - var variable = new LocalVariable(rangeToken, name, value.Type, false); + var variable = new LocalVariable(tok, name, value.Type, false); variable.type = value.Type; Expression variableExpr = new IdentifierExpr(tok, variable); - var variableUpdateStmt = new AssignStatement(rangeToken, Util.Singleton(variableExpr), + var variableUpdateStmt = new AssignStatement(tok, Util.Singleton(variableExpr), Util.Singleton(new ExprRhs(value))); - var variableAssignStmt = new SingleAssignStmt(rangeToken, variableUpdateStmt.Lhss[0], variableUpdateStmt.Rhss[0]); + var variableAssignStmt = new SingleAssignStmt(tok, variableUpdateStmt.Lhss[0], variableUpdateStmt.Rhss[0]); variableUpdateStmt.ResolvedStatements = new List() { variableAssignStmt }; - return new VarDeclStmt(rangeToken, Util.Singleton(variable), variableUpdateStmt); + return new VarDeclStmt(tok, Util.Singleton(variable), variableUpdateStmt); } public static PrintStmt CreatePrintStmt(IOrigin tok, params Expression[] exprs) { - var rangeToken = new RangeToken(tok, tok); - return new PrintStmt(rangeToken, exprs.ToList()); + return new PrintStmt(tok, exprs.ToList()); } public override string ToString() { diff --git a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs index a90255050d9..9583c6ee97a 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssertStmt.cs @@ -25,7 +25,7 @@ public static AssertStmt CreateErrorAssert(INode node, string message, Expressio return assertFalse; } - public AssertStmt(RangeToken rangeOrigin, Expression expr, AssertLabel/*?*/ label, Attributes attrs) + public AssertStmt(IOrigin rangeOrigin, Expression expr, AssertLabel/*?*/ label, Attributes attrs) : base(rangeOrigin, expr, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(expr != null); diff --git a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs index 688e90052a8..d19e6bcaf71 100644 --- a/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/AssumeStmt.cs @@ -12,7 +12,7 @@ public AssumeStmt Clone(Cloner cloner) { public AssumeStmt(Cloner cloner, AssumeStmt original) : base(cloner, original) { } - public AssumeStmt(RangeToken rangeOrigin, Expression expr, Attributes attrs) + public AssumeStmt(IOrigin rangeOrigin, Expression expr, Attributes attrs) : base(rangeOrigin, expr, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(expr != null); diff --git a/Source/DafnyCore/AST/Statements/Verification/ExpectStmt.cs b/Source/DafnyCore/AST/Statements/Verification/ExpectStmt.cs index 18ee1402e59..ac944983c00 100644 --- a/Source/DafnyCore/AST/Statements/Verification/ExpectStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/ExpectStmt.cs @@ -16,7 +16,7 @@ public ExpectStmt(Cloner cloner, ExpectStmt original) : base(cloner, original) { Message = cloner.CloneExpr(original.Message); } - public ExpectStmt(RangeToken rangeOrigin, Expression expr, Expression message, Attributes attrs) + public ExpectStmt(IOrigin rangeOrigin, Expression expr, Expression message, Attributes attrs) : base(rangeOrigin, expr, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(expr != null); diff --git a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs index 59edec6a9e2..39e5b9cde32 100644 --- a/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs @@ -44,14 +44,14 @@ public HideRevealStmt(Cloner cloner, HideRevealStmt original) : base(cloner, ori } } - public HideRevealStmt(RangeToken rangeOrigin, HideRevealCmd.Modes mode) + public HideRevealStmt(IOrigin rangeOrigin, HideRevealCmd.Modes mode) : base(rangeOrigin) { Wildcard = true; this.Exprs = null; Mode = mode; } - public HideRevealStmt(RangeToken rangeOrigin, List exprs, HideRevealCmd.Modes mode) + public HideRevealStmt(IOrigin rangeOrigin, List exprs, HideRevealCmd.Modes mode) : base(rangeOrigin) { Contract.Requires(exprs != null); this.Exprs = exprs; diff --git a/Source/DafnyCore/AST/Statements/Verification/ModifyStmt.cs b/Source/DafnyCore/AST/Statements/Verification/ModifyStmt.cs index 0ea1d682057..7ac88dee9bb 100644 --- a/Source/DafnyCore/AST/Statements/Verification/ModifyStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/ModifyStmt.cs @@ -16,7 +16,7 @@ public ModifyStmt(Cloner cloner, ModifyStmt original) : base(cloner, original) { Body = cloner.CloneBlockStmt(original.Body); } - public ModifyStmt(RangeToken rangeOrigin, List mod, Attributes attrs, BlockStmt body) + public ModifyStmt(IOrigin rangeOrigin, List mod, Attributes attrs, BlockStmt body) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(mod != null); diff --git a/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs b/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs index 673cc68aead..43ed1ef4950 100644 --- a/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs +++ b/Source/DafnyCore/AST/Statements/Verification/PredicateStmt.cs @@ -13,14 +13,14 @@ protected PredicateStmt(Cloner cloner, PredicateStmt original) : base(cloner, or Expr = cloner.CloneExpr(original.Expr); } - protected PredicateStmt(RangeToken rangeOrigin, Expression expr, Attributes attrs) + protected PredicateStmt(IOrigin rangeOrigin, Expression expr, Attributes attrs) : base(rangeOrigin, attrs) { Contract.Requires(rangeOrigin != null); Contract.Requires(expr != null); this.Expr = expr; } - protected PredicateStmt(RangeToken rangeOrigin, Expression expr) + protected PredicateStmt(IOrigin rangeOrigin, Expression expr) : this(rangeOrigin, expr, null) { Contract.Requires(rangeOrigin != null); Contract.Requires(expr != null); diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index a60cce44249..5cee5fea23e 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/Source/DafnyCore/AST/SystemModuleManager.cs @@ -302,7 +302,7 @@ Function CreateMember(string name, Type resultType, Function readsFunction = nul var args = Util.Map(Enumerable.Range(0, arity), i => new Formal(tok, "x" + i, tys[i], true, false, null)); var argExprs = args.ConvertAll(a => (Expression)new IdentifierExpr(tok, a.Name) { Var = a, Type = a.Type }); - var readsIS = new FunctionCallExpr(tok, "reads", new ImplicitThisExpr(tok), tok, tok, argExprs) { + var readsIS = new FunctionCallExpr(tok, "reads", new ImplicitThisExpr(tok), tok, Token.NoToken, argExprs) { Type = ObjectSetType(), }; var readsFrame = new List { new FrameExpression(tok, readsIS, null) }; @@ -333,7 +333,7 @@ Function CreateMember(string name, Type resultType, Function readsFunction = nul var id = new BoundVar(tok, "f", new ArrowType(tok, arrowDecl, tys)); var partialArrow = new SubsetTypeDecl(RangeToken.NoToken, new Name(ArrowType.PartialArrowTypeName(arity)), new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule, - id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, reads, tps, false), SubsetTypeDecl.WKind.Special, null, DontCompile()); + id, ArrowSubtypeConstraint(tok, tok, id, reads, tps, false), SubsetTypeDecl.WKind.Special, null, DontCompile()); ((RedirectingTypeDecl)partialArrow).ConstraintIsCompilable = false; PartialArrowTypeDecls.Add(arity, partialArrow); SystemModule.SourceDecls.Add(partialArrow); @@ -348,7 +348,7 @@ Function CreateMember(string name, Type resultType, Function readsFunction = nul id = new BoundVar(tok, "f", new UserDefinedType(tok, partialArrow.Name, partialArrow, tys)); var totalArrow = new SubsetTypeDecl(RangeToken.NoToken, new Name(ArrowType.TotalArrowTypeName(arity)), new TypeParameter.TypeParameterCharacteristics(false), tps, SystemModule, - id, ArrowSubtypeConstraint(tok, tok.ToRange(), id, req, tps, true), SubsetTypeDecl.WKind.Special, null, DontCompile()); + id, ArrowSubtypeConstraint(tok, tok, id, req, tps, true), SubsetTypeDecl.WKind.Special, null, DontCompile()); ((RedirectingTypeDecl)totalArrow).ConstraintIsCompilable = false; TotalArrowTypeDecls.Add(arity, totalArrow); SystemModule.SourceDecls.Add(totalArrow); @@ -360,7 +360,7 @@ Function CreateMember(string name, Type resultType, Function readsFunction = nul /// the built-in total-arrow type (if "total", in which case "member" is expected to denote the "requires" member). /// The given "id" is expected to be already resolved. /// - private Expression ArrowSubtypeConstraint(IOrigin tok, RangeToken rangeOrigin, BoundVar id, Function member, List tps, bool total) { + private Expression ArrowSubtypeConstraint(IOrigin tok, IOrigin rangeOrigin, BoundVar id, Function member, List tps, bool total) { Contract.Requires(tok != null); Contract.Requires(id != null); Contract.Requires(member != null); @@ -384,7 +384,7 @@ private Expression ArrowSubtypeConstraint(IOrigin tok, RangeToken rangeOrigin, B TypeApplicationJustMember = new List(), Type = GetTypeOfFunction(member, tps.ConvertAll(tp => (Type)new UserDefinedType(tp)), new List()) }; - Expression body = new ApplyExpr(tok, fn, args, tok); + Expression body = new ApplyExpr(tok, fn, args, Token.NoToken); body.Type = member.ResultType; // resolve here if (!total) { Expression emptySet = new SetDisplayExpr(tok, true, new List()); diff --git a/Source/DafnyCore/AST/Tokens.cs b/Source/DafnyCore/AST/Tokens.cs index 997528bb905..fff05fbb4a5 100644 --- a/Source/DafnyCore/AST/Tokens.cs +++ b/Source/DafnyCore/AST/Tokens.cs @@ -14,6 +14,8 @@ public class Token : IOrigin { public static readonly Token NoToken = new(); public static readonly Token Cli = new(1, 1); public static readonly Token Ide = new(1, 1); + public string filename => Path.GetFileName(Filepath); + public Token() : this(0, 0) { } public Token(int linenum, int colnum) { @@ -25,9 +27,17 @@ public Token(int linenum, int colnum) { public bool IsSourceToken => this != NoToken; public int kind { get; set; } // Used by coco, so we can't rename it to Kind + public bool IsInherited(ModuleDefinition m) { + return false; + } + + public bool InclusiveEnd => true; + public bool IncludesRange => false; public string ActualFilename => Filepath; public string Filepath => Uri?.LocalPath; public Uri Uri { get; set; } + public Token StartToken => this; + public Token EndToken => this; public int pos { get; set; } // Used by coco, so we can't rename it to Pos @@ -53,6 +63,8 @@ public Token(int linenum, int colnum) { public bool IsValid => this.ActualFilename != null; + public RangeToken To(Token end) => new(this, end); + public IOrigin WithVal(string newVal) { return new Token { pos = pos, @@ -94,10 +106,56 @@ public int CompareTo(IOrigin other) { public static class TokenExtensions { + public static DafnyRange ToDafnyRange(this IOrigin origin, bool includeTrailingWhitespace = false) { + var startLine = origin.StartToken.line - 1; + var startColumn = origin.StartToken.col - 1; + var endLine = origin.EndToken.line - 1; + int whitespaceOffset = 0; + if (includeTrailingWhitespace) { + string trivia = origin.EndToken.TrailingTrivia; + // Don't want to remove newlines or comments -- just spaces and tabs + while (whitespaceOffset < trivia.Length && (trivia[whitespaceOffset] == ' ' || trivia[whitespaceOffset] == '\t')) { + whitespaceOffset++; + } + } + + var endColumn = origin.EndToken.col + (origin.InclusiveEnd ? origin.EndToken.val.Length : 0) + whitespaceOffset - 1; + return new DafnyRange( + new DafnyPosition(startLine, startColumn), + new DafnyPosition(endLine, endColumn)); + } + + public static BoogieRangeOrigin ToToken(this IOrigin origin) { + return new BoogieRangeOrigin(origin.StartToken, origin.EndToken, null); + } + + public static IOrigin MakeAutoGenerated(this IOrigin origin) { + return new AutoGeneratedOrigin(origin); + } + + public static IOrigin MakeRefined(this IOrigin origin, ModuleDefinition module) { + return new RefinementOrigin(origin, module); + } + + public static bool Contains(this IOrigin container, IOrigin otherToken) { + return container.StartToken.Uri == otherToken.Uri && + container.StartToken.pos <= otherToken.pos && + (container.EndToken == null || otherToken.pos <= container.EndToken.pos); + } + + public static bool Intersects(this IOrigin origin, IOrigin other) { + return !(other.EndToken.pos + other.EndToken.val.Length <= origin.StartToken.pos + || origin.EndToken.pos + origin.EndToken.val.Length <= other.StartToken.pos); + } + + public static string PrintOriginal(this IOrigin origin) { + return new RangeToken(origin.StartToken, origin.EndToken).PrintOriginal(); + } + public static bool IsSet(this IOrigin token) => token.Uri != null; public static string TokenToString(this IOrigin tok, DafnyOptions options) { - if (tok == Token.Cli) { + if (ReferenceEquals(tok, Token.Cli)) { return "CLI"; } @@ -116,23 +174,12 @@ public static string TokenToString(this IOrigin tok, DafnyOptions options) { return $"{filename}({tok.line},{tok.col - 1})"; } - - public static RangeToken ToRange(this IOrigin token) { - if (token is BoogieRangeOrigin boogieRangeToken) { - return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken); - } - - if (token is NestedOrigin nestedToken) { - return ToRange(nestedToken.Outer); - } - return token as RangeToken ?? new RangeToken(token, token); - } } public class BoogieRangeOrigin : OriginWrapper { // The wrapped token is the startTok - public IOrigin StartToken { get; } - public IOrigin EndToken { get; } + public override Token StartToken { get; } + public override Token EndToken { get; } /// /// If only a single position is used to refer to this piece of code, this position is the best @@ -142,7 +189,7 @@ public class BoogieRangeOrigin : OriginWrapper { // Used for range reporting public override string val => new(' ', Math.Max(EndToken.pos + EndToken.val.Length - pos, 1)); - public BoogieRangeOrigin(IOrigin startTok, IOrigin endTok, IOrigin center) : base( + public BoogieRangeOrigin(Token startTok, Token endTok, IOrigin center) : base( center ?? startTok) { StartToken = startTok; EndToken = endTok; @@ -152,10 +199,6 @@ public BoogieRangeOrigin(IOrigin startTok, IOrigin endTok, IOrigin center) : bas public override IOrigin WithVal(string newVal) { return this; } - - public string PrintOriginal() { - return new RangeToken(StartToken, EndToken).PrintOriginal(); - } } public class NestedOrigin : OriginWrapper { diff --git a/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs index 8e1cc55648e..471974265b6 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/AbstractTypeDecl.cs @@ -11,7 +11,7 @@ public bool SupportsEquality { get { return Characteristics.EqualitySupport != TypeParameter.EqualitySupportValue.Unspecified; } } - public AbstractTypeDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, + public AbstractTypeDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeArgs, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs index 2adb01a91b5..af54ff39e4b 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassDecl.cs @@ -15,7 +15,7 @@ void ObjectInvariant() { Contract.Invariant(ParentTraits != null); } - public ClassDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, + public ClassDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List/*?*/ traits) : base(rangeOrigin, name, module, typeArgs, members, attributes, isRefining, traits) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs index ec287a98579..828f0796fa2 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/ClassLikeDecl.cs @@ -24,7 +24,7 @@ public bool IsObjectTrait { public TopLevelDecl AsTopLevelDecl => this; public TypeDeclSynonymInfo SynonymInfo { get; set; } - public ClassLikeDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, + public ClassLikeDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List/*?*/ traits) : base(rangeOrigin, name, module, typeArgs, members, attributes, isRefining, traits) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs index b86272eab7b..d1de640ee9d 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/CoDatatypeDecl.cs @@ -8,7 +8,7 @@ public class CoDatatypeDecl : DatatypeDecl { public override string WhatKind { get { return "codatatype"; } } [FilledInDuringResolution] public CoDatatypeDecl SscRepr; - public CoDatatypeDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, List typeArgs, + public CoDatatypeDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List ctors, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeArgs, ctors, parentTraits, members, attributes, isRefining) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs index 03439bd52b4..15368e12935 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs @@ -24,7 +24,7 @@ void ObjectInvariant() { [FilledInDuringResolution] public SpecialField QueryField; [FilledInDuringResolution] public List Destructors = new List(); // includes both implicit (not mentionable in source) and explicit destructors - public DatatypeCtor(RangeToken rangeOrigin, Name name, bool isGhost, [Captured] List formals, Attributes attributes) + public DatatypeCtor(IOrigin rangeOrigin, Name name, bool isGhost, [Captured] List formals, Attributes attributes) : base(rangeOrigin, name, attributes, false) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs index 3cfbb646c25..bd6a62e9ae6 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs @@ -21,7 +21,7 @@ void ObjectInvariant() { public override IEnumerable PreResolveChildren => Ctors.Concat(base.PreResolveChildren); - public DatatypeDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, List typeArgs, + public DatatypeDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List ctors, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeArgs, members, attributes, isRefining, parentTraits) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs index ce0dab4b9d0..c931962af34 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/Declaration.cs @@ -15,8 +15,8 @@ void ObjectInvariant() { public IOrigin BodyStartTok = Token.NoToken; public Name NameNode; - public override IOrigin Tok => NameNode.StartToken; - public virtual IOrigin NavigationToken => NameNode.StartToken; + public override IOrigin Tok => NameNode.Origin; + public virtual IOrigin NavigationToken => NameNode.Origin; public string Name => NameNode.Value; public bool IsRefining; @@ -32,7 +32,7 @@ protected Declaration(Cloner cloner, Declaration original) : base(cloner, origin Attributes = cloner.CloneAttributes(original.Attributes); } - protected Declaration(RangeToken rangeOrigin, Name name, Attributes attributes, bool isRefining) : base(rangeOrigin) { + protected Declaration(IOrigin rangeOrigin, Name name, Attributes attributes, bool isRefining) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); this.NameNode = name; diff --git a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs index 3a37788c0eb..34868ddaedd 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IndDatatypeDecl.cs @@ -32,7 +32,7 @@ public bool[] TypeParametersUsedInConstructionByGroundingCtor { public enum ES { NotYetComputed, Never, ConsultTypeArguments } public ES EqualitySupport = ES.NotYetComputed; - public IndDatatypeDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, List typeArgs, + public IndDatatypeDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List ctors, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeArgs, ctors, parentTraits, members, attributes, isRefining) { Contract.Requires(rangeOrigin != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs index 54a54811461..e0e980b1118 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs @@ -29,7 +29,7 @@ public class IteratorDecl : ClassDecl, IMethodCodeContext, ICanVerify, ICodeCont [FilledInDuringResolution] public Method Member_MoveNext; // created during registration phase of resolution; public readonly LocalVariable YieldCountVariable; - public IteratorDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, List typeArgs, + public IteratorDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, List ins, List outs, Specification reads, Specification mod, Specification decreases, List requires, diff --git a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs index f58836510a8..608e237235e 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs @@ -32,7 +32,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { [FilledInDuringResolution] public bool TargetTypeCoversAllBitPatterns; // "target complete" -- indicates that any bit pattern that can fill the target type is a value of the newtype - public NewtypeDecl(RangeToken rangeOrigin, Name name, List typeParameters, ModuleDefinition module, + public NewtypeDecl(IOrigin rangeOrigin, Name name, List typeParameters, ModuleDefinition module, Type baseType, SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeParameters, members, attributes, isRefining, parentTraits) { @@ -47,7 +47,7 @@ public NewtypeDecl(RangeToken rangeOrigin, Name name, List typePa WitnessKind = witnessKind; this.NewSelfSynonym(); } - public NewtypeDecl(RangeToken rangeOrigin, Name name, List typeParameters, ModuleDefinition module, + public NewtypeDecl(IOrigin rangeOrigin, Name name, List typeParameters, ModuleDefinition module, BoundVar bv, Expression constraint, SubsetTypeDecl.WKind witnessKind, Expression witness, List parentTraits, List members, Attributes attributes, bool isRefining) : base(rangeOrigin, name, module, typeParameters, members, attributes, isRefining, parentTraits) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs index d26493ee8d6..23905cb3776 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs @@ -26,7 +26,7 @@ bool RedirectingTypeDecl.ConstraintIsCompilable { } } - public SubsetTypeDecl(RangeToken rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, + public SubsetTypeDecl(IOrigin rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, BoundVar id, Expression constraint, WKind witnessKind, Expression witness, Attributes attributes) : base(rangeOrigin, name, characteristics, typeArgs, module, id.Type, attributes) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs index e001ee55a0a..926ba85da96 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs @@ -20,7 +20,7 @@ protected TopLevelDecl(Cloner cloner, TopLevelDecl original, ModuleDefinition pa EnclosingModuleDefinition = parent; } - protected TopLevelDecl(RangeToken rangeOrigin, Name name, ModuleDefinition enclosingModule, List typeArgs, Attributes attributes, bool isRefining) + protected TopLevelDecl(IOrigin rangeOrigin, Name name, ModuleDefinition enclosingModule, List typeArgs, Attributes attributes, bool isRefining) : base(rangeOrigin, name, attributes, isRefining) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs index 810772a50b5..7d3fa2a0a03 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs @@ -87,7 +87,7 @@ public void Extend(TraitDecl parent, InheritanceInformationClass parentInfo, Dic } } - protected TopLevelDeclWithMembers(RangeToken rangeOrigin, Name name, ModuleDefinition module, + protected TopLevelDeclWithMembers(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, List members, Attributes attributes, bool isRefining, List/*?*/ traits = null) : base(rangeOrigin, name, module, typeArgs, attributes, isRefining) { diff --git a/Source/DafnyCore/AST/TypeDeclarations/TraitDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TraitDecl.cs index eaf9a399c76..760e9959072 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TraitDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TraitDecl.cs @@ -25,7 +25,7 @@ internal void SetUpAsReferenceType(bool isReferenceType) { /// This constructor creates a TraitDecl object. However, before the object really functions as a TraitDecl, it is necessary /// to call SetUpAsReferenceType, which sets .NonNullTypeDecl (if necessary) and calls NewSelfSynonym(). /// - public TraitDecl(RangeToken rangeOrigin, Name name, ModuleDefinition module, + public TraitDecl(IOrigin rangeOrigin, Name name, ModuleDefinition module, List typeArgs, [Captured] List members, Attributes attributes, bool isRefining, List /*?*/ traits) : base(rangeOrigin, name, module, typeArgs, members, attributes, isRefining, traits) { } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs index 457fefd4e9b..925daa2e69c 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDecl.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; public class TypeSynonymDecl : TypeSynonymDeclBase, RevealableTypeDecl { public override string WhatKind => "type synonym"; - public TypeSynonymDecl(RangeToken rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + public TypeSynonymDecl(IOrigin rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) : base(rangeOrigin, name, characteristics, typeArgs, module, rhs, attributes) { this.NewSelfSynonym(); } @@ -20,7 +20,7 @@ public override string GetDescription(DafnyOptions options) { public class InternalTypeSynonymDecl : TypeSynonymDeclBase { public override string WhatKind { get { return "export-provided type"; } } - public InternalTypeSynonymDecl(RangeToken rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + public InternalTypeSynonymDecl(IOrigin rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) : base(rangeOrigin, name, characteristics, typeArgs, module, rhs, attributes) { } diff --git a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs index ef5b9f637e3..e1f248b004a 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs +++ b/Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs @@ -13,7 +13,7 @@ public bool SupportsEquality { } public readonly Type Rhs; - protected TypeSynonymDeclBase(RangeToken rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) + protected TypeSynonymDeclBase(IOrigin rangeOrigin, Name name, TypeParameter.TypeParameterCharacteristics characteristics, List typeArgs, ModuleDefinition module, Type rhs, Attributes attributes) : base(rangeOrigin, name, module, typeArgs, attributes, false) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); diff --git a/Source/DafnyCore/AST/Types/TypeParameter.cs b/Source/DafnyCore/AST/Types/TypeParameter.cs index a1258c454ff..86f31b4b290 100644 --- a/Source/DafnyCore/AST/Types/TypeParameter.cs +++ b/Source/DafnyCore/AST/Types/TypeParameter.cs @@ -186,7 +186,7 @@ public IEnumerable TypeBoundHeads { } } - public TypeParameter(RangeToken rangeOrigin, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics, + public TypeParameter(IOrigin rangeOrigin, Name name, TPVarianceSyntax varianceS, TypeParameterCharacteristics characteristics, List typeBounds) : base(rangeOrigin, name, null, new List(), null, false) { Contract.Requires(rangeOrigin != null); @@ -196,13 +196,13 @@ public TypeParameter(RangeToken rangeOrigin, Name name, TPVarianceSyntax varianc TypeBounds = typeBounds; } - public TypeParameter(RangeToken rangeOrigin, Name name, TPVarianceSyntax varianceS) + public TypeParameter(IOrigin rangeOrigin, Name name, TPVarianceSyntax varianceS) : this(rangeOrigin, name, varianceS, new TypeParameterCharacteristics(false), new List()) { Contract.Requires(rangeOrigin != null); Contract.Requires(name != null); } - public TypeParameter(RangeToken tok, Name name, int positionalIndex, ParentType parent) + public TypeParameter(IOrigin tok, Name name, int positionalIndex, ParentType parent) : this(tok, name, TPVarianceSyntax.NonVariant_Strict) { PositionalIndex = positionalIndex; Parent = parent; diff --git a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs index 01d1bf254ab..a410cf89780 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchAst.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchAst.cs @@ -142,7 +142,7 @@ public MatchStmt(Cloner cloner, MatchStmt original) : base(cloner, original) { } } - public MatchStmt(RangeToken rangeOrigin, Expression source, [Captured] List cases, + public MatchStmt(IOrigin rangeOrigin, Expression source, [Captured] List cases, bool usesOptionalBraces, MatchingContext context = null) : base(rangeOrigin) { Contract.Requires(rangeOrigin != null); @@ -154,7 +154,7 @@ public MatchStmt(RangeToken rangeOrigin, Expression source, [Captured] List cases, + public MatchStmt(IOrigin rangeOrigin, Expression source, [Captured] List cases, bool usesOptionalBraces, Attributes attrs, MatchingContext context = null) : base(rangeOrigin, attrs) { Contract.Requires(rangeOrigin != null); @@ -250,7 +250,7 @@ void ObjectInvariant() { public override IEnumerable Children => body; public override IEnumerable PreResolveChildren => Children; - public MatchCaseStmt(RangeToken rangeOrigin, DatatypeCtor ctor, bool fromBoundVar, [Captured] List arguments, [Captured] List body, Attributes attrs = null) + public MatchCaseStmt(IOrigin rangeOrigin, DatatypeCtor ctor, bool fromBoundVar, [Captured] List arguments, [Captured] List body, Attributes attrs = null) : base(rangeOrigin.StartToken, ctor, arguments) { Origin = rangeOrigin; Contract.Requires(tok != null); diff --git a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs index c6df0fb3c53..62993b18750 100644 --- a/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs +++ b/Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs @@ -414,7 +414,7 @@ private MatchCase CreateMatchCase(IOrigin tok, DatatypeCtor ctor, List var cloner = new Cloner(false, true); if (bodyContainer.Node is Statement statement) { var body = UnboxStmt(statement).Select(stmt => cloner.CloneStmt(stmt, false)).ToList(); - newMatchCase = new MatchCaseStmt(tok.ToRange(), ctor, fromBoundVar, freshPatBV, body, bodyContainer.Attributes); + newMatchCase = new MatchCaseStmt(tok, ctor, fromBoundVar, freshPatBV, body, bodyContainer.Attributes); } else { var body = (Expression)(bodyContainer.Node); var attrs = bodyContainer.Attributes; @@ -533,7 +533,7 @@ private CaseBody CreateIfElseIfChain(MatchCompilationState mti, MatchingContext blocks = blocks.Skip(1).ToList(); var tok = matchee.Tok; - var range = matchee.Tok.ToRange(); + var range = matchee.Tok; var guard = new BinaryExpr(mti.Match.Tok, BinaryExpr.Opcode.Eq, matchee, currBlock.Item1) { ResolvedOp = BinaryExpr.ResolvedOpcode.EqCommon, Type = Type.Bool @@ -584,7 +584,7 @@ record CaseBody(IOrigin Tok, Node Node, Attributes Attributes = null); private CaseBody PackBody(IOrigin tok, PatternPath path) { if (path is StmtPatternPath br) { - return new CaseBody(tok, new BlockStmt(tok.ToRange(), br.Body.ToList()), br.Attributes); + return new CaseBody(tok, new BlockStmt(tok, br.Body.ToList()), br.Attributes); } if (path is ExprPatternPath) { @@ -602,7 +602,7 @@ private List UnboxStmt(Statement statement) { return new List() { statement }; } - private BlockStmt BlockStmtOfCStmt(RangeToken rangeOrigin, Statement stmt) { + private BlockStmt BlockStmtOfCStmt(IOrigin rangeOrigin, Statement stmt) { if (stmt is BlockStmt) { return (BlockStmt)stmt; } diff --git a/Source/DafnyCore/CoverageReport/CoverageReport.cs b/Source/DafnyCore/CoverageReport/CoverageReport.cs index 3271f8f063b..9b5db49f03b 100644 --- a/Source/DafnyCore/CoverageReport/CoverageReport.cs +++ b/Source/DafnyCore/CoverageReport/CoverageReport.cs @@ -40,7 +40,7 @@ public CoverageReport(string name, string units, string suffix, Program program) /// /// Assign a coverage label to the code indicated by the range token. /// - public void LabelCode(RangeToken span, CoverageLabel label) { + public void LabelCode(IOrigin span, CoverageLabel label) { Contract.Assert(labelsByFile.ContainsKey(span.Uri)); var labeledFile = labelsByFile[span.Uri]; var coverageSpan = new CoverageSpan(span, label); diff --git a/Source/DafnyCore/CoverageReport/CoverageSpan.cs b/Source/DafnyCore/CoverageReport/CoverageSpan.cs index a6bef7345a2..c2345141535 100644 --- a/Source/DafnyCore/CoverageReport/CoverageSpan.cs +++ b/Source/DafnyCore/CoverageReport/CoverageSpan.cs @@ -6,10 +6,10 @@ namespace Microsoft.Dafny; public class CoverageSpan : IComparable { - public readonly RangeToken Span; + public readonly IOrigin Span; public readonly CoverageLabel Label; - public CoverageSpan(RangeToken span, CoverageLabel label) { + public CoverageSpan(IOrigin span, CoverageLabel label) { Contract.Assert(span.Uri != null); Contract.Assert(span.StartToken != null); Contract.Assert(span.EndToken != null); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 284c2f8d8f6..3794f9981b8 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -331,7 +331,7 @@ ModuleDefinition } (. ApplyOptionsFromAttributes(dmod.Attributes); .) ModuleQualifiedName (. var name = names[^1]; - prefixIds = names.GetRange(0,names.Count-1).Select(n => n.StartToken).ToList(); + prefixIds = names.GetRange(0,names.Count-1).Select(n => (IOrigin)n.StartToken).ToList(); .) [ "refines" ModuleQualifiedName (. implementationKind = ImplementationKind.Refinement; .) @@ -450,7 +450,7 @@ ModuleExport Name name; if (exportId.val == "export" || exportId.val == parent.Name) { isDefault = true; - name = new Name(exportId.ToRange(), parent.Name); + name = new Name(exportId, parent.Name); } else { name = new Name(exportId); } @@ -1253,7 +1253,7 @@ MethodDecl ] (. var range = new RangeToken(dmod.FirstToken, t); if (isConstructor) { - m = new Constructor(range, hasName ? name : new Name(dmod.FirstToken.ToRange(), "_ctor"), dmod.IsGhost, typeArgs, ins, + m = new Constructor(range, hasName ? name : new Name(dmod.FirstToken, "_ctor"), dmod.IsGhost, typeArgs, ins, req, new Specification(reads, readsAttrs), new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), @@ -1418,14 +1418,14 @@ Formals<.bool incoming, bool allowGhostKeyword, bool allowNewKeyword, bool allow { Attribute } GIdentType ParameterDefaultValue - (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) + (. formals.Add(new Formal(name.Tok, name, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) { Origin = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) { "," { Attribute } GIdentType ParameterDefaultValue - (. formals.Add(new Formal(name.Tok, name.Value, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) + (. formals.Add(new Formal(name.Tok, name, ty, incoming, isGhost, defaultValue, attrs, isOld, isNameOnly, isOlder) { Origin = defaultValue != null ? new RangeToken(range.StartToken, defaultValue.EndToken) : range } ); .) } @@ -1456,12 +1456,12 @@ FormalsOptionalIds<.List/*!*/ formals.> "(" [ TypeIdentOptional - (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) + (. formals.Add(new Formal(name.Tok, name, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) { Origin = range } ); .) { "," TypeIdentOptional - (. formals.Add(new Formal(name.Tok, name.Value, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) + (. formals.Add(new Formal(name.Tok, name, ty, true, isGhost, defaultValue, attributes, false, isNameOnly) { Origin = range } ); .) @@ -1481,7 +1481,7 @@ TypeAndToken Contract.Ensures(Contract.ValueAtReturn(out ty) != null); tok = Token.NoToken; ty = new BoolType(); /*keep compiler happy*/ - IOrigin startToken = null; + Token startToken = null; List gt; List tupleArgTypes = null; List argumentGhostTokens = null; @@ -1637,7 +1637,7 @@ TupleType<.out Type ty, out Token tok, out List tupleArgTypes, out List = - (. Expression e; IOrigin startToken = null; .) + (. Expression e; Token startToken = null; .) NameSegmentForTypeName (. tok = t; startToken = e.StartToken; .) { "." TypeNameOrCtorSuffix (. List typeArgs; .) @@ -1749,7 +1749,7 @@ FunctionDecl "(" GIdentType (. Contract.Assert(!resultIsGhost && !isOld && !isNameOnly && !isOlder); - result = new Formal(resultName.Tok, resultName.Value, ty, false, false, null, null, false) + result = new Formal(resultName.Tok, resultName, ty, false, false, null, null, false) { Origin = range2 }; .) ")" @@ -2054,7 +2054,7 @@ PredicateResult if (ty is not BoolType) { SemErr(ErrorId.p_predicate_return_type_must_be_bool, new RangeToken(ty.StartToken, t), $"{name} return type should be bool, got {ty}"); } - result = new Formal(nameId.Tok, nameId.Value, ty, false, false, null, attributes, false) + result = new Formal(nameId.Tok, nameId, ty, false, false, null, attributes, false) { Origin = range }; .) ")" @@ -2320,7 +2320,7 @@ AssignStatement BlockStmt proof = null; IOrigin x = Token.NoToken; Token endTok = Token.NoToken; - IOrigin startToken = Token.NoToken; + Token startToken = Token.NoToken; Attributes attrs = null; Attributes tokenAttrs = null; AttributedToken suchThatAssume = null; @@ -2416,7 +2416,7 @@ Rhs List display = null; r = dummyRhs; // to please compiler Attributes attrs = null; - IOrigin startToken = null; + Token startToken = null; .) ( IF(la.val == "new") "new" (. newToken = t; startToken = t; .) @@ -2544,11 +2544,11 @@ VarDeclStatement<.out Statement/*!*/ s.> var lhsExprs = new List(); if (isGhost || (rhss.Count == 0 && exceptionRhs == null && suchThat == null)) { // explicitly ghost or no init foreach (var lhs in lhss) { - lhsExprs.Add(new IdentifierExpr(lhs.Tok, lhs.Name) { Origin = new RangeToken(lhs.Tok, lhs.Tok) } ); + lhsExprs.Add(new IdentifierExpr(lhs.Tok, lhs.Name) { Origin = new RangeToken(lhs.StartToken, lhs.EndToken) } ); } } else { // not explicitly ghost, but with init - so auto-ghost foreach (var lhs in lhss) { - lhsExprs.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name) { Origin = new RangeToken(lhs.Tok, lhs.Tok) } ); + lhsExprs.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name) { Origin = new RangeToken(lhs.StartToken, lhs.EndToken) } ); } } var rangeToken = new RangeToken(startToken, t); @@ -2845,11 +2845,11 @@ Guard /* null represents demonic-choice */ BindingGuard = (. var bvars = new List(); BoundVar bv; - IOrigin x; + Token x; Attributes attrs = null; Expression body; .) - IdentTypeOptional (. bvars.Add(bv); x = bv.tok; .) + IdentTypeOptional (. bvars.Add(bv); x = bv.StartToken; .) { "," IdentTypeOptional (. bvars.Add(bv); .) } @@ -3202,7 +3202,7 @@ CalcStmt /* now for the hint, which we build up as a possibly empty sequence of statements placed into one BlockStmt */ (. var subhints = new List(); Token hintStart = la; - IOrigin hintEnd = hintStart.Prev; + Token hintEnd = hintStart.Prev; Token t0, t1; BlockStmt subBlock; Statement subCalc; .) @@ -3380,7 +3380,7 @@ ImpliesExpression = (. Contract.Ensures(Contract.ValueAtReturn(out e0) != null); Token/*!*/ x = null; Expression/*!*/ e1; Expression first; - IOrigin startToken = null; + Token startToken = null; Token/*!*/ firstOp = null; Token/*!*/ prefixOp = null; e0 = dummyExpr; /* mute the warning */ @@ -3422,7 +3422,7 @@ RelationalExpression ops = null; List opLocs = null; List prefixLimits = null; - IOrigin startToken = null; + Token startToken = null; Expression k; int kind = 0; // 0 ("uncommitted") indicates chain of ==, possibly with one != // 1 ("ascending") indicates chain of ==, <, <=, possibly with one != diff --git a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs index 4c9048b8666..5b84329569b 100644 --- a/Source/DafnyCore/Generic/ConsoleErrorReporter.cs +++ b/Source/DafnyCore/Generic/ConsoleErrorReporter.cs @@ -45,7 +45,7 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri if (Options.Get(Snippets.ShowSnippets) && tok.Uri != null) { var tw = new StringWriter(); - Snippets.WriteSourceCodeSnippet(Options, tok.ToRange(), tw); + Snippets.WriteSourceCodeSnippet(Options, tok, tw); errorLine += tw.ToString(); } @@ -68,7 +68,7 @@ protected override bool MessageCore(MessageSource source, ErrorLevel level, stri errorLine += $"{innerToken.TokenToString(Options)}: {innerMessage}\n"; if (Options.Get(Snippets.ShowSnippets) && tok.Uri != null) { var tw = new StringWriter(); - Snippets.WriteSourceCodeSnippet(Options, innerToken.ToRange(), tw); + Snippets.WriteSourceCodeSnippet(Options, innerToken, tw); errorLine += tw.ToString(); } } diff --git a/Source/DafnyCore/Generic/EmptyNode.cs b/Source/DafnyCore/Generic/EmptyNode.cs index 2e690b0a5c7..fcc9e27e06a 100644 --- a/Source/DafnyCore/Generic/EmptyNode.cs +++ b/Source/DafnyCore/Generic/EmptyNode.cs @@ -4,7 +4,7 @@ namespace Microsoft.Dafny; public class EmptyNode : Node { - public override RangeToken Origin { get; set; } = new(new Token(), new Token()); + public override IOrigin Origin { get; set; } = new Token(); public override IOrigin Tok => new Token(); public override IEnumerable Children => Enumerable.Empty(); public override IEnumerable PreResolveChildren => Enumerable.Empty(); diff --git a/Source/DafnyCore/Generic/ErrorRegistry.cs b/Source/DafnyCore/Generic/ErrorRegistry.cs index 3b09fccfdd2..ebf2d15341a 100644 --- a/Source/DafnyCore/Generic/ErrorRegistry.cs +++ b/Source/DafnyCore/Generic/ErrorRegistry.cs @@ -29,7 +29,7 @@ public bool Contains(DafnyPosition position) { /// The range to replace. The start is given by the token's start, and the length is given by the val's length. /// public record DafnyCodeActionEdit(DafnyRange Range, string Replacement = "") { - public DafnyCodeActionEdit(RangeToken rangeOrigin, string replacement = "", bool includeTrailingWhitespace = false) + public DafnyCodeActionEdit(IOrigin rangeOrigin, string replacement = "", bool includeTrailingWhitespace = false) : this(rangeOrigin.ToDafnyRange(includeTrailingWhitespace), replacement) { } } @@ -70,7 +70,7 @@ public static DafnyCodeActionEdit[] OneEdit(RangeToken range, string newContent, return new[] { new DafnyCodeActionEdit(range, newContent, includeTrailingWhitespace) }; } - public static DafnyAction OneAction(string title, RangeToken range, string newContent, bool includeTrailingWhitespace = false) { + public static DafnyAction OneAction(string title, IOrigin range, string newContent, bool includeTrailingWhitespace = false) { return new(title, new[] { new DafnyCodeActionEdit(range, newContent, includeTrailingWhitespace) }); } @@ -86,7 +86,7 @@ public static RangeToken IncludeComma(RangeToken range) { public static RangeToken ExpandStart(RangeToken range, TokenPredicate pred, bool include) { var t = range.StartToken; - IOrigin p = null; + Token p = null; while (!pred(t)) { p = t; t = t.Prev; @@ -99,7 +99,7 @@ public static RangeToken ExpandStart(RangeToken range, TokenPredicate pred, bool public static RangeToken ExpandEnd(RangeToken range, TokenPredicate pred, bool include) { var t = range.EndToken; - IOrigin p = null; + Token p = null; while (!pred(t)) { p = t; t = t.Prev; diff --git a/Source/DafnyCore/Generic/Name.cs b/Source/DafnyCore/Generic/Name.cs index 24da06cc512..55e17377f99 100644 --- a/Source/DafnyCore/Generic/Name.cs +++ b/Source/DafnyCore/Generic/Name.cs @@ -28,11 +28,11 @@ public Name(Cloner cloner, Name original) : base(cloner, original) { Value = original.Value; } - public Name(RangeToken range, string value) : base(range) { + public Name(IOrigin range, string value) : base(range) { this.Value = value; } - public Name(IOrigin token) : this(new RangeToken(token, token), token.val) { + public Name(IOrigin token) : this(token, token.val) { } public Name(string value) : base(RangeToken.NoToken) { diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs index b7c07e25ba0..a98e55b3bc2 100644 --- a/Source/DafnyCore/Generic/Node.cs +++ b/Source/DafnyCore/Generic/Node.cs @@ -10,10 +10,10 @@ namespace Microsoft.Dafny; public interface INode { bool SingleFileToken { get; } - public IOrigin StartToken => Origin.StartToken; - public IOrigin EndToken => Origin.EndToken; + public Token StartToken => Origin.StartToken; + public Token EndToken => Origin.EndToken; IEnumerable OwnedTokens { get; } - RangeToken Origin { get; } + IOrigin Origin { get; } IOrigin Tok { get; } IEnumerable Children { get; } IEnumerable PreResolveChildren { get; } @@ -34,9 +34,9 @@ public abstract class Node : INode { protected IReadOnlyList OwnedTokensCache; public virtual bool SingleFileToken => true; - public IOrigin StartToken => Origin?.StartToken; + public Token StartToken => Origin?.StartToken; - public IOrigin EndToken => Origin?.EndToken; + public Token EndToken => Origin?.EndToken; public abstract IOrigin Tok { get; } /// @@ -54,7 +54,7 @@ public abstract class Node : INode { /// public abstract IEnumerable PreResolveChildren { get; } - public IEnumerable CoveredTokens { + public IEnumerable CoveredTokens { get { var token = StartToken; if (token == Token.NoToken) { @@ -128,7 +128,7 @@ private static IEnumerable GetConcreteChildren(INode node) { } } - public abstract RangeToken Origin { get; set; } + public abstract IOrigin Origin { get; set; } // // Returns all assumptions contained in this node or its descendants. diff --git a/Source/DafnyCore/Generic/NodeExtensions.cs b/Source/DafnyCore/Generic/NodeExtensions.cs index 9fee476b3b9..021df5669a7 100644 --- a/Source/DafnyCore/Generic/NodeExtensions.cs +++ b/Source/DafnyCore/Generic/NodeExtensions.cs @@ -151,7 +151,13 @@ public static LList FindNodeChain(this INode node, DafnyPosition position private static LList FindNodeChain(this INode node, DafnyPosition position, LList parent, Func predicate) { - if (node.Tok is AutoGeneratedOrigin || (node.Tok != Token.NoToken && !node.Origin.ToDafnyRange().Contains(position))) { + if (node.Tok is AutoGeneratedOrigin) { + return null; + } + + // Example of a fillerNode is the default class, although we could give it the same origin as the module it is in. + var fillerNode = !ReferenceEquals(node.Origin, Token.NoToken); + if (fillerNode && !node.Origin.ToDafnyRange().Contains(position)) { return null; } @@ -163,7 +169,7 @@ private static LList FindNodeChain(this INode node, DafnyPosition positio } } - if (node.Tok == Token.NoToken || !predicate(node)) { + if (ReferenceEquals(node.Tok, Token.NoToken) || !predicate(node)) { return null; } diff --git a/Source/DafnyCore/Generic/RangeNode.cs b/Source/DafnyCore/Generic/RangeNode.cs index 75df8390223..9c121b4f645 100644 --- a/Source/DafnyCore/Generic/RangeNode.cs +++ b/Source/DafnyCore/Generic/RangeNode.cs @@ -2,18 +2,18 @@ namespace Microsoft.Dafny; public abstract class RangeNode : Node { // TODO merge into Node when TokenNode is gone. - public override IOrigin Tok => StartToken; // TODO rename to ReportingToken in separate PR + public override IOrigin Tok => Origin; public IOrigin tok => Tok; // TODO replace with Tok in separate PR // TODO rename to Range in separate PR - public override RangeToken Origin { get; set; } // TODO remove setter when TokenNode is gone. + public override IOrigin Origin { get; set; } // TODO remove setter when TokenNode is gone. protected RangeNode(Cloner cloner, RangeNode original) { Origin = cloner.Origin(original.Origin); } - protected RangeNode(RangeToken rangeOrigin) { + protected RangeNode(IOrigin rangeOrigin) { Origin = rangeOrigin; } } \ No newline at end of file diff --git a/Source/DafnyCore/Generic/ReporterExtensions.cs b/Source/DafnyCore/Generic/ReporterExtensions.cs index 631c1038572..1b55f4d272d 100644 --- a/Source/DafnyCore/Generic/ReporterExtensions.cs +++ b/Source/DafnyCore/Generic/ReporterExtensions.cs @@ -55,12 +55,12 @@ private static string FormatRelated(string related) { public static IEnumerable CreateDiagnosticRelatedInformationFor(IOrigin token, string? message, bool usingSnippets) { var (tokenForMessage, inner, newMessage) = token is NestedOrigin nestedToken ? (nestedToken.Outer, nestedToken.Inner, nestedToken.Message) : (token, null, null); var dafnyToken = BoogieGenerator.ToDafnyToken(true, tokenForMessage); - if (!usingSnippets && dafnyToken is RangeToken rangeToken) { + if (!usingSnippets && dafnyToken.IncludesRange) { if (message == PostConditionFailingMessage) { - var postcondition = rangeToken.PrintOriginal(); + var postcondition = dafnyToken.PrintOriginal(); message = $"this postcondition might not hold: {postcondition}"; } else if (message == null || message == RelatedLocationMessage) { - message = FormatRelated(rangeToken.PrintOriginal()); + message = FormatRelated(dafnyToken.PrintOriginal()); } } diff --git a/Source/DafnyCore/Generic/TokenNode.cs b/Source/DafnyCore/Generic/TokenNode.cs index 41db4088585..605cf0b07a7 100644 --- a/Source/DafnyCore/Generic/TokenNode.cs +++ b/Source/DafnyCore/Generic/TokenNode.cs @@ -7,9 +7,9 @@ public abstract class TokenNode : Node { // Contains tokens that did not make it in the AST but are part of the expression, // Enables ranges to be correct. // TODO: Re-add format tokens where needed until we put all the formatting to replace the tok of every expression - internal IOrigin[] FormatTokens = null; + internal Token[] FormatTokens = null; - protected RangeToken RangeOrigin = null; + protected IOrigin RangeOrigin = null; public IOrigin tok = Token.NoToken; @@ -18,14 +18,14 @@ public override IOrigin Tok { get => tok; } - public override RangeToken Origin { + public override IOrigin Origin { get { if (RangeOrigin == null) { - var startTok = tok; - var endTok = tok; + var startTok = tok.StartToken; + var endTok = tok.EndToken; - void UpdateStartEndToken(IOrigin token1) { + void UpdateStartEndToken(Token token1) { if (token1.Filepath != tok.Filepath) { return; } diff --git a/Source/DafnyCore/JsonDiagnostics.cs b/Source/DafnyCore/JsonDiagnostics.cs index 3eb4562d862..37c25d806e1 100644 --- a/Source/DafnyCore/JsonDiagnostics.cs +++ b/Source/DafnyCore/JsonDiagnostics.cs @@ -24,10 +24,9 @@ private static JsonObject SerializeRange(Boogie.IToken tok) { var range = new JsonObject { ["start"] = SerializePosition(tok), }; - if (tok is RangeToken rangeToken1) { - range["end"] = SerializePosition(rangeToken1.EndToken); - } else if (tok is BoogieRangeOrigin rangeToken2) { - range["end"] = SerializePosition(rangeToken2.EndToken); + var origin = BoogieGenerator.ToDafnyToken(true, tok); + if (origin.IncludesRange) { + range["end"] = SerializePosition(origin.EndToken); } return range; } diff --git a/Source/DafnyCore/Pipeline/BoogieExtensions.cs b/Source/DafnyCore/Pipeline/BoogieExtensions.cs index 3477a1dce0a..2a49e554999 100644 --- a/Source/DafnyCore/Pipeline/BoogieExtensions.cs +++ b/Source/DafnyCore/Pipeline/BoogieExtensions.cs @@ -30,7 +30,7 @@ public static Range ToLspRange(this DafnyRange range) { /// The token to get the range of. /// An optional other token to get the end of the range of. /// The LSP range of the token. - public static Range ToLspRange(this RangeToken range) { + public static Range ToLspRange(this IOrigin range) { return range.ToDafnyRange().ToLspRange(); } @@ -62,10 +62,7 @@ public static Range GetLspRange(this Boogie.IToken token, bool nameRange = false return GetLspRange(nestedToken.Outer, nameRange); } var dafnyToken = BoogieGenerator.ToDafnyToken(!nameRange, token); - if (dafnyToken is RangeToken rangeToken) { - return GetLspRangeGeneric(rangeToken.StartToken, rangeToken.EndToken); - } - return GetLspRangeGeneric(token, token); + return GetLspRangeGeneric(dafnyToken.StartToken, dafnyToken.EndToken); } public static Position GetLspPosition(this DafnyPosition position) { diff --git a/Source/DafnyCore/Pipeline/Compilation.cs b/Source/DafnyCore/Pipeline/Compilation.cs index 863fbd7adab..cc60ec7dd53 100644 --- a/Source/DafnyCore/Pipeline/Compilation.cs +++ b/Source/DafnyCore/Pipeline/Compilation.cs @@ -366,9 +366,11 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT await ticket; if (!onlyPrepareVerificationForGutterTests) { - var groups = tasks.GroupBy(t => - // We unwrap so that we group on tokens as they are displayed to the user by Reporter.Info - OriginWrapper.Unwrap(BoogieGenerator.ToDafnyToken(true, t.Token))). + var groups = tasks.GroupBy(t => { + var dafnyToken = BoogieGenerator.ToDafnyToken(true, t.Token); + // We normalize so that we group on tokens as they are displayed to the user by Reporter.Info + return new RangeToken(dafnyToken.StartToken, dafnyToken.EndToken); + }). OrderBy(g => g.Key); foreach (var tokenTasks in groups) { var functions = tokenTasks.SelectMany(t => t.Split.HiddenFunctions.Select(f => f.tok). diff --git a/Source/DafnyCore/ProofDependencyWarnings.cs b/Source/DafnyCore/ProofDependencyWarnings.cs index b26e2a4d105..acd9234fe16 100644 --- a/Source/DafnyCore/ProofDependencyWarnings.cs +++ b/Source/DafnyCore/ProofDependencyWarnings.cs @@ -165,7 +165,7 @@ private static void SuggestByProofRefactoring(string scopeName, continue; } - RangeToken range = null; + IOrigin range = null; var factProvider = ""; var factConsumer = ""; var recommendation = ""; diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs index 439d4f475c4..0b2e4de385e 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs +++ b/Source/DafnyCore/Resolver/BoundsDiscovery/BoundsDiscovery.cs @@ -151,7 +151,7 @@ public static Expression FrameArrowToObjectSet(Expression e) { var objUse = new IdentifierExpr(e.tok, objVar.Name) { Type = objVar.Type, Var = objVar }; boundVarDecls.Add(objVar); - var collection = new ApplyExpr(e.tok, e, boundVarUses, e.tok) { + var collection = new ApplyExpr(e.tok, e, boundVarUses, Token.NoToken) { Type = collectionType }; var resolvedOpcode = collectionType.ResolvedOpcodeForIn; diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 9be547760f5..48d8d0947d4 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -783,7 +783,7 @@ public void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) { var fn = new ApplySuffix(tok, null, new ExprDotName(tok, receiver, f.Name, f.TypeArgs.ConvertAll(typeParameter => (Type)new UserDefinedType(f.tok, typeParameter))), new ActualBindings(f.Ins.ConvertAll(Expression.CreateIdentExpr)).ArgumentBindings, - tok); + Token.NoToken); var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn)); Specification reads; if (Options.Get(Method.ReadsClausesOnMethods)) { @@ -3150,7 +3150,7 @@ internal Type ResolvedArrayType(IOrigin tok, int dims, Type arg, ResolutionConte } public Expression VarDotMethod(IOrigin tok, string varname, string methodname) { - return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varname), methodname, null), new List(), tok); + return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varname), methodname, null), new List(), Token.NoToken); } public Expression makeTemp(String prefix, AssignOrReturnStmt s, ResolutionContext resolutionContext, Expression ex) { @@ -3329,7 +3329,7 @@ public static UserDefinedType GetReceiverType(IOrigin tok, MemberDecl member) { } internal Expression VarDotFunction(IOrigin tok, string varname, string functionname) { - return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varname), functionname, null), new List(), tok); + return new ApplySuffix(tok, null, new ExprDotName(tok, new IdentifierExpr(tok, varname), functionname, null), new List(), Token.NoToken); } // TODO search for occurrences of "new LetExpr" which could benefit from this helper diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index c4e3259de51..61a39299b1f 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -4272,7 +4272,7 @@ static void FillInTypeArguments(IOrigin tok, int n, List typeArgs, List() { s }); + var thn = new BlockStmt(tok, new List() { s }); thn.IsGhost = true; - s = new IfStmt(tok.ToRange(), false, e, thn, null); + s = new IfStmt(tok, false, e, thn, null); s.IsGhost = true; // finally, add s to the block block.AppendStmt(s); @@ -464,7 +464,7 @@ private static Expression CreateUnresolvedThisRepr(IOrigin tok) { public static Expression CreateUnresolvedValidCall(IOrigin tok) { return new ApplySuffix(tok, null, new ExprDotName(tok, new ImplicitThisExpr(tok), "Valid", null), - new List(), tok); + new List(), Token.NoToken); } /// diff --git a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs index d2f930b5a0b..3c6e34cf05d 100644 --- a/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs +++ b/Source/DafnyCore/Rewriters/AutoRevealFunctionDependencies.cs @@ -343,7 +343,7 @@ public static HideRevealStmt BuildRevealStmt(Function func, IOrigin tok, ModuleD List expressionList = new List { new ApplySuffix(tok, null, resolveExpr, - new List(), tok) + new List(), Token.NoToken) }; var revealStmt = new HideRevealStmt(func.Origin, expressionList, HideRevealCmd.Modes.Reveal); diff --git a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs index 7197ae11e6c..0f2cd3e7f8e 100644 --- a/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs +++ b/Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs @@ -82,7 +82,7 @@ protected void ProcessOpaqueClassMembers(TopLevelDeclWithMembers c) { // Nothing to do } else if (member is Function { Body: null }) { // Nothing to do - } else if (!RefinementOrigin.IsInherited(member.tok, c.EnclosingModuleDefinition)) { + } else if (!member.tok.IsInherited(c.EnclosingModuleDefinition)) { GenerateRevealLemma(member, newDecls); } } diff --git a/Source/DafnyCore/Rewriters/RefinementTransformer.cs b/Source/DafnyCore/Rewriters/RefinementTransformer.cs index ac163893472..1abdc45e8c4 100644 --- a/Source/DafnyCore/Rewriters/RefinementTransformer.cs +++ b/Source/DafnyCore/Rewriters/RefinementTransformer.cs @@ -44,27 +44,8 @@ public override IOrigin WithVal(string newVal) { public override bool IsCopy => true; - public static bool IsInherited(IOrigin tok, ModuleDefinition m) { - if (tok is AutoGeneratedOrigin agt) { - tok = agt.WrappedToken; - } - while (tok is NestedOrigin) { - var n = (NestedOrigin)tok; - // check Outer - var r = n.Outer as RefinementOrigin; - if (r == null || r.InheritingModule != m) { - return false; - } - - // continue to check Inner - tok = n.Inner; - if (tok is AutoGeneratedOrigin nestedAtg) { - tok = nestedAtg.WrappedToken; - } - } - - var rtok = tok as RefinementOrigin; - return rtok != null && rtok.InheritingModule == m; + public override bool IsInherited(ModuleDefinition m) { + return InheritingModule == m; } public override string Filepath => WrappedToken.Filepath + "[" + InheritingModule.Name + "]"; @@ -1077,7 +1058,7 @@ List MergeStmtList(List skeleton, List oldStmt, // that the condition is inherited. var e = refinementCloner.CloneExpr(oldAssume.Expr); var attrs = refinementCloner.MergeAttributes(oldAssume.Attributes, skel.Attributes); - body.Add(new AssertStmt(new RangeToken(new BoogieGenerator.ForceCheckOrigin(skel.Origin.StartToken), skel.Origin.EndToken), + body.Add(new AssertStmt(new BoogieGenerator.ForceCheckOrigin(skel.Origin), e, skel.Label, new Attributes("_prependAssertToken", new List(), attrs))); Reporter.Info(MessageSource.RefinementTransformer, c.ConditionEllipsis, "assume->assert: " + Printer.ExprToString(Reporter.Options, e)); i++; j++; @@ -1223,8 +1204,8 @@ List MergeStmtList(List skeleton, List oldStmt, body.Add(cNew); i++; j++; if (addedAssert != null) { - var tok = new BoogieGenerator.ForceCheckOrigin(addedAssert.Origin.StartToken); - body.Add(new AssertStmt(new RangeToken(tok, addedAssert.Origin.EndToken), addedAssert, null, null)); + var tok = new BoogieGenerator.ForceCheckOrigin(addedAssert.Origin); + body.Add(new AssertStmt(tok, addedAssert, null, null)); } } else { MergeAddStatement(cur, body); @@ -1568,13 +1549,13 @@ void CheckIsOkayUpdateStmt(ConcreteAssignStatement stmt, ModuleDefinition m) { if (l is IdentifierExpr) { var ident = (IdentifierExpr)l; Contract.Assert(ident.Var is LocalVariable || ident.Var is Formal); // LHS identifier expressions must be locals or out parameters (ie. formals) - if ((ident.Var is LocalVariable && RefinementOrigin.IsInherited(((LocalVariable)ident.Var).Tok, m)) || ident.Var is Formal) { + if ((ident.Var is LocalVariable && ((LocalVariable)ident.Var).Tok.IsInherited(m)) || ident.Var is Formal) { // for some reason, formals are not considered to be inherited. Error(ErrorId.ref_invalid_variable_assignment, l.tok, "refinement method cannot assign to variable defined in parent module ('{0}')", ident.Var.Name); } } else if (l is MemberSelectExpr) { var member = ((MemberSelectExpr)l).Member; - if (RefinementOrigin.IsInherited(member.tok, m)) { + if (member.tok.IsInherited(m)) { Error(ErrorId.ref_invalid_field_assignment, l.tok, "refinement method cannot assign to a field defined in parent module ('{0}')", member.Name); } } else { @@ -1642,6 +1623,10 @@ public T WithRefinementTokenWrapping(Func action, bool wrap = false) { } public override IOrigin Origin(IOrigin tok) { + if (tok == null) { + return null; + } + if (wrapWithRefinementToken) { return new RefinementOrigin(tok, moduleUnderConstruction); } diff --git a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs index 11322217052..5fbd4d89c40 100644 --- a/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs +++ b/Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs @@ -178,15 +178,15 @@ internal override void PostResolve(Program program) { } } - var callStmt = new CallStmt(tok.ToRange(), lhss, methodSelectExpr, new List()); + var callStmt = new CallStmt(tok, lhss, methodSelectExpr, new List()); tryBodyStatements.Add(callStmt); Statement passedStmt = Statement.CreatePrintStmt(tok, Expression.CreateStringLiteral(tok, "PASSED\n")); - var passedBlock = new BlockStmt(tok.ToRange(), Util.Singleton(passedStmt)); + var passedBlock = new BlockStmt(tok, Util.Singleton(passedStmt)); if (resultVarExpr?.Type is UserDefinedType udt && udt.ResolvedClass is TopLevelDeclWithMembers resultClass) { var failureGuardExpr = - new FunctionCallExpr(tok, "IsFailure", resultVarExpr, tok, tok, new List()); + new FunctionCallExpr(tok, "IsFailure", resultVarExpr, tok, Token.NoToken, new List()); var isFailureMember = resultClass.Members.First(m => m.Name == "IsFailure"); failureGuardExpr.Function = (Function)isFailureMember; failureGuardExpr.Type = Type.Bool; @@ -194,12 +194,12 @@ internal override void PostResolve(Program program) { failureGuardExpr.TypeApplication_AtEnclosingClass = new List(); var failedBlock = PrintTestFailureStatement(tok, successVarExpr, resultVarExpr); - tryBodyStatements.Add(new IfStmt(tok.ToRange(), false, failureGuardExpr, failedBlock, passedBlock)); + tryBodyStatements.Add(new IfStmt(tok, false, failureGuardExpr, failedBlock, passedBlock)); } else { // Result is not a failure type tryBodyStatements.Add(passedBlock); } - var tryBody = new BlockStmt(tok.ToRange(), tryBodyStatements); + var tryBody = new BlockStmt(tok, tryBodyStatements); // Wrap the code above with: // @@ -210,7 +210,7 @@ internal override void PostResolve(Program program) { // success := false; // } // - var haltMessageVar = new LocalVariable(tok.ToRange(), "haltMessage", seqCharType, false) { + var haltMessageVar = new LocalVariable(tok, "haltMessage", seqCharType, false) { type = seqCharType }; var haltMessageVarExpr = new IdentifierExpr(tok, haltMessageVar); @@ -229,7 +229,7 @@ internal override void PostResolve(Program program) { // // expect success, "Test failures occurred: see above.\n"; // - Statement expectSuccess = new ExpectStmt(tok.ToRange(), successVarExpr, + Statement expectSuccess = new ExpectStmt(tok, successVarExpr, Expression.CreateStringLiteral(tok, "Test failures occurred: see above.\n"), null); mainMethodStatements.Add(expectSuccess); @@ -237,7 +237,7 @@ internal override void PostResolve(Program program) { // than the Method we added in PreResolve). var hasMain = Compilers.SinglePassCodeGenerator.HasMain(program, out var mainMethod); Contract.Assert(hasMain); - mainMethod.Body = new BlockStmt(tok.ToRange(), mainMethodStatements); + mainMethod.Body = new BlockStmt(tok, mainMethodStatements); } private BlockStmt PrintTestFailureStatement(IOrigin tok, Expression successVarExpr, Expression failureValueExpr) { @@ -246,7 +246,7 @@ private BlockStmt PrintTestFailureStatement(IOrigin tok, Expression successVarEx failureValueExpr, Expression.CreateStringLiteral(tok, "\n")); var failSuiteStmt = - new SingleAssignStmt(tok.ToRange(), successVarExpr, new ExprRhs(Expression.CreateBoolLiteral(tok, false))); - return new BlockStmt(tok.ToRange(), Util.List(failedPrintStmt, failSuiteStmt)); + new SingleAssignStmt(tok, successVarExpr, new ExprRhs(Expression.CreateBoolLiteral(tok, false))); + return new BlockStmt(tok, Util.List(failedPrintStmt, failSuiteStmt)); } } \ No newline at end of file diff --git a/Source/DafnyCore/Snippets.cs b/Source/DafnyCore/Snippets.cs index c5b0b9665f6..9af17403c51 100644 --- a/Source/DafnyCore/Snippets.cs +++ b/Source/DafnyCore/Snippets.cs @@ -31,8 +31,8 @@ public static void WriteSourceCodeSnippet(DafnyOptions options, IOrigin tok, Tex var lineEndPos = lineStartPos + line.Length; var tokEndPos = tok.pos + tok.val.Length; - if (tok is RangeToken rangeToken) { - tokEndPos = rangeToken.EndToken.pos + rangeToken.EndToken.val.Length; + if (tok.IncludesRange) { + tokEndPos = tok.EndToken.pos + tok.EndToken.val.Length; } var underlineLength = Math.Max(1, Math.Min(tokEndPos - tok.pos, lineEndPos - tok.pos)); string underline = new string('^', underlineLength); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs index ff1359a62dc..356620f289e 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs @@ -62,7 +62,7 @@ void CheckCallTermination(IOrigin tok, List contextDecreases, List(); var oldExpressions = new List(); var newExpressions = new List(); - if (RefinementOrigin.IsInherited(tok, currentModule) && contextDecreases.All(e => !RefinementOrigin.IsInherited(e.tok, currentModule))) { + if (tok.IsInherited(currentModule) && contextDecreases.All(e => !e.tok.IsInherited(currentModule))) { // the call site is inherited but all the context decreases expressions are new tok = new ForceCheckOrigin(tok); } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs index d1ae8856c03..ca85aea63dc 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs @@ -294,7 +294,7 @@ Expression PrefixSubstitution(PrefixPredicate pp, Expression body) { Expression recursiveCallReceiver; List recursiveCallArgs; pp.RecursiveCallParameters(pp.tok, pp.TypeArgs, pp.Ins, null, substMap, out recursiveCallReceiver, out recursiveCallArgs); - var ppCall = new FunctionCallExpr(pp.tok, pp.Name, recursiveCallReceiver, pp.tok, pp.tok, recursiveCallArgs); + var ppCall = new FunctionCallExpr(pp.tok, pp.Name, recursiveCallReceiver, pp.tok, Token.NoToken, recursiveCallArgs); ppCall.Function = pp; ppCall.Type = Type.Bool; ppCall.TypeApplication_AtEnclosingClass = pp.EnclosingClass.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index e94c42ab6cf..17b1df880c9 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -49,7 +49,7 @@ public void Check(Function f) { bool splitHappened /*we actually don't care*/ = generator.TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, etran); var (errorMessage, successMessage) = generator.CustomErrorMessage(ensures.Attributes); foreach (var s in splits) { - if (s.IsChecked && !RefinementOrigin.IsInherited(s.Tok, generator.currentModule)) { + if (s.IsChecked && !s.Tok.IsInherited(generator.currentModule)) { generator.AddEnsures(ens, generator.EnsuresWithDependencies(s.Tok, false, ensures.E, s.E, errorMessage, successMessage, null)); } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index fc49e51c660..e78338feed2 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -94,11 +94,11 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { // don't include this precondition here, but record it for later use p.Label.E = etran.Old.TrExpr(p.E); } else { - foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { - if (kind == MethodTranslationKind.Call && RefinementOrigin.IsInherited(s.Tok, currentModule)) { + foreach (var split in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { + if (kind == MethodTranslationKind.Call && split.Tok.IsInherited(currentModule)) { // this precondition was inherited into this module, so just ignore it } else { - req.Add(Requires(s.Tok, s.IsOnlyFree, p.E, s.E, errorMessage, successMessage, comment)); + req.Add(Requires(split.Tok, split.IsOnlyFree, p.E, split.E, errorMessage, successMessage, comment)); comment = null; // the free here is not linked to the free on the original expression (this is free things generated in the splitting.) } @@ -107,11 +107,11 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } comment = "user-defined postconditions"; foreach (var p in iter.Ensures) { - foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { - if (kind == MethodTranslationKind.Implementation && RefinementOrigin.IsInherited(s.Tok, currentModule)) { + foreach (var split in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { + if (kind == MethodTranslationKind.Implementation && split.Tok.IsInherited(currentModule)) { // this postcondition was inherited into this module, so just ignore it } else { - ens.Add(Ensures(s.Tok, s.IsOnlyFree, p.E, s.E, null, null, comment)); + ens.Add(Ensures(split.Tok, split.IsOnlyFree, p.E, split.E, null, null, comment)); comment = null; } } @@ -188,7 +188,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { new List())); // assume the automatic yield-requires precondition (which is always well-formed): this.Valid() - var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, iter.tok, new List()); + var validCall = new FunctionCallExpr(iter.tok, "Valid", th, iter.tok, Token.NoToken, new List()); validCall.Function = iter.Member_Valid; // resolve here validCall.Type = Type.Bool; // resolve here validCall.TypeApplication_AtEnclosingClass = iter.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp)); // resolve here diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index fdf8f5f019e..d924d824074 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -762,7 +762,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables TypeApplicationJustMember = m.TypeArgs.ConvertAll(tp => (Type)new UserDefinedType(tp.tok, tp)), Type = new InferredTypeProxy() }; - var recursiveCall = new CallStmt(m.tok.ToRange(), new List(), methodSel, recursiveCallArgs) { + var recursiveCall = new CallStmt(m.tok, new List(), methodSel, recursiveCallArgs) { IsGhost = m.IsGhost }; @@ -990,7 +990,7 @@ private void AddFunctionOverrideCheckImpl(Function f) { } else { var pp = f.OverriddenFunction.Result; Contract.Assert(!pp.IsOld); - pOut = new Formal(pp.tok, pp.Name, f.ResultType, false, pp.IsGhost, null); + pOut = new Formal(pp.tok, pp.NameNode, f.ResultType, false, pp.IsGhost, null); } var varType = TrType(pOut.Type); var wh = GetWhereClause(pOut.tok, new Boogie.IdentifierExpr(pOut.tok, pOut.AssignUniqueName(f.IdGenerator), varType), pOut.Type, etran, NOALLOC); @@ -1659,7 +1659,7 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt // Return a way to know if an assertion should be converted to an assumption private void SetAssertionOnlyFilter(Node m) { - List rangesOnly = new List(); + List rangesOnly = new List(); m.Visit(node => { if (node is AssertStmt assertStmt && assertStmt.HasAssertOnlyAttribute(out var assertOnlyKind)) { @@ -1834,18 +1834,18 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); AddEnsures(ens, Ensures(p.E.tok, true, p.E, etran.CanCallAssumption(p.E), errorMessage, successMessage, comment)); comment = null; - foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, kind)) { - var post = s.E; - if (kind == MethodTranslationKind.Implementation && RefinementOrigin.IsInherited(s.Tok, currentModule)) { + foreach (var split in TrSplitExprForMethodSpec(new BodyTranslationContext(m.ContainsHide), p.E, etran, kind)) { + var post = split.E; + if (kind == MethodTranslationKind.Implementation && split.Tok.IsInherited(currentModule)) { // this postcondition was inherited into this module, so make it into the form "$_reverifyPost ==> s.E" - post = BplImp(new Boogie.IdentifierExpr(s.E.tok, "$_reverifyPost", Boogie.Type.Bool), post); + post = BplImp(new Boogie.IdentifierExpr(split.E.tok, "$_reverifyPost", Boogie.Type.Bool), post); } - if (s.IsOnlyFree && bodyKind) { + if (split.IsOnlyFree && bodyKind) { // don't include in split -- it would be ignored, anyhow - } else if (s.IsOnlyChecked && !bodyKind) { + } else if (split.IsOnlyChecked && !bodyKind) { // don't include in split } else { - AddEnsures(ens, EnsuresWithDependencies(s.Tok, s.IsOnlyFree || this.assertionOnlyFilter != null, p.E, post, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithDependencies(split.Tok, split.IsOnlyFree || this.assertionOnlyFilter != null, p.E, post, errorMessage, successMessage, null)); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs index b162f4c8bae..4511fee3708 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs @@ -482,7 +482,7 @@ private bool TrSplitFunctionCallExpr(BodyTranslationContext context, var functionHeight = module.CallGraph.GetSCCRepresentativePredecessorCount(f); if (functionHeight < heightLimit && f.Body != null && RevealedInScope(f)) { - if (RefinementOrigin.IsInherited(fexp.tok, currentModule) && + if (fexp.tok.IsInherited(currentModule) && f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition && (codeContext == null || !codeContext.MustReverify)) { // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index 27e63bae54a..f7f9e0b5056 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -3305,6 +3305,10 @@ public static IOrigin Unwrap(IOrigin tok) { public override IOrigin WithVal(string newVal) { return new ForceCheckOrigin(WrappedToken.WithVal(newVal)); } + + public override bool IsInherited(ModuleDefinition m) { + return false; + } } public Bpl.PredicateCmd Assert(IOrigin tok, Bpl.Expr condition, ProofObligationDescription description, @@ -3321,7 +3325,7 @@ private PredicateCmd Assert(IOrigin tok, Expr condition, ProofObligationDescript Bpl.PredicateCmd cmd; if (context.AssertMode == AssertMode.Assume || (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) - || (RefinementOrigin.IsInherited(refinesToken, currentModule) && codeContext is not { MustReverify: true })) { + || (refinesToken.IsInherited(currentModule) && codeContext is not { MustReverify: true })) { // produce an assume instead cmd = TrAssumeCmd(tok, condition, kv); proofDependencies?.AddProofDependencyId(cmd, tok, new AssumedProofObligationDependency(tok, description)); @@ -3345,7 +3349,7 @@ PredicateCmd AssertAndForget(BodyTranslationContext context, IOrigin tok, Bpl.Ex PredicateCmd cmd; if (context.AssertMode == AssertMode.Assume || (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || - (RefinementOrigin.IsInherited(refinesTok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { + (refinesTok.IsInherited(currentModule) && (codeContext == null || !codeContext.MustReverify))) { // produce a "skip" instead cmd = TrAssumeCmd(tok, Bpl.Expr.True, kv); } else { @@ -4055,7 +4059,7 @@ public BoogieWrapper(Bpl.Expr expr, Type dafnyType) : base(ToDafnyToken(false, expr.tok)) { Contract.Requires(expr != null); Contract.Requires(dafnyType != null); - Origin = ToDafnyToken(true, expr.tok).ToRange(); + Origin = ToDafnyToken(true, expr.tok); Expr = expr; Type = dafnyType; // resolve immediately } @@ -4564,7 +4568,7 @@ protected override void VisitOneExpr(Expression expr) { bool TrSplitNeedsTokenAdjustment(Expression expr) { Contract.Requires(expr != null); - return RefinementOrigin.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule); + return expr.tok.IsInherited(currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule); } /// diff --git a/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs b/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs index 81810a395e4..5c0bff48b6c 100644 --- a/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs +++ b/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs @@ -163,10 +163,8 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) { Action, List>, List, List, List, Bpl.Variable, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr, Bpl.Expr>> CoAxHelper = (typeOfK, K) => { - Func> renew = s => - Map(codecl.TypeArgs, tp => - new TypeParameter(tp.Origin, tp.NameNode.Append("#" + s), tp.PositionalIndex, tp.Parent)); - List typaramsL = renew("l"), typaramsR = renew("r"); + List Renew(string s) => Map(codecl.TypeArgs, tp => new TypeParameter(tp.Origin, tp.NameNode.Append("#" + s), tp.PositionalIndex, tp.Parent)); + List typaramsL = Renew("l"), typaramsR = Renew("r"); var lvars = MkTyParamBinders(typaramsL, out var lexprs); var rvars = MkTyParamBinders(typaramsR, out var rexprs); Func, List> Types = l => Map(l, tp => (Type)new UserDefinedType(tp)); diff --git a/Source/DafnyCore/Verifier/ProofDependency.cs b/Source/DafnyCore/Verifier/ProofDependency.cs index 967b5355da0..4d4f202f3c5 100644 --- a/Source/DafnyCore/Verifier/ProofDependency.cs +++ b/Source/DafnyCore/Verifier/ProofDependency.cs @@ -18,7 +18,7 @@ namespace DafnyCore.Verifier; public abstract class ProofDependency { public abstract string Description { get; } - public abstract RangeToken Range { get; } + public abstract IOrigin Range { get; } public string LocationString() { if (Range?.StartToken is null) { @@ -52,7 +52,7 @@ public string OriginalString() { // assertion batch can be proved without proving one of the assertions that is // a proof obligation within it, that assertion must have been proved vacuously. public class ProofObligationDependency : ProofDependency { - public override RangeToken Range { get; } + public override IOrigin Range { get; } public ProofObligationDescription ProofObligation { get; } @@ -60,13 +60,13 @@ public class ProofObligationDependency : ProofDependency { $"{ProofObligation.SuccessDescription}"; public ProofObligationDependency(Microsoft.Boogie.IToken tok, ProofObligationDescription proofObligation) { - Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? BoogieGenerator.ToDafnyToken(true, tok).ToRange(); + Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? BoogieGenerator.ToDafnyToken(true, tok); ProofObligation = proofObligation; } } public class AssumedProofObligationDependency : ProofDependency { - public override RangeToken Range { get; } + public override IOrigin Range { get; } public ProofObligationDescription ProofObligation { get; } @@ -74,7 +74,7 @@ public class AssumedProofObligationDependency : ProofDependency { $"assumption that {ProofObligation.SuccessDescription}"; public AssumedProofObligationDependency(IOrigin tok, ProofObligationDescription proofObligation) { - Range = tok as RangeToken ?? (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? new RangeToken(tok, tok); + Range = tok.IncludesRange ? tok : (proofObligation as AssertStatementDescription)?.AssertStatement.Origin ?? tok; ProofObligation = proofObligation; } } @@ -86,7 +86,7 @@ public class RequiresDependency : ProofDependency { private IOrigin tok; - public override RangeToken Range => + public override IOrigin Range => tok as RangeToken ?? requires.Origin; public override string Description => @@ -104,7 +104,7 @@ public class EnsuresDependency : ProofDependency { private readonly IOrigin tok; - public override RangeToken Range => + public override IOrigin Range => tok as RangeToken ?? ensures.Origin; public override string Description => @@ -122,7 +122,7 @@ public class CallRequiresDependency : ProofDependency { public readonly CallDependency call; private readonly RequiresDependency requires; - public override RangeToken Range => + public override IOrigin Range => call.Range; public override string Description => @@ -140,7 +140,7 @@ public class CallEnsuresDependency : ProofDependency { public readonly CallDependency call; private readonly EnsuresDependency ensures; - public override RangeToken Range => + public override IOrigin Range => call.Range; public override string Description => @@ -156,7 +156,7 @@ public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) { public class CallDependency : ProofDependency { public readonly CallStmt call; - public override RangeToken Range => + public override IOrigin Range => call.Origin; public override string Description => @@ -169,7 +169,7 @@ public CallDependency(CallStmt call) { // Represents the assumption of a predicate in an `assume` statement. public class AssumptionDependency : ProofDependency { - public override RangeToken Range => + public override IOrigin Range => Expr.Origin; public override string Description => @@ -192,7 +192,7 @@ public AssumptionDependency(bool warnWhenUnused, string comment, Expression expr public class InvariantDependency : ProofDependency { private readonly Expression invariant; - public override RangeToken Range => + public override IOrigin Range => invariant.Origin; public override string Description => @@ -206,19 +206,19 @@ public InvariantDependency(Expression invariant) { // Represents an assignment statement. This includes the assignment to an // out parameter implicit in a return statement. public class AssignmentDependency : ProofDependency { - public override RangeToken Range { get; } + public override IOrigin Range { get; } public override string Description => "assignment (or return)"; - public AssignmentDependency(RangeToken rangeOrigin) { + public AssignmentDependency(IOrigin rangeOrigin) { this.Range = rangeOrigin; } } // Represents dependency of a proof on the definition of a specific function. public class FunctionDefinitionDependency : ProofDependency { - public override RangeToken Range => function.Origin; + public override IOrigin Range => function.Origin; public override string Description => $"function definition for {function.Name}"; diff --git a/Source/DafnyCore/Verifier/ProofObligationDescription.cs b/Source/DafnyCore/Verifier/ProofObligationDescription.cs index bb6114a913a..2e262dd5208 100644 --- a/Source/DafnyCore/Verifier/ProofObligationDescription.cs +++ b/Source/DafnyCore/Verifier/ProofObligationDescription.cs @@ -1891,7 +1891,7 @@ public static Expression MakeCharBoundsCheckUnicode(Expression expr) { public static void MakeQuantifierVarsForDims(List dims, out List vars, out List varExprs, out Expression range) { var zero = new LiteralExpr(Token.NoToken, 0); - vars = dims.Select((_, i) => new BoundVar(Token.NoToken, "i" + i, Type.Int)).ToList(); + vars = dims.Select((_, i) => new BoundVar("i" + i, Type.Int)).ToList(); // can't assign to out-param immediately, since it's accessed in the lambda below var tempVarExprs = vars.Select(var => new IdentifierExpr(Token.NoToken, var) as Expression).ToList(); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs index f6f763880b3..620302c0b09 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs @@ -350,7 +350,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E proofDependencies?.AddProofDependencyId(call, tok, new CallDependency(cs)); if ( (assertionOnlyFilter != null && !assertionOnlyFilter(tok)) || - (module != currentModule && RefinementOrigin.IsInherited(tok, currentModule) && (codeContext == null || !codeContext.MustReverify))) { + (module != currentModule && tok.IsInherited(currentModule) && (codeContext == null || !codeContext.MustReverify))) { // The call statement is inherited, so the refined module already checked that the precondition holds. Note, // preconditions are not allowed to be strengthened, except if they use a predicate whose body has been strengthened. // But if the callee sits in a different module, then any predicate it uses will be treated as opaque (that is, diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs index fbc1b15b3e3..21881cfe559 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs @@ -374,7 +374,7 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, loopBodyBuilder, " at end of loop iteration", false, false); var description = new Terminates(loop.InferredDecreases, prevGhostLocals, null, initDecrsDafny, theDecreases, false); - loopBodyBuilder.Add(Assert(loop.Tok, decrCheck, description, builder.Context)); + loopBodyBuilder.Add(Assert(loop.NavigationToken, decrCheck, description, builder.Context)); } } } else if (isBodyLessLoop) { diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index f0615b58049..1ef206ad9de 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs @@ -121,7 +121,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, foreach (var p in iter.YieldEnsures) { var ss = TrSplitExpr(builder.Context, p.E, yeEtran, true, out var splitHappened); foreach (var split in ss) { - if (RefinementOrigin.IsInherited(split.Tok, currentModule)) { + if (split.Tok.IsInherited(currentModule)) { // this postcondition was inherited into this module, so just ignore it } else if (split.IsChecked) { var yieldToken = new NestedOrigin(s.Tok, split.Tok); @@ -796,7 +796,7 @@ public void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListB } public void TrStmtList(List stmts, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran, - RangeToken scopeRange = null, bool processLabels = true) { + IOrigin scopeRange = null, bool processLabels = true) { Contract.Requires(stmts != null); Contract.Requires(builder != null); Contract.Requires(locals != null); diff --git a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs index 4119cf4dff3..c91063b2fac 100644 --- a/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/DiagnosticMigrationTest.cs @@ -101,7 +101,7 @@ public async Task ResolutionDiagnosticsAreKeptWhenNonEdgeCrossingChangesAreMade( Assert.Equal(verificationDiagnostics.Length, resolutionDiagnostics.Length); Assert.Equal(IdeState.OutdatedPrefix + verificationDiagnostics[0].Message, resolutionDiagnostics[0].Message); Assert.Equal(verificationDiagnostics[0].RelatedInformation, resolutionDiagnostics[0].RelatedInformation); - Assert.Equal(new Range(4, 7, 4, 13), resolutionDiagnostics[0].Range); + Assert.Equal(new Range(4, 7, 4, 14), resolutionDiagnostics[0].Range); } [Fact] diff --git a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs index f48d0707235..dc4ae7e7ad9 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyDocumentSymbolHandler.cs @@ -67,7 +67,7 @@ private IEnumerable FromSymbol(ISymbol symbol) { Detail = documentation, Range = range, Kind = symbol.Kind.Value, - SelectionRange = symbol.NavigationToken == Token.NoToken ? range : symbol.NavigationToken.ToRange().ToLspRange() + SelectionRange = symbol.NavigationToken == Token.NoToken ? range : symbol.NavigationToken.ToLspRange() } }; } diff --git a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs index 52a9900a318..a972647deec 100644 --- a/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/DafnyHoverHandler.cs @@ -73,7 +73,7 @@ protected override HoverRegistrationOptions CreateRegistrationOptions(HoverCapab } else { // If we hover over a usage, display the information of the declaration symbol = declarationOrUsage as ISymbol; - if (symbol != null && !symbol.NavigationToken.ToRange().ToLspRange().Contains(request.Position)) { + if (symbol != null && !symbol.NavigationToken.ToLspRange().Contains(request.Position)) { symbol = null; } } @@ -311,8 +311,8 @@ string MoreInformation(Boogie.IToken? token, bool hoveringPostcondition) { // It's not necessary to restate the postcondition itself if the user is already hovering it // however, nested postconditions should be displayed - if (dafnyToken is RangeToken rangeToken && !hoveringPostcondition) { - var originalText = rangeToken.PrintOriginal(); + if (dafnyToken.IncludesRange && !hoveringPostcondition) { + var originalText = dafnyToken.PrintOriginal(); deltaInformation += " \n" + (token == null ? couldProveOrNotPrefix : "Inside ") + "`" + originalText + "`"; } diff --git a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionHelpers.cs b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionHelpers.cs index d420a8f99c3..4d7b62f2a24 100644 --- a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionHelpers.cs +++ b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionHelpers.cs @@ -133,10 +133,10 @@ private static (RangeToken? beforeEndBrace, string indentationExtra, string inde /// The line of the opening brace /// The column of the opening brace /// The token of a matching closing brace, typically the `ÈndTok` of a BlockStmt - private static IOrigin? GetMatchingEndToken(Node program, Uri documentUri, int line, int col) { + private static Token? GetMatchingEndToken(Node program, Uri documentUri, int line, int col) { // Look in methods for BlockStmt with the IToken as opening brace // Return the EndTok of them. - IOrigin? tokenFound = null; + Token? tokenFound = null; program.Visit((INode n) => { if (tokenFound != null) { return false; @@ -167,7 +167,7 @@ private static (RangeToken? beforeEndBrace, string indentationExtra, string inde /// returns the closing brace token, else null. /// Visit substatements recursively /// - private static IOrigin? GetMatchingEndToken(int line, int col, Statement stmt) { + private static Token? GetMatchingEndToken(int line, int col, Statement stmt) { // Look in methods for BlockStmt with the IToken as opening brace // Return the EndTok of them. if (stmt is BlockStmt blockStmt && blockStmt.Tok.line == line && blockStmt.Tok.col == col) { diff --git a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs index 573bb05cfb1..e69edd7c466 100644 --- a/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs +++ b/Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs @@ -34,7 +34,7 @@ public abstract class DafnyCodeActionProvider { // When building DafnyCodeActionEdit (what DafnyCodeAction return), // use this to create ranges suitable for insertion - protected static RangeToken InsertBefore(IOrigin tok) { + protected static RangeToken InsertBefore(Token tok) { return new RangeToken(tok, null); } protected static RangeToken InsertAfter(IOrigin tok) { diff --git a/Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs b/Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs index ae53f82359c..84eb4ab5358 100644 --- a/Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs +++ b/Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs @@ -608,7 +608,7 @@ private AssertionVerificationTree WithImmediatelyRelatedChanges() { if (counterExample is ReturnCounterexample returnCounterexample) { tok = returnCounterexample.FailingReturn.tok; if (tok.filename == assertion.tok.filename) { - result.Add(returnCounterexample.FailingReturn.tok.GetLspRange()); + result.Add(BoogieGenerator.ToDafnyToken(true, returnCounterexample.FailingReturn.tok).StartToken.GetLspRange()); } } diff --git a/Source/DafnyTestGeneration/Inlining/RemoveShortCircuitRewriter.cs b/Source/DafnyTestGeneration/Inlining/RemoveShortCircuitRewriter.cs index 4b908867aa4..2fab23efc67 100644 --- a/Source/DafnyTestGeneration/Inlining/RemoveShortCircuitRewriter.cs +++ b/Source/DafnyTestGeneration/Inlining/RemoveShortCircuitRewriter.cs @@ -315,14 +315,14 @@ private Expression CreateIf(string tmpVarName, Type typ, Expression initialExpr, newStmtStack.Last().Add(updateStmt); } var thenStmt = new AssignStatement( - new RangeToken(thenToken, thenToken), + thenToken, new List { identifierExpr }, new List { new ExprRhs(thenExpr) }); var elseStmt = elseExpr != null - ? new AssignStatement(new RangeToken(elseToken, elseToken), new List { identifierExpr }, + ? new AssignStatement(elseToken, new List { identifierExpr }, new List { new ExprRhs(elseExpr) }) : null; - var ifStmt = new IfStmt(new RangeToken(original.StartToken, original.StartToken), false, testExpr, + var ifStmt = new IfStmt(original.StartToken, false, testExpr, new BlockStmt(thenStmt.Origin, new List { thenStmt }), elseStmt); newStmtStack.Last().Add(ifStmt); return identifierExpr; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect index 585ba6c28b2..7420ef1bf1d 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/bymethod.dfy.expect @@ -1,3 +1,3 @@ -Dafny program verifier finished with 8 verified, 0 errors +Dafny program verifier finished with 6 verified, 0 errors Everything ok \ No newline at end of file diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect index eba5fb51b86..1bec4593a8f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Refinement.dfy.expect @@ -18,7 +18,7 @@ Refinement.dfy(276,7): Warning: the ... refinement feature in statements is depr Refinement.dfy(233,4): Warning: this loop has no body (loop frame: i) Refinement.dfy(15,4): Error: a postcondition could not be proved on this return path Refinement.dfy(14,16): Related location: this is the postcondition that could not be proved -Refinement.dfy[B](15,4): Error: a postcondition could not be proved on this return path +Refinement.dfy(15,4): Error: a postcondition could not be proved on this return path Refinement.dfy(33,19): Related location: this is the postcondition that could not be proved Refinement.dfy(69,15): Error: assertion might not hold Refinement.dfy(80,16): Error: assertion might not hold diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect index 1f42fd81bad..53730d6858a 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_combined_limited.html.expect @@ -258,7 +258,7 @@ method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat) requires x < 10 // not required for the proof { // cause at least a little proof work to be necessary, for nat bounds - if (x > 5) { return x + 2; } else { return x + 1; } + if (x > 5) { return x + 2; } else { return x + 1; } } // Code obviously not constrained by ensures clause. @@ -317,8 +317,8 @@ method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int) requires x == 11 // implied by the previous two, but neither individually ensures r == 11 { - return x; -} + return x; +} // Contradiction between three different requires clauses, with at least one of // the three being partly in a separately-defined function (function and @@ -338,8 +338,8 @@ method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns requires y != 11 // contradicts the previous two ensures r == 11 // provable from first two preconditions, but shouldn't be covered { - return x; -} + return x; +} function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int) requires x > 1 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect index 17c0fdc81c1..3e334e1e315 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencies.dfy_verification.html.expect @@ -258,7 +258,7 @@ method {:testEntry} ObviouslyUnnecessaryRequiresMethod(x: nat) returns (r: nat) requires x < 10 // not required for the proof { // cause at least a little proof work to be necessary, for nat bounds - if (x > 5) { return x + 2; } else { return x + 1; } + if (x > 5) { return x + 2; } else { return x + 1; } } // Code obviously not constrained by ensures clause. @@ -317,8 +317,8 @@ method {:testEntry} MultiPartRedundantRequiresMethod(x: int) returns (r: int) requires x == 11 // implied by the previous two, but neither individually ensures r == 11 { - return x; -} + return x; +} // Contradiction between three different requires clauses, with at least one of // the three being partly in a separately-defined function (function and @@ -338,8 +338,8 @@ method {:testEntry} MultiPartContradictoryRequiresMethod(x: int, y: int) returns requires y != 11 // contradicts the previous two ensures r == 11 // provable from first two preconditions, but shouldn't be covered { - return x; -} + return x; +} function {:testEntry} ContradictoryEnsuresClauseFunc(x: int): (r: int) requires x > 1 diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy index a51792b658f..2c1506c9176 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy @@ -167,7 +167,7 @@ // CHECK: ProofDependencies.dfy\(417,13\)-\(417,17\): ensures clause // CHECK: ProofDependencies.dfy\(420,7\)-\(420,15\): assignment \(or return\) // CHECK: Unused by proof: -// CHECK: ProofDependencies.dfy\(428,7\)-\(428,7\): assumption that divisor is always non-zero. +// CHECK: ProofDependencies.dfy\(428,5\)-\(428,9\): assumption that divisor is always non-zero. // CHECK: ProofDependencies.dfy\(428,5\)-\(429,13\): calc statement result // // CHECK: Results for M.GetX \(well-formedness\)