Improved rank axioms for containers

1 files changed, 55 insertions, 56 deletions

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index b1298784..b2c688d9 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -706,8 +706,6 @@ namespace Microsoft.Dafny {
       sink.AddTopLevelDeclaration(dt_const);

 

       foreach (DatatypeCtor ctor in dt.Ctors) {

-        int i;

-

         // Add:  function #dt.ctor(tyVars, paramTypes) returns (DatatypeType);

 

         List<Bpl.Variable> argTypes = new List<Bpl.Variable>();

@@ -794,14 +792,13 @@ namespace Microsoft.Dafny {
           Bpl.Expr h;

           var hVar = BplBoundVar("$h", predef.HeapType, out h);

           Bpl.Expr conj = Bpl.Expr.True;

-          i = 0;

-          foreach (Formal arg in ctor.Formals) {

+          for (var i = 0; i < ctor.Formals.Count; i++) {

+            var arg = ctor.Formals[i];

             if (is_alloc) {

               conj = BplAnd(conj, MkIsAlloc(args[i], arg.Type, h));

             } else {

               conj = BplAnd(conj, MkIs(args[i], arg.Type));

             }

-            i++;

           }

           var c_params = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

           var c_ty = ClassTyCon((TopLevelDecl)dt, tyexprs);

@@ -837,8 +834,8 @@ namespace Microsoft.Dafny {
         }

 

         // Injectivity axioms for normal arguments

-        i = 0;

-        foreach (Formal arg in ctor.Formals) {

+        for (int i = 0; i < ctor.Formals.Count; i++) {

+          var arg = ctor.Formals[i];

           // function ##dt.ctor#i(DatatypeType) returns (Ti);

           var sf = ctor.Destructors[i];

           Contract.Assert(sf != null);

@@ -854,81 +851,83 @@ namespace Microsoft.Dafny {
           if (dt is IndDatatypeDecl) {

             var argType = arg.Type.NormalizeExpand();

             if (argType.IsDatatype || argType.IsTypeParameter) {

-              // for datatype:             axiom (forall params :: DtRank(params_i) < DtRank(#dt.ctor(params)));

-              // for type-parameter type:  axiom (forall params :: DtRank(Unbox(params_i)) < DtRank(#dt.ctor(params)));

+              // for datatype:             axiom (forall params :: {#dt.ctor(params)} DtRank(params_i) < DtRank(#dt.ctor(params)));

+              // for type-parameter type:  axiom (forall params :: {#dt.ctor(params)} BoxRank(params_i) < DtRank(#dt.ctor(params)));

               CreateBoundVariables(ctor.Formals, out bvs, out args);

               Bpl.Expr lhs = FunctionCall(ctor.tok, arg.Type.IsDatatype ? BuiltinFunction.DtRank : BuiltinFunction.BoxRank, null, args[i]);

               /* CHECK

               Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,

                 argType.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i]));

-              */

-              Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

-              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              // TRIG (forall a#11#0#0: Box, a#11#1#0: DatatypeType :: BoxRank(a#11#0#0) < DtRank(#_module.List.Cons(a#11#0#0, a#11#1#0)))

-              var trigger = (Trigger)null; // FIXME new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { lhs, rhs }); // TRIGGERS: THIS IS BROKEN // NEW_TRIGGER 

-              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs)); // CLEMENT: Trigger not is use, because it breaks termination checks for match statements

+              */                           

+              Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+              var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);

+              var trigger = BplTrigger(ct);

+              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs));

               sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive rank"));

             } else if (argType is SeqType) {

-              // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params)));

+              // axiom (forall params, i: int {#dt.ctor(params)} :: 0 <= i && i < |arg| ==> DtRank(arg[i]) < DtRank(#dt.ctor(params)));

               // that is:

-              // axiom (forall params, i: int :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params)));

-              CreateBoundVariables(ctor.Formals, out bvs, out args);

-              Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));

-              bvs.Add(iVar);

-              Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);

-              Bpl.Expr ante = Bpl.Expr.And(

-                Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),

-                Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));

