type 'a tree =

    Empty : 'a tree

  | Tree : 'a tree * 'a * 'a tree -> 'a tree

let rec depth : 'a.'a tree -> int = function

    Empty -> 0

  | Tree (l,_,r) -> 1 + max (depth l) (depth r)

let top : 'a.'a tree -> 'a option = function

    Empty -> None

  | Tree (_,v,_) -> Some v

let rec swivel : 'a.'a tree -> 'a tree = function

    Empty -> Empty

  | Tree (l,v,r) -> Tree (swivel r, v, swivel l)

type 'a perfect =

    ZeroP : 'a -> 'a perfect

  | SuccP : ('a * 'a) perfect -> 'a perfect

type _ ntree =

    EmptyN : 'a ntree

  | TreeN : 'a * ('a * 'a) ntree -> 'a ntree

let rec depthN : 'a.'a ntree -> int = function

    EmptyN -> 0

  | TreeN (_,t) -> 1 + depthN t

let rec topN : 'a.'a ntree -> 'a option = function

    EmptyN -> None

  | TreeN (v,_) -> Some v

let rec swiv : 'a.('a->'a) -> 'a ntree -> 'a ntree =

  fun f t -> match t with

      EmptyN -> EmptyN

    | TreeN (v,t) -> 

      TreeN (f v,swiv (fun (x,y) -> (f y, f x)) t)

let id x = x

let swivelN p = swiv id p

type z = Z

type _ s = S : 'n -> 'n s

type ('a, _) gtree =

    EmptyG : ('a,z) gtree

  | TreeG : ('a,'n) gtree * 'a * ('a,'n) gtree -> ('a,'n s) gtree

let rec depthG : type a n.(a, n) gtree -> n = function

    EmptyG -> Z

  | TreeG (l,_,_) -> S (depthG l)

let topG : type a n.(a,n s) gtree -> a =

  function TreeG (_,v,_) -> v

let rec swivelG : type a n.(a,n) gtree -> (a,n) gtree = function

    EmptyG -> EmptyG

  | TreeG (l,v,r) -> TreeG (swivelG r, v, swivelG l)

let rec zipTree :

  type a n.(a,n) gtree -> (a,n) gtree -> (a * a,n) gtree =

  fun x y -> match x, y with

      EmptyG, EmptyG -> EmptyG

    | TreeG (l,v,r), TreeG (m,w,s) ->

      TreeG (zipTree l m, (v,w), zipTree r s)

let rec nestify : type a n.(a,n) gtree -> a ntree = function

    EmptyG -> EmptyN

  | TreeG (l, v, r) -> 

    TreeN (v, nestify (zipTree l r))

type (_,_) eql = Refl : ('a,'a) eql

type (_,_,_) max =

    MaxEq : ('a,'b) eql -> ('a,'b,'a) max

  | MaxFlip : ('a,'b,'c) max -> ('b,'a,'c) max

  | MaxSuc : ('a,'b,'a) max -> ('a s,'b,'a s) max

type ('a,_) dtree =

    EmptyD : ('a,z) dtree

  | TreeD : ('a,'m) dtree * 'a * ('a,'n) dtree * ('m,'n,'o) max 

    -> ('a,'o s) dtree

let rec max : type a b c.(a,b,c) max -> a -> b -> c

  = fun mx m n -> match mx,m with

      MaxEq Refl , _    -> m

    | MaxFlip mx', _    -> max mx' n m

    | MaxSuc mx' , S m' -> S (max mx' m' n)

let rec depthD : type a n.(a,n) dtree -> n = function

    EmptyD -> Z

  | TreeD (l,_,r,mx) -> S (max mx (depthD l) (depthD r))

let topD : type a n.(a,n s) dtree -> a =

  function TreeD (_,v,_,_) -> v

let rec swivelD :

  type a n.(a,n) dtree -> (a,n) dtree = function

    EmptyD -> EmptyD

  | TreeD (l,v,r,m) ->

    TreeD (swivelD r, v, swivelD l, MaxFlip m)