/* Map

Keys are integers and values may have an arbitrary type.
*/
module map

// TODO: write test

type skewnessck/map/skewness: V
  Lck/map/L: skewness
  Eck/map/E: skewness
  Rck/map/R: skewness

abstract type mapck/map/map: V -> V<bb: V>
  Empck/map/Emp: forall<a> map<a>
  Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>{ keykey: int: intstd/core/types/int: V; valuevalue: 7: bb: V; skewskew: skewness: skewnessck/map/skewness: V; leftleft: map<7>: mapck/map/map: V -> V<bb: V>; rightright: map<7>: mapck/map/map: V -> V<bb: V> }

fun showck/map/show: (s : skewness) -> string(ss: skewness: skewnessck/map/skewness: V): stringstd/core/types/string: V
  match ss: skewness
    Lck/map/L: skewness -> "L"
    Eck/map/E: skewness -> "E"
    Rck/map/R: skewness -> "R"

pub fun showck/map/show.1: forall<a> (t : map<a>, show' : (a) -> string) -> string(tt: map<$1504>: mapck/map/map: V -> V<bb: V>, show'show': ($1504) -> string: bb: V -> stringstd/core/types/string: V): stringstd/core/types/string: V
  match tt: map<$1504>
    Empck/map/Emp: forall<a> map<a> -> "Emp"
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(kk: int, vv: $1504, ss: skewness, ll: map<$1504>, rr: map<$1504>) ->
      "Bra(" ++std/core/(++).1: (x : string, y : string) -> string kk: int.showstd/core/show: (i : int) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string vv: $1504.show'show': ($1504) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string ss: skewness.showck/map/show: (s : skewness) -> string ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string ll: map<$1504>.showck/map/show.1: forall<a> (t : map<a>, show' : (a) -> string) -> string(show'show': ($1504) -> string) ++std/core/(++).1: (x : string, y : string) -> string ", " ++std/core/(++).1: (x : string, y : string) -> string rr: map<$1504>.showck/map/show.1: forall<a> (t : map<a>, show' : (a) -> string) -> string(show'show': ($1504) -> string) ++std/core/(++).1: (x : string, y : string) -> string ")"

// Check whether a map is empty
pub fun is-emptyck/map/is-empty: forall<a> (t : map<a>) -> bool(tt: map<$572>: mapck/map/map: V -> V<bb: V>): boolstd/core/types/bool: V
  match tt: map<$572>
    Empck/map/Emp: forall<a> map<a> -> Truestd/core/types/True: bool
    _ -> Falsestd/core/types/False: bool

// Create an empty map.
pub fun emptyck/map/empty: forall<a> () -> map<a>(): mapck/map/map: V -> V<bb: V>
  Empck/map/Emp: forall<a> map<a>

// 左の部分木が 2 だけ高くなっていたら修正する
// 要素の挿入の場合、この関数を呼び出すのは左の部分木に挿入したときだが、
// 要素の削除の場合、「右」の部分木から削除したときであり、逆になるので注意が必要
// 2番目の戻り値が True のとき、修正前後で木の高さは変わらない
fun adjust-lck/map/adjust-l: forall<a> (t : map<a>) -> (map<a>, bool)(tt: map<$166>: mapck/map/map: V -> V<bb: V>): (std/core/types/(,): (V, V) -> Vmapck/map/map: V -> V<bb: V>, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  match tt: map<$166>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Eck/map/E: skewness, ll: map<$166>, rr: map<$166>) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, ll: map<$166>, rr: map<$166>), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Rck/map/R: skewness, ll: map<$166>, rr: map<$166>) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Eck/map/E: skewness, ll: map<$166>, rr: map<$166>), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Lck/map/L: skewness, l'l': map<$166>, r'r': map<$166>), rr: map<$166>) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Eck/map/E: skewness, l'l': map<$166>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Eck/map/E: skewness, r'r': map<$166>, rr: map<$166>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Eck/map/E: skewness, l'l': map<$166>, r'r': map<$166>), rr: map<$166>) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Rck/map/R: skewness, l'l': map<$166>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, r'r': map<$166>, rr: map<$166>)), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Rck/map/R: skewness, l'l': map<$166>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Lck/map/L: skewness, l''l'': map<$166>, r''r'': map<$166>)), rr: map<$166>) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Eck/map/E: skewness, l'l': map<$166>, l''l'': map<$166>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Rck/map/R: skewness, r''r'': map<$166>, rr: map<$166>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Rck/map/R: skewness, l'l': map<$166>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Eck/map/E: skewness, l''l'': map<$166>, r''r'': map<$166>)), rr: map<$166>) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Eck/map/E: skewness, l'l': map<$166>, l''l'': map<$166>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Eck/map/E: skewness, r''r'': map<$166>, rr: map<$166>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Rck/map/R: skewness, l'l': map<$166>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Rck/map/R: skewness, l''l'': map<$166>, r''r'': map<$166>)), rr: map<$166>) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $166, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $166, Lck/map/L: skewness, l'l': map<$166>, l''l'': map<$166>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $166, Eck/map/E: skewness, r''r'': map<$166>, rr: map<$166>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    _ -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)tt: map<$166>, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

