Merge

1 files changed, 22 insertions, 13 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index f0baeef3..a150eecd 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -4453,7 +4453,12 @@ namespace Microsoft.Dafny {
         if (canCall != Bpl.Expr.True) {

           List<Variable> bvars = new List<Variable>();

           Bpl.Expr typeAntecedent = etran.TrBoundVariables(e.BoundVars, bvars);

-          canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), Bpl.Expr.Imp(typeAntecedent, canCall));

+          if (Attributes.Contains(e.Attributes, "trigger")) {

+            Bpl.Trigger tr = TrTrigger(etran, e.Attributes, expr.tok);

+            canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), tr, Bpl.Expr.Imp(typeAntecedent, canCall));

+          } else {

+            canCall = new Bpl.ForallExpr(expr.tok, Concat(tyvars, bvars), Bpl.Expr.Imp(typeAntecedent, canCall));

+          }

         }

         return canCall;

       } else if (expr is StmtExpr) {

@@ -4863,7 +4868,8 @@ namespace Microsoft.Dafny {
           Formal p = e.Function.Formals[i];

           // Note, in the following, the "##" makes the variable invisible in BVD.  An alternative would be to communicate

           // to BVD what this variable stands for and display it as such to the user.

-          LocalVariable local = new LocalVariable(p.tok, p.tok, "##" + p.Name, p.Type, p.IsGhost);

+          Type et = Resolver.SubstType(p.Type, e.TypeArgumentSubstitutions);

+          LocalVariable local = new LocalVariable(p.tok, p.tok, "##" + p.Name, et, p.IsGhost);

           local.type = local.OptionalType;  // resolve local here

           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator));

           ie.Var = local; ie.Type = ie.Var.Type;  // resolve ie here

@@ -4871,9 +4877,8 @@ namespace Microsoft.Dafny {
           locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))));

           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

           Expression ee = e.Args[i];

-          Type et = Resolver.SubstType(p.Type, e.TypeArgumentSubstitutions);

           CheckSubrange(ee.tok, etran.TrExpr(ee), et, builder);

-          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type));

+          Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), et));

           builder.Add(cmd);

           builder.Add(new Bpl.CommentCmd("assume allocatedness for argument to function"));

           builder.Add(new Bpl.AssumeCmd(e.Args[i].tok, MkIsAlloc(lhs, et, etran.HeapExpr)));

@@ -5096,7 +5101,8 @@ namespace Microsoft.Dafny {
             if (tup.Item1.Count != 0) {

               var bvs = new List<Variable>();

               var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

-              body = new Bpl.ExistsExpr(e.tok, bvs, BplAnd(typeAntecedent, body));

+              var triggers = TrTrigger(etran, e.Attributes, e.tok);

+              body = new Bpl.ExistsExpr(e.tok, bvs, triggers, BplAnd(typeAntecedent, body));

             }

             w = BplOr(body, w);

           }

@@ -7050,7 +7056,8 @@ namespace Microsoft.Dafny {
             if (tup.Item1.Count != 0) {

               var bvs = new List<Variable>();

               var typeAntecedent = etran.TrBoundVariables(tup.Item1, bvs);

-              body = new Bpl.ExistsExpr(s.Tok, bvs, BplAnd(typeAntecedent, body));

+              var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap);

+              body = new Bpl.ExistsExpr(s.Tok, bvs, triggers, BplAnd(typeAntecedent, body));

             }

             w = BplOr(body, w);

           }

@@ -8241,7 +8248,8 @@ namespace Microsoft.Dafny {
 

       Bpl.Expr qq = Bpl.Expr.Imp(ante, post);

       if (bvars.Count != 0) {

-        qq = new Bpl.ForallExpr(s.Tok, bvars, qq);

+        var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap);

+        qq = new Bpl.ForallExpr(s.Tok, bvars, triggers, qq);

       }

       exporter.Add(new Bpl.AssumeCmd(s.Tok, qq));

     }

@@ -11187,14 +11195,15 @@ namespace Microsoft.Dafny {
           // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))".

           List<Variable> bvars = new List<Variable>();

           Bpl.Expr typeAntecedent = TrBoundVariables(e.BoundVars, bvars);

-          Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

+          Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

 

           var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.CurrentIdGenerator.FreshId("$y#"), predef.BoxType));

           Bpl.Expr y = new Bpl.IdentifierExpr(expr.tok, yVar);

 

           var eq = Bpl.Expr.Eq(y, BoxIfNecessary(expr.tok, TrExpr(e.Term), e.Term.Type));

           var ebody = Bpl.Expr.And(BplAnd(typeAntecedent, TrExpr(e.Range)), eq);

-          var exst = new Bpl.ExistsExpr(expr.tok, bvars, ebody);

+          var triggers = translator.TrTrigger(this, e.Attributes, e.tok);

+          var exst = new Bpl.ExistsExpr(expr.tok, bvars, triggers, ebody);

 

           return new Bpl.LambdaExpr(expr.tok, new List<TypeVariable>(), new List<Variable> { yVar }, kv, exst);

 

@@ -11208,7 +11217,7 @@ namespace Microsoft.Dafny {
           var bv = e.BoundVars[0];

           TrBoundVariables(e.BoundVars, bvars);

 

-          Bpl.QKeyValue kv = TrAttributes(e.Attributes, null);

+          Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger");

 

           var yVar = new Bpl.BoundVariable(expr.tok, new Bpl.TypedIdent(expr.tok, translator.CurrentIdGenerator.FreshId("$y#"), predef.BoxType));

 

@@ -13417,9 +13426,9 @@ namespace Microsoft.Dafny {
           Attributes newAttrs = SubstAttributes(e.Attributes);

           if (newBoundVars != e.BoundVars || newRange != e.Range || newTerm != e.Term || newAttrs != e.Attributes) {

             if (e is SetComprehension) {

-              newExpr = new SetComprehension(expr.tok, newBoundVars, newRange, newTerm);

+              newExpr = new SetComprehension(expr.tok, newBoundVars, newRange, newTerm, newAttrs);

             } else if (e is MapComprehension) {

-              newExpr = new MapComprehension(expr.tok, ((MapComprehension)e).Finite, newBoundVars, newRange, newTerm);

+              newExpr = new MapComprehension(expr.tok, ((MapComprehension)e).Finite, newBoundVars, newRange, newTerm, newAttrs);

             } else if (expr is ForallExpr) {

               newExpr = new ForallExpr(expr.tok, ((QuantifierExpr)expr).TypeArgs, newBoundVars, newRange, newTerm, newAttrs);

             } else if (expr is ExistsExpr) {

@@ -13697,7 +13706,7 @@ namespace Microsoft.Dafny {
           r = rr;

         } else if (stmt is AssignSuchThatStmt) {

           var s = (AssignSuchThatStmt)stmt;

-          r = new AssignSuchThatStmt(s.Tok, s.EndTok, s.Lhss.ConvertAll(Substitute), Substitute(s.Expr), s.AssumeToken == null ? null : s.AssumeToken);

+          r = new AssignSuchThatStmt(s.Tok, s.EndTok, s.Lhss.ConvertAll(Substitute), Substitute(s.Expr), s.AssumeToken == null ? null : s.AssumeToken, null);

         } else if (stmt is UpdateStmt) {

           var s = (UpdateStmt)stmt;

           var resolved = s.ResolvedStatements;