From c38ad7de79e9a3b351ba9f1a8648f43893ec7ca7 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Wed, 9 Nov 2011 10:31:35 -0800
Subject: Dafny: moved definition of class.array into prelude, anticipating
 writing axioms that use it

---
 Source/Dafny/Translator.cs | 26 ++++++++++++++++++++------
 1 file changed, 20 insertions(+), 6 deletions(-)

(limited to 'Source/Dafny/Translator.cs')

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) }
-- 
cgit v1.2.3