val balance (#a: eqtype) (#b: Type) (t: tree a b) : tree a b
let balance (#a:eqtype) (#b:Type) (t:tree a b) : tree a b =
  match t with
  | Node _ _ _ l r ->
    let hl = height l in
    let hr = height r in
    if hl >= hr + 2 then rotate_r t else
    if hr >= hl + 2 then rotate_l t else
    t
  | _ -> t
val balance (#a: eqtype) (#b: Type) (t: tree a b) : tree a b
let balance (#a: eqtype) (#b: Type) (t: tree a b) : tree a b =
match t with
| Node _ _ _ l r ->
  let hl = height l in
  let hr = height r in
  if hl >= hr + 2 then rotate_r t else if hr >= hl + 2 then rotate_l t else t
| _ -> t
Vale.Lib.MapTree.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Lib.MapTree.fst
Prims.eqtype Vale.Lib.MapTree.tree Prims.nat Prims.op_GreaterThanOrEqual Prims.op_Addition Vale.Lib.MapTree.rotate_r Prims.bool Vale.Lib.MapTree.rotate_l Vale.Lib.MapTree.height
module Vale.Lib.MapTree
open FStar.Mul

(** Balanced tree implementation *)

type tree (a:eqtype) (b:Type) =
  | Empty : tree a b
  | Node : a -> b -> nat -> tree a b -> tree a b -> tree a b

let height (#a:eqtype) (#b:Type) (t:tree a b) : nat =
  match t with
  | Empty -> 0
  | Node _ _ h _ _ -> h

let mkNode (#a:eqtype) (#b:Type) (key:a) (value:b) (l r:tree a b) : tree a b =
  let hl = height l in
  let hr = height r in
  let h = if hl > hr then hl else hr in
  Node key value (h + 1) l r

let rotate_l (#a:eqtype) (#b:Type) (t:tree a b) : tree a b =
  match t with
  | Node kl vl _ l (Node kr vr _ lr rr) -> mkNode kr vr (mkNode kl vl l lr) rr
  | _ -> t

let rotate_r (#a:eqtype) (#b:Type) (t:tree a b) : tree a b =
  match t with
  | Node kr vr _ (Node kl vl _ ll rl) r -> mkNode kl vl ll (mkNode kr vr rl r)
  | _ -> t
val balance (#a: eqtype) (#b: Type) (t: tree a b) : tree a b
t: Vale.Lib.MapTree.tree a b -> Vale.Lib.MapTree.tree a b