Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Introduce IOrigin to make the Dafny AST easier to work with #5931

Open
wants to merge 16 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
4 changes: 2 additions & 2 deletions Source/DafnyCore.Test/ClonerTest.cs
Original file line number Diff line number Diff line change
Expand Up @@ -45,9 +45,9 @@ public void ClonerKeepsBodyStartTok() {
var cloner = new Cloner();
var dummyDecl2 = cloner.CloneMethod(dummyDecl);
Assert.Equal(2, dummyDecl2.BodyStartTok.line);
Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line);
Assert.Equal(2, dummyDecl2.Ins[0].Origin.StartToken.line);
Assert.True(dummyDecl2.Ins[0].IsTypeExplicit);
Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line);
Assert.Equal(2, dummyDecl2.Ins[1].Origin.StartToken.line);
Assert.False(dummyDecl2.Ins[1].IsTypeExplicit);
}
}
13 changes: 10 additions & 3 deletions Source/DafnyCore.Test/NodeTests.cs
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,20 @@ namespace DafnyCore.Test;
public class NodeTests {

class ConcreteNode : Node {
private IOrigin origin;

public ConcreteNode(RangeToken rangeToken, IEnumerable<INode>? children = null) {
RangeToken = rangeToken;
origin = rangeToken;
Children = children ?? Enumerable.Empty<INode>();
}

public override RangeToken RangeToken { get; set; }
public override IToken Tok => RangeToken.StartToken;
public override IOrigin Origin => origin;

public override IOrigin RangeToken {
set => origin = value;
}

public override IOrigin Tok => origin.StartToken;
public override IEnumerable<INode> Children { get; }
public override IEnumerable<INode> PreResolveChildren => Children;
}
Expand Down
16 changes: 8 additions & 8 deletions Source/DafnyCore/AST/Attributes.cs
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
var bindings = atAttribute.UserSuppliedPreResolveBindings;

if (name == null) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, "Attribute not recognized: " + atAttribute.ToString());
program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, "Attribute not recognized: " + atAttribute.ToString());
return null;
}

Expand All @@ -316,7 +316,7 @@ public static Attributes ExpandAtAttribute(Program program, UserSuppliedAtAttrib
}

