(*
  ``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