-              Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,

-                FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType,

-                  FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie)));

-              Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

-              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List<Bpl.Expr> { lhs, rhs }), Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

-              sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q));

-              // axiom (forall params, SeqRank(arg) < DtRank(#dt.ctor(params)));

-              CreateBoundVariables(ctor.Formals, out bvs, out args);

-              lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]);

-              rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

-              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              var trigger = new Trigger(lhs.tok, true, new List<Bpl.Expr> { lhs, rhs });

-              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs));

-              sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive seq rank"));

+              // axiom (forall params, i: int {#dt.ctor(params)} :: 0 <= i && i < |arg| ==> DtRank(Unbox(Seq#Index(arg,i))) < DtRank(#dt.ctor(params)));

+              {

+                CreateBoundVariables(ctor.Formals, out bvs, out args);

+                Bpl.Variable iVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "i", Bpl.Type.Int));

+                bvs.Add(iVar);

+                Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, iVar);

+                Bpl.Expr ante = Bpl.Expr.And(

+                  Bpl.Expr.Le(Bpl.Expr.Literal(0), ie),

+                  Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i])));

+                var seqIndex = FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie);

+                Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null,

+                  FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType, seqIndex));

+                var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+                var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);

+                q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List<Bpl.Expr> { seqIndex, ct }), Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

+                sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q));

+              }

+

+              // axiom (forall params {#dt.ctor(params)} :: SeqRank(arg) < DtRank(#dt.ctor(params)));

+              {

+                CreateBoundVariables(ctor.Formals, out bvs, out args);

+                var lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]);

+                var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+                var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);

+                var trigger = BplTrigger(ct);

+                q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs));

+                sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive seq rank"));

+              }

             } else if (argType is SetType) {

-              // axiom (forall params, d: Datatype :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));

+              // axiom (forall params, d: Datatype {arg[d], #dt.ctor(params)}  :: arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));

               // that is:

-              // axiom (forall params, d: Datatype :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));

+              // axiom (forall params, d: Datatype {arg[Box(d)], #dt.ctor(params)} :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));

               CreateBoundVariables(ctor.Formals, out bvs, out args);

               Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));

               bvs.Add(dVar);

               Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);

-              Bpl.Expr ante = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));

+              Bpl.Expr inSet = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));

               Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);

-              Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

-              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { lhs, rhs });

-              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

+              var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+              var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);

+              var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inSet, ct });

+              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(inSet, Bpl.Expr.Lt(lhs, rhs)));

               sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive set rank"));

             } else if (argType is MultiSetType) {

-              // axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));

+              // axiom (forall params, d: Datatype {arg[d], #dt.ctor(params)} :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));

               // that is:

-              // axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));

+              // axiom (forall params, d: Datatype {arg[Box(d)], #dt.ctor(params)} :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));

               CreateBoundVariables(ctor.Formals, out bvs, out args);

               Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));

               bvs.Add(dVar);

               Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);

-              Bpl.Expr ante = Bpl.Expr.Gt(Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)), Bpl.Expr.Literal(0));

+              var inMultiset = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie));

+              Bpl.Expr ante = Bpl.Expr.Gt(inMultiset, Bpl.Expr.Literal(0));

               Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);

-              Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

-              rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);

-              // CLEMENT: Does the test suite cover this?

-              q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));  // W_TRIGGER

+              var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+              var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct);

+              var trigger = new Bpl.Trigger(ctor.tok, true, new List<Bpl.Expr> { inMultiset, ct });

+              q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));

               sink.AddTopLevelDeclaration(new Bpl.Axiom(ctor.tok, q, "Inductive multiset rank"));

-              // CLEMENT: I don't understand what this case disjunction does here; I don't think it's covered by the test suite

             }

           }

-

-          i++;

         }

       }