if (!builtinSyntax.CanBeApplied(attributeHost)) {
program.Reporter.Error(MessageSource.Resolver, atAttribute.RangeToken, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
program.Reporter.Error(MessageSource.Resolver, atAttribute.Origin, UserSuppliedAtAttribute.AtName + atAttribute.UserSuppliedName + " attribute cannot be applied to " + attributeHost.WhatKind);
}

var resolver = new ModuleResolver(new ProgramResolver(program), program.Options) {
Expand Down Expand Up @@ -614,7 +614,7 @@ private static void ResolveLikeDatatypeConstructor(Program program, Formal[] for
// Verify that provided arguments are given literally
foreach (var binding in bindings.ArgumentBindings) {
if (binding.Actual is not LiteralExpr) {
program.Reporter.Error(MessageSource.Resolver, binding.Actual.RangeToken, $"Argument to attribute {attrName} must be a literal");
program.Reporter.Error(MessageSource.Resolver, binding.Actual.Origin, $"Argument to attribute {attrName} must be a literal");
}
}
}
Expand Down Expand Up @@ -681,10 +681,10 @@ public static IEnumerable<Attributes> AsEnumerable(this Attributes attr) {

// {:..} Attributes parsed are built using this class
public class UserSuppliedAttributes : Attributes {
public readonly IToken OpenBrace;
public readonly IToken CloseBrace;
public readonly IOrigin OpenBrace;
public readonly IOrigin CloseBrace;
public bool Recognized; // set to true to indicate an attribute that is processed by some part of Dafny; this allows it to be colored in the IDE
public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, List<Expression> args, Attributes prev)
public UserSuppliedAttributes(IOrigin tok, IOrigin openBrace, IOrigin closeBrace, List<Expression> args, Attributes prev)
: base(tok.val, args, prev) {
Contract.Requires(tok != null);
Contract.Requires(openBrace != null);
Expand All @@ -699,10 +699,10 @@ public UserSuppliedAttributes(IToken tok, IToken openBrace, IToken closeBrace, L
// @-Attributes parsed are built using this class
public class UserSuppliedAtAttribute : Attributes {
public static readonly string AtName = "@";
public readonly IToken AtSign;
public readonly IOrigin AtSign;
public bool Builtin; // set to true to indicate it was recognized as a builtin attribute
// Otherwise it's a user-defined one and Arg needs to be fully resolved
public UserSuppliedAtAttribute(IToken tok, Expression arg, Attributes prev)
public UserSuppliedAtAttribute(IOrigin tok, Expression arg, Attributes prev)
: base(AtName, new List<Expression>() { arg }, prev) {
Contract.Requires(tok != null);
this.tok = tok;
Expand Down
74 changes: 35 additions & 39 deletions Source/DafnyCore/AST/Cloner.cs
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne

if (d is AbstractTypeDecl) {
var dd = (AbstractTypeDecl)d;
return new AbstractTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent,
return new AbstractTypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent,
CloneTPChar(dd.Characteristics), dd.TypeArgs.ConvertAll(CloneTypeParam),
dd.ParentTraits.ConvertAll(CloneType),
dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
Expand All @@ -75,23 +75,23 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
!(d is NonNullTypeDecl)); // don't clone the non-null type declaration; close the class, which will create a new non-null type declaration
var dd = (SubsetTypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
return new SubsetTypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps,
return new SubsetTypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps,
newParent, CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness),
CloneAttributes(dd.Attributes));
} else if (d is TypeSynonymDecl) {
var dd = (TypeSynonymDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
return new TypeSynonymDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps,
return new TypeSynonymDecl(Range(dd.Origin), dd.NameNode.Clone(this), CloneTPChar(dd.Characteristics), tps,
newParent, CloneType(dd.Rhs), CloneAttributes(dd.Attributes));
} else if (d is NewtypeDecl) {
var dd = (NewtypeDecl)d;
if (dd.Var == null) {
return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
return new NewtypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
CloneType(dd.BaseType), dd.WitnessKind, CloneExpr(dd.Witness),
dd.ParentTraits.ConvertAll(CloneType),
dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
} else {
return new NewtypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
return new NewtypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), dd.TypeArgs.ConvertAll(CloneTypeParam), newParent,
CloneBoundVar(dd.Var, false), CloneExpr(dd.Constraint), dd.WitnessKind, CloneExpr(dd.Witness),
dd.ParentTraits.ConvertAll(CloneType),
dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
Expand All @@ -104,15 +104,15 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
var dt = new IndDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors,
var dt = new IndDatatypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent, tps, ctors,
dd.ParentTraits.ConvertAll(CloneType),
dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
return dt;
} else if (d is CoDatatypeDecl) {
var dd = (CoDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
var dt = new CoDatatypeDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, ctors,
var dt = new CoDatatypeDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent, tps, ctors,
dd.ParentTraits.ConvertAll(CloneType),
dd.Members.ConvertAll(d => CloneMember(d, false)), CloneAttributes(dd.Attributes), dd.IsRefining);
return dt;
Expand All @@ -129,7 +129,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
var ens = dd.Ensures.ConvertAll(CloneAttributedExpr);
var yens = dd.YieldEnsures.ConvertAll(CloneAttributedExpr);
var body = CloneBlockStmt(dd.Body);
var iter = new IteratorDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent,
var iter = new IteratorDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent,
tps, ins, outs, reads, mod, decr,
req, ens, yreq, yens,
body, CloneAttributes(dd.Attributes), dd.SignatureEllipsis);
Expand All @@ -138,7 +138,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
var dd = (TraitDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(member => CloneMember(member, false));
var cl = new TraitDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, mm,
var cl = new TraitDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent, tps, mm,
CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType));
return cl;
} else if (d is DefaultClassDecl) {
Expand All @@ -150,7 +150,7 @@ public virtual TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition ne
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(member => CloneMember(member, false));
return new ClassDecl(Range(dd.RangeToken), dd.NameNode.Clone(this), newParent, tps, mm,
return new ClassDecl(Range(dd.Origin), dd.NameNode.Clone(this), newParent, tps, mm,
CloneAttributes(dd.Attributes), dd.IsRefining, dd.ParentTraits.ConvertAll(CloneType));
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl moduleDecl) {
Expand Down Expand Up @@ -188,13 +188,13 @@ public TypeParameter.TypeParameterCharacteristics CloneTPChar(
}

public DatatypeCtor CloneCtor(DatatypeCtor ct) {
return new DatatypeCtor(Range(ct.RangeToken), ct.NameNode.Clone(this), ct.IsGhost,
return new DatatypeCtor(Range(ct.Origin), ct.NameNode.Clone(this), ct.IsGhost,
ct.Formals.ConvertAll(bv => CloneFormal(bv, false)), CloneAttributes(ct.Attributes));
}

public TypeParameter CloneTypeParam(TypeParameter tp) {
return (TypeParameter)typeParameterClones.GetOrCreate(tp,
() => new TypeParameter(Range(tp.RangeToken), tp.NameNode.Clone(this), tp.VarianceSyntax,
() => new TypeParameter(Range(tp.Origin), tp.NameNode.Clone(this), tp.VarianceSyntax,
CloneTPChar(tp.Characteristics), tp.TypeBounds.ConvertAll(CloneType)));
}

Expand Down Expand Up @@ -272,7 +272,7 @@ public virtual Formal CloneFormal(Formal formal, bool isReference) {
: new Formal(Tok(formal.tok), formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost,
CloneExpr(formal.DefaultValue), CloneAttributes(formal.Attributes),
formal.IsOld, formal.IsNameOnly, formal.IsOlder, formal.NameForCompilation) {
RangeToken = formal.RangeToken,
RangeToken = formal.Origin,
IsTypeExplicit = formal.IsTypeExplicit
});
}
Expand Down Expand Up @@ -337,7 +337,7 @@ public Attributes CloneAttributes(Attributes attrs) {
} else if (attrs is UserSuppliedAttributes usa) {
return new UserSuppliedAttributes(Tok(usa.tok), Tok(usa.OpenBrace), Tok(usa.CloseBrace),
attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
RangeToken = Tok(usa.RangeToken)
RangeToken = Tok(usa.Origin)
};
} else if (attrs is UserSuppliedAtAttribute usaa) {
var arg = CloneExpr(usaa.Arg);
Expand All @@ -346,12 +346,12 @@ public Attributes CloneAttributes(Attributes attrs) {
arg.PreType = usaa.Arg.PreType;
}
return new UserSuppliedAtAttribute(Tok(usaa.tok), arg, CloneAttributes(usaa.Prev)) {
RangeToken = Tok(usaa.RangeToken),
RangeToken = Tok(usaa.Origin),
Builtin = usaa.Builtin
};
} else {
return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneExpr), CloneAttributes(attrs.Prev)) {
RangeToken = Tok(attrs.RangeToken)
RangeToken = Tok(attrs.Origin)
};
}
}
Expand All @@ -365,7 +365,7 @@ public AttributedExpression CloneAttributedExpr(AttributedExpression expr) {
}

public virtual ActualBinding CloneActualBinding(ActualBinding binding) {
return new ActualBinding(binding.FormalParameterName == null ? null : Tok(binding.FormalParameterName),
return new ActualBinding(binding.FormalParameterName,
CloneExpr(binding.Actual));
}

Expand Down Expand Up @@ -418,15 +418,15 @@ public virtual BlockStmt CloneBlockStmt(BlockStmt stmt) {
if (stmt == null) {
return null;
} else {
return new BlockStmt(Tok(stmt.RangeToken), stmt.Body.ConvertAll(stmt1 => CloneStmt(stmt1, false)));
return new BlockStmt(Tok(stmt.Origin), stmt.Body.ConvertAll(stmt1 => CloneStmt(stmt1, false)));
}
}

public virtual DividedBlockStmt CloneDividedBlockStmt(DividedBlockStmt stmt) {
if (stmt == null) {
return null;
} else {
return new DividedBlockStmt(Tok(stmt.RangeToken), stmt.BodyInit.ConvertAll(stmt1 => CloneStmt(stmt1, false)),
return new DividedBlockStmt(Tok(stmt.Origin), stmt.BodyInit.ConvertAll(stmt1 => CloneStmt(stmt1, false)),
stmt.SeparatorTok == null ? null : Tok(stmt.SeparatorTok), stmt.BodyProper.ConvertAll(stmt1 => CloneStmt(stmt1, false)));
}
}
Expand Down Expand Up @@ -461,7 +461,7 @@ public virtual Statement CloneStmt(Statement stmt, bool isReference) {
public MatchCaseStmt CloneMatchCaseStmt(MatchCaseStmt c) {
Contract.Requires(c != null);
Contract.Assert(c.Arguments != null);
return new MatchCaseStmt(Tok(c.RangeToken), c.Ctor, c.FromBoundVar,
return new MatchCaseStmt(Tok(c.Origin), c.Ctor, c.FromBoundVar,
c.Arguments.ConvertAll(v => CloneBoundVar(v, false)),
c.Body.ConvertAll(stmt => CloneStmt(stmt, false)), CloneAttributes(c.Attributes));
}
Expand Down Expand Up @@ -518,13 +518,13 @@ public GuardedAlternative CloneGuardedAlternative(GuardedAlternative alt) {
public virtual Field CloneField(Field f) {
Contract.Requires(f != null);
return f switch {
ConstantField c => new ConstantField(Range(c.RangeToken), c.NameNode.Clone(this), CloneExpr(c.Rhs),
ConstantField c => new ConstantField(Range(c.Origin), c.NameNode.Clone(this), CloneExpr(c.Rhs),
c.HasStaticKeyword, c.IsGhost, c.IsOpaque, CloneType(c.Type), CloneAttributes(c.Attributes)),
// We don't expect a SpecialField to ever be cloned. However, it can happen for malformed programs, for example if
// an iterator in a refined module is replaced by a class in the refining module.
SpecialField s => new SpecialField(Range(s.RangeToken), s.Name, s.SpecialId, s.IdParam, s.IsGhost, s.IsMutable,
SpecialField s => new SpecialField(Range(s.Origin), s.Name, s.SpecialId, s.IdParam, s.IsGhost, s.IsMutable,
s.IsUserMutable, CloneType(s.Type), CloneAttributes(s.Attributes)),
_ => new Field(Range(f.RangeToken), f.NameNode.Clone(this), f.HasStaticKeyword, f.IsGhost, f.IsMutable,
_ => new Field(Range(f.Origin), f.NameNode.Clone(this), f.HasStaticKeyword, f.IsGhost, f.IsMutable,
f.IsUserMutable, CloneType(f.Type), CloneAttributes(f.Attributes))
};
}
Expand All @@ -544,32 +544,32 @@ public virtual Function CloneFunction(Function f, string newName = null) {
newName = f.Name;
}

var newNameNode = new Name(Range(f.NameNode.RangeToken), newName);
var newNameNode = new Name(Range(f.NameNode.Origin), newName);

if (f is Predicate) {
return new Predicate(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsGhost, f.IsOpaque, tps, formals,
return new Predicate(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsGhost, f.IsOpaque, tps, formals,
result,
req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited,
f.ByMethodTok == null ? null : Tok(f.ByMethodTok), byMethodBody,
CloneAttributes(f.Attributes), null);
} else if (f is LeastPredicate) {
return new LeastPredicate(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsOpaque,
return new LeastPredicate(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsOpaque,
((LeastPredicate)f).TypeOfK, tps, formals, result,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
} else if (f is GreatestPredicate greatestPredicate) {
return new GreatestPredicate(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsOpaque,
return new GreatestPredicate(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsOpaque,
((GreatestPredicate)f).TypeOfK, tps, formals, result,
req, reads, ens, body, CloneAttributes(f.Attributes), null);
} else if (f is TwoStatePredicate) {
return new TwoStatePredicate(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsOpaque, tps, formals,
return new TwoStatePredicate(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsOpaque, tps, formals,
result,
req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);
} else if (f is TwoStateFunction) {
return new TwoStateFunction(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsOpaque, tps, formals,
return new TwoStateFunction(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsOpaque, tps, formals,
result, CloneType(f.ResultType),
req, reads, ens, decreases, body, CloneAttributes(f.Attributes), null);
} else {
return new Function(Range(f.RangeToken), newNameNode, f.HasStaticKeyword, f.IsGhost, f.IsOpaque, tps, formals,
return new Function(Range(f.Origin), newNameNode, f.HasStaticKeyword, f.IsGhost, f.IsOpaque, tps, formals,
result, CloneType(f.ResultType),
req, reads, ens, decreases, body, f.ByMethodTok == null ? null : Tok(f.ByMethodTok), byMethodBody,
CloneAttributes(f.Attributes), null);
Expand All @@ -596,29 +596,25 @@ public virtual BlockStmt CloneMethodBody(Method m) {
}
}

public virtual RangeToken Range(RangeToken range) {
public virtual IOrigin Range(IOrigin range) {
if (range == null) {
return null;
}
return new RangeToken(Tok(range.StartToken), Tok(range.EndToken));
}

public virtual IToken Tok(IToken tok) {
Contract.Requires(tok != null);
return tok;
return Tok(range);
}

public RangeToken Tok(RangeToken tok) {
public virtual IOrigin Tok(IOrigin tok) {
Contract.Requires(tok != null);
return new RangeToken(Tok(tok.StartToken), Tok(tok.EndToken));
return tok;
}

public virtual AttributedToken AttributedTok(AttributedToken tok) {
if (tok == null) {
return null;
}

return new AttributedToken(Tok(tok.Token), CloneAttributes(tok.Attrs));
return tok with { Attrs = CloneAttributes(tok.Attrs) };
}
}

Expand Down
Loading
Loading