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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// ------------------ generic list, non-generic tree
datatype List<T> = Nil | Cons(T, List<T>)
datatype Tree = Node(int, List<Tree>)
function Inc(t: Tree): Tree
{
match t
case Node(n, children) => Tree.Node(n+1, ForestInc(children))
}
function ForestInc(forest: List<Tree>): List<Tree>
{
match forest
case Nil => forest
case Cons(tree, tail) => List.Cons(Inc(tree), ForestInc(tail))
}
// ------------------ generic list, generic tree (but GInc defined only for GTree<int>
datatype GTree<T> = Node(T, List<GTree<T>>)
function GInc(t: GTree<int>): GTree<int>
{
match t
case Node(n, children) => GTree.Node(n+1, GForestInc(children))
}
function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
{
match forest
case Nil => forest
case Cons(tree, tail) => List.Cons(GInc(tree), GForestInc(tail))
}
// ------------------ non-generic structures
datatype TreeList = Nil | Cons(OneTree, TreeList)
datatype OneTree = Node(int, TreeList)
function XInc(t: OneTree): OneTree
{
match t
case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
}
function XForestInc(forest: TreeList): TreeList
{
match forest
case Nil => forest
case Cons(tree, tail) => TreeList.Cons(XInc(tree), XForestInc(tail))
}
// ------------------ fun with recursive functions
function len<T>(l: List<T>): int
{
match l
case Nil => 0
case Cons(h,t) => 1 + len(t)
}
function SingletonList<T>(h: T): List<T>
ensures len(SingletonList(h)) == 1;
{
List.Cons(h, List.Nil)
}
function Append<T>(a: List<T>, b: List<T>): List<T>
ensures len(Append(a,b)) == len(a) + len(b);
{
match a
case Nil => b
case Cons(h,t) => List.Cons(h, Append(t, b))
}
function Rotate<T>(n: int, l: List<T>): List<T>
requires 0 <= n;
ensures len(Rotate(n, l)) == len(l);
{
match l
case Nil => l
case Cons(h, t) =>
if n == 0 then l else
Rotate(n-1, Append(t, SingletonList(h)))
}
|
