mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
102 lines
2.4 KiB
Plaintext
102 lines
2.4 KiB
Plaintext
|
|
(*
|
|
``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
|