val put (#a: eqtype) (#b: Type) (is_le: (a -> a -> bool)) (t: tree a b) (key: a) (value: b)
    : tree a b
let rec put (#a:eqtype) (#b:Type) (is_le:a -> a -> bool) (t:tree a b) (key:a) (value:b) : tree a b =
  match t with
  | Empty -> mkNode key value Empty Empty
  | Node k v _ l r ->
    if key = k then mkNode k value l r
    else if is_le key k then
      balance (mkNode k v (put is_le l key value) r)
    else
      balance (mkNode k v l (put is_le r key value))
val put (#a: eqtype) (#b: Type) (is_le: (a -> a -> bool)) (t: tree a b) (key: a) (value: b)
    : tree a b
let rec put (#a: eqtype) (#b: Type) (is_le: (a -> a -> bool)) (t: tree a b) (key: a) (value: b)
    : tree a b =
match t with
| Empty -> mkNode key value Empty Empty
| Node k v _ l r ->
  if key = k
  then mkNode k value l r
  else
    if is_le key k
    then balance (mkNode k v (put is_le l key value) r)
    else balance (mkNode k v l (put is_le r key value))
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 Prims.bool Vale.Lib.MapTree.tree Vale.Lib.MapTree.mkNode Vale.Lib.MapTree.Empty Prims.nat Prims.op_Equality Vale.Lib.MapTree.balance Vale.Lib.MapTree.put
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

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

let rec get (#a:eqtype) (#b:Type) (is_le:a -> a -> bool) (t:tree a b) (key:a) : option b =
  match t with
  | Empty -> None
  | Node k v h l r ->
    if key = k then Some v
    else if is_le key k then
      get is_le l key
    else
      get is_le r key
val put (#a: eqtype) (#b: Type) (is_le: (a -> a -> bool)) (t: tree a b) (key: a) (value: b)
    : tree a b
is_le: (_: a -> _: a -> Prims.bool) -> t: Vale.Lib.MapTree.tree a b -> key: a -> value: b
  -> Vale.Lib.MapTree.tree a b