fun adjust-rck/map/adjust-r: forall<a> (t : map<a>) -> (map<a>, bool)(tt: map<$365>: mapck/map/map: V -> V<bb: V>): (std/core/types/(,): (V, V) -> Vmapck/map/map: V -> V<bb: V>, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  match tt: map<$365>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Lck/map/L: skewness, ll: map<$365>, rr: map<$365>) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Eck/map/E: skewness, ll: map<$365>, rr: map<$365>), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Eck/map/E: skewness, ll: map<$365>, rr: map<$365>) -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, rr: map<$365>), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Rck/map/R: skewness, l'l': map<$365>, r'r': map<$365>)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Eck/map/E: skewness, ll: map<$365>, l'l': map<$365>), r'r': map<$365>), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Eck/map/E: skewness, l'l': map<$365>, r'r': map<$365>)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, l'l': map<$365>), r'r': map<$365>), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Lck/map/L: skewness, l''l'': map<$365>, r''r'': map<$365>), r'r': map<$365>)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Eck/map/E: skewness, ll: map<$365>, l''l'': map<$365>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Rck/map/R: skewness, r''r'': map<$365>, r'r': map<$365>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Eck/map/E: skewness, l''l'': map<$365>, r''r'': map<$365>), r'r': map<$365>)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Eck/map/E: skewness, ll: map<$365>, l''l'': map<$365>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Eck/map/E: skewness, r''r'': map<$365>, r'r': map<$365>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Rck/map/R: skewness, ll: map<$365>, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Lck/map/L: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Rck/map/R: skewness, l''l'': map<$365>, r''r'': map<$365>), r'r': map<$365>)) ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(cc: int, zz: $365, Eck/map/E: skewness, Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $365, Lck/map/L: skewness, ll: map<$365>, l''l'': map<$365>), Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(bb: int, yy: $365, Eck/map/E: skewness, r''r'': map<$365>, r'r': map<$365>)), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    _ -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)tt: map<$365>, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) // for exhaustive check

