(* let test1 k = if eq_int 0 (k + k) then 0 else if ge_int (k + k) 2 then 0 else 1 withtype {k:nat} int(k) -> int(0) ;; let test2 k = if eq_int k 0 then 0 else if eq_int (k mod 2) 0 then if lt_int k 2 then 1 else 0 else 0 withtype {k:nat} int(k) -> int(0) ;; *) datatype 'a brauntree with nat = (* height and size *) L(0) | {m:nat}{n:nat | n <= m <= n+1} B(m+n+1) of 'a * 'a brauntree(m) * 'a brauntree(n) ;; let rec size = function L -> 0 | B(_, l, r) -> 1 + size(l) + size(r) withtype {n:nat} 'a brauntree(n) -> int(n) ;; exception Illegal_argument ;; let make_brauntree x l r = let m = size l and n = size r in if le_int n m && le_int m (n+1) then B(x, l, r) else raise Illegal_argument withtype 'a -> 'a brauntree -> 'a brauntree -> 'a brauntree ;; let rec diff k = function L -> 0 | B(_, l, r) -> if eq_int k 0 then 1 else if eq_int (k mod 2) 1 then diff (k/2) l else diff (k/2 - 1) r withtype {k:nat}{n:nat | k <= n <= k+1} int(k) -> 'a brauntree(n) -> int(n-k) ;; let rec size = function L -> 0 | B(_, l, r) -> let n = size r in 1 + n + n + diff n l withtype {n:nat} 'a brauntree(n) -> int(n) ;; let rec copy2 x k = if eq_int k 0 then (B(x, L, L), L) else let (s, t) = copy2 x ((k - 1) / 2) in if eq_int (k mod 2) 0 then (B(x, s, s), B(x, s, t)) else (B(x, s, t), B(x, t, t)) withtype {k:nat} 'a -> int(k) -> 'a brauntree(k+1) * 'a brauntree(k) ;; let copy x k = let (_, t) = copy2 x k in t withtype {k:nat} 'a -> int(k) -> 'a brauntree(k) ;; let make_brauntree x l r = let m = size(l) and n = size(r) in if le_int n m && lt_int m (n+1) then B(x, l, r) else raise Illegal_argument withtype 'a -> 'a brauntree -> 'a brauntree -> 'a brauntree ;; (* sort sb == {a:int | 0 <= a <= 1 } ;; datatype 'a braunlist with (sb, nat) = {m:nat} Bnil(0,m) | {b:sb}{m:nat}{n:nat | n <= m <= n+1-b} Bcons(m-n+b,m) of 'a brauntree(m) * 'a braunlist(b, n) ;; exception Split_empty ;; let rec split k = function Bnil -> (Bnil, Bnil) | Bcons(t, ts') as ts -> if k = 0 then (Bnil, ts) else let (ts1, ts2) = split (k-1) ts' in (Bcons(t, ts1), ts2) withtype {b:sb}{m:nat} int -> 'a braunlist(b, m) -> [b1:sb][b2:sb][n:nat | n <= m /\ b1+b2+m-n<=1] ('a braunlist(b1, m) * 'a braunlist(b2, n)) ;; let rec mk_braunlist xs ts1 ts2 = match (xs, ts1, ts2) with (x :: xs, Bcons(t1, ts1), Bcons(t2, ts2)) -> Bcons(B(x, t1, t2), mk_braunlist xs ts1 ts2) | ([], _, _) -> Bnil withtype {b1:sb}{b2:sb}{n1:nat}{n2:nat | n2+b1 <= n1 /\ b1+b2+n1-n2 <= 1} 'a list -> 'a braunlist(b1, n1) -> 'a braunlist(b2, n2) -> [b:sb][n:nat | n <= n1+n2+1 <= n+1] 'a braunlist(b, n) ;; *)