From 4cbe4583b329a39dee2b4b456758cafbe7e2fa79 Mon Sep 17 00:00:00 2001
From: Dan Rosén <danr@chalmers.se>
Date: Mon, 11 Aug 2014 14:57:27 -0700
Subject: 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
---
 Binaries/DafnyPrelude.bpl | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'Binaries/DafnyPrelude.bpl')

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