Merge pull request #8 from imaqtkatt/refactor-book

Refactor book

book/BBT.kind2

@@ -1,15 +1,19 @@
-BBT
-: ∀(K: *) ∀(V: *) *
-= λK λV
-  $(self: (BBT K V))
-  ∀(P: ∀(bbt: (BBT K V)) *)
-  ∀(bin: 
-    ∀(size: U60)
-    ∀(key: K)
-    ∀(val: V)
-    ∀(lft: (BBT K V))
-    ∀(rgt: (BBT K V))
-    (P (BBT.bin K V size key val lft rgt))
-  )
-  ∀(tip: (P (BBT.tip K V)))
-  (P self)
+//BBT
+//: ∀(K: *) ∀(V: *) *
+//= λK λV
+  //$(self: (BBT K V))
+  //∀(P: ∀(bbt: (BBT K V)) *)
+  //∀(bin:
+    //∀(size: U60)
+    //∀(key: K)
+    //∀(val: V)
+    //∀(lft: (BBT K V))
+    //∀(rgt: (BBT K V))
+    //(P (BBT.bin K V size key val lft rgt))
+  //)
+  //∀(tip: (P (BBT.tip K V)))
+  //(P self)
+
+data BBT K V
+| bin (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V))
+| tip

book/BBT/balance.kind2