// insert-intl(t, k, v) = (t', grown)
//    t' : t に (k, v) を挿入して得られる木
// grown : 高さが 1 増えたか
fun insert-intlck/map/insert-intl: forall<a> (t : map<a>, k : int, v : a) -> (map<a>, bool)(tt: map<$1239>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V, vv: $1239: bb: V): (std/core/types/(,): (V, V) -> Vmapck/map/map: V -> V<bb: V>, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  match tt: map<$1239>
    Empck/map/Emp: forall<a> map<a> -> (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(kk: int, vv: $1239, Eck/map/E: skewness, Empck/map/Emp: forall<a> map<a>, Empck/map/Emp: forall<a> map<a>), Truestd/core/types/True: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, _, ss: skewness, ll: map<$1239>, rr: map<$1239>) | kk: int ==std/core/(==).1: (x : int, y : int) -> bool aa: int ->
      (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, vv: $1239, ss: skewness, ll: map<$1239>, rr: map<$1239>), Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) // k がすでに存在するときは値を更新する
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $1239, ss: skewness, ll: map<$1239>, rr: map<$1239>) | kk: int <std/core/(<).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)l'l': map<$1239>, growngrown: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = ll: map<$1239>.insert-intlck/map/insert-intl: forall<a> (t : map<a>, k : int, v : a) -> (map<a>, bool)(kk: int, vv: $1239)
      val t't': map<$1239> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $1239, ss: skewness, l'l': map<$1239>, rr: map<$1239>)
      if !std/core/types/(!).1: (b : bool) -> boolgrowngrown: bool then returnreturn: (map<$1239>, bool) (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': map<$1239>, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      t't': map<$1239>.adjust-lck/map/adjust-l: forall<a> (t : map<a>) -> (map<a>, bool)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $1239, ss: skewness, ll: map<$1239>, rr: map<$1239>) ->
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)r'r': map<$1239>, growngrown: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = rr: map<$1239>.insert-intlck/map/insert-intl: forall<a> (t : map<a>, k : int, v : a) -> (map<a>, bool)(kk: int, vv: $1239)
      val t't': map<$1239> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $1239, ss: skewness, ll: map<$1239>, r'r': map<$1239>)
      if !std/core/types/(!).1: (b : bool) -> boolgrowngrown: bool then returnreturn: (map<$1239>, bool) (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': map<$1239>, Falsestd/core/types/False: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)
      t't': map<$1239>.adjust-rck/map/adjust-r: forall<a> (t : map<a>) -> (map<a>, bool)

// Add a key-value pair to a map.
// If the given key already exists, update the corresponding value
pub fun insertck/map/insert: forall<a> (t : map<a>, k : int, v : a) -> map<a>(tt: map<$1414>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V, vv: $1414: bb: V): mapck/map/map: V -> V<bb: V>
  tt: map<$1414>.insert-intlck/map/insert-intl: forall<a> (t : map<a>, k : int, v : a) -> (map<a>, bool)(kk: int, vv: $1414).fststd/core/types/fst: forall<a,b> ((a, b)) -> a

// Return the key-value pair of the smallest key in a map
pub fun min-bindingck/map/min-binding: forall<a> (t : map<a>) -> maybe<(int, a)>(tt: map<$617>: mapck/map/map: V -> V<bb: V>): maybestd/core/types/maybe: V -> V<(std/core/types/(,): (V, V) -> Vintstd/core/types/int: V, bb: V)std/core/types/(,): (V, V) -> V>
  match tt: map<$617>
    Empck/map/Emp: forall<a> map<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $617, _, Empck/map/Emp: forall<a> map<a>, _) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)aa: int, xx: $617)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b))
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(_, _, _, ll: map<$617>, _) -> ll: map<$617>.min-bindingck/map/min-binding: forall<a> (t : map<a>) -> maybe<(int, a)>

// Return the key-value pair of the largest key in a map
pub fun max-bindingck/map/max-binding: forall<a> (t : map<a>) -> maybe<(int, a)>(tt: map<$585>: mapck/map/map: V -> V<bb: V>): maybestd/core/types/maybe: V -> V<(std/core/types/(,): (V, V) -> Vintstd/core/types/int: V, bb: V)std/core/types/(,): (V, V) -> V>
  match tt: map<$585>
    Empck/map/Emp: forall<a> map<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $585, _, _, Empck/map/Emp: forall<a> map<a>) -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)aa: int, xx: $585)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b))
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(_, _, _, _, rr: map<$585>) -> rr: map<$585>.max-bindingck/map/max-binding: forall<a> (t : map<a>) -> maybe<(int, a)>

