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
|
(** {1 Polymorphic n-ary trees} *)
(** {2 Basic theory with polymorphic lists of children} *)
module Tree
use list.List
type forest 'a = list (tree 'a)
with tree 'a = Node 'a (forest 'a)
end
(** {2 Tree size} *)
module Size
use Tree
use list.List
use int.Int
let rec function size_forest (f: forest 'a) : int
ensures { result >= 0 }
= match f with
| Nil -> 0
| Cons t f -> size_tree t + size_forest f
end
with function size_tree (t: tree 'a) : int
ensures { result > 0 }
= match t with
| Node _ f -> 1 + size_forest f
end
end
(** {2 Forests} *)
module Forest
use int.Int
type forest 'a =
| E
| N 'a (forest 'a) (forest 'a)
end
(** {2 Forest size} *)
module SizeForest
use Forest
use int.Int
let rec function size_forest (f: forest 'a) : int
ensures { result >= 0 }
= match f with
| E -> 0
| N _ f1 f2 -> 1 + size_forest f1 + size_forest f2
end
end
(** {2 Membership in a forest} *)
module MemForest
use Forest
predicate mem_forest (n: 'a) (f: forest 'a) = match f with
| E -> false
| N i f1 f2 -> i = n || mem_forest n f1 || mem_forest n f2
end
end
|