@@ -1,66 +1,97 @@
-BBT.balance
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(set_key: K)
-  ∀(node_key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λcmp λset_key λnode_key λval λlft λrgt
-  use P = λx (BBT K V)
-  use new = λlft.size λlft
-    use P = λx (BBT K V)
-    use new = λrgt.size λrgt
-      use new_size = (+ 1 (U60.max lft.size rgt.size))
-      use balance = (U60.abs_diff lft.size rgt.size)
-      use P = λx
-        ∀(new_size: U60)
-        ∀(node_key: K)
-        ∀(val: V)
-        ∀(lft: (BBT K V))
-        ∀(rgt: (BBT K V))
-        (BBT K V)
-      use true = λnew_size λnode_key λval λlft λrgt
-        use P = λx
-          ∀(K: *)
-          ∀(V: *)
-          ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-          ∀(new_size: U60)
-          ∀(node_key: K)
-          ∀(set_key: K)
-          ∀(val: V)
-          ∀(lft: (BBT K V))
-          ∀(rgt: (BBT K V))
-          (BBT K V)
-        use true = BBT.balance.lft_heavier
-        use false = BBT.balance.rgt_heavier
-        (~(U60.to_bool (< rgt.size lft.size))
-          P
-          true
-          false
-          K
-          V
-          cmp
-          new_size
-          node_key
-          set_key
-          val
-          lft
-          rgt
-        )
-      use false = λnew_size λnode_key λval λlft λrgt
-        (BBT.bin K V new_size node_key val lft rgt)
-      (~(U60.to_bool (> balance 1))
-        P
-        true
-        false
-        new_size
-        node_key
-        val
-        lft
-        rgt
-      )
-    (~(BBT.got_size K V rgt) P new)
-  (~(BBT.got_size K V lft) P new)
+use BBT/{bin,tip}
+use Bool/{true,false}
+
+balance <K> <V>
+  (cmp: ∀(a: K) ∀(b: K) Cmp)
+  (set_key: K)
+  (node_key: K)
+  (val: V)
+  (lft: (BBT K V))
+  (rgt: (BBT K V))
+: (BBT K V) =
+ match got_lft = (BBT/got_size lft) {
+   Pair/new:
+     match got_rgt = (BBT/got_size rgt) {
+       Pair/new:
+        use new_size = (+ got_lft.fst got_rgt.fst)
+        use balance = (U60/abs_diff got_lft.fst got_rgt.fst)
+
+        match _ = (U60/to_bool (> balance 1)) {
+          true:
+            match _ = (U60/to_bool (< got_lft.fst got_rgt.fst)) {
+              true: (BBT/balance/lft_heavier cmp new_size node_key set_key val lft rgt)
+              false: (BBT/balance/rgt_heavier cmp new_size node_key set_key val lft rgt)
+            }
+          false: (bin K V new_size node_key val lft rgt)
+        }
+     }
+ }
+
+
+
+//BBT.balance
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(set_key: K)
+  //∀(node_key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λcmp λset_key λnode_key λval λlft λrgt
+  //use P = λx (BBT K V)
+  //use new = λlft.size λlft
+    //use P = λx (BBT K V)
+    //use new = λrgt.size λrgt
+      //use new_size = (+ 1 (U60.max lft.size rgt.size))
+      //use balance = (U60.abs_diff lft.size rgt.size)
+      //use P = λx
+        //∀(new_size: U60)
+        //∀(node_key: K)
+        //∀(val: V)
+        //∀(lft: (BBT K V))
+        //∀(rgt: (BBT K V))
+        //(BBT K V)
+      //use true = λnew_size λnode_key λval λlft λrgt
+        //use P = λx
+          //∀(K: *)
+          //∀(V: *)
+          //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+          //∀(new_size: U60)
+          //∀(node_key: K)
+          //∀(set_key: K)
+          //∀(val: V)
+          //∀(lft: (BBT K V))
+          //∀(rgt: (BBT K V))
+          //(BBT K V)
+        //use true = BBT.balance.lft_heavier
+        //use false = BBT.balance.rgt_heavier
+        //(~(U60.to_bool (< rgt.size lft.size))
+          //P
+          //true
+          //false
+          //K
+          //V
+          //cmp
+          //new_size
+          //node_key
+          //set_key
+          //val
+          //lft
+          //rgt
+        //)
+      //use false = λnew_size λnode_key λval λlft λrgt
+        //(BBT.bin K V new_size node_key val lft rgt)
+      //(~(U60.to_bool (> balance 1))
+        //P
+        //true
+        //false
+        //new_size
+        //node_key
+        //val
+        //lft
+        //rgt
+      //)
+    //(~(BBT.got_size K V rgt) P new)
+  //(~(BBT.got_size K V lft) P new)

book/BBT/balance/lft_heavier.kind2

@@ -1,53 +1,80 @@
-BBT.balance.lft_heavier
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(new_size: U60)
-  ∀(node_key: K)
-  ∀(set_key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
-  use P = λx (BBT K V)
-  use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
-    use P = λx
-      ∀(new_size: U60)
-      ∀(key: K)
-      ∀(val: V)
-      ∀(lft.key: K)
-      ∀(lft.val: V)
-      ∀(lft.lft: (BBT K V))
-      ∀(lft.rgt: (BBT K V))
-      ∀(rgt: (BBT K V))
-      (BBT K V)
-    use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
-      use lft = (BBT.lft_rotate
-          K
-          V
-          lft.size
-          lft.key
-          lft.val
-          lft.lft
-          lft.rgt
-        )
-      (BBT.rgt_rotate K V new_size key val lft rgt)
-    use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
-      use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
-      (BBT.rgt_rotate K V new_size key val lft rgt)
-    (~(Cmp.is_gtn (cmp set_key lft.key))
-      P
-      true
-      false
-      new_size
-      node_key
-      val
-      lft.key
-      lft.val
-      lft.lft
-      lft.rgt
-      rgt
-    )
-  use tip = (BBT.tip K V)
-  (~lft P bin tip)
+use BBT/{bin,tip,lft_rotate,rgt_rotate}
+use Bool/{true,false}
+
+lft_heavier <K> <V>
+  (cmp: ∀(a: K) ∀(b: K) Cmp)
+  (new_size: U60)
+  (node_key: K)
+  (set_key: K)
+  (val: V)
+  (lft: (BBT K V))
+  (rgt: (BBT K V))
+: (BBT K V) =
+  match lft {
+    bin:
+      match _ = (Cmp/is_gtn (cmp set_key lft.key)) {
+        true:
+          use lft = (lft_rotate lft.size lft.key lft.val lft.lft lft.rgt)
+          (rgt_rotate new_size lft.key val lft rgt)
+        false:
+          use lft = (bin K V lft.size lft.key lft.val lft.lft lft.rgt)
+          (rgt_rotate new_size lft.key val lft rgt)
+      }
+    tip: (tip K V)
+  }
+
+
+
+//BBT.balance.lft_heavier
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(new_size: U60)
+  //∀(node_key: K)
+  //∀(set_key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
+  //use P = λx (BBT K V)
+  //use bin = λlft.size λlft.key λlft.val λlft.lft λlft.rgt
+    //use P = λx
+      //∀(new_size: U60)
+      //∀(key: K)
+      //∀(val: V)
+      //∀(lft.key: K)
+      //∀(lft.val: V)
+      //∀(lft.lft: (BBT K V))
+      //∀(lft.rgt: (BBT K V))
+      //∀(rgt: (BBT K V))
+      //(BBT K V)
+    //use true = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
+      //use lft = (BBT.lft_rotate
+          //K
+          //V
+          //lft.size
+          //lft.key
+          //lft.val
+          //lft.lft
+          //lft.rgt
+        //)
+      //(BBT.rgt_rotate K V new_size key val lft rgt)
+    //use false = λnew_size λkey λval λlft.key λlft.val λlft.lft λlft.rgt λrgt
+      //use lft = (BBT.bin K V lft.size lft.key lft.val lft.lft lft.rgt)
+      //(BBT.rgt_rotate K V new_size key val lft rgt)
+    //(~(Cmp.is_gtn (cmp set_key lft.key))
+      //P
+      //true
+      //false
+      //new_size
+      //node_key
+      //val
+      //lft.key
+      //lft.val
+      //lft.lft
+      //lft.rgt
+      //rgt
+    //)
+  //use tip = (BBT.tip K V)
+  //(~lft P bin tip)

book/BBT/balance/rgt_heavier.kind2

@@ -1,53 +1,80 @@
-BBT.balance.rgt_heavier
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(new_size: U60)
-  ∀(node_key: K)
-  ∀(set_key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
-  use P = λx (BBT K V)
-  use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
-    use P = λx
-      ∀(new_size: U60)
-      ∀(key: K)
-      ∀(val: V)
-      ∀(lft: (BBT K V))
-      ∀(rgt.key: K)
-      ∀(rgt.val: V)
-      ∀(rgt.lft: (BBT K V))
-      ∀(rgt.rgt: (BBT K V))
-      (BBT K V)
-    use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
-      use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
-      (BBT.lft_rotate K V new_size key val lft rgt)
-    use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
-      use rgt = (BBT.rgt_rotate
-          K
-          V
-          rgt.size
-          rgt.key
-          rgt.val
-          rgt.lft
-          rgt.rgt
-        )
-      (BBT.lft_rotate K V new_size key val lft rgt)
-    (~(Cmp.is_gtn (cmp set_key rgt.key))
-      P
-      true
-      false
-      new_size
-      node_key
-      val
-      lft
-      rgt.key
-      rgt.val
-      rgt.lft
-      rgt.rgt
-    )
-  use tip = (BBT.tip K V)
-  (~rgt P bin tip)
+use BBT/{bin,tip,lft_rotate,rgt_rotate}
+use Bool/{true,false}
+
+rgt_heavier <K> <V>
+  (cmp: ∀(a: K) ∀(b: K) Cmp)
+  (new_size: U60)
+  (node_key: K)
+  (set_key: K)
+  (val: V)
+  (lft: (BBT K V))
+  (rgt: (BBT K V))
+: (BBT K V) =
+  match rgt {
+    bin:
+      match _ = (Cmp/is_gtn (cmp set_key rgt.key)) {
+        true:
+          use rgt = (bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
+          (lft_rotate new_size rgt.key val lft rgt)
+        false:
+          use rgt = (rgt_rotate rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
+          (lft_rotate new_size rgt.key val lft rgt)
+      }
+    tip: (tip K V)
+  }
+
+
+
+//BBT.balance.rgt_heavier
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(new_size: U60)
+  //∀(node_key: K)
+  //∀(set_key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λcmp λnew_size λnode_key λset_key λval λlft λrgt
+  //use P = λx (BBT K V)
+  //use bin = λrgt.size λrgt.key λrgt.val λrgt.lft λrgt.rgt
+    //use P = λx
+      //∀(new_size: U60)
+      //∀(key: K)
+      //∀(val: V)
+      //∀(lft: (BBT K V))
+      //∀(rgt.key: K)
+      //∀(rgt.val: V)
+      //∀(rgt.lft: (BBT K V))
+      //∀(rgt.rgt: (BBT K V))
+      //(BBT K V)
+    //use true = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
+      //use rgt = (BBT.bin K V rgt.size rgt.key rgt.val rgt.lft rgt.rgt)
+      //(BBT.lft_rotate K V new_size key val lft rgt)
+    //use false = λnew_size λkey λval λlft λrgt.key λrgt.val λrgt.lft λrgt.rgt
+      //use rgt = (BBT.rgt_rotate
+          //K
+          //V
+          //rgt.size
+          //rgt.key
+          //rgt.val
+          //rgt.lft
+          //rgt.rgt
+        //)
+      //(BBT.lft_rotate K V new_size key val lft rgt)
+    //(~(Cmp.is_gtn (cmp set_key rgt.key))
+      //P
+      //true
+      //false
+      //new_size
+      //node_key
+      //val
+      //lft
+      //rgt.key
+      //rgt.val
+      //rgt.lft
+      //rgt.rgt
+    //)
+  //use tip = (BBT.tip K V)
+  //(~rgt P bin tip)

book/BBT/bin.kind2

@@ -8,4 +8,4 @@ BBT.bin
   ∀(rgt: (BBT K V))
   (BBT K V)
 = λK λV λsize λkey λval λlft λrgt
-  ~λP λbin λtip (bin size key val lft rgt)
+  ~λP λbin λtip (bin size key val lft rgt)

book/BBT/from_list.kind2

@@ -1,15 +1,28 @@
-BBT.from_list
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(list: (List (Pair K V)))
-  (BBT K V)
-= λK λV λcmp λlist
-  use P = λx (BBT K V)
-  use cons = λhead λtail
-    use P = λx (BBT K V)
-    use new = λkey λval
-      (BBT.set K V cmp key val (BBT.from_list K V cmp tail))
-    (~head P new)
-  use nil = (BBT.tip K V)
-  (~list P cons nil)
+use BBT/{bin,tip,set}
+
+from_list <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (list: (List (Pair K V))) : (BBT K V) =
+  match list {
+    List/cons:
+      match pair = list.head {
+        Pair/new: (set cmp pair.fst pair.snd (from_list cmp list.tail))
+      }
+    List/nil: (tip K V)
+  }
+
+
+
+//BBT.from_list
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(list: (List (Pair K V)))
+  //(BBT K V)
+//= λK λV λcmp λlist
+  //use P = λx (BBT K V)
+  //use cons = λhead λtail
+    //use P = λx (BBT K V)
+    //use new = λkey λval
+      //(BBT.set K V cmp key val (BBT.from_list K V cmp tail))
+    //(~head P new)
+  //use nil = (BBT.tip K V)
+  //(~list P cons nil)

book/BBT/get.kind2

@@ -1,18 +1,34 @@
-BBT.get
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(key: K)
-  ∀(map: (BBT K V))
-  (Maybe V)
-= λK λV λcmp λkey λmap
-  use P = λx (Maybe V)
-  use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
-    use P = λx
-      ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
-    use ltn = λcmp λkey (BBT.get K V cmp key next.lft)
-    use eql = λcmp λkey (Maybe.some V next.val)
-    use gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
-    (~(cmp key next.key) P ltn eql gtn cmp key)
-  use tip = (Maybe.none V)
-  (~map P bin tip)
+use BBT/{bin,tip}
+use Cmp/{ltn,eql,gtn}
+
+get <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Maybe V) =
+  match map {
+    bin:
+      match _ = (cmp key map.key) {
+        ltn: (get cmp key map.lft)
+        eql: (Maybe/some map.val)
+        gtn: (get cmp key map.rgt)
+      }
+    tip: Maybe/none
+  }
+
+
+
+//BBT.get
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(key: K)
+  //∀(map: (BBT K V))
+  //(Maybe V)
+//= λK λV λcmp λkey λmap
+  //use P = λx (Maybe V)
+  //use bin = λ_size λnext.key λnext.val λnext.lft λnext.rgt
+    //use P = λx
+      //∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) (Maybe V)
+    //use ltn = λcmp λkey (BBT.get K V cmp key next.lft)
+    //use eql = λcmp λkey (Maybe.some V next.val)
+    //use gtn = λcmp λkey (BBT.get K V cmp key next.rgt)
+    //(~(cmp key next.key) P ltn eql gtn cmp key)
+  //use tip = (Maybe.none V)
+  //(~map P bin tip)

book/BBT/got.kind2

@@ -1,43 +1,70 @@
-BBT.got
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(key: K)
-  ∀(map: (BBT K V))
-  (Pair (Maybe V) (BBT K V))
-= λK λV λcmp λkey λmap
-  use P = λx (Pair (Maybe V) (BBT K V))
-  use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
-    use P = λx
-      ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K)
-      (Pair (Maybe V) (BBT K V))
-    use ltn = λcmp λkey
-      use new_pair = (BBT.got K V cmp key next.lft)
-      use P = λx (Pair (Maybe V) (BBT K V))
-      use new = λval λlft
-        use map = (BBT.bin K V size next.key next.val lft next.rgt)
-        (Pair.new (Maybe V) (BBT K V) val map)
-      (~new_pair P new)
-    use eql = λcmp λkey
-      use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
-      (Pair.new
-        (Maybe V)
-        (BBT K V)
-        (Maybe.some V next.val)
-        map
-      )
-    use gtn = λcmp λkey
-      use new_pair = (BBT.got K V cmp key next.rgt)
-      use P = λx (Pair (Maybe V) (BBT K V))
-      use new = λval λrgt
-        use map = (BBT.bin K V size next.key next.val next.lft rgt)
-        (Pair.new (Maybe V) (BBT K V) val map)
-      (~new_pair P new)
-    (~(cmp key next.key) P ltn eql gtn cmp key)
-  use tip = (Pair.new
-      (Maybe V)
-      (BBT K V)
-      (Maybe.none V)
-      (BBT.tip K V)
-    )
-  (~map P bin tip)
+use BBT/{bin,tip}
+use Maybe/{some,none}
+use Cmp/{ltn,eql,gtn}
+
+got <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair (Maybe V) (BBT K V)) =
+  match map {
+    bin:
+      match _ = (cmp key map.key) {
+        ltn:
+          match new_pair = (got cmp key map.lft) {
+            Pair/new:
+              let map = (bin K V map.size map.key map.val new_pair.snd map.rgt)
+              (Pair/new new_pair.fst map)
+          }
+        eql: (Pair/new (some map.val) map)
+        gtn:
+          match new_pair = (got cmp key map.rgt) {
+            Pair/new:
+              let map = (bin K V map.size map.key map.val map.lft new_pair.snd)
+              (Pair/new new_pair.fst map)
+          }
+      }
+    tip: (Pair/new none (tip K V))
+  }
+
+
+
+//BBT.got
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(key: K)
+  //∀(map: (BBT K V))
+  //(Pair (Maybe V) (BBT K V))
+//= λK λV λcmp λkey λmap
+  //use P = λx (Pair (Maybe V) (BBT K V))
+  //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
+    //use P = λx
+      //∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K)
+      //(Pair (Maybe V) (BBT K V))
+    //use ltn = λcmp λkey
+      //use new_pair = (BBT.got K V cmp key next.lft)
+      //use P = λx (Pair (Maybe V) (BBT K V))
+      //use new = λval λlft
+        //use map = (BBT.bin K V size next.key next.val lft next.rgt)
+        //(Pair.new (Maybe V) (BBT K V) val map)
+      //(~new_pair P new)
+    //use eql = λcmp λkey
+      //use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
+      //(Pair.new
+        //(Maybe V)
+        //(BBT K V)
+        //(Maybe.some V next.val)
+        //map
+      //)
+    //use gtn = λcmp λkey
+      //use new_pair = (BBT.got K V cmp key next.rgt)
+      //use P = λx (Pair (Maybe V) (BBT K V))
+      //use new = λval λrgt
+        //use map = (BBT.bin K V size next.key next.val next.lft rgt)
+        //(Pair.new (Maybe V) (BBT K V) val map)
+      //(~new_pair P new)
+    //(~(cmp key next.key) P ltn eql gtn cmp key)
+  //use tip = (Pair.new
+      //(Maybe V)
+      //(BBT K V)
+      //(Maybe.none V)
+      //(BBT.tip K V)
+    //)
+  //(~map P bin tip)

book/BBT/got_size.kind2

@@ -1,10 +1,20 @@
-BBT.got_size
-: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
-  (Pair U60 (BBT K V))
-= λK λV λmap
-  use P = λx (Pair U60 (BBT K V))
-  use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
-    use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
-    (Pair.new U60 (BBT K V) size map)
-  use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
-  (~map P bin tip)
+use BBT/{bin,tip}
+
+got_size <K> <V> (map: (BBT K V)) : (Pair U60 (BBT K V)) =
+  match map {
+    bin: (Pair/new map.size map)
+    tip: (Pair/new 0 (tip K V))
+  }
+
+
+
+//BBT.got_size
+//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
+  //(Pair U60 (BBT K V))
+//= λK λV λmap
+  //use P = λx (Pair U60 (BBT K V))
+  //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt
+    //use map = (BBT.bin K V size next.key next.val next.lft next.rgt)
+    //(Pair.new U60 (BBT K V) size map)
+  //use tip = (Pair.new U60 (BBT K V) 0 (BBT.tip K V))
+  //(~map P bin tip)

book/BBT/has.kind2

@@ -1,17 +1,33 @@
-BBT.has
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(key: K)
-  ∀(map: (BBT K V))
-  Bool
-= λK λV λcmp λkey λmap
-  use P = λx Bool
-  use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
-    use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
-    use ltn = λcmp λkey (BBT.has K V cmp key next.lft)
-    use eql = λcmp λkey Bool.true
-    use gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
-    (~(cmp key next.key) P ltn eql gtn cmp key)
-  use tip = Bool.false
-  (~map P bin tip)
+use BBT/{bin,tip}
+use Cmp/{ltn,eql,gtn}
+
+has <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : Bool =
+  match map {
+    bin:
+      match _ = (cmp key map.key) {
+        ltn: (has cmp key map.lft)
+        eql: Bool/true
+        gtn: (has cmp key map.rgt)
+      }
+    tip: Bool/false
+  }
+
+
+
+//BBT.has
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(key: K)
+  //∀(map: (BBT K V))
+  //Bool
+//= λK λV λcmp λkey λmap
+  //use P = λx Bool
+  //use bin = λnext.size λnext.key λnext.val λnext.lft λnext.rgt
+    //use P = λx ∀(cmp: ∀(a: K) ∀(b: K) Cmp) ∀(key: K) Bool
+    //use ltn = λcmp λkey (BBT.has K V cmp key next.lft)
+    //use eql = λcmp λkey Bool.true
+    //use gtn = λcmp λkey (BBT.has K V cmp key next.rgt)
+    //(~(cmp key next.key) P ltn eql gtn cmp key)
+  //use tip = Bool.false
+  //(~map P bin tip)

book/BBT/has/linear.kind2

@@ -1,51 +1,74 @@
-BBT.has.linear
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(key: K)
-  ∀(map: (BBT K V))
-  (Pair Bool (BBT K V))
-= λK λV λcmp λhas_key λmap
-  use P = λx (Pair Bool (BBT K V))
-  use bin = λsize λnode_key λval λlft λrgt
-    use P = λx
-      ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-      ∀(size: U60)
-      ∀(node_key: K)
-      ∀(val: V)
-      ∀(lft: (BBT K V))
-      ∀(rgt: (BBT K V))
-      ∀(key: K)
-      (Pair Bool (BBT K V))
-    use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key
-      use P = λx (Pair Bool (BBT K V))
-      use new = λbool λlft
-        use map = (BBT.bin K V size node_key val lft rgt)
-        (Pair.new Bool (BBT K V) bool map)
-      (~(BBT.has.linear K V cmp has_key lft) P new)
-    use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key
-      (Pair.new
-        Bool
-        (BBT K V)
-        Bool.true
-        (BBT.bin K V size node_key val lft rgt)
-      )
-    use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key
-      use P = λx (Pair Bool (BBT K V))
-      use new = λbool λrgt
-        use map = (BBT.bin K V size node_key val lft rgt)
-        (Pair.new Bool (BBT K V) bool rgt)
-      (~(BBT.has.linear K V cmp has_key rgt) P new)
-    ((~(cmp has_key node_key) P ltn eql gtn)
-      cmp
-      size
-      node_key
-      val
-      lft
-      rgt
-      has_key
-    )
-  use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
-  (~map P bin tip)
+use BBT/{bin,tip}
+use Bool/{false,true}
+use Cmp/{ltn,eql,gtn}
 
-  
+linear <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (map: (BBT K V)) : (Pair Bool (BBT K V)) =
+  match map {
+    bin:
+      match _ = (cmp key map.key) {
+        ltn:
+          match result = (linear cmp key map.lft) {
+            Pair/new:
+              (Pair/new result.fst (bin K V map.size map.key map.val result.snd map.rgt))
+          }
+        eql: (Pair/new true (bin K V map.size map.key map.val map.lft map.rgt))
+        gtn:
+          match result = (linear cmp key map.rgt) {
+            Pair/new:
+              (Pair/new result.fst (bin K V map.size map.key map.val map.lft result.snd))
+          }
+      }
+    tip: (Pair/new false (tip K V))
+  }
+
+
+
+//BBT.has.linear
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(key: K)
+  //∀(map: (BBT K V))
+  //(Pair Bool (BBT K V))
+//= λK λV λcmp λhas_key λmap
+  //use P = λx (Pair Bool (BBT K V))
+  //use bin = λsize λnode_key λval λlft λrgt
+    //use P = λx
+      //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+      //∀(size: U60)
+      //∀(node_key: K)
+      //∀(val: V)
+      //∀(lft: (BBT K V))
+      //∀(rgt: (BBT K V))
+      //∀(key: K)
+      //(Pair Bool (BBT K V))
+    //use ltn = λcmp λsize λnode_key λval λlft λrgt λhas_key
+      //use P = λx (Pair Bool (BBT K V))
+      //use new = λbool λlft
+        //use map = (BBT.bin K V size node_key val lft rgt)
+        //(Pair.new Bool (BBT K V) bool map)
+      //(~(BBT.has.linear K V cmp has_key lft) P new)
+    //use eql = λcmp λsize λnode_key λval λlft λrgt λhas_key
+      //(Pair.new
+        //Bool
+        //(BBT K V)
+        //Bool.true
+        //(BBT.bin K V size node_key val lft rgt)
+      //)
+    //use gtn = λcmp λsize λnode_key λval λlft λrgt λhas_key
+      //use P = λx (Pair Bool (BBT K V))
+      //use new = λbool λrgt
+        //use map = (BBT.bin K V size node_key val lft rgt)
+        //(Pair.new Bool (BBT K V) bool rgt)
+      //(~(BBT.has.linear K V cmp has_key rgt) P new)
+    //((~(cmp has_key node_key) P ltn eql gtn)
+      //cmp
+      //size
+      //node_key
+      //val
+      //lft
+      //rgt
+      //has_key
+    //)
+  //use tip = (Pair.new Bool (BBT K V) Bool.false (BBT.tip K V))
+  //(~map P bin tip)

book/BBT/lft_rotate.kind2

@@ -1,18 +1,31 @@
-BBT.lft_rotate
-: ∀(K: *)
-  ∀(V: *)
-  ∀(size: U60)
-  ∀(key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λsize λkey λval λlft λrgt
-  use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
-  use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft
-    use b = (BBT.new_node K V key val lft rgt.lft)
-    use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
-    a
-  use tip = λkey λval λlft
-    (BBT.bin K V size key val lft (BBT.tip K V))
-  (~rgt P bin tip key val lft)
+use BBT/{bin,tip}
+
+lft_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
+  match rgt {
+    bin:
+      use b = (BBT/new_node key val lft rgt.lft)
+      use a = (BBT/new_node rgt.key rgt.val b rgt.rgt)
+      a
+    tip: (bin K V size key val lft (tip K V))
+  }
+
+
+
+//BBT.lft_rotate
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(size: U60)
+  //∀(key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λsize λkey λval λlft λrgt
+  //use P = λx ∀(key: K) ∀(val: V) ∀(lft: (BBT K V)) (BBT K V)
+  //use bin = λ_size λrgt.key λrgt.val λrgt.lft λrgt.rgt λkey λval λlft
+    //use b = (BBT.new_node K V key val lft rgt.lft)
+    //use a = (BBT.new_node K V rgt.key rgt.val b rgt.rgt)
+    //a
+  //use tip = λkey λval λlft
+    //(BBT.bin K V size key val lft (BBT.tip K V))
+  //(~rgt P bin tip key val lft)

book/BBT/new_node.kind2

@@ -1,17 +1,30 @@
-BBT.new_node
-: ∀(K: *)
-  ∀(V: *)
-  ∀(key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λkey λval λlft λrgt
-  use P = λx (BBT K V)
-  use new = λlft.size λlft
-    use P = λx (BBT K V)
-    use new = λrgt.size λrgt
-      use new_size = (+ 1 (U60.max rgt.size lft.size))
-      (BBT.bin K V new_size key val lft rgt)
-    (~(BBT.got_size K V rgt) P new)
-  (~(BBT.got_size K V lft) P new)
+use BBT/{bin}
+
+new_node <K> <V> (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
+  match lft_size = (BBT/got_size lft) {
+    Pair/new: match rgt_size = (BBT/got_size rgt) {
+      Pair/new:
+        use new_size = (+ 1 (U60/max lft_size.fst rgt_size.fst))
+        (bin K V new_size key val lft rgt)
+    }
+  }
+
+
+
+//BBT.new_node
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λkey λval λlft λrgt
+  //use P = λx (BBT K V)
+  //use new = λlft.size λlft
+    //use P = λx (BBT K V)
+    //use new = λrgt.size λrgt
+      //use new_size = (+ 1 (U60.max rgt.size lft.size))
+      //(BBT.bin K V new_size key val lft rgt)
+    //(~(BBT.got_size K V rgt) P new)
+  //(~(BBT.got_size K V lft) P new)

book/BBT/rgt_rotate.kind2

@@ -1,18 +1,31 @@
-BBT.rgt_rotate
-: ∀(K: *)
-  ∀(V: *)
-  ∀(size: U60)
-  ∀(key: K)
-  ∀(val: V)
-  ∀(lft: (BBT K V))
-  ∀(rgt: (BBT K V))
-  (BBT K V)
-= λK λV λsize λkey λval λlft λrgt
-  use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
-  use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt
-    use b = (BBT.new_node K V key val lft.rgt rgt)
-    use a = (BBT.new_node K V lft.key lft.val lft.lft b)
-    a
-  use tip = λkey λval λrgt
-    (BBT.bin K V size key val (BBT.tip K V) rgt)
-  (~lft P bin tip key val rgt)
+use BBT/{bin,tip}
+
+rgt_rotate <K> <V> (size: U60) (key: K) (val: V) (lft: (BBT K V)) (rgt: (BBT K V)) : (BBT K V) =
+  match lft {
+    bin:
+      use b = (BBT/new_node key val lft.rgt rgt)
+      use a = (BBT/new_node lft.key lft.val lft.lft b)
+      a
+    tip: (bin K V size key val (tip K V) rgt)
+  }
+
+
+
+//BBT.rgt_rotate
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(size: U60)
+  //∀(key: K)
+  //∀(val: V)
+  //∀(lft: (BBT K V))
+  //∀(rgt: (BBT K V))
+  //(BBT K V)
+//= λK λV λsize λkey λval λlft λrgt
+  //use P = λx ∀(key: K) ∀(val: V) ∀(rgt: (BBT K V)) (BBT K V)
+  //use bin = λ_size λlft.key λlft.val λlft.lft λlft.rgt λkey λval λrgt
+    //use b = (BBT.new_node K V key val lft.rgt rgt)
+    //use a = (BBT.new_node K V lft.key lft.val lft.lft b)
+    //a
+  //use tip = λkey λval λrgt
+    //(BBT.bin K V size key val (BBT.tip K V) rgt)
+  //(~lft P bin tip key val rgt)

book/BBT/set.kind2

@@ -1,61 +1,81 @@
-BBT.set
-: ∀(K: *)
-  ∀(V: *)
-  ∀(cmp: ∀(a: K) ∀(b: K) Cmp)
-  ∀(key: K)
-  ∀(val: V)
-  ∀(map: (BBT K V))
-  (BBT K V)
-= λK λV λcmp λkey λval λmap
-  use P = λx ∀(key: K) ∀(val: V) (BBT K V)
-  use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
-    use P = λx
-      ∀(key: K)
-      ∀(next.key: K)
-      ∀(next.val: V)
-      ∀(next.lft: (BBT K V))
-      ∀(next.rgt: (BBT K V))
-      ∀(key: K)
-      ∀(val: V)
-      (BBT K V)
-    use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
-      use new_lft = (BBT.set K V cmp key val next.lft)
-      (BBT.balance
-        K
-        V
-        cmp
-        key
-        next.key
-        next.val
-        new_lft
-        next.rgt
-      )
-    use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
-      (BBT.bin K V size next.key val next.lft next.rgt)
-    use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
-      use new_rgt = (BBT.set K V cmp key val next.rgt)
-      (BBT.balance
-        K
-        V
-        cmp
-        key
-        next.key
-        next.val
-        next.lft
-        new_rgt
-      )
-    (~(cmp key next.key)
-      P
-      ltn
-      eql
-      gtn
-      key
-      next.key
-      next.val
-      next.lft
-      next.rgt
-      key
-      val
-    )
-  use tip = λkey λval (BBT.singleton K V key val)
-  (~map P bin tip key val)
+use BBT/{bin,tip}
+use Cmp/{ltn,eql,gtn}
+
+set <K> <V> (cmp: ∀(a: K) ∀(b: K) Cmp) (key: K) (val: V) (map: (BBT K V)) : (BBT K V) =
+  match map {
+    bin:
+      match _ = (cmp key map.key) {
+        ltn:
+          use new_lft = (set cmp key val map.lft)
+          (BBT/balance cmp key map.key map.val new_lft map.rgt)
+        eql: (bin K V map.size map.key val map.lft map.rgt)
+        gtn:
+          use new_rgt = (set cmp key val map.rgt)
+          (BBT/balance cmp key map.key map.val map.lft new_rgt)
+      }
+    tip: (BBT/singleton key val)
+  }
+
+
+
+//BBT.set
+//: ∀(K: *)
+  //∀(V: *)
+  //∀(cmp: ∀(a: K) ∀(b: K) Cmp)
+  //∀(key: K)
+  //∀(val: V)
+  //∀(map: (BBT K V))
+  //(BBT K V)
+//= λK λV λcmp λkey λval λmap
+  //use P = λx ∀(key: K) ∀(val: V) (BBT K V)
+  //use bin = λsize λnext.key λnext.val λnext.lft λnext.rgt λkey λval
+    //use P = λx
+      //∀(key: K)
+      //∀(next.key: K)
+      //∀(next.val: V)
+      //∀(next.lft: (BBT K V))
+      //∀(next.rgt: (BBT K V))
+      //∀(key: K)
+      //∀(val: V)
+      //(BBT K V)
+    //use ltn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
+      //use new_lft = (BBT.set K V cmp key val next.lft)
+      //(BBT.balance
+        //K
+        //V
+        //cmp
+        //key
+        //next.key
+        //next.val
+        //new_lft
+        //next.rgt
+      //)
+    //use eql = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
+      //(BBT.bin K V size next.key val next.lft next.rgt)
+    //use gtn = λkey λnext.key λnext.val λnext.lft λnext.rgt λkey λval
+      //use new_rgt = (BBT.set K V cmp key val next.rgt)
+      //(BBT.balance
+        //K
+        //V
+        //cmp
+        //key
+        //next.key
+        //next.val
+        //next.lft
+        //new_rgt
+      //)
+    //(~(cmp key next.key)
+      //P
+      //ltn
+      //eql
+      //gtn
+      //key
+      //next.key
+      //next.val
+      //next.lft
+      //next.rgt
+      //key
+      //val
+    //)
+  //use tip = λkey λval (BBT.singleton K V key val)
+  //(~map P bin tip key val)

book/BBT/singleton.kind2

@@ -1,4 +1,10 @@
-BBT.singleton
-: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
-= λK λV λkey λval
-  (BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))
+singleton <K> <V> (key: K) (val: V) : (BBT K V) =
+  use tip = (BBT/tip K V)
+  (BBT/bin K V 1 key val tip tip)
+
+
+
+//BBT.singleton
+//: ∀(K: *) ∀(V: *) ∀(key: K) ∀(val: V) (BBT K V)
+//= λK λV λkey λval
+  //(BBT.bin K V 1 key val (BBT.tip K V) (BBT.tip K V))

book/BBT/tip.kind2

@@ -1,3 +1,3 @@
 BBT.tip
 : ∀(K: *) ∀(V: *) (BBT K V)
-= λK λV ~λP λbin λtip tip
+= λK λV ~λP λbin λtip tip

book/BBT/to_list.kind2

@@ -1,17 +1,32 @@
-BBT.to_list
-: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
-  (List (Pair K V))
-= λK λV λmap
-  use P = λx (List (Pair K V))
-  use bin = λsize λkey λval λlft λrgt
-    use lft = (BBT.to_list K V lft)
-    use rgt = (BBT.to_list K V rgt)
-    use pair = (Pair.new K V key val)
-    use list = (List.cons
-        (Pair K V)
-        pair
-        (List.concat (Pair K V) lft rgt)
-      )
-    list
-  use tip = (List.nil (Pair K V))
-  (~map P bin tip)
+use BBT/{bin,tip}
+
+to_list <K> <V> (map: (BBT K V)) : (List (Pair K V)) =
+  match map {
+    bin:
+      use lft = (to_list map.lft)
+      use rgt = (to_list map.rgt)
+      use pair = (Pair/new map.key map.val)
+      use list = (List/cons pair (List/concat lft rgt))
+      list
+    tip: List/nil
+  }
+
+
+
+//BBT.to_list
+//: ∀(K: *) ∀(V: *) ∀(map: (BBT K V))
+  //(List (Pair K V))
+//= λK λV λmap
+  //use P = λx (List (Pair K V))
+  //use bin = λsize λkey λval λlft λrgt
+    //use lft = (BBT.to_list K V lft)
+    //use rgt = (BBT.to_list K V rgt)
+    //use pair = (Pair.new K V key val)
+    //use list = (List.cons
+        //(Pair K V)
+        //pair
+        //(List.concat (Pair K V) lft rgt)
+      //)
+    //list
+  //use tip = (List.nil (Pair K V))
+  //(~map P bin tip)

book/BMap.kind2

@@ -0,0 +1,3 @@
+data BMap A
+| node (lft: (BMap A)) (val: A) (rgt: (BMap A))
+| leaf

book/BMap/leaf.kind2

@@ -0,0 +1,3 @@
+BMap.leaf
+: ∀(A: *) (BMap A)
+= λA ~λP λnode λleaf leaf

book/BMap/node.kind2

@@ -0,0 +1,8 @@
+BMap.node
+: ∀(A: *)
+  ∀(lft: (BMap A))
+  ∀(val: A)
+  ∀(rgt: (BMap A))
+  (BMap A)
+= λA λlft λval λrgt
+  ~λP λnode λleaf (node lft val rgt)

book/Bool/and.kind2

@@ -1,7 +1,7 @@
 use Bool/{true,false,and}
 
 and (a: Bool) (b: Bool) : Bool =
-  match b {
+  match a {
     true: b
     false: false
   }

book/HVM/load.kind2

@@ -1,3 +1,8 @@
-HVM.load
-: ∀(A: *) ∀(file: String) ∀(cont: ∀(x: String) A) A
-= λA λfile λcont (cont String.nil)
+load <A> (file: String) (cont: String -> A) : A =
+  (cont String/nil)
+
+
+
+//HVM.load
+//: ∀(A: *) ∀(file: String) ∀(cont: ∀(x: String) A) A
+//= λA λfile λcont (cont String.nil)

book/HVM/log.kind2

@@ -1,3 +1,6 @@
-HVM.log
-: ∀(A: *) ∀(B: *) ∀(msg: A) ∀(ret: B) B
-= λA λB λmsg λret ret
+log <A> <B> (msg: A) (ret: B) : B =
+  ret
+
+//HVM.log
+//: ∀(A: *) ∀(B: *) ∀(msg: A) ∀(ret: B) B
+//= λA λB λmsg λret ret

book/HVM/print.kind2

@@ -1,3 +1,8 @@
-HVM.print
-: ∀(A: *) ∀(msg: String) ∀(ret: A) A
-= λA λmsg λret ret
+print <A> (msg: String) (ret: A) : A =
+  ret
+
+
+
+//HVM.print
+//: ∀(A: *) ∀(msg: String) ∀(ret: A) A
+//= λA λmsg λret ret

book/HVM/print/many.kind2

@@ -1,8 +1,18 @@
-HVM.print.many
-: ∀(A: *) ∀(msgs: (List String)) ∀(ret: A) A
-= λA λmsgs λret
-  use P = λx A
-  use cons = λmsg λmsgs
-    (HVM.print A msg (HVM.print.many A msgs ret))
-  use nil = ret
-  (~msgs P cons nil)
+use List/{cons,nil}
+
+many <A> (msgs: (List String)) (ret: A) : A =
+  match msgs {
+    cons: (HVM/print msgs.head (HVM/print/many msgs.tail ret))
+    nil: ret
+  }
+
+
+
+//HVM.print.many
+//: ∀(A: *) ∀(msgs: (List String)) ∀(ret: A) A
+//= λA λmsgs λret
+  //use P = λx A
+  //use cons = λmsg λmsgs
+    //(HVM.print A msg (HVM.print.many A msgs ret))
+  //use nil = ret
+  //(~msgs P cons nil)

book/HVM/save.kind2

@@ -1,4 +1,9 @@
-HVM.save
-: ∀(A: *) ∀(file: String) ∀(data: String) ∀(cont: A)
-  A
-= λA λfile λdata λcont cont
+save <A> (file: String) (data: String) (cont: A) : A =
+  cont
+
+
+
+//HVM.save
+//: ∀(A: *) ∀(file: String) ∀(data: String) ∀(cont: A)
+  //A
+//= λA λfile λdata λcont cont

book/IO.kind2

@@ -1,10 +1,18 @@
-IO
-: ∀(A: *) *
-= λA
-  $(self: (IO A))
-  ∀(P: ∀(x: (IO A)) *)
-  ∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
-  ∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
-  ∀(save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file text then)))
-  ∀(done: ∀(term: A) (P (IO.done A term)))
-  (P self)
+data IO A
+| print (text: String) (then: ∀(x: Unit) (IO A))
+| load (file: String) (then: ∀(x: String) (IO A))
+| save (file: String) (text: String) (then: ∀(x: Unit) (IO A))
+| done (term: A)
+
+
+
+//IO
+//: ∀(A: *) *
+//= λA
+  //$(self: (IO A))
+  //∀(P: ∀(x: (IO A)) *)
+  //∀(print: ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.print A text then)))
+  //∀(load: ∀(file: String) ∀(then: ∀(x: String) (IO A)) (P (IO.load A file then)))
+  //∀(save: ∀(file: String) ∀(text: String) ∀(then: ∀(x: Unit) (IO A)) (P (IO.save A file text then)))
+  //∀(done: ∀(term: A) (P (IO.done A term)))
+  //(P self)

book/IO/bind.kind2

@@ -1,21 +1,31 @@
-IO.bind
-: ∀(A: *)
-  ∀(B: *)
-  ∀(a: (IO A))
-  ∀(b: ∀(x: A) (IO B))
-  (IO B)
-= λA λB λa λb
-  use P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
-  use print = λtext λthen λb
-    (IO.print B text λx (IO.bind A B (then x) b))
-  use load = λfile λthen λb
-    (IO.load B file λs (IO.bind A B (then s) b))
-  use save = λfile λdata λthen λb
-    (IO.save
-      B
-      file
-      data
-      λx (IO.bind A B (then Unit.one) b)
-    )
-  use done = λterm λb (b term)
-  (~a P print load save done b)
+bind <A> <B> (a: (IO A)) (b: A -> (IO B)) : (IO B) =
+  match a {
+    IO/print: (IO/print B a.text λx (IO/bind (a.then x) b))
+    IO/load: (IO/load B a.file λs (IO/bind (a.then s) b))
+    IO/save: (IO/save B a.file a.text λx (IO/bind (a.then Unit/new) b))
+    IO/done: (b a.term)
+  }
+
+
+
+//IO.bind
+//: ∀(A: *)
+  //∀(B: *)
+  //∀(a: (IO A))
+  //∀(b: ∀(x: A) (IO B))
+  //(IO B)
+//= λA λB λa λb
+  //use P = λx ∀(b: ∀(x: A) (IO B)) (IO B)
+  //use print = λtext λthen λb
+    //(IO.print B text λx (IO.bind A B (then x) b))
+  //use load = λfile λthen λb
+    //(IO.load B file λs (IO.bind A B (then s) b))
+  //use save = λfile λdata λthen λb
+    //(IO.save
+      //B
+      //file
+      //data
+      //λx (IO.bind A B (then Unit.one) b)
+    //)
+  //use done = λterm λb (b term)
+  //(~a P print load save done b)

book/IO/load/do.kind2

@@ -1,3 +1,8 @@
-IO.load.do
-: ∀(file: String) (IO String)
-= λfile (IO.load String file λx (IO.done String x))
+do (file: String) : (IO String) =
+  (IO/load String file λx (IO/done String x))
+
+
+
+//IO.load.do
+//: ∀(file: String) (IO String)
+//= λfile (IO.load String file λx (IO.done String x))

book/IO/print/do.kind2

@@ -1,3 +1,8 @@
-IO.print.do
-: ∀(text: String) (IO Unit)
-= λtext (IO.print Unit text λx (IO.done Unit x))
+do (text: String) : (IO Unit) =
+  (IO/print Unit text λx (IO/done Unit x))
+
+
+
+//IO.print.do
+//: ∀(text: String) (IO Unit)
+//= λtext (IO.print Unit text λx (IO.done Unit x))

book/IO/run.kind2

@@ -1,12 +1,22 @@
-IO.run
-: ∀(A: *) ∀(x: (IO A)) (IO A)
-= λA λx
-  use P = λx (IO A)
-  use print = λtext λthen
-    (HVM.print (IO A) text (IO.run A (then Unit.one)))
-  use load = λfile λthen
-    (HVM.load (IO A) file λs (IO.run A (then s)))
-  use save = λfile λtext λthen
-    (HVM.save (IO A) file text (IO.run A (then Unit.one)))
-  use done = λterm (IO.done A term)
-  (~x P print load save done)
+run <A> (x: (IO A)) : (IO A) =
+  match x {
+    IO/print: (HVM/print x.text (run (x.then Unit/new)))
+    IO/load: (HVM/load x.file λs (IO/run (x.then s)))
+    IO/save: (HVM/save x.file x.text (IO/run (x.then Unit/new)))
+    IO/done: (IO/done A x.term)
+  }
+
+
+
+//IO.run
+//: ∀(A: *) ∀(x: (IO A)) (IO A)
+//= λA λx
+  //use P = λx (IO A)
+  //use print = λtext λthen
+    //(HVM.print (IO A) text (IO.run A (then Unit.one)))
+  //use load = λfile λthen
+    //(HVM.load (IO A) file λs (IO.run A (then s)))
+  //use save = λfile λtext λthen
+    //(HVM.save (IO A) file text (IO.run A (then Unit.one)))
+  //use done = λterm (IO.done A term)
+  //(~x P print load save done)

book/IO/save/do.kind2

@@ -1,4 +1,9 @@
-IO.save.do
-: ∀(file: String) ∀(text: String) (IO Unit)
-= λfile λtext
-  (IO.save Unit file text λx (IO.done Unit x))
+do (file: String) (text: String) : (IO Unit) =
+  (IO/save Unit file text λx (IO/done Unit x))
+
+
+
+//IO.save.do
+//: ∀(file: String) ∀(text: String) (IO Unit)
+//= λfile λtext
+  //(IO.save Unit file text λx (IO.done Unit x))

book/List/and.kind2

@@ -0,0 +1,8 @@
+use List/{cons,nil}
+use Bool/{true}
+
+and (list: (List Bool)) : Bool =
+  fold list {
+    cons: (Bool/and list.head list.tail)
+    nil: true
+  }

book/List/drop.kind2

@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+drop <A> (n: Nat) (list: (List A)) : (List A) =
+  match n with (list: (List A)) {
+    zero: list
+    succ: match list {
+      cons: (drop n.pred list.tail)
+      nil: nil
+    }
+  }

book/List/filter.kind2

@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+filter <A> (cond: A -> Bool) (list: (List A)) : (List A) =
+  match list {
+    nil: nil
+    cons:
+      (Bool/if (cond list.head) (List A)
+        (cons list.head (filter cond list.tail))
+        (filter cond list.tail))
+  }

book/List/or.kind2

@@ -0,0 +1,8 @@
+use List/{cons,nil}
+use Bool/{false}
+
+or (list: (List Bool)) : Bool =
+  fold list {
+    cons: (Bool/or list.head list.tail)
+    nil: false
+  }

book/List/take.kind2

@@ -0,0 +1,11 @@
+use List/{cons,nil}
+use Nat/{succ,zero}
+
+take <A> (n: Nat) (list: (List A)) : (List A) =
+  match n with (list: (List A)) {
+    zero: nil
+    succ: match list {
+      cons: (cons list.head (take n.pred list.tail))
+      nil: nil
+    }
+  }

book/List/zip.kind2

@@ -0,0 +1,10 @@
+use List/{cons,nil}
+
+zip <A> <B> (as: (List A)) (bs: (List B)) : (List (Pair A B)) =
+  match as with (bs: (List B)) {
+    cons: match bs {
+      cons: (cons (Pair/new as.head bs.head) (zip as.tail bs.tail))
+      nil: nil
+    }
+    nil: nil
+  }

book/Monad.kind2

@@ -3,8 +3,8 @@ Monad
 = λM
   $(self: (Monad M))
   ∀(P: ∀(x: (Monad M)) *)
-  ∀(new: 
-    ∀(bind: 
+  ∀(new:
+    ∀(bind:
       ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B))
       (M B)
     )
@@ -12,3 +12,8 @@ Monad
     (P (Monad/new M bind pure))
   )
   (P self)
+
+//data Monad (M: * -> *)
+//| new
+    //(bind: ∀(A: *) ∀(B: *) ∀(a: (M A)) ∀(b: ∀(a: A) (M B)) (M B))
+    //(pure: ∀(A: *) ∀(a: A) (M A))

book/Nat/is_gtn.kind2

@@ -0,0 +1,11 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+is_gtn (a: Nat) (b: Nat) : Bool =
+  match a with (b: Nat) {
+    zero: false
+    succ: match b {
+      zero: true
+      succ: (is_gtn a.pred b.pred)
+    }
+  }

book/Nat/is_ltn.kind2

@@ -0,0 +1,14 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+is_ltn (a: Nat) (b: Nat) : Bool =
+  match a with (b: Nat) {
+    zero: match b {
+      zero: false
+      succ: true
+    }
+    succ: match b {
+      zero: false
+      succ: (is_ltn a.pred b.pred)
+    }
+  }

book/Nat/is_ltn_or_eql.kind2

@@ -0,0 +1,8 @@
+use Nat/{succ,zero}
+use Bool/{true,false}
+
+is_ltn_or_eql (a: Nat) (b: Nat) : Bool =
+  match _ = (Nat/is_ltn a b) {
+    true: true
+    false: (Nat/equal a b)
+  }

book/Nat/mul.kind2

@@ -0,0 +1,7 @@
+use Nat/{succ,zero}
+
+mul (a: Nat) (b: Nat) : Nat =
+  match b {
+    succ: (Nat/add a (Nat/mul a b.pred))
+    zero: zero
+  }

book/Parser/bind.kind2

@@ -8,4 +8,4 @@ Parser.bind
   use P = λx ∀(b: ∀(x: A) (Parser B)) (Parser.Result B)
   use done = λa.code λa.value λb (b a.value a.code)
   use fail = λa.error λb (Parser.Result.fail B a.error)
-  (~(a code) P done fail b)
+  (~(a code) P done fail b)

book/Parser/char.kind2

@@ -8,4 +8,4 @@ Parser.char
     use false = (Parser.Result.done Char tail head)
     (~(Char.is_slash head) P true false)
   use nil = (Parser.Result.fail Char "eof")
-  (~code P cons nil)
+  (~code P cons nil)

book/String/Map/from_list.kind2

@@ -1,4 +1,2 @@
-String.Map.from_list
-: ∀(V: *) ∀(list: (List (Pair String V)))
-  (String.Map V)
-= λV λlist (BBT.from_list String V String.cmp list)
+from_list <V> (list: (List (Pair String V))) : (String/Map V) =
+  (BBT/from_list String/cmp list)

book/String/Map/get.kind2

@@ -1,4 +1,2 @@
-String.Map.get
-: ∀(V: *) ∀(key: String) ∀(map: (String.Map V))
-  (Maybe V)
-= λV λkey λmap (BBT.get String V String.cmp key map)
+get <V> (key: String) (map: (String/Map V)) : (Maybe V) =
+  (BBT/get String/cmp key map)

book/String/Map/got.kind2

@@ -1,4 +1,2 @@
-String.Map.got
-: ∀(V: *) ∀(key: String) ∀(map: (String.Map V))
-  (Pair (Maybe V) (String.Map V))
-= λV λkey λmap (BBT.got String V String.cmp key map)
+got <V> (key: String) (map: (String/Map V)) : (Pair (Maybe V) (String/Map V)) =
+  (BBT/got String/cmp key map)

book/String/Map/has.kind2

@@ -1,3 +1,2 @@
-String.Map.has
-: ∀(V: *) ∀(key: String) ∀(map: (BBT String V)) Bool
-= λV λkey λmap (BBT.has String V String.cmp key map)
+has <V> (key: String) (map: (BBT String V)) : Bool =
+  (BBT/has String/cmp key map)

book/String/Map/has/linear.kind2

@@ -1,5 +1,2 @@
-String.Map.has.linear
-: ∀(V: *) ∀(key: String) ∀(map: (BBT String V))
-  (Pair Bool (BBT String V))
-= λV λkey λmap
-  (BBT.has.linear String V String.cmp key map)
+linear <V> (key: String) (map: (BBT String V)) : (Pair Bool (BBT String V)) =
+  (BBT/has/linear String/cmp key map)

book/String/Map/new.kind2

@@ -1,3 +1 @@
-String.Map.new
-: ∀(V: *) (String.Map V)
-= λV (BBT.tip String V)
+new <V> : (String/Map V) = (BBT/tip String V)

book/String/Map/set.kind2

@@ -1,8 +1,2 @@
-String.Map.set
-: ∀(V: *)
-  ∀(key: String)
-  ∀(val: V)
-  ∀(map: (String.Map V))
-  (String.Map V)
-= λV λkey λval λmap
-  (BBT.set String V String.cmp key val map)
+set <V> (key: String) (val: V) (map: (String/Map V)) : (String/Map V) =
+  (BBT/set String/cmp key val map)

book/String/Map/to_list.kind2

@@ -1,4 +1,2 @@
-String.Map.to_list
-: ∀(V: *) ∀(map: (String.Map V))
-  (List (Pair String V))
-= λV λmap (BBT.to_list String V map)
+to_list <V> (map: (String/Map V)) : (List (Pair String V)) =
+  (BBT/to_list map)

book/String/join.kind2

@@ -1,7 +1,15 @@
-join
-: ∀(sep: String) ∀(strs: (List String)) String
-= λsep λstrs
-  use P = λx String
-  use cons = λh λt (String/concat h (String/join/go sep t))
-  use nil = String/nil
-  (~strs P cons nil)
+join (sep: String) (strs: (List String)) : String =
+  match strs {
+    List/cons: (String/concat strs.head (String/join/go sep strs.tail))
+    List/nil: String/nil
+  }
+
+
+
+//join
+//: ∀(sep: String) ∀(strs: (List String)) String
+//= λsep λstrs
+  //use P = λx String
+  //use cons = λh λt (String/concat h (String/join/go sep t))
+  //use nil = String/nil
+  //(~strs P cons nil)

book/String/join/go.kind2

@@ -1,11 +1,19 @@
-go
-: ∀(sep: String) ∀(strs: (List String)) String
-= λsep λstrs
-  use P = λx String
-  use cons = λh λt
-    (String/concat
-      sep
-      (String/concat h (go sep t))
-    )
-  use nil = String/nil
-  (~strs P cons nil)
+go (sep: String) (strs: (List String)) : String =
+  match strs {
+    List/cons: (String/concat sep (String/concat strs.head (go sep strs.tail)))
+    List/nil: String/nil
+  }
+
+
+
+//go
+//: ∀(sep: String) ∀(strs: (List String)) String
+//= λsep λstrs
+  //use P = λx String
+  //use cons = λh λt
+    //(String/concat
+      //sep
+      //(String/concat h (go sep t))
+    //)
+  //use nil = String/nil
+  //(~strs P cons nil)

book/String/length.kind2

@@ -1,3 +1,5 @@
-String/length
-: ∀(a: String) Nat
-= λa (List/length a)
+length (s: String) : Nat = (List/length s)
+
+//String/length
+//: ∀(a: String) Nat
+//= λa (List/length a)