Dafny: moved definition of class.array into prelude, anticipating writing axioms that use it

2 files changed, 29 insertions, 6 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 1fe21204..c954c019 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -326,6 +326,14 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
 axiom (forall h: HeapType, i: int, v: BoxType, a: ref ::

   { Seq#FromArray(update(h, a, IndexField(i), v), a) }

     0 <= i && i < array.Length(a) ==> Seq#FromArray(update(h, a, IndexField(i), v), a) == Seq#Update(Seq#FromArray(h, a), i, v) );

+/**** Someday:

+axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h, a) }

+    $IsGoodHeap(h) &&

+    a != null && read(h, a, alloc) && dtype(a) == class.array && TypeParams(a, 0) == class.bool

+    ==>

+    (forall i: int :: { Seq#Index(Seq#FromArray(h, a), i) }

+      0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==>  $IsCanonicalBoolBox(Seq#Index(Seq#FromArray(h, a), i))));

+****/

 

 // Commutability of Take and Drop with Update.

 axiom (forall<T> s: Seq T, i: int, v: T, n: int ::

@@ -379,6 +387,7 @@ const unique class.bool: ClassName;
 const unique class.set: ClassName;

 const unique class.seq: ClassName;

 const unique class.multiset: ClassName;

+const unique class.array: ClassName;

 

 function /*{:never_pattern true}*/ dtype(ref): ClassName;

 function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 66cfbc57..e455561a 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -54,6 +54,7 @@ namespace Microsoft.Dafny {
       public readonly Bpl.Type DtCtorId;

       public readonly Bpl.Expr Null;

       private readonly Bpl.Constant allocField;

+      public readonly Bpl.Constant ClassDotArray;

       [ContractInvariantMethod]

       void ObjectInvariant() {

         Contract.Invariant(RefType != null);

@@ -71,6 +72,7 @@ namespace Microsoft.Dafny {
         Contract.Invariant(DtCtorId != null);

         Contract.Invariant(Null != null);

         Contract.Invariant(allocField != null);

+        Contract.Invariant(ClassDotArray != null);

       }

 

 

@@ -116,7 +118,7 @@ namespace Microsoft.Dafny {
                              Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,

                              Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,

                              Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,

-                             Bpl.Constant allocField) {

+                             Bpl.Constant allocField, Bpl.Constant classDotArray) {

         #region Non-null preconditions on parameters

         Contract.Requires(refType != null);

         Contract.Requires(boxType != null);

@@ -130,6 +132,7 @@ namespace Microsoft.Dafny {
         Contract.Requires(datatypeType != null);

         Contract.Requires(dtCtorId != null);

         Contract.Requires(allocField != null);

+        Contract.Requires(classDotArray != null);

         #endregion

 

         Bpl.CtorType refT = new Bpl.CtorType(Token.NoToken, refType, new Bpl.TypeSeq());

@@ -148,6 +151,7 @@ namespace Microsoft.Dafny {
         this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());

         this.allocField = allocField;

         this.Null = new Bpl.IdentifierExpr(Token.NoToken, "null", refT);

+        this.ClassDotArray = classDotArray;

       }

     }

 

@@ -171,6 +175,7 @@ namespace Microsoft.Dafny {
       Bpl.TypeCtorDecl tickType = null;

       Bpl.GlobalVariable heap = null;

       Bpl.Constant allocField = null;

+      Bpl.Constant classDotArray = null;

       foreach (var d in prog.TopLevelDeclarations) {

         if (d is Bpl.TypeCtorDecl) {

           Bpl.TypeCtorDecl dt = (Bpl.TypeCtorDecl)d;

@@ -203,6 +208,8 @@ namespace Microsoft.Dafny {
           Bpl.Constant c = (Bpl.Constant)d;

           if (c.Name == "alloc") {

             allocField = c;

+          } else if (c.Name == "class.array") {

+            classDotArray = c;

           }

         } else if (d is Bpl.GlobalVariable) {

           Bpl.GlobalVariable v = (Bpl.GlobalVariable)d;

@@ -241,10 +248,12 @@ namespace Microsoft.Dafny {
         Console.WriteLine("Error: Dafny prelude is missing declaration of $Heap");

       } else if (allocField == null) {

         Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");

+      } else if (classDotArray == null) {

+        Console.WriteLine("Error: Dafny prelude is missing declaration of class.array");

       } else {

         return new PredefinedDecls(refType, boxType, tickType,

                                    setTypeCtor, multiSetTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,

-                                   allocField);

+                                   allocField, classDotArray);

       }

       return null;

     }

@@ -520,7 +529,11 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(sink != null && predef != null);

       Contract.Requires(c != null);

-      sink.TopLevelDeclarations.Add(GetClass(c));

+      if (c.Name == "array") {

+        classes.Add(c, predef.ClassDotArray);

+      } else {

+        sink.TopLevelDeclarations.Add(GetClass(c));

+      }

 

       foreach (MemberDecl member in c.Members) {

         if (member is Field) {

@@ -4532,13 +4545,14 @@ namespace Microsoft.Dafny {
         Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));

         Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);

 

+        Bpl.Expr isGoodMultiset = FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);

         Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);

         if (wh != null) {

           Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));

-          return Bpl.Expr.And(FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, Bpl.Type.Bool, x),

-                              new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh)));

+          var q = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

+          isGoodMultiset = Bpl.Expr.And(isGoodMultiset, q);

         }

-        return FunctionCall(tok, BuiltinFunction.IsGoodMultiSet, null, x);

+        return isGoodMultiset;

       } else if (type is SeqType) {

         SeqType st = (SeqType)type;

         // (forall i: int :: { Seq#Index(x,i) }