summaryrefslogtreecommitdiff
path: root/Test/hofs/TreeMapSimple.dfy
blob: a853b82c251eeb97819f81938b5313e40ec51ca0 (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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
// RUN: %dafny /compile:3 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

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

datatype Tree<A> = Branch(val: A,trees: List<Tree<A>>)

function ListData(xs : List) : set
  ensures forall x :: x in ListData(xs) ==> x < xs;
{
  match xs
    case Nil => {}
    case Cons(x,xs) => {x} + ListData(xs)
}

function TreeData(t0 : Tree) : set
  ensures forall t :: t in TreeData(t0) ==> t < t0;
{
  var Branch(x,ts) := t0;
  {x} + set t, y | t in ListData(ts) && y in TreeData(t) :: y
}

function Pre(f : A -> B, s : set<A>) : bool
  reads (set x, y | x in s && y in f.reads(x) :: y);
{
  forall x :: x in s ==> f.reads(x) == {} && f.requires(x)
}

function method Map(xs : List<A>, f : A -> B): List<B>
  reads Pre.reads(f, ListData(xs));
  requires Pre(f, ListData(xs));
  decreases xs;
{
  match xs
    case Nil => Nil
    case Cons(x,xs) => Cons(f(x),Map(xs,f))
}

function method TMap(t0 : Tree<A>, f : A -> B) : Tree<B>
  reads Pre.reads(f, TreeData(t0));
  requires Pre(f, TreeData(t0));
  decreases t0;
{
  var Branch(x,ts) := t0;
  Branch(f(x),Map(ts, t  requires t in ListData(ts)
                         requires Pre(f, TreeData(t))
                      => TMap(t,f)))
}

method Main()
{
  var t := TMap(Branch(1,Cons(Branch(2,Nil),Nil)), x requires x != 0 => 100 / x);
  assert t   == Branch(100,Cons(Branch(50,Nil),Nil));
  print t, "\n";
}