Merge, and refactored bit in Cloner into class ClonerButDropMethodBodies.

1 files changed, 9 insertions, 352 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d0e95248..2cc6010a 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1076,366 +1076,23 @@ namespace Microsoft.Dafny
       ResolveModuleDefinition(mod, sig);

       return sig;

     }

+

     TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List<ModuleDefinition> mods, string Name) {

       Contract.Requires(d != null);

       Contract.Requires(m != null);

 

-      if (d is OpaqueTypeDecl) {

-        var dd = (OpaqueTypeDecl)d;

-        return new OpaqueTypeDecl(dd.tok, dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), null);

-      } else if (d is TypeSynonymDecl) {

-        var dd = (TypeSynonymDecl)d;

-        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

-        return new TypeSynonymDecl(dd.tok, dd.Name, tps, m, CloneType(dd.Rhs), null);

-      } else if (d is TupleTypeDecl) {

-        var dd = (TupleTypeDecl)d;

-        return new TupleTypeDecl(dd.Dims, dd.Module);

-      } else if (d is IndDatatypeDecl) {

-        var dd = (IndDatatypeDecl)d;

-        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

-        var ctors = dd.Ctors.ConvertAll(CloneCtor);

-        var dt = new IndDatatypeDecl(dd.tok, dd.Name, m, tps, ctors, null);

-        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(dd.tok, dd.Name, m, tps, ctors, null);

-        return dt;

-      } else if (d is ClassDecl) {

-        var dd = (ClassDecl)d;

-        var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);

-        var mm = dd.Members.ConvertAll(CloneMember);

-        List<IToken> trait = null;

-        if (dd is DefaultClassDecl) {

-          return new DefaultClassDecl(m, mm);

-        } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null,trait);

-      } else if (d is ModuleDecl) {

-        if (d is LiteralModuleDecl) {

-          return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);

-        } else if (d is AliasModuleDecl) {

-          var a = (AliasModuleDecl)d;

-          var alias = new AliasModuleDecl(a.Path, a.tok, m, a.Opened);

-          alias.ModuleReference = a.ModuleReference;

-          alias.Signature = a.Signature;

-          return alias;

-        } else if (d is ModuleFacadeDecl) {

-          var abs = (ModuleFacadeDecl)d;

-          var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);

-          var a = new ModuleFacadeDecl(abs.Path, abs.tok, m, abs.CompilePath, abs.Opened);

-          a.Signature = sig;

-          a.OriginalSignature = abs.OriginalSignature;

-          return a;

-        } else {

-          Contract.Assert(false);  // unexpected declaration

-          return null;  // to please compiler

-        }

-      } else {

-        Contract.Assert(false);  // unexpected declaration

-        return null;  // to please compiler

-      }

-    }

-    MemberDecl CloneMember(MemberDecl member) {

-      if (member is Field) {

-        Contract.Assert(!(member is SpecialField));  // we don't expect a SpecialField to be cloned (or do we?)

-        var f = (Field)member;

-        return new Field(f.tok, f.Name, f.IsGhost, f.IsMutable, f.IsUserMutable, CloneType(f.Type), null);

-      } else if (member is Function) {

-        var f = (Function)member;

-        return CloneFunction(f.tok, f, f.IsGhost);

-      } else {

-        var m = (Method)member;

-        return CloneMethod(m);

-      }

-    }

-    TypeParameter CloneTypeParam(TypeParameter tp) {

-      return new TypeParameter(tp.tok, tp.Name);

-    }

-

-    DatatypeCtor CloneCtor(DatatypeCtor ct) {

-      return new DatatypeCtor(ct.tok, ct.Name, ct.Formals.ConvertAll(CloneFormal), null);

-    }

-    Formal CloneFormal(Formal formal) {

-      return new Formal(formal.tok, formal.Name, CloneType(formal.Type), formal.InParam, formal.IsGhost);

-    }

