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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
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);
{
}
|
