Add higher-order-functions and some other goodies

  * The reads clause now needs to be self framing.

  * The requires clause now needs to be framed by the reads clause.

  * There are one-shot lambdas, with a single arrow, but they will probably be
    removed.

  * There is a {:heapQuantifier} attribute to quantifiers, but they will
    probably be removed.

  * Add smart handling of type variables

  * Add < and > for datatype & type parameter

1 files changed, 11 insertions, 0 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 7b52f69f..3d5bf111 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -243,6 +243,10 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
   TypeTupleCar(TypeTuple(a,b)) == a &&

   TypeTupleCdr(TypeTuple(a,b)) == b);

 

+// -- Function handles -------------------------------------------

+

+type HandleType;

+

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

 // -- Datatypes --------------------------------------------------

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

@@ -257,6 +261,9 @@ type DtCtorId;
 function DatatypeCtorId(DatatypeType): DtCtorId;

 

 function DtRank(DatatypeType): int;

+function BoxRank(Box): int;

+

+axiom (forall d: DatatypeType :: {BoxRank($Box(d))} BoxRank($Box(d)) == DtRank(d));

 

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

 // -- Axiom contexts ---------------------------------------------

@@ -274,6 +281,10 @@ type LayerType;
 const $LZ: LayerType;

 function $LS(LayerType): LayerType;

 

+function AtLayer<A>([LayerType]A, LayerType): A;

+axiom (forall<A> f : [LayerType]A, ly : LayerType :: { AtLayer(f,ly) } AtLayer(f,ly) == f[ly]);

+axiom (forall<A> f : [LayerType]A, ly : LayerType :: { AtLayer(f,$LS(ly)) } AtLayer(f,$LS(ly)) == AtLayer(f,ly));

+

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

 // -- Fields -----------------------------------------------------

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