(* some simple stuff related to trees *) datatype 'a tree = Leaf | Branch of 'a * 'a tree * 'a tree typeref 'a tree of nat * nat with Leaf <| 'a tree(0,0) | Branch <| {sl:nat, hl:nat, sr:nat, hr:nat} 'a * 'a tree(sl,hl) * 'a tree(sr,hr) -> 'a tree(1+sl+sr, 1+max(hl, hr)) fun('a) size Leaf = 0 | size (Branch(v,t1,t2)) = 1 + size t1 + size t2 where size <| {s:nat, h:nat} 'a tree(s,h) -> int(s) fun('a) depth Leaf = 0 | depth (Branch(v,t1,t2)) = 1 + max(depth t1, depth t2) where depth <| {s:nat, h:nat} 'a tree(s,h) -> int(h) fun('a) reflect Leaf = Leaf | reflect (Branch(v,t1,t2)) = Branch(v, reflect t2, reflect t1) where reflect <| {s:nat, h:nat} 'a tree(s,h) -> 'a tree(s,h) fun('a) preord (Leaf, vs) = vs | preord (Branch(v,t1,t2), vs) = v :: preord (t1, preord (t2, vs)) where preord <| {s:nat,h:nat,t:nat} 'a tree(s,h) * 'a list(t) -> 'a list(s+t) fun('a) inord (Leaf, vs) = vs | inord (Branch(v,t1,t2), vs) = inord (t1, v::inord (t2, vs)) where inord <| {s:nat,h:nat,t:nat} 'a tree(s,h) * 'a list(t) -> 'a list(s+t) fun('a) postord (Leaf, vs) = vs | postord (Branch(v,t1,t2), vs) = postord (t1, postord (t2, v::vs)) where postord <| {s:nat,h:nat,t:nat} 'a tree(s,h) * 'a list(t) -> 'a list(s+t) fun('a) balpre(nil) = Leaf | balpre(x::xs) = let val k = listLength(xs) div 2 in Branch(x, balpre(listTake(xs,k)), balpre(listDrop(xs,k))) end where balpre <| {n:nat} 'a list(n) -> [h:nat] 'a tree(n,h) fun('a) balin [] = Leaf | balin xs = let val k = listLength(xs) div 2 val y::ys = listDrop(xs,k) in Branch(y, balin(listTake(xs,k)), balin ys) end where balin <| {n:nat} 'a list(n) -> [h:nat] 'a tree(n,h) fun('a) balpost xs = reflect (balpre (rev xs)) where balpost <| {n:nat} 'a list(n) -> [h:nat] 'a tree(n,h)