module btree.

kind btree    type.
type root     btree.
type bt       int -> btree -> btree -> btree.

type insert   int -> btree -> btree -> o.
type lookup   int -> btree -> o.

insert X root (bt X root root).
insert X (bt D L R) (bt D NewL R) :- X =< D, insert X L NewL.
insert X (bt D L R) (bt D L NewR) :- X > D,  insert X R NewR.

lookup X (bt X L R).
lookup X (bt D L R) :- X =< D, lookup X L.
lookup X (bt D L R) :- X > D,  lookup X R.

kind dlist    type -> type.
type minus    list A -> list A -> dlist A.
infix minus   5.

type concat    dlist A -> dlist A -> dlist A -> o.
type build     list A -> btree -> o.
type traverse  btree ->  dlist int -> o.
type tsort     list int -> list int -> o.

concat (L1 minus L2) (L2 minus L3) (L1 minus L3).

build nil root.
build (X::L) T1 :- build L T2, insert X T2 T1.

tsort List1 List2 :-
  build List1 T, traverse T (List2 minus nil).

traverse root (L minus L).
traverse (bt D L R) (L1 minus L3) :- 
   traverse L (L1 minus (D::L2)),
   traverse R (L2 minus L3).