(COMMENT from Gluck and Kawabe's paper)
(COMMENT
The function treelist encodes the structure of a binary tree as a
list of binary numbers where each number indicates the number of
nodes in the left subtree of a branch. An example of binary trees
is (bin (bin (leaf) (bin (leaf) (leaf))) (leaf)) which represents
the following binary tree:
B
/ \
B L
/ \
L B
/ \
L L
)
(COMMENT
fun inc [] = [0]
| inc (0::xs) = 1 :: xs
| inc (1::xs) = 0 :: inc xs;
datatype Tree = Leaf | Bin of Tree * Tree;
fun appendn ([], ys) = ([], ys)
| appendn (x::xs, ys) =
let
val (n,zs) = appendn (xs,ys)
in
(inc n, x::zs)
end;
fun treelist Leaf = [[]]
| treelist (Bin(t1,t2)) =
let
val (n,rs) = appendn (treelist(t1), treelist(t2))
in
n :: rs
end;
)
(VAR t1 t2 u1 u2 n rs y x1 xs z)
(RULES
treelist(leaf) -> cons(nil,nil)
treelist(bin(t1,t2)) -> cons(n,rs)
| treelist(t1) -> u1,
treelist(t2) -> u2,
appendn(u1,u2) -> tuple2(n,rs)
appendn(nil,y) -> tuple2(nil,y)
appendn(cons(x1,xs),y) -> tuple2(inc(n),cons(x1,z))
| appendn(xs,y) -> tuple2(n,z)
inc(nil) -> cons(0,nil)
inc(cons(0,xs)) -> cons(1,xs)
inc(cons(1,xs)) -> cons(0,inc(xs))
)