-    Type CloneType(Type t) {

-      if (t is BasicType) {

-        return t;

-      } else if (t is SetType) {

-        var tt = (SetType)t;

-        return new SetType(CloneType(tt.Arg));

-      } else if (t is SeqType) {

-        var tt = (SeqType)t;

-        return new SeqType(CloneType(tt.Arg));

-      } else if (t is MultiSetType) {

-        var tt = (MultiSetType)t;

-        return new MultiSetType(CloneType(tt.Arg));

-      } else if (t is MapType) {

-        var tt = (MapType)t;

-        return new MapType(CloneType(tt.Domain), CloneType(tt.Range));

-      } else if (t is ArrowType) {

-        var tt = (ArrowType)t;

-        return new ArrowType(tt.tok, tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

-      } else if (t is UserDefinedType) {

-        var tt = (UserDefinedType)t;

-        return new UserDefinedType(tt.tok, tt.Name, tt.TypeArgs.ConvertAll(CloneType), tt.Path.ConvertAll(x => x));

-      } else if (t is InferredTypeProxy) {

-        return new InferredTypeProxy();

-      } else if (t is ParamTypeProxy) {

-        var tt = (ParamTypeProxy)t;

-        return new ParamTypeProxy(CloneTypeParam(tt.orig));

-      } else {

-        Contract.Assert(false);  // unexpected type (e.g., no other type proxies are expected at this time)

-        return null;  // to please compiler

-      }

-    }

-    Function CloneFunction(IToken tok, Function f, bool isGhost) {

-

-      var tps = f.TypeArgs.ConvertAll(CloneTypeParam);

-      var formals = f.Formals.ConvertAll(CloneFormal);

-      var req = f.Req.ConvertAll(CloneExpr);

-      var reads = f.Reads.ConvertAll(CloneFrameExpr);

-      var decreases = CloneSpecExpr(f.Decreases);

-

-      var ens = f.Ens.ConvertAll(CloneExpr);

-

-      Expression body = CloneExpr(f.Body);

-

-      if (f is Predicate) {

-        return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,

-          req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, null);

-      } else if (f is CoPredicate) {

-        return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,

-          req, reads, ens, body, null, null);

-      } else {

-        return new Function(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),

-          req, reads, ens, decreases, body, null, null);

-      }

-    }

-    Method CloneMethod(Method m) {

-      Contract.Requires(m != null);

-

-      var tps = m.TypeArgs.ConvertAll(CloneTypeParam);

-      var ins = m.Ins.ConvertAll(CloneFormal);

-      var req = m.Req.ConvertAll(CloneMayBeFreeExpr);

-      var mod = CloneSpecFrameExpr(m.Mod);

-      var decreases = CloneSpecExpr(m.Decreases);

-

-      var ens = m.Ens.ConvertAll(CloneMayBeFreeExpr);

-

-      if (m is Constructor) {

-        return new Constructor(m.tok, m.Name, tps, ins,

-          req, mod, ens, decreases, null, null, null);

-      } else if (m is CoLemma) {

-        return new CoLemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, null, null, null);

-      } else if (m is Lemma) {

-        return new Lemma(m.tok, m.Name, m.IsStatic, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, null, null, null);

-      } else {

-        return new Method(m.tok, m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),

-          req, mod, ens, decreases, null, null, null);

-      }

-    }

-    Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {

-      var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);

-      return new Specification<Expression>(ee, null);

-    }

-    Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {

-      var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);

-      return new Specification<FrameExpression>(ee, null);

-    }

-    FrameExpression CloneFrameExpr(FrameExpression frame) {

-      return new FrameExpression(frame.tok, CloneExpr(frame.E), frame.FieldName);

-    }

-    MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {

-      return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);

-    }

-    BoundVar CloneBoundVar(BoundVar bv) {

-      return new BoundVar(bv.tok, bv.Name, CloneType(bv.Type));

-    }

-    // ToDo: Remove this and use cloner

