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
|
// RUN: %dafny /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function Apply(f: A -> B, x: A): B
reads f.reads(x);
requires f.requires(x);
{
f(x)
}
function Apply'(f: A -> B) : A -> B
{
x reads f.reads(x)
requires f.requires(x)
=> f(x)
}
function Compose(f: B -> C, g:A -> B): A -> C
{
x reads g.reads(x)
reads if g.requires(x) then f.reads(g(x)) else {}
requires g.requires(x)
requires f.requires(g(x))
=> f(g(x))
}
function W(f : (A,A) -> A): A -> A
{
x requires f.requires(x,x)
reads f.reads(x,x)
=> f(x,x)
}
function Curry(f : (A,B) -> C) : A -> B -> C
{
x => y requires f.requires(x,y)
reads f.reads(x,y)
=> f(x,y)
}
function Uncurry(f : A -> B -> C) : (A,B) -> C
{
(x,y) requires f.requires(x)
requires f(x).requires(y)
reads f.reads(x)
reads if f.requires(x) then f(x).reads(y) else {}
=> f(x)(y)
}
function S(f : (A,B) -> C, g : A -> B): A -> C
{
x requires g.requires(x)
requires f.requires(x,g(x))
reads g.reads(x)
reads if g.requires(x) then f.reads(x,g(x)) else {}
=> f(x,g(x))
}
|
