From 7cd74a6c41a90023ba1c33fa00b2a140fc4c935d Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 5 Jan 2012 18:01:38 -0800
Subject: Dafny: fully qualify (with module names) names of types in the
 translation into Boogie Dafny: started cloning of refined classes Dafny:
 added /rprint switch to print the (syntax of the) resolved Dafny program

---
 Binaries/DafnyPrelude.bpl | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'Binaries')

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index c954c019..b3fc7e24 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -317,7 +317,7 @@ axiom (forall<T> s, t: Seq T ::
 function Seq#FromArray(h: HeapType, a: ref): Seq BoxType;
 axiom (forall h: HeapType, a: ref ::
   { Seq#Length(Seq#FromArray(h,a)) }
-    Seq#Length(Seq#FromArray(h, a)) == array.Length(a));
+    Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a));
 axiom (forall h: HeapType, a: ref :: { Seq#FromArray(h,a): Seq BoxType }
    (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i))));
 axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
@@ -325,11 +325,11 @@ axiom (forall<alpha> h: HeapType, o: ref, f: Field alpha, v: alpha, a: ref ::
     o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) );
 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) );
+    0 <= i && i < _System.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
+    a != null && read(h, a, alloc) && dtype(a) == class._System.array && TypeParams(a, 0) == class._System.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))));
@@ -351,7 +351,7 @@ axiom (forall<T> s: Seq T, i: int, v: T, n: int ::
 // Extension axiom, triggers only on Takes from arrays.
 axiom (forall h: HeapType, a: ref, n0, n1: int ::
   { Seq#Take(Seq#FromArray(h, a), n0), Seq#Take(Seq#FromArray(h, a), n1) }
-    n0 + 1 == n1 && 0 <= n0 && n1 <= array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );
+    n0 + 1 == n1 && 0 <= n0 && n1 <= _System.array.Length(a) ==> Seq#Take(Seq#FromArray(h, a), n1) == Seq#Build(Seq#Take(Seq#FromArray(h, a), n0), read(h, a, IndexField(n0): Field BoxType)) );
 // drop commutes with build.
 axiom (forall<T> s: Seq T, v: T, n: int ::
   { Seq#Drop(Seq#Build(s, v), n) }
@@ -382,12 +382,12 @@ axiom (forall b: BoxType :: { $Unbox(b): bool } $IsCanonicalBoolBox(b) ==> $Box(
 // ---------------------------------------------------------------
 
 type ClassName;
-const unique class.int: ClassName;
-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;
+const unique class._System.int: ClassName;
+const unique class._System.bool: ClassName;
+const unique class._System.set: ClassName;
+const unique class._System.seq: ClassName;
+const unique class._System.multiset: ClassName;
+const unique class._System.array: ClassName;
 
 function /*{:never_pattern true}*/ dtype(ref): ClassName;
 function /*{:never_pattern true}*/ TypeParams(ref, int): ClassName;
@@ -495,8 +495,8 @@ axiom (forall r: ref, h: HeapType ::
 // -- Arrays -----------------------------------------------------
 // ---------------------------------------------------------------
 
-function array.Length(a: ref): int;
-axiom (forall o: ref :: 0 <= array.Length(o));
+function _System.array.Length(a: ref): int;
+axiom (forall o: ref :: 0 <= _System.array.Length(o));
 
 // ---------------------------------------------------------------
 // -- The heap ---------------------------------------------------
-- 
cgit v1.2.3