(COMMENT from Gluck and Kawabe's paper)
(COMMENT
Given a binary tree, the function treepaths outputs a list of paths
to each leaf. A path from the root to a leaf is a list of 0's and
1's that indicate which branch to choose at each internal node where
0 refers to the left subtree and 1 to the right subtree. A binary
tree consists of internal nodes B(l,r) and leaves L.
)
(COMMENT
datatype Tree = Leaf | Bin of Tree * Tree;
fun paths Leaf p ps = p :: ps
| paths (Bin(l,r)) p ps = paths l (0 :: p) (paths r (1 :: p) ps);
fun treepath t = paths t [] [];
)
(VAR x y t p ps l r c1 c2)
(RULES
treepaths(t) -> paths(t,nil,nil)
paths(leaf,p,ps) -> cons(p,ps)
paths(bin(l,r),p,ps) -> paths(l,cons(0,p),paths(r,cons(1,p),ps))
)