summaryrefslogtreecommitdiff
path: root/Test/hofs/Fold.dfy
blob: 9bcd9e02589c73bfb68a360f108c1c9754c6a8a6 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

datatype List<A> = Nil | Cons(A,List<A>)

datatype Expr = Add(List<Expr>) | Mul(List<Expr>) | Lit(int)

function method Eval(e : Expr): int
{
  match e
    case Add(es) => Fold(es,0,(e,v) requires e < es => Eval(e) + v)
    case Mul(es) => Fold(es,1,(e,v) requires e < es => Eval(e) * v)
    case Lit(i)  => i
}

function method Fold<A,B>(xs : List<A>, unit : B, f : (A,B) -> B): B
  reads f.reads;
  requires forall x, y :: x < xs ==> f.requires(x,y);
{
  match xs
    case Nil => unit
    case Cons(x,xs) => f(x,Fold(xs,unit,f))
}

method Main() {
  var two := Lit(2);
  var add := (x,y) => Add(Cons(x,Cons(y,Nil)));
  assert Eval(add(two,two)) == 4;
  print "3 = ", Eval(add(Lit(1),two)), "\n";
}