Resolve match before compile

Source/DafnyCore/AST/AstVisitor.cs

@@ -253,6 +253,11 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context)
  VisitUserProvidedType(v.Type, context);
  }
  }
+ } else if (expr is NestedMatchExpr nestedMatchExpr) {
+ foreach (IdPattern mc in nestedMatchExpr.Cases.SelectMany(c => c.Pat.DescendantsAndSelf).OfType<IdPattern>()
+ .Where(id => id.BoundVar != null)) {
+ VisitUserProvidedType(mc.BoundVar.Type, context);
+ }
  }
 
  // Visit substatements

Source/DafnyCore/AST/Cloner.cs

@@ -16,9 +16,14 @@ interface ICloneable<out T> {
 
  public class Cloner {
  public bool CloneResolvedFields { get; }
+ private readonly Dictionary<Statement, Statement> statementClones = new();
  private readonly Dictionary<IVariable, IVariable> clones = new();
  private readonly Dictionary<MemberDecl, MemberDecl> memberClones = new();
 
+ public void AddStatementClone(Statement original, Statement clone) {
+ statementClones.Add(original, clone);
+ }
+
  public Cloner(bool cloneResolvedFields = false) {
  this.CloneResolvedFields = cloneResolvedFields;
  }
@@ -409,7 +414,6 @@ private Expression CloneExprInner(Expression expr) {
  } else if (expr is TernaryExpr) {
  var e = (TernaryExpr)expr;
  return new TernaryExpr(Tok(e.tok), e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2));
-
  } else if (expr is WildcardExpr) {
  return new WildcardExpr(Tok(expr.tok));
  } else if (expr is StmtExpr) {
@@ -421,14 +425,6 @@ private Expression CloneExprInner(Expression expr) {
  } else if (expr is ParensExpression) {
  var e = (ParensExpression)expr;
  return CloneExpr(e.E); // skip the parentheses in the clone
- } else if (expr is NestedMatchExpr) {
- var e = (NestedMatchExpr)expr;
- return new NestedMatchExpr(Tok(e.tok), CloneExpr(e.Source), e.Cases.ConvertAll(CloneNestedMatchCaseExpr),
- e.UsesOptionalBraces);
- } else if (expr is MatchExpr) {
- var e = (MatchExpr)expr;
- return new MatchExpr(Tok(e.tok), CloneExpr(e.Source), e.Cases.ConvertAll(CloneMatchCaseExpr),
- e.UsesOptionalBraces);
  }
  if (expr is Resolver_IdentifierExpr resolverIdentifierExpr) {
  return new Resolver_IdentifierExpr(Tok(resolverIdentifierExpr.tok), resolverIdentifierExpr.Decl, resolverIdentifierExpr.TypeArgs);
@@ -461,25 +457,17 @@ public virtual NameSegment CloneNameSegment(Expression expr) {
 
  public virtual AssignmentRhs CloneRHS(AssignmentRhs rhs) {
  AssignmentRhs c;
+ if (rhs is ICloneable<AssignmentRhs> cloneable) {
+ return cloneable.Clone(this);
+ }
+
  if (rhs is ExprRhs) {
  var r = (ExprRhs)rhs;
  c = new ExprRhs(CloneExpr(r.Expr), CloneAttributes(rhs.Attributes));
  } else if (rhs is HavocRhs) {
  c = new HavocRhs(Tok(rhs.Tok));
  } else {
- var r = (TypeRhs)rhs;
- if (r.ArrayDimensions != null) {
- if (r.InitDisplay != null) {
- Contract.Assert(r.ArrayDimensions.Count == 1);
- c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), CloneExpr(r.ArrayDimensions[0]), r.InitDisplay.ConvertAll(CloneExpr));
- } else {
- c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr), CloneExpr(r.ElementInit));
- }
- } else if (r.Bindings == null) {
- c = new TypeRhs(Tok(r.Tok), CloneType(r.EType));
- } else {
- c = new TypeRhs(Tok(r.Tok), CloneType(r.Path), r.Bindings.ArgumentBindings.ConvertAll(CloneActualBinding));
- }
+ throw new cce.UnreachableException();
  }
  return c;
  }
@@ -506,6 +494,10 @@ public virtual Statement CloneStmt(Statement stmt) {
  return null;
  }
 