-    Expression CloneExpr(Expression expr) {

-      if (expr == null) {

-        return null;

-      } else if (expr is LiteralExpr) {

-        var e = (LiteralExpr)expr;

-        if (e is StaticReceiverExpr) {

-          return new StaticReceiverExpr(e.tok, CloneType(e.Type));

-        } else if (e.Value == null) {

-          return new LiteralExpr(e.tok);

-        } else if (e.Value is bool) {

-          return new LiteralExpr(e.tok, (bool)e.Value);

-        } else if (e.Value is Basetypes.BigDec) {

-          return new LiteralExpr(e.tok, (Basetypes.BigDec)e.Value);

-        } else {

-          return new LiteralExpr(e.tok, (BigInteger)e.Value);

-        }

-

-      } else if (expr is ThisExpr) {

-        if (expr is ImplicitThisExpr) {

-          return new ImplicitThisExpr(expr.tok);

-        } else {

-          return new ThisExpr(expr.tok);

-        }

-

-      } else if (expr is IdentifierExpr) {

-        var e = (IdentifierExpr)expr;

-        return new IdentifierExpr(e.tok, e.Name);

-

-      } else if (expr is DatatypeValue) {

-        var e = (DatatypeValue)expr;

-        return new DatatypeValue(e.tok, e.DatatypeName, e.MemberName, e.Arguments.ConvertAll(CloneExpr));

-

-      } else if (expr is DisplayExpression) {

-        DisplayExpression e = (DisplayExpression)expr;

-        if (expr is SetDisplayExpr) {

-          return new SetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

-        } else if (expr is MultiSetDisplayExpr) {

-          return new MultiSetDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

-        } else {

-          Contract.Assert(expr is SeqDisplayExpr);

-          return new SeqDisplayExpr(e.tok, e.Elements.ConvertAll(CloneExpr));

-        }

-

-      } else if (expr is MapDisplayExpr) {

-        MapDisplayExpr e = (MapDisplayExpr)expr;

-        List<ExpressionPair> pp = new List<ExpressionPair>();

-        foreach (ExpressionPair p in e.Elements) {

-          pp.Add(new ExpressionPair(CloneExpr(p.A), CloneExpr(p.B)));

-        }

-        return new MapDisplayExpr(expr.tok, pp);

-      } else if (expr is ExprDotName) {

-        var e = (ExprDotName)expr;

-        return new ExprDotName(e.tok, CloneExpr(e.Obj), e.SuffixName);

-

-      } else if (expr is MemberSelectExpr) {

-        var e = (MemberSelectExpr)expr;

-        return new MemberSelectExpr(e.tok, CloneExpr(e.Obj), e.MemberName);

-

-      } else if (expr is SeqSelectExpr) {

-        var e = (SeqSelectExpr)expr;

-        return new SeqSelectExpr(e.tok, e.SelectOne, CloneExpr(e.Seq), CloneExpr(e.E0), CloneExpr(e.E1));

-

-      } else if (expr is MultiSelectExpr) {

-        var e = (MultiSelectExpr)expr;

-        return new MultiSelectExpr(e.tok, CloneExpr(e.Array), e.Indices.ConvertAll(CloneExpr));

-

-      } else if (expr is SeqUpdateExpr) {

-        var e = (SeqUpdateExpr)expr;

-        return new SeqUpdateExpr(e.tok, CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));

-

-      } else if (expr is FunctionCallExpr) {

-        var e = (FunctionCallExpr)expr;

-        return new FunctionCallExpr(e.tok, e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : (e.OpenParen), e.Args.ConvertAll(CloneExpr));

-

-      } else if (expr is OldExpr) {

-        var e = (OldExpr)expr;

-        return new OldExpr(e.tok, CloneExpr(e.E));

-

-      } else if (expr is MultiSetFormingExpr) {

-        var e = (MultiSetFormingExpr)expr;

-        return new MultiSetFormingExpr(e.tok, CloneExpr(e.E));

-

-      } else if (expr is UnaryOpExpr) {

-        var e = (UnaryOpExpr)expr;

-        return new UnaryOpExpr(e.tok, e.Op, CloneExpr(e.E));

-

-      } else if (expr is ConversionExpr) {

-        var e = (ConversionExpr)expr;

-        return new ConversionExpr(e.tok, CloneExpr(e.E), CloneType(e.ToType));

-

-      } else if (expr is BinaryExpr) {

-        var e = (BinaryExpr)expr;

-        return new BinaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1));

-

