blob: b01ec0533f8cc078340ab124b19bc938bac48f97 (
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
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
|
(* Examples which use divDefLib.DefineDiv *)
open HolKernel
open divDefLib
val _ = new_theory "divDefLibTest"
(* nth *)
Datatype:
list_t =
ListCons 't list_t
| ListNil
End
(* A version of [nth] which doesn't use machine integers *)
val [nth0_def] = DefineDiv ‘
nth0 (ls : 't list_t) (i : int) : 't result =
case ls of
| ListCons x tl =>
if i = (0:int)
then (Return x)
else
do
nth0 tl (i - 1)
od
| ListNil => Fail Failure
’
val _ = primitivesLib.assert_return “nth0 (ListCons 0 ListNil) 0”
val [nth_def] = DefineDiv ‘
nth (ls : 't list_t) (i : u32) : 't result =
case ls of
| ListCons x tl =>
if u32_to_int i = (0:int)
then (Return x)
else
do
i0 <- u32_sub i (int_to_u32 1);
nth tl i0
od
| ListNil => Fail Failure
’
val _ = primitivesLib.assert_return “nth (ListCons 0 ListNil) (int_to_u32 0)”
(* even, odd *)
val [even_def, odd_def] = DefineDiv ‘
(even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\
(odd (i : int) : bool result = if i = 0 then Return F else even (i - 1))
’
(* btree *)
Datatype:
btree =
BLeaf 'a
| BNode btree btree
End
val [btree_height_def] = DefineDiv ‘
btree_height (tree : 'a btree) : int result =
case tree of
| BLeaf _ => Return 1
| BNode l r =>
do
hl <- btree_height l;
hr <- btree_height r;
Return (hl + hr)
od
’
(* tree 2 *)
Datatype:
tree =
TLeaf 'a
| TNode node ;
node =
Node (tree list)
End
val [tree_height_def, tree_nodes_height_def] = DefineDiv ‘
(tree_height (tree : 'a tree) : int result =
case tree of
TLeaf _ => Return 1
| TNode n =>
case n of Node ls => tree_nodes_height ls) ∧
(tree_nodes_height (ls : ('a tree) list) : int result =
case ls of
[] => Return 0
| t :: tl =>
do
h1 <- tree_height t;
h2 <- tree_nodes_height tl;
Return (h1 + h2)
od)
’
val _ = export_theory ()
|
