Merge my autoTriggers work into the master branch

This contains trigger related things under the autoTriggers flag (disabled by
default), and some bug-fixes and cleanups that are already enabled.

1 files changed, 12 insertions, 9 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index be77f6b4..f959b537 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -17,12 +17,15 @@ namespace Microsoft.Dafny
       if (m is DefaultModuleDecl) {

         nw = new DefaultModuleDecl();

       } else {

-        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true);

+        nw = new ModuleDefinition(Tok(m.tok), name, m.IsAbstract, m.IsFacade, m.IsExclusiveRefinement, m.RefinementBaseName, m.Module, CloneAttributes(m.Attributes), true);

       }

       foreach (var d in m.TopLevelDecls) {

         nw.TopLevelDecls.Add(CloneDeclaration(d, nw));

       }

-      nw.RefinementBase = m.RefinementBase;

+      if (null != m.RefinementBase) {

+          nw.RefinementBase = m.RefinementBase;

+      }

+      nw.ClonedFrom = m;

       nw.Height = m.Height;

       return nw;

     }

@@ -33,7 +36,7 @@ namespace Microsoft.Dafny
 

       if (d is OpaqueTypeDecl) {

         var dd = (OpaqueTypeDecl)d;

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

+        return new OpaqueTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, dd.TypeArgs.ConvertAll(CloneTypeParam), CloneAttributes(dd.Attributes), d);

       } else if (d is TypeSynonymDecl) {

         var dd = (TypeSynonymDecl)d;

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

@@ -41,9 +44,9 @@ namespace Microsoft.Dafny
       } else if (d is NewtypeDecl) {

         var dd = (NewtypeDecl)d;

         if (dd.Var == null) {

-          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneType(dd.BaseType), CloneAttributes(dd.Attributes), dd);

         } else {

-          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes));

+          return new NewtypeDecl(Tok(dd.tok), dd.Name, m, CloneBoundVar(dd.Var), CloneExpr(dd.Constraint), CloneAttributes(dd.Attributes), dd);

         }

       } else if (d is TupleTypeDecl) {

         var dd = (TupleTypeDecl)d;

@@ -52,7 +55,7 @@ namespace Microsoft.Dafny
         var dd = (IndDatatypeDecl)d;

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

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

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

+        var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes), dd);

         return dt;

       } else if (d is CoDatatypeDecl) {

         var dd = (CoDatatypeDecl)d;

@@ -105,7 +108,7 @@ namespace Microsoft.Dafny
         if (d is DefaultClassDecl) {

           return new DefaultClassDecl(m, mm);

         } else {

-          return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType));

+          return new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes), dd.TraitsTyp.ConvertAll(CloneType), dd);

         }

       } else if (d is ModuleDecl) {

         if (d is LiteralModuleDecl) {

@@ -138,7 +141,7 @@ namespace Microsoft.Dafny
     }

 

     public TypeParameter CloneTypeParam(TypeParameter tp) {

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

+      return new TypeParameter(Tok(tp.tok), tp.Name, tp.EqualitySupport, tp);

     }

 

     public MemberDecl CloneMember(MemberDecl member) {

@@ -545,7 +548,7 @@ namespace Microsoft.Dafny
 

       } else if (stmt is CalcStmt) {

           var s = (CalcStmt)stmt;

-          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp));

+          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;