(* This code extends 'mini_prelude'. *) val empty = Nil ; val is_empty = (fn v3 => (case v3 of Nil => true | (Cons (v2, v1)) => false)) ; datatype ('a) tree = Node of int * ('a) tree * ('a) tree | Leaf of 'a ; val size = (fn v5 => (case v5 of (Leaf (v1)) => 1 | (Node (v4, v3, v2)) => v4)) ; val link = (fn v1 => (fn v2 => (Node (((size v1) + (size v2)), v1, v2)))) ; datatype ('a) digit = One of ('a) tree | Zero ; fun cons_tree v4 = (fn v5 => (case v5 of Nil => (Cons ((One (v4)), Nil)) | (Cons (v3, v2)) => (case v3 of Zero => (Cons ((One (v4)), v2)) | (One (v1)) => (Cons (Zero, ((cons_tree ((link v4) v1)) v2)))))) ; fun uncons_tree x = (case x of Nil => (raise Bind) | (Cons (v11, v10)) => (case v11 of Zero => (case (uncons_tree v10) of (Pair (v6, v5)) => (case v6 of (Leaf (v1)) => (raise Bind) | (Node (v4, v3, v2)) => (Pair (v3, (Cons ((One (v2)), v5)))))) | (One (v9)) => (case v10 of Nil => (Pair (v9, Nil)) | (Cons (v8, v7)) => (Pair (v9, (Cons (Zero, (Cons (v8, v7))))))))) ; val cons = (fn v2 => (fn v1 => ((cons_tree (Leaf (v2))) v1))) ; val head = (fn v7 => (case (uncons_tree v7) of (Pair (v6, v5)) => (case v6 of (Leaf (v1)) => v1 | (Node (v4, v3, v2)) => (raise Bind)))) ; val tail = (fn v4 => let val v3 = (uncons_tree v4) in (case v3 of (Pair (v2, v1)) => v1) end ) ; fun lookup_tree x1 = (fn x2 => (case x2 of (Leaf (v1)) => (if (x1 <= 0) then v1 else (raise Bind)) | (Node (v4, v3, v2)) => (if (x1 < (v4 div 2)) then ((lookup_tree x1) v3) else ((lookup_tree let val k = (x1 - (v4 div 2)) in (if (k < 0) then 0 else k) end ) v2)))) ; fun update_tree x1 = (fn x2 => (fn x3 => (case x3 of (Leaf (v1)) => (if (x1 <= 0) then (Leaf (x2)) else (raise Bind)) | (Node (v4, v3, v2)) => (if (x1 < (v4 div 2)) then (Node (v4, (((update_tree x1) x2) v3), v2)) else (Node (v4, v3, (((update_tree let val k = (x1 - (v4 div 2)) in (if (k < 0) then 0 else k) end ) x2) v2))))))) ; fun lookup x = (fn x1 => (case x1 of Nil => (raise Bind) | (Cons (v3, v2)) => (case v3 of Zero => ((lookup x) v2) | (One (v1)) => (if (x < (size v1)) then ((lookup_tree x) v1) else ((lookup let val k = (x - (size v1)) in (if (k < 0) then 0 else k) end ) v2))))) ; fun update x = (fn x1 => (fn x2 => (case x2 of Nil => (raise Bind) | (Cons (v3, v2)) => (case v3 of Zero => (Cons (Zero, (((update x) x1) v2))) | (One (v1)) => (if (x < (size v1)) then (Cons ((One ((((update_tree x) x1) v1))), v2)) else (Cons ((One (v1)), (((update let val k = (x - (size v1)) in (if (k < 0) then 0 else k) end ) x1) v2)))))))) ;