-      } else if (expr is TernaryExpr) {

-        var e = (TernaryExpr)expr;

-        return new TernaryExpr(e.tok, e.Op, CloneExpr(e.E0), CloneExpr(e.E1), CloneExpr(e.E2));

-

-      } else if (expr is ChainingExpression) {

-        var e = (ChainingExpression)expr;

-        return CloneExpr(e.E);  // just clone the desugaring, since it's already available

-

-      } else if (expr is LetExpr) {

-        var e = (LetExpr)expr;

-        return new LetExpr(e.tok, e.LHSs.ConvertAll(CloneCasePattern), e.RHSs.ConvertAll(CloneExpr), CloneExpr(e.Body), e.Exact);

-

-      } else if (expr is ComprehensionExpr) {

-        var e = (ComprehensionExpr)expr;

-        var tk = e.tok;

-        var bvs = e.BoundVars.ConvertAll(CloneBoundVar);

-        var range = CloneExpr(e.Range);

-        var term = CloneExpr(e.Term);

-        if (e is QuantifierExpr) {

-          var q = (QuantifierExpr)e;

-          var tvs = q.TypeArgs.ConvertAll(CloneTypeParam);

-          if (e is ForallExpr) {

-            return new ForallExpr(tk, tvs, bvs, range, term, null);

-          } else if (e is ExistsExpr) {

-            return new ExistsExpr(tk, tvs, bvs, range, term, null);

-          } else {

-            Contract.Assert(false); throw new cce.UnreachableException();  // unexpected quantifier expression

-          }

-        } else if (e is MapComprehension) {

-          return new MapComprehension(tk, bvs, range, term);

-        } else if (e is LambdaExpr) {

-          var l = (LambdaExpr)e;

-          return new LambdaExpr(tk, l.OneShot, bvs, range, l.Reads.ConvertAll(CloneFrameExpr), term);

-        } else {

-          Contract.Assert(e is SetComprehension);

-          return new SetComprehension(tk, bvs, range, term);

-        }

-

-      } else if (expr is WildcardExpr) {

-        return new WildcardExpr(expr.tok);

-

-      } else if (expr is StmtExpr) {

-        var e = (StmtExpr)expr;

-        return new StmtExpr(e.tok, (new Cloner()).CloneStmt(e.S), CloneExpr(e.E));

-

-      } else if (expr is ITEExpr) {

-        var e = (ITEExpr)expr;

-        return new ITEExpr(e.tok, CloneExpr(e.Test), CloneExpr(e.Thn), CloneExpr(e.Els));

-

-      } else if (expr is AutoGeneratedExpression) {

-        var e = (AutoGeneratedExpression)expr;

-        var a = CloneExpr(e.E);

-        return new AutoGeneratedExpression(e.tok, a);

-

-      } else if (expr is ParensExpression) {

-        var e = (ParensExpression)expr;

-        return CloneExpr(e.E);  // skip the parentheses in the clone

-

-      } else if (expr is IdentifierSequence) {

-        var e = (IdentifierSequence)expr;

-        var aa = e.Arguments == null ? null : e.Arguments.ConvertAll(CloneExpr);

-        return new IdentifierSequence(e.Tokens.ConvertAll(tk => (tk)), e.OpenParen == null ? null : (e.OpenParen), aa);

-

-      } else if (expr is MatchExpr) {

-        var e = (MatchExpr)expr;

-        return new MatchExpr(e.tok, CloneExpr(e.Source),

-          e.Cases.ConvertAll(c => new MatchCaseExpr(c.tok, c.Id, c.Arguments.ConvertAll(CloneBoundVar), CloneExpr(c.Body))), e.UsesOptionalBraces);

-

-      } else if (expr is NegationExpression) {

-        var e = (NegationExpression)expr;

-        return new NegationExpression(e.tok, CloneExpr(e.E));

-

+      if (d is ModuleFacadeDecl) {

+        var abs = (ModuleFacadeDecl)d;

+        var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);

+        var a = new ModuleFacadeDecl(abs.Path, abs.tok, m, abs.CompilePath, abs.Opened);

+        a.Signature = sig;

+        a.OriginalSignature = abs.OriginalSignature;

+        return a;

       } else {

-        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

+        return new ClonerButDropMethodBodies().CloneDeclaration(d, m);

       }

     }

 

-    public CasePattern CloneCasePattern(CasePattern pat) {

-      Contract.Requires(pat != null);

-      if (pat.Var != null) {

-        return new CasePattern(pat.tok, CloneBoundVar(pat.Var));

-      } else if (pat.Arguments == null) {

-        return new CasePattern(pat.tok, pat.Id, null);

-      } else {

-        return new CasePattern(pat.tok, pat.Id, pat.Arguments.ConvertAll(CloneCasePattern));

-      }

-    }

 

     public static bool ResolvePath(ModuleDecl root, List<IToken> Path, out ModuleSignature p, ResolutionErrorReporter reporter) {

       Contract.Requires(reporter != null);