// erase-intl(t, k) = (t', deleted, shrinked)
//          t' : t から k をなくした木
//     deleted : k を削除したか (元からなければ False)
//    shrinked : 高さが 1 減ったか
fun erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(tt: map<$649>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V): (std/core/types/(,,): (V, V, V) -> Vmapck/map/map: V -> V<bb: V>, boolstd/core/types/bool: V, boolstd/core/types/bool: V)std/core/types/(,,): (V, V, V) -> V
  match tt: map<$649>
    Empck/map/Emp: forall<a> map<a> -> (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/map/Emp: forall<a> map<a>, Falsestd/core/types/False: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $649, ss: skewness, ll: map<$649>, rr: map<$649>) | kk: int <std/core/(<).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': map<$649>, deleteddeleted: bool, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: map<$649>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(kk: int)
      val t't': map<$649> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $649, ss: skewness, l'l': map<$649>, rr: map<$649>)
      if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': map<$649>, deleteddeleted: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': map<$649>, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': map<$649>.adjust-rck/map/adjust-r: forall<a> (t : map<a>) -> (map<a>, bool)
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': map<$649>, deleteddeleted: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $649, ss: skewness, ll: map<$649>, rr: map<$649>) | kk: int >std/core/(>).1: (x : int, y : int) -> bool aa: int ->
      val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': map<$649>, deleteddeleted: bool, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: map<$649>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(kk: int)
      val t't': map<$649> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $649, ss: skewness, ll: map<$649>, r'r': map<$649>)
      if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': map<$649>, deleteddeleted: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
      val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': map<$649>, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': map<$649>.adjust-lck/map/adjust-l: forall<a> (t : map<a>) -> (map<a>, bool)
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': map<$649>, deleteddeleted: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(_, _, ss: skewness, ll: map<$649>, rr: map<$649>) ->
      match rr: map<$649>.min-bindingck/map/min-binding: forall<a> (t : map<a>) -> maybe<(int, a)>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)mnkmnk: int, mnvmnv: $649)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)) ->
          val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)r'r': map<$649>, _, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = rr: map<$649>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(mnkmnk: int)
          val t't': map<$649> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(mnkmnk: int, mnvmnv: $649, ss: skewness, ll: map<$649>, r'r': map<$649>)
          if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': map<$649>, Truestd/core/types/True: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': map<$649>, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': map<$649>.adjust-lck/map/adjust-l: forall<a> (t : map<a>) -> (map<a>, bool)
          returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': map<$649>, Truestd/core/types/True: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/(): ())std/core/types/(): ()
      match ll: map<$649>.max-bindingck/map/max-binding: forall<a> (t : map<a>) -> maybe<(int, a)>
        Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>((std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)mxkmxk: int, mxvmxv: $649)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)) ->
          val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)l'l': map<$649>, _, shrinkedshrinked: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = ll: map<$649>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(mxkmxk: int)
          val t't': map<$649> = Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(mxkmxk: int, mxvmxv: $649, ss: skewness, l'l': map<$649>, rr: map<$649>)
          if !std/core/types/(!).1: (b : bool) -> boolshrinkedshrinked: bool then returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': map<$649>, Truestd/core/types/True: bool, Falsestd/core/types/False: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
          val (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t''t'': map<$649>, not-shrinked'not-shrinked': bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b) = t't': map<$649>.adjust-rck/map/adjust-r: forall<a> (t : map<a>) -> (map<a>, bool)
          returnreturn: (map<$649>, bool, bool) (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t''t'': map<$649>, Truestd/core/types/True: bool, !std/core/types/(!).1: (b : bool) -> boolnot-shrinked'not-shrinked': bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)
        _ -> (std/core/types/(): ())std/core/types/(): ()
      (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)Empck/map/Emp: forall<a> map<a>, Truestd/core/types/True: bool, Truestd/core/types/True: bool)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)

// Remove a key and the corresponding value from a map.
// Do nothing if the given key does not exist
pub fun eraseck/map/erase: forall<a> (t : map<a>, k : int) -> map<a>(tt: map<$1074>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V): mapck/map/map: V -> V<bb: V>
  tt: map<$1074>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(kk: int).fststd/core/types/fst.1: forall<a,b,c> ((a, b, c)) -> a

pub fun erase-with-statusck/map/erase-with-status: forall<a> (t : map<a>, k : int) -> (map<a>, bool)(tt: map<$1157>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V): (std/core/types/(,): (V, V) -> Vmapck/map/map: V -> V<bb: V>, boolstd/core/types/bool: V)std/core/types/(,): (V, V) -> V
  val (std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c)t't': map<$1157>, deleteddeleted: bool, _)std/core/types/(,,): forall<a,b,c> (fst : a, snd : b, thd : c) -> (a, b, c) = tt: map<$1157>.erase-intlck/map/erase-intl: forall<a> (t : map<a>, k : int) -> (map<a>, bool, bool)(kk: int)
  (std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)t't': map<$1157>, deleteddeleted: bool)std/core/types/(,): forall<a,b> (fst : a, snd : b) -> (a, b)

