diff options
| author |  Rustan Leino <unknown> | 2013-08-02 18:43:08 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-02 18:43:08 -0700 |
| commit | 0c2d9800db9d910c286450d112a83cbf1cd40fdd (patch) | |
| tree | 58691e045654123915b90e89326a08a2c6db2241 /Binaries/DafnyPrelude.bpl | |
| parent | 97404d89e5c945d41899ed74e5aa234a61b91c65 (diff) | |
Changed the encoding of recursive functions. Previous, three hardcoded layers were used: F#2, F, and F#limited. Now, recursive functions take a layer argument, which is specified by Peano numbers.
Also, cleaned up and made more consistent the emission of axioms regarding functions.
Diffstat (limited to 'Binaries/DafnyPrelude.bpl')
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index db08a280..6508df2d 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -555,6 +555,14 @@ const $FunctionContextHeight: int; const $InMethodContext: bool;
// ---------------------------------------------------------------
+// -- Layers of function encodings -------------------------------
+// ---------------------------------------------------------------
+
+type LayerType;
+const $LZ: LayerType;
+function $LS(LayerType): LayerType;
+
+// ---------------------------------------------------------------
// -- Fields -----------------------------------------------------
// ---------------------------------------------------------------
@@ -686,6 +694,13 @@ axiom (forall h: HeapType, k: HeapType :: { $HeapSuccGhost(h,k) } !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));
// ---------------------------------------------------------------
+// -- Non-determinism --------------------------------------------
+// ---------------------------------------------------------------
+
+type TickType;
+var $Tick: TickType;
+
+// ---------------------------------------------------------------
// -- Useful macros ----------------------------------------------
// ---------------------------------------------------------------
@@ -723,10 +738,3 @@ procedure $IterCollectNewObjects(prevHeap: HeapType, newHeap: HeapType, this: re ($Unbox(bx) != null && !read(prevHeap, $Unbox(bx):ref, alloc) && read(newHeap, $Unbox(bx):ref, alloc)));
// ---------------------------------------------------------------
-// -- Non-determinism --------------------------------------------
-// ---------------------------------------------------------------
-
-type TickType;
-var $Tick: TickType;
-
-// ---------------------------------------------------------------
|