Add lambda compilation example, and remove some unused files from the tests

5 files changed, 20 insertions, 465 deletions

diff --git a/Test/hofs/Compilation.dfy b/Test/hofs/Compilation.dfy
index c3132db2..2033dabf 100644
--- a/Test/hofs/Compilation.dfy
+++ b/Test/hofs/Compilation.dfy
@@ -1,3 +1,5 @@
+// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
 
 class Ref<A> {
   var val : A;
diff --git a/Test/hofs/Compilation.dfy.expect b/Test/hofs/Compilation.dfy.expect
index 0c6452d2..06c13679 100644
--- a/Test/hofs/Compilation.dfy.expect
+++ b/Test/hofs/Compilation.dfy.expect
@@ -1,3 +1,20 @@
 

 Dafny program verifier finished with 2 verified, 0 errors

-Compiled assembly into Compilation.exe

+Program compiled successfully

+Running...

+

+1 = 1
+3 = 3
+3 = 3
+0 = 0
+3 = 3
+4 = 4
+3 = 3
+4 = 4
+3 = 3
+4 = 4
+4 = 4
+5 = 5
+55 = 55
+0 = 0
+1 = 1
diff --git a/Test/hofs/Map.dfy b/Test/hofs/Map.dfy
deleted file mode 100644
index a55be2be..00000000
--- a/Test/hofs/Map.dfy
+++ /dev/null
@@ -1,117 +0,0 @@
-
-datatype List<A> = Nil | Cons(hd: A,tl: List<A>);
-
-function method Map<A,B>(f : A -> B, xs : List<A>) : List<B>
-  requires forall x :: f.requires(x);
-  reads *;
-  decreases xs;
-{
-  match xs
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),Map(f,xs))
-}
-
-function method Id<A>(x : A) : A { x }
-
-method Test() {
-  assert Map(Id, Cons(1,Nil)) == Cons(1,Nil);
-  var inc := x => x + 1;
-  assert Map(inc, Cons(1,Nil)) == Cons(2,Nil);
-  assert Map(x => x + 1, Cons(1,Nil)) == Cons(2,Nil);
-  assert Map((x) requires x > 0 => x + 1, Nil) == Nil;
-}
-
-function CanCall<A,B>(f : A -> B, xs : List<A>) : bool
-  decreases xs;
-  reads *;
-{
-  match xs
-    case Nil => true
-    case Cons(x,xs) => f.requires(x) && CanCall(f, xs)
-}
-
-function method MegaMap<A,B>(f : A -> B, xs : List<A>) : List<B>
-  requires CanCall(f, xs);
-  reads *;
-  decreases xs;
-{
-  match xs
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),MegaMap(f,xs))
-}
-
-method Test2() {
-  assert MegaMap((x) requires x != 0 => 100 / x, Cons(2, Nil)).hd == 50;
-}
-
-function All<A>(p : A -> bool, xs : List<A>) : bool
-  requires forall x :: p.requires(x) /* && p.reads(x) == {} */;
-  reads *;
-  decreases xs;
-{
-  match xs
-    case Nil => true
-    case Cons(x,xs) => p(x) && All(p,xs)
-}
-
-/*
-function UnionMap(i : A -> set<B>, ys : List<A>): set<B>
-  requires forall x :: i.requires(x) && i.reads(x) == {};
-  decreases ys;
-{
-  match ys
-    case Nil => {}
-    case Cons(x,xs) => i(x) + UnionMap(i,xs)
-}
-*/
-
-function method NinjaMap<A,B>(f : A -> B, ys : List<A>) : List<B>
-  requires All(f.requires, ys);
-//  reads UnionMap(f.reads, ys);
-  reads *;
-  decreases ys;
-{
-  match ys
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),NinjaMap(f,xs))
-}
-
-function method Compose(f : B -> C, g : A -> B) : A -> C
-{
-  x requires g.requires(x) && f.requires(g(x))
-    reads    g.reads(x) + f.reads(g(x))
-    => f(g(x))
-}
-
-lemma {:induction 0} MapCompose(f : B -> C, g : A -> B, xs : List<A>)
-  requires All(g.requires, xs);
-  requires All(f.requires, NinjaMap(g,xs));
-  requires All(Compose(f,g).requires, xs);
-
-  decreases xs;
-  ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs);
-{
-  match xs
-    case Nil =>
-    case Cons(x,xs) =>
-      calc {
-            NinjaMap(f,NinjaMap(g,Cons(x,xs)));
-         == NinjaMap(f,Cons(g(x),NinjaMap(g,xs)));
-         == Cons(f(g(x)),NinjaMap(f,NinjaMap(g,xs)));
-         == { MapCompose(f,g,xs); }
-            Cons(f(g(x)),NinjaMap(Compose(f,g),xs));
-         == Cons(Compose(f,g)(x),NinjaMap(Compose(f,g),xs));
-         == NinjaMap(Compose(f,g),Cons(x,xs));
-      }
-}
-
-// auto-mode
-lemma MapCompose2(f : B -> C, g : A -> B, xs : List<A>)
-  requires All(g.requires, xs);
-  requires All(f.requires, NinjaMap(g,xs));
-  requires All(Compose(f,g).requires, xs);
-  decreases xs;
-  ensures NinjaMap(f,NinjaMap(g,xs)) == NinjaMap(Compose(f,g),xs);
-{
-}
-
diff --git a/Test/hofs/Quant.dfy b/Test/hofs/Quant.dfy
deleted file mode 100644
index 70d15902..00000000
--- a/Test/hofs/Quant.dfy
+++ /dev/null
@@ -1,132 +0,0 @@
-
-module QuantReads {
-
-  function All<A>(p : A -> bool) : bool
-    reads set x : A, y : object | y in p.reads(x) :: y;
-    requires forall x : A :: p.requires(x);
-  {
-    forall x : A :: p(x)
-  }
-
-  lemma AllQuant<A>(p : A -> bool)
-    requires All.requires(p);
-    requires All(p);
-    ensures forall x : A :: p(x);
-  {
-  }
-
-}
-
-module Forall {
-
-  function All<A>(p : A -> bool) : bool
-  {
-    forall x :: p.requires(x) && p(x)
-  }
-
-  function CallMe(f : int -> int) : int
-    requires All(f.requires);
-  {
-    f(1) + f(2)
-  }
-
-}
-
-module Quant {
-
-  function All<A>(p : A -> bool) : bool
-    requires forall x : A :: p.requires(x);
-  {
-    forall x : A :: p(x)
-  }
-
-  lemma AllBool(p : bool -> bool)
-    requires forall x : bool :: p.requires(x);
-    requires All(p);
-    ensures p(true) && p(false);
-  {
-  }
-
-  method Boo()
-    requires All(x => x);
-    ensures false;
-  {
-    AllBool(x => x);
-  }
-
-  lemma AllQuant<A>(p : A -> bool)
-    requires All.requires(p);
-    requires All(p);
-    ensures forall x : A :: p(x);
-  {
-  }
-
-  method Boo2()
-    requires All(x => x);
-    ensures false;
-  {
-    assert (x => x)(false);
-  }
-
-
-  method Koo(s : set<int>, t : set<int>)
-    requires All(x => (x in s ==> x in t) && (x in t ==> x in s));
-    ensures All(x => x in s <==> x in t);
-  {
-  }
-
-}
-
-module ReadAll {
-
-  datatype List<A> = Nil | Cons(A,List<A>);
-
-  function All(p : A -> bool, xs : List) : bool
-    reads (set x, y | y in p.reads(x) :: y);
-    requires forall x :: p.reads(x) == {} && p.requires(x);
-    decreases xs;
-  {
-    match xs
-      case Nil => true
-      case Cons(x,xs) => p(x) && All(p,xs)
-  }
-
-  function Div(xs : List<int>) : List<int>
-    requires All(x => x > 0, xs);
-  {
-    match xs
-      case Nil => Nil
-      case Cons(x,xs) => Cons(100 / x,Div(xs))
-  }
-
-}
-
-module Requires {
-
-  method SmallTest(f : int -> int)
-    requires f.requires(0);
-  {
-    print f(0);
-  }
-
-  datatype List<A> = Nil | Cons(hd: A,tl: List<A>);
-
-  function All<A>(p : A -> bool, xs : List<A>) : bool
-    requires forall x :: p.requires(x);
-    decreases xs;
-  {
-    match xs
-      case Nil => true
-      case Cons(x,xs) => p(x) && All(p,xs)
-  }
-
-  function method Map<A,B>(f : A -> B, ys : List<A>) : List<B>
-    requires All(f.requires, ys);
-    decreases ys;
-  {
-    match ys
-      case Nil => Nil
-      case Cons(x,xs) => Cons(f(x),Map(f,xs))
-  }
-
-}
diff --git a/Test/hofs/TreeMap.dfy b/Test/hofs/TreeMap.dfy
deleted file mode 100644
index 95b07590..00000000
--- a/Test/hofs/TreeMap.dfy
+++ /dev/null
@@ -1,215 +0,0 @@
-
-datatype List<A> = Nil | Cons(head: A,tail: List<A>);
-
-datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>);
-
-function Set(xs : List) : set
-  ensures forall x :: x in Set(xs) ==> x < xs;
-{
-  match xs
-    case Nil => {}
-    case Cons(x,xs) => {x} + Set(xs)
-}
-
-function TSet(t0 : Tree) : set
-  ensures forall t :: t in TSet(t0) ==> t < t0;
-{
-  match t0 case Branch(x,ts) => {x} + set t, y | t in Set(ts) && y in TSet(t) :: y
-}
-
-// reads {}
-
-function ReadNothingMap(f : A -> B, xs: List<A>): List<B>
-  requires forall x :: x in Set(xs) ==> f.requires(x);
-  requires forall x :: f.reads(x) == {};
-  decreases xs;
-{
-  match xs
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),ReadNothingMap(f,xs))
-}
-
-function TReadNothingMap(f: A -> B, t0: Tree<A>): Tree<B>
-  requires forall x {:heapQuantifier} :: f.requires(x);
-  requires forall x {:heapQuantifier} :: f.reads(x) == {};
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(f(x), ReadNothingMap(t requires t in Set(ts) => TReadNothingMap(f,t), ts))
-}
-
-function TReadNothingMap2(f: A -> B, t0: Tree<A>): Tree<B>
-  requires forall x :: f.requires(x);
-  requires forall x :: f.reads(x) == {};
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(f(x), ReadNothingMap(t requires t in Set(ts) -> TReadNothingMap2(f,t), ts))
-}
-
-function TReadNothingMap3(f: A -> B, t0: Tree<A>): Tree<B>
-  requires forall x :: f.requires(x);
-  requires forall x :: f.reads(x) == {};
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(f(x), ReadNothingMap(
-    t requires t in Set(ts)
-      requires (forall x :: x in TSet(t) ==> f.requires(x))
-    => TReadNothingMap(f,t), ts))
-}
-
-method TestReadNothingStar() {
-  assert TReadNothingMap(x => x + 1, Branch(1,Nil)).Branch?;
-
-  assert TReadNothingMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil);
-
-  assert TReadNothingMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
-      == Branch(2,Cons(Branch(1,Nil),Nil));
-
-  assert TReadNothingMap2(x -> x + 1, Branch(1,Nil)).Branch?;
-
-  assert TReadNothingMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
-
-  assert TReadNothingMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
-      == Branch(2,Cons(Branch(1,Nil),Nil));
-}
-
-/// reads *
-
-function ReadStarMap(f : A -> B, xs: List<A>): List<B>
-  requires forall x :: x in Set(xs) ==> f.requires(x);
-  reads *;
-  decreases xs;
-{
-  match xs
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),ReadStarMap(f,xs))
-}
-
-function TReadStarMap(f: A -> B, t0: Tree<A>): Tree<B>
-  requires forall x {:heapQuantifier} :: f.requires(x);
-  reads *;
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) => TReadStarMap(f,t), ts))
-}
-
-function TReadStarMap2(f: A -> B, t0: Tree<A>): Tree<B>
-  requires forall x :: f.requires(x);
-  reads *;
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts))
-}
-
-lemma LitTReadStarMap2(f : A -> B, x : A, ts: List<Tree<A>>)
-  requires forall u :: f.requires(u);
-  ensures TReadStarMap2(f, Branch(x,ts)) ==
-    Branch(f(x), ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t), ts));
-{
-  assert TReadStarMap2(f, Branch(x,ts)).val == f(x);
-  if (ts.Nil?) {
-    assert TReadStarMap2(f, Branch(x,ts)).trees ==
-      ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts);
-  } else {
-    assert TReadStarMap2(f, Branch(x,ts)).trees ==
-      ReadStarMap(t reads * requires t in Set(ts) -> TReadStarMap2(f,t),ts);
-  }
-}
-
-method TestReadStar() {
-  assert TReadStarMap(x => x + 1, Branch(1,Nil)).Branch?;
-
-  assert TReadStarMap(x => x + 1, Branch(0,Nil)) == Branch(1,Nil);
-
-  assert ReadStarMap(t reads * requires t in Set(Cons(Branch(0,Nil),Nil)) -> TReadStarMap(x => x + 1,t)
-                    , Cons(Branch(0,Nil),Nil))
-      == Cons(Branch(1,Nil),Nil);
-
-  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).Branch?;
-
-  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).val == 2;
-
-  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil))).trees == Cons(Branch(1,Nil),Nil);
-
-  assert TReadStarMap(x => x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
-      == Branch(2,Cons(Branch(1,Nil),Nil));
-
-  assert TReadStarMap2(x -> x + 1, Branch(1,Nil)).Branch?;
-
-  assert TReadStarMap2(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
-
-  assert TReadStarMap2(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
-      == Branch(2,Cons(Branch(1,Nil),Nil));
-}
-
-/// reads exact
-
-function Map(f : A -> B, xs: List<A>): List<B>
-  requires forall x :: x in Set(xs) ==> f.requires(x);
-  reads set x, y | x in Set(xs) && y in f.reads(x) :: y;
-  decreases xs;
-{
-  match xs
-    case Nil => Nil
-    case Cons(x,xs) => Cons(f(x),Map(f,xs))
-}
-
-function TMap(f : A -> B, t0: Tree<A>): Tree<B>
-  requires forall t :: t in TSet(t0) ==> f.requires(t);
-  reads set x, y | x in TSet(t0) && y in f.reads(x) :: y;
-  decreases t0;
-{
-  var Branch(x,ts) := t0;
-  Branch(
-    f(x),
-    Map( t requires t in Set(ts)
-           reads set x, y | x in TSet(t) && y in f.reads(x) :: y
-           -> TMap(f,t)
-       , ts)
-  )
-}
-
-lemma LitTMap(f : A -> B,x : A, ts: List<Tree<A>>)
-  requires f.requires(x);
-  requires forall t, u :: t in Set(ts) && u in TSet(t) ==> f.requires(u);
-  ensures TMap(f, Branch(x,ts)) ==
-    Branch(f(x),
-      Map( t requires t in Set(ts)
-             reads set x, y | x in TSet(t) && y in f.reads(x) :: y
-             -> TMap(f,t),ts));
-{
-  assert TMap(f, Branch(x,ts)).val == f(x);
-  assert TMap(f, Branch(x,ts)).trees ==
-      Map(t requires t in Set(ts)
-            reads set x, y | x in TSet(t) && y in f.reads(x) :: y
-            -> TMap(f,t),ts);
-}
-
-method Test() {
-  assert TMap(x -> x + 1, Branch(1,Nil)).Branch?;
-
-  assert TMap(x -> x + 1, Branch(0,Nil)) == Branch(1,Nil);
-
-  calc {
-       TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)));
-    == { LitTMap(x -> x + 1,1, Cons(Branch(0,Nil),Nil)); }
-       Branch((x -> x + 1)(1),Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
-    ==
-       Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
-    ==
-       Branch(2,Map(t -> TMap(x -> x + 1,t),Cons(Branch(0,Nil),Nil)));
-    ==
-       Branch(2,Cons(TMap(x -> x + 1,Branch(0,Nil)),Nil));
-    ==
-       Branch(2,Cons(Branch((x -> x + 1)(0),Nil),Nil));
-    ==
-       Branch(2,Cons(Branch(1,Nil),Nil));
-  }
-
-  assert TMap(x -> x + 1, Branch(1,Cons(Branch(0,Nil),Nil)))
-      == Branch(2,Cons(Branch(1,Nil),Nil));
-}