// Get the value of a specified key
pub fun getck/map/get: forall<a> (t : map<a>, k : int) -> maybe<a>(tt: map<$1180>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V): maybestd/core/types/maybe: V -> V<bb: V>
  match tt: map<$1180>
    Empck/map/Emp: forall<a> map<a> -> Nothingstd/core/types/Nothing: forall<a> maybe<a>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $1180, _, _, _) | kk: int ==std/core/(==).1: (x : int, y : int) -> bool aa: int -> Juststd/core/types/Just: forall<a> (value : a) -> maybe<a>(xx: $1180)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, _, _, ll: map<$1180>, _) | kk: int <std/core/(<).1: (x : int, y : int) -> bool aa: int -> ll: map<$1180>.getck/map/get: forall<a> (t : map<a>, k : int) -> maybe<a>(kk: int)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(_, _, _, _, rr: map<$1180>) -> rr: map<$1180>.getck/map/get: forall<a> (t : map<a>, k : int) -> maybe<a>(kk: int)

// Update the value of a specified key.
// Do nothing if the key does not exist
pub fun updateck/map/update: forall<a,e> (t : map<a>, k : int, f : (a) -> e a) -> e map<a>(tt: map<$2008>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V, ff: ($2008) -> $2009 $2008: bb: V -> ee: E bb: V): ee: E mapck/map/map: V -> V<bb: V>
  match tt: map<$2008>
    Empck/map/Emp: forall<a> map<a> -> Empck/map/Emp: forall<a> map<a>
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $2008, ss: skewness, ll: map<$2008>, rr: map<$2008>) | kk: int ==std/core/(==).1: (x : int, y : int) -> bool aa: int -> Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, ff: ($2008) -> $2009 $2008(xx: $2008), ss: skewness, ll: map<$2008>, rr: map<$2008>)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $2008, ss: skewness, ll: map<$2008>, rr: map<$2008>) | kk: int <std/core/(<).1: (x : int, y : int) -> bool aa: int -> Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $2008, ss: skewness, ll: map<$2008>.updateck/map/update: forall<a,e> (t : map<a>, k : int, f : (a) -> e a) -> e map<a>(kk: int, ff: ($2008) -> $2009 $2008), rr: map<$2008>)
    Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $2008, ss: skewness, ll: map<$2008>, rr: map<$2008>) -> Brack/map/Bra: forall<a> (key : int, value : a, skew : skewness, left : map<a>, right : map<a>) -> map<a>(aa: int, xx: $2008, ss: skewness, ll: map<$2008>, rr: map<$2008>.updateck/map/update: forall<a,e> (t : map<a>, k : int, f : (a) -> e a) -> e map<a>(kk: int, ff: ($2008) -> $2009 $2008))

pub fun update-or-insertck/map/update-or-insert: forall<a,e> (t : map<a>, k : int, f : (a) -> e a, v : a) -> e map<a>(tt: map<$2091>: mapck/map/map: V -> V<bb: V>, kk: int: intstd/core/types/int: V, ff: ($2091) -> $2092 $2091: bb: V -> ee: E bb: V, vv: $2091: bb: V): ee: E mapck/map/map: V -> V<bb: V>
  if tt: map<$2091>.getck/map/get: forall<a> (t : map<a>, k : int) -> maybe<a>(kk: int).is-juststd/core/types/is-just: forall<a> (maybe : maybe<a>) -> bool then
    tt: map<$2091>.updateck/map/update: forall<a,e> (t : map<a>, k : int, f : (a) -> e a) -> e map<a>(kk: int, ff: ($2091) -> $2092 $2091)
  else
    tt: map<$2091>.insertck/map/insert: forall<a> (t : map<a>, k : int, v : a) -> map<a>(kk: int, vv: $2091)