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
|
(*
``Same fringe'' is a famous problem.
Given two binary search trees, you must decide whether they contain the
same elements. See for instance http://www.c2.com/cgi/wiki?SameFringeProblem
*)
module SameFringe
use int.Int
use list.List
use list.Length
use list.Append
(* binary trees with elements at the nodes *)
type elt
val eq (x y: elt) : bool ensures { result <-> x=y }
type tree =
| Empty
| Node tree elt tree
function elements (t : tree) : list elt = match t with
| Empty -> Nil
| Node l x r -> elements l ++ Cons x (elements r)
end
(* the left spine of a tree, as a bottom-up list *)
type enum =
| Done
| Next elt tree enum
function enum_elements (e : enum) : list elt = match e with
| Done -> Nil
| Next x r e -> Cons x (elements r ++ enum_elements e)
end
(* the enum of a tree [t], prepended to a given enum [e] *)
let rec enum t e variant { t }
ensures { enum_elements result = elements t ++ enum_elements e }
= match t with
| Empty -> e
| Node l x r -> enum l (Next x r e)
end
let rec eq_enum e1 e2 variant { length (enum_elements e1) }
ensures { result=True <-> enum_elements e1 = enum_elements e2 }
= match e1, e2 with
| Done, Done ->
True
| Next x1 r1 e1, Next x2 r2 e2 ->
eq x1 x2 && eq_enum (enum r1 e1) (enum r2 e2)
| _ ->
False
end
let same_fringe t1 t2
ensures { result=True <-> elements t1 = elements t2 }
= eq_enum (enum t1 Done) (enum t2 Done)
let test1 () = enum Empty Done
let test2 () = eq_enum Done Done
let test3 () = same_fringe Empty Empty
val constant a : elt
val constant b : elt
let leaf x = Node Empty x Empty
let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))
exception BenchFailure
let bench () raises { BenchFailure -> true } =
if not (test4 ()) then raise BenchFailure
end
module Test
use int.Int
clone SameFringe with type elt = int
let test1 () = enum Empty Done
let test2 () = eq_enum Done Done
let test3 () = same_fringe Empty Empty
constant a : int = 1
constant b : int = 2
let leaf x = Node Empty x Empty
let test4 () = same_fringe (Node (leaf a) b Empty) (Node Empty a (leaf b))
let test5 () = same_fringe (Node (leaf a) b Empty) (Node Empty b (leaf a))
end
|