+ if (statementClones.TryGetValue(stmt, out var cachedResult)) {
+ return cachedResult;
+ }
+
  if (stmt is ICloneable<Statement> cloneable) {
  var r = cloneable.Clone(this);
  // add labels to the cloned statement
@@ -924,14 +916,6 @@ public override Expression CloneExpr(Expression expr) {
  return base.CloneExpr(expr);
  }
 
- public override Statement CloneStmt(Statement stmt) {
- var s = stmt as MatchStmt;
- if (s != null && s.OrigUnresolved != null) {
- return CloneStmt(s.OrigUnresolved);
- }
- return base.CloneStmt(stmt);
- }
-
  public ModuleSignature CloneModuleSignature(ModuleSignature org, ModuleSignature newSig) {
  var sig = new ModuleSignature();
  sig.ModuleDef = newSig.ModuleDef;

Source/DafnyCore/AST/DafnyAst.cs

@@ -46,10 +46,11 @@ public ISet<INode> Visit(Func<INode, bool> beforeChildren = null, Action<INode>
  afterChildren ??= node => { };
 
  var visited = new HashSet<INode>();
- var toVisit = new Stack<INode>();
- toVisit.Push(this);
+ var toVisit = new LinkedList<INode>();
+ toVisit.AddFirst(this);
  while (toVisit.Any()) {
- var current = toVisit.Pop();
+ var current = toVisit.First();
+ toVisit.RemoveFirst();
  if (!visited.Add(current)) {
  continue;
  }
@@ -58,11 +59,17 @@ public ISet<INode> Visit(Func<INode, bool> beforeChildren = null, Action<INode>
  continue;
  }
 
+ var nodeAfterChildren = toVisit.First;
  foreach (var child in current.Children) {
  if (child == null) {
  throw new InvalidOperationException($"Object of type {current.GetType()} has null child");
  }
- toVisit.Push(child);
+
+ if (nodeAfterChildren == null) {
+ toVisit.AddLast(child);
+ } else {
+ toVisit.AddBefore(nodeAfterChildren, child);
+ }
  }
 
  afterChildren(current);

Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs

@@ -421,7 +421,7 @@ protected ComprehensionExpr(Cloner cloner, ComprehensionExpr original) : base(cl
  Term = cloner.CloneExpr(original.Term);
 
  if (cloner.CloneResolvedFields) {
- Bounds = original.Bounds?.Select(b => b.Clone(cloner)).ToList();
+ Bounds = original.Bounds?.Select(b => b?.Clone(cloner)).ToList();
  }
  }
  public override IEnumerable<INode> Children => (Attributes != null ? new List<INode> { Attributes } : Enumerable.Empty<INode>()).Concat(SubExpressions);

Source/DafnyCore/AST/Expressions/DisjunctivePattern.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 
 namespace Microsoft.Dafny;
 
@@ -11,4 +12,21 @@ public DisjunctivePattern(IToken tok, List<ExtendedPattern> alternatives, bool i
  }
 
  public override IEnumerable<INode> Children => Alternatives;
+ public override void Resolve(Resolver resolver, ResolutionContext resolutionContext,
+ Type sourceType, bool isGhost, bool mutable,
+ bool inPattern, bool inDisjunctivePattern) {
+
+ if (inPattern) {
+ resolver.reporter.Error(MessageSource.Resolver, Tok, "Disjunctive patterns are not allowed inside other patterns");
+ }
+
+ foreach (var alternative in Alternatives) {
+ alternative.Resolve(resolver, resolutionContext, sourceType, isGhost, mutable, true, true);
+ }
+ }
+
+ public override IEnumerable<(BoundVar var, Expression usage)> ReplaceTypesWithBoundVariables(Resolver resolver,
+ ResolutionContext resolutionContext) {
+ return Enumerable.Empty<(BoundVar var, Expression usage)>();
+ }
 }

Source/DafnyCore/AST/Expressions/Expressions.cs

@@ -1500,6 +1500,8 @@ public FunctionCallExpr(Cloner cloner, FunctionCallExpr original) : base(cloner,
  TypeApplication_JustFunction = original.TypeApplication_JustFunction;
  IsByMethodCall = original.IsByMethodCall;
  Function = original.Function;
+ CoCall = original.CoCall;
+ CoCallHint = original.CoCallHint;
  }
  }
 
@@ -2455,6 +2457,8 @@ public class CasePattern<VT> : INode
  where VT : class, IVariable {
  public readonly string Id;
  // After successful resolution, exactly one of the following two fields is non-null.
+
+ [FilledInDuringResolution]
  public DatatypeCtor Ctor; // finalized by resolution (null if the pattern is a bound variable)
  public VT Var; // finalized by resolution (null if the pattern is a constructor) Invariant: Var != null ==> Arguments == null
  public List<CasePattern<VT>> Arguments;
@@ -2474,6 +2478,7 @@ public CasePattern(Cloner cloner, CasePattern<VT> original) {
 
  if (cloner.CloneResolvedFields) {
  Expr = cloner.CloneExpr(original.Expr);
+ Ctor = original.Ctor;
  }
 
  if (original.Arguments != null) {
@@ -2535,24 +2540,6 @@ public IEnumerable<VT> Vars {
  public override IEnumerable<INode> Children => Arguments ?? Enumerable.Empty<INode>();
 }
 
-/*
-ExtendedPattern is either:
-1 - A LitPattern of a LiteralExpr, representing a constant pattern
-2 - An IdPattern of a string and a list of ExtendedPattern, representing either
- a bound variable or a constructor applied to n arguments or a symbolic constant
-*/
-
-public abstract class NestedMatchCase : INode {
- public readonly ExtendedPattern Pat;
-
- public NestedMatchCase(IToken tok, ExtendedPattern pat) {
- Contract.Requires(tok != null);
- Contract.Requires(pat != null);
- this.Tok = tok;
- this.Pat = pat;
- }
-}
-
 public class BoxingCastExpr : Expression { // a BoxingCastExpr is used only as a temporary placeholding during translation
  public readonly Expression E;
  public readonly Type FromType;
@@ -2704,14 +2691,12 @@ public IEnumerable<IDeclarationOrUsage> GetResolvedDeclarations() {
 /// it gets "replaced" by the expression in "ResolvedExpression".
 /// </summary>
 public abstract class ConcreteSyntaxExpression : Expression {
-
- // [FilledInDuringResolution] public Expression ResolvedExpression; // after resolution, manipulation of "this" should proceed as with manipulating "this.ResolvedExpression"
-
  protected ConcreteSyntaxExpression(Cloner cloner, ConcreteSyntaxExpression original) : base(cloner, original) {
  if (cloner.CloneResolvedFields && original.ResolvedExpression != null) {
  ResolvedExpression = cloner.CloneExpr(original.ResolvedExpression);
  }
  }
+
  [FilledInDuringResolution]
  private Expression resolvedExpression;
 
@@ -2740,35 +2725,6 @@ public override IEnumerable<Expression> SubExpressions {
  public override IEnumerable<Type> ComponentTypes => ResolvedExpression.ComponentTypes;
 }
 
-/// <summary>
-/// This class represents a piece of concrete syntax in the parse tree. During resolution,
-/// it gets "replaced" by the statement in "ResolvedStatement".
-/// Adapted from ConcreteSyntaxStatement
-/// </summary>
-public abstract class ConcreteSyntaxStatement : Statement {
- [FilledInDuringResolution] public Statement ResolvedStatement; // after resolution, manipulation of "this" should proceed as with manipulating "this.ResolvedExpression"
-
- public override IEnumerable<INode> Children =>
- ResolvedStatement == null ? base.Children : new[] { ResolvedStatement };
-
- public ConcreteSyntaxStatement(Cloner cloner, ConcreteSyntaxStatement original) : base(cloner, original) {
- if (cloner.CloneResolvedFields) {
- ResolvedStatement = cloner.CloneStmt(original.ResolvedStatement);
- }
- }
-
- public ConcreteSyntaxStatement(IToken tok, IToken endtok)
- : base(tok, endtok) {
- }
- public ConcreteSyntaxStatement(IToken tok, IToken endtok, Attributes attrs)
- : base(tok, endtok, attrs) {
- }
- public override IEnumerable<Statement> SubStatements {
- get {
- yield return ResolvedStatement;
- }
- }
-}
 public class ParensExpression : ConcreteSyntaxExpression {
  public readonly Expression E;
  public ParensExpression(IToken tok, Expression e)