Redesigned the encoding of Dafny generics, including the built-in types set and seq.

Regrettably, these changes--although improvements in Dafny's functionality--have caused Test/dafny0/BinaryTree.bpl and Test/dafny0/SchorrWaite.dfy to be significantly slower (the dafny0 test directory now takes 6:11 whereas it used to take 1:43).

Improved some of the VSI-Benchmarks to use generics more fully, where the previous designed had just crashed.

Included the previously commented-out loop invariants and assertions in VSI-Benchmarks/b8.dfy.

Added a space in the pretty printing of Boogie coercion expressions.

1 files changed, 9 insertions, 2 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 75c5777e..9615586a 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -148,10 +148,17 @@ axiom (forall<T> s: Seq T, n: int, j: int :: { Seq#Index(Seq#Drop(s,n), j) }
 // -- Boxing and unboxing ----------------------------------------

 // ---------------------------------------------------------------

 

-function $Box<T>(T) returns (ref);

-function $Unbox<T>(ref) returns (T);

+type BoxType;

+

+function $Box<T>(T) returns (BoxType);

+function $Unbox<T>(BoxType) returns (T);

 

 axiom (forall<T> x: T :: { $Box(x) } $Unbox($Box(x)) == x);

+axiom (forall b: BoxType :: { $Unbox(b): int } $Box($Unbox(b): int) == b);

+axiom (forall b: BoxType :: { $Unbox(b): ref } $Box($Unbox(b): ref) == b);

+axiom (forall b: BoxType :: { $Unbox(b): Set BoxType } $Box($Unbox(b): Set BoxType) == b);

+axiom (forall b: BoxType :: { $Unbox(b): Seq BoxType } $Box($Unbox(b): Seq BoxType) == b);

+// note: an axiom like this for bool would not be sound

 

 // ---------------------------------------------------------------