implement kind->js/html5 compiler, quadtrees and some other demo files and libs

TODO

@@ -0,0 +1,29 @@
+PLANS - can finish by 20h?
+
+[X] Build a Kind2 -> JavaScript compiler ~ 1 hour
+
+[X] Build a simple spec for live CanvasApps on Kind2
+
+[X] Build a Kind2 -> HTML5 canvas renderer
+
+[X] Implement a QuadTree type on Kind2
+
+[X] Implement a n-body particle integrator
+
+[ ] Render that live as a Solar System emulator
+
+___________________________________
+|                |       | O  |   |
+|                |       |____|___|
+|                |       |        |
+-----|---|-------|-------|---------
+|____|___|       |       |        |
+| O  |   |       |       |        |
+-----|---|-------|-------|--------|
+|                |                |
+|                |                |
+|                |                |
+|                |                |
+|                |                |
+|                |                |
+-----------------|-----------------

book/App/_.kind2

@@ -0,0 +1,22 @@
+/// Defines the App type, representing an application with state management and rendering.
+///
+/// # Type Parameters
+///
+/// * `S` - The type of the application state.
+///
+/// # Constructor
+///
+/// * `new` - Creates a new App instance with the following components:
+///
+/// # Fields
+///
+/// * `tick` - A function that updates the state on each tick.
+/// * `draw` - A function that converts the state to a list of shapes for rendering.
+/// * `when` - A function that updates the state based on keyboard input.
+
+data App <S: *>
+| new
+  (init: S)
+  (tick: S -> S)
+  (draw: S -> (List Shape))
+  (when: U48 -> S -> S)

book/App/new.kind2

@@ -0,0 +1,24 @@
+/// Creates a new App instance.
+///
+/// # Type Parameters
+///
+/// * `S` - The type of the application state.
+///
+/// # Inputs
+///
+/// * `tick` - A function that updates the state on each tick.
+/// * `draw` - A function that converts the state to a list of shapes for rendering.
+/// * `onkb` - A function that updates the state based on keyboard input.
+///
+/// # Output
+///
+/// A new App instance with the specified behaviors.
+
+new <S>
+- init: S
+- tick: ∀(state: S) S
+- draw: ∀(state: S) (List Shape)
+- when: ∀(key: U48) ∀(state: S) S
+: (App S)
+
+~λP λnew (new init tick draw when)

book/Bits/reverse.kind2

@@ -0,0 +1,17 @@
+/// Reverses the order of bits in a Bits value.
+///
+/// # Input
+///
+/// * `bits` - The Bits value to reverse.
+///
+/// # Output
+///
+/// A new Bits value with the bits in reverse order.
+
+use Bits/{O,I,E}
+
+reverse
+- bits: Bits
+: Bits
+
+(Bits/reverse/go bits E)

book/Bits/reverse/go.kind2

@@ -0,0 +1,13 @@
+use Bits/{O,I,E}
+
+go
+- bits: Bits
+- acc: Bits
+: Bits
+
+match bits {
+  O: (go bits.tail (O acc))
+  I: (go bits.tail (I acc))
+  E: acc
+}
+

book/List/concat.kind2

@@ -1,3 +1,18 @@
+/// Concatenates two lists of the same type.
+///
+/// # Parameters
+///
+/// * `T` - The type of elements in both lists.
+///
+/// # Inputs
+///
+/// * `xs` - The first list to concatenate.
+/// * `ys` - The second list to concatenate.
+///
+/// # Output
+///
+/// A new list containing all elements from `xs` followed by all elements from `ys`.
+
 use List/{cons,nil}
 
 concat <T>
@@ -6,6 +21,10 @@ concat <T>
 : (List T)
 
 match xs {
-  cons: (cons _ xs.head (concat _ xs.tail ys))
-  nil: ys
+  cons: 
+    // If `xs` is non-empty, add its head to the result and recurse on the tail
+    (cons _ xs.head (concat _ xs.tail ys))
+  nil: 
+    // If `xs` is empty, return `ys`
+    ys
 }

book/List/flatten.kind2

@@ -0,0 +1,25 @@
+/// Flattens a list of lists into a single list.
+///
+/// # Parameters
+///
+/// * `T` - The type of elements in the inner lists.
+///
+/// # Input
+///
+/// * `xss` - A list of lists to be flattened.
+///
+/// # Output
+///
+/// A single list containing all elements from the inner lists.
+
+use List/{cons,nil}
+use List/concat
+
+flatten <T>
+- xss: (List (List T))
+: (List T)
+
+match xss {
+  cons: (List/concat _ xss.head (flatten _ xss.tail))
+  nil: (nil _)
+}

book/List/head.kind2

@@ -0,0 +1,27 @@
+/// Returns the head of a list, or None if the list is empty.
+///
+/// # Parameters
+///
+/// * `A` - The type of elements in the list.
+///
+/// # Input
+///
+/// * `xs` - The input list.
+///
+/// # Output
+///
+/// Returns `(Maybe A)`:
+/// - `(Maybe/some A head)` if the list is non-empty
+/// - `(Maybe/none A)` if the list is empty
+
+use List/{cons,nil}
+use Maybe/{some,none}
+
+head <A>
+- xs: (List A)
+: (Maybe A)
+
+match xs {
+  cons: (some _ xs.head)
+  nil: (none _)
+}

book/List/is_empty.kind2

@@ -0,0 +1,25 @@
+/// Checks if a list is empty.
+///
+/// # Parameters
+///
+/// * `A` - The type of elements in the list.
+///
+/// # Input
+///
+/// * `xs` - The list to check.
+///
+/// # Output
+///
+/// Returns `true` if the list is empty, `false` otherwise.
+
+use List/{cons,nil}
+use Bool/{true,false}
+
+is_empty <A>
+- xs: (List A)
+: Bool
+
+match xs {
+  cons: false
+  nil: true
+}

book/List/tail.kind2

@@ -0,0 +1,27 @@
+/// Returns the tail of a list, or None if the list is empty.
+///
+/// # Parameters
+///
+/// * `A` - The type of elements in the list.
+///
+/// # Input
+///
+/// * `xs` - The input list.
+///
+/// # Output
+///
+/// Returns `(Maybe (List A))`:
+/// - `(Maybe/some (List A) tail)` if the list is non-empty
+/// - `(Maybe/none (List A))` if the list is empty
+
+use List/{cons,nil}
+use Maybe/{some,none}
+
+tail <A>
+- xs: (List A)
+: (Maybe (List A))
+
+match xs {
+  cons: (some _ xs.tail)
+  nil: (none _)
+}

book/Nat/half.kind2

@@ -27,5 +27,21 @@ match n {
     succ: (succ (half n.pred.pred))
     zero: zero
   }
-  zero: zero
+  zero: (succ zero)
 }
+
+
+//half 0 == 1 wrong
+//half 1 == 1 wrong
+//half 2 == correct
+//half 3 == correct
+//half 4 == correct
+//half 5 == correct
+
+
+
+
+
+
+
+

book/Planet/_.kind2

@@ -0,0 +1,2 @@
+data Planet
+| new (pos: V2) (vel: V2) (rad: U48) : Planet

book/Planet/draw.kind2

@@ -0,0 +1,23 @@
+/// Draws a Planet as a list of shapes.
+///
+/// This function creates a list of shapes representing the planet,
+/// including its position and velocity vector.
+///
+/// # Input
+///
+/// * `planet` - The Planet to be drawn
+///
+/// # Output
+///
+/// A list of shapes representing the drawn Planet
+
+draw
+- planet: Planet
+: (List Shape)
+
+match planet {
+  Planet/new:
+    let pos = (V2/div planet.pos (V2/new 1000 1000))
+    let rad = planet.rad
+    [(Shape/circle pos rad)]
+}

book/Planet/interact.kind2

@@ -0,0 +1,47 @@
+// this function implements gravity interaction
+// between two planets
+// it receives a pair of planets A and B
+// and returns the updated plane A
+// with its velocity changed based on their
+// squared distances (V2/sqr_dist).
+
+use Planet/{new}
+use V2/{add,sub,mul,div,neg,sqr_dist}
+
+interact
+- a: Planet
+- b: Planet
+: Planet
+
+match a {
+  new: match b {
+    new:
+      let dist  = (sqr_dist a.pos b.pos)
+      let force = (sub b.pos a.pos)
+      let force = (mul force (V2/new 1000000 1000000))
+      let force = (div force (V2/new dist dist))
+      let force = (mul force (V2/new a.rad a.rad))
+      let force = (div force (V2/new b.rad b.rad))
+      //let force = (div force (V2/new mass mass))
+      let b.vel = (add b.vel (neg force))
+      (new b.pos b.vel b.rad)
+  }
+}
+
+//dist     = 100_000
+//sqr_dist = 10_000_000_000
+
+
+//sun   = 200 200
+//earth = 400 200
+
+//sqrdist = 200 ** 2 = 40000
+
+
+//100 = 
+
+
+
+
+
+

book/Planet/interactions.kind2

@@ -0,0 +1,15 @@
+interactions
+- planets: (List Planet)
+- others: (List Planet) -> (List Planet)
+: (List Planet)
+
+match planets {
+  List/cons:
+    let head = planets.head
+    let tail = planets.tail
+    let head = (List/fold _ _ Planet/interact head (others tail))
+    let tail = (interactions tail λk(others (List/cons _ head k)))
+    (List/cons _ head tail)
+  List/nil:
+    []
+}

book/Planet/match.kind2

@@ -0,0 +1,22 @@
+/// Provides a way to pattern match on Planet values.
+///
+/// # Parameters
+///
+/// * `P` - The motive of the elimination, a type family indexed by Planet.
+///
+/// # Inputs
+///
+/// * `n` - The case for when the Planet is constructed with 'new'.
+/// * `p` - The Planet value to match on.
+///
+/// # Output
+///
+/// The result of the elimination, which has type `(P p)`.
+
+match
+- P: Planet -> *
+- n: ∀(pos: V2) ∀(vel: V2) ∀(rad: U48) (P (Planet/new pos vel rad))
+- p: Planet
+: (P p)
+
+(~p P n)

book/Planet/new.kind2

@@ -0,0 +1,19 @@
+/// Creates a new Planet.
+///
+/// # Input
+///
+/// * `pos` - The position of the planet (V2)
+/// * `vel` - The velocity of the planet (V2)
+/// * `rad` - The radius of the planet (U48)
+///
+/// # Output
+///
+/// A new Planet with the given position, velocity, and radius
+
+new
+- pos: V2
+- vel: V2
+- rad: U48
+: Planet
+
+~λP λnew (new pos vel rad)

book/Planet/tick.kind2

@@ -0,0 +1,11 @@
+tick
+- planet: Planet
+: Planet
+
+match planet {
+  Planet/new:
+    let pos = (V2/add planet.pos planet.vel)
+    let vel = planet.vel
+    let rad = planet.rad
+    (Planet/new pos vel rad)
+}

book/QuadTree/_.kind2

@@ -0,0 +1,14 @@
+/// Defines a QuadTree data structure for spatial partitioning.
+///
+/// # Parameters
+///
+/// * `A` - The type of data stored in the QuadTree
+///
+/// # Constructors
+///
+/// * `node` - An internal node with four children
+/// * `leaf` - A leaf node containing data
+
+data QuadTree <A: *>
+| node (nw: (QuadTree A)) (ne: (QuadTree A)) (sw: (QuadTree A)) (se: (QuadTree A))
+| leaf (xs: (List A))

book/QuadTree/del.kind2

@@ -0,0 +1,30 @@
+use QuadTree/{node,leaf}
+use Bits/{O,I,E}
+use Maybe/{some,none}
+
+del <A>
+- t: (QuadTree A)
+- x: Bits
+- y: Bits
+: (QuadTree A)
+
+let emp = (QuadTree/leaf _ [])
+
+match t {
+  node:
+    match x {
+      O: match y {
+        O: (QuadTree/node _ (del _ t.nw x.tail y.tail) t.ne t.sw t.se)
+        I: (QuadTree/node _ t.nw t.ne (del _ t.sw x.tail y.tail) t.se)
+        E: emp
+      }
+      I: match y {
+        O: (QuadTree/node _ t.nw (del _ t.ne x.tail y.tail) t.sw t.se)
+        I: (QuadTree/node _ t.nw t.ne t.sw (del _ t.se x.tail y.tail))
+        E: emp
+      }
+      E: emp
+    }
+  leaf:
+    emp
+}

book/QuadTree/draw/_.kind2

@@ -0,0 +1,42 @@
+/// Draws a QuadTree as a list of shapes.
+///
+/// This function recursively traverses the QuadTree and generates a list of shapes
+/// representing the structure of the tree. For internal nodes, it draws a square
+/// and recursively draws its four children. For leaf nodes, it draws a single square.
+///
+/// # Parameters
+///
+/// * `qt` - The QuadTree to be drawn.
+/// * `pos` - The position (V2) of the current node's center.
+/// * `rad` - The radius (half-width) of the current node.
+///
+/// # Returns
+///
+/// A list of shapes representing the drawn QuadTree.
+
+use List/{concat,flatten}
+use QuadTree/{node,leaf}
+use V2/new
+
+draw <A>
+- qt: (QuadTree A)
+- pos: V2
+- rad: U48
+: (List Shape)
+
+match qt {
+  node:
+    let half_r = (/ rad 2)
+    let nw_pos = (V2/new (- (V2/get_x pos) half_r) (+ (V2/get_y pos) half_r))
+    let ne_pos = (V2/new (+ (V2/get_x pos) half_r) (+ (V2/get_y pos) half_r))
+    let sw_pos = (V2/new (- (V2/get_x pos) half_r) (- (V2/get_y pos) half_r))
+    let se_pos = (V2/new (+ (V2/get_x pos) half_r) (- (V2/get_y pos) half_r))
+    let nw_rec = (draw A qt.nw nw_pos half_r)
+    let ne_rec = (draw A qt.ne ne_pos half_r)
+    let sw_rec = (draw A qt.sw sw_pos half_r)
+    let se_rec = (draw A qt.se se_pos half_r)
+    let square = (QuadTree/draw/area pos rad)
+    (List/flatten _ [ square nw_rec ne_rec sw_rec se_rec ])
+  leaf:
+    (QuadTree/draw/area pos rad)
+}

book/QuadTree/draw/area.kind2

@@ -0,0 +1,38 @@
+/// Draws the outline of a square area centered at a given position.
+///
+/// # Inputs
+///
+/// * `pos` - The center position of the square (V2 coordinate).
+/// * `rad` - The radius (half-width) of the square.
+///
+/// # Output
+///
+/// A list of `Shape`s representing the four sides of the square.
+
+use List/{cons,nil}
+
+area
+- pos: V2
+- rad: U48
+: (List Shape)
+
+let r = rad
+let x = (V2/get_x pos)
+let y = (V2/get_y pos)
+
+let top_lft = (V2/new (- x r) (+ y r))
+let top_rgt = (V2/new (+ x r) (+ y r))
+let bot_lft = (V2/new (- x r) (- y r))
+let bot_rgt = (V2/new (+ x r) (- y r))
+
+let top_side = (Shape/line top_lft top_rgt)
+let rgt_side = (Shape/line top_rgt bot_rgt)
+let bot_side = (Shape/line bot_rgt bot_lft)
+let lft_side = (Shape/line bot_lft top_lft)
+
+[
+  top_side
+  rgt_side
+  bot_side
+  lft_side
+]

book/QuadTree/foo/_.kind2

@@ -0,0 +1,3 @@
+foo : U48
+
+42

book/QuadTree/get.kind2

@@ -0,0 +1,27 @@
+use QuadTree/{node,leaf}
+use Bits/{O,I,E}
+use Maybe/{some,none}
+
+get <A>
+- t: (QuadTree A)
+- x: Bits
+- y: Bits
+: (List A)
+
+match t {
+  node:
+    match x {
+      O: match y {
+        O: (get _ t.nw x.tail y.tail)
+        I: (get _ t.sw x.tail y.tail)
+        E: []
+      }
+      I: match y {
+        O: (get _ t.ne x.tail y.tail)
+        I: (get _ t.se x.tail y.tail)
+        E: []
+      }
+      E: []
+    }
+  leaf: t.xs
+}

book/QuadTree/is_empty.kind2

@@ -0,0 +1,26 @@
+/// Checks if a QuadTree is an empty leaf
+///
+/// # Parameters
+///
+/// * `A` - The type of data stored in the QuadTree
+///
+/// # Input
+///
+/// * `tree` - The QuadTree to check
+///
+/// # Output
+///
+/// Returns `true` if the QuadTree is an empty leaf, `false` otherwise
+
+use QuadTree/{node,leaf}
+use Bool/{true,false}
+use List/is_empty
+
+is_empty <A>
+- tree: (QuadTree A)
+: Bool
+
+match tree {
+  node: false
+  leaf: (List/is_empty _ tree.xs)
+}

book/QuadTree/leaf.kind2

@@ -0,0 +1,19 @@
+/// Creates a leaf node in a QuadTree.
+///
+/// # Parameters
+///
+/// * `A` - The type of data stored in the QuadTree
+///
+/// # Input
+///
+/// * `data` - The data to be stored in the leaf node
+///
+/// # Output
+///
+/// A new QuadTree leaf containing the given data
+
+leaf <A>
+- xs: (List A)
+: (QuadTree A)
+
+~λP λnode λleaf (leaf xs)

book/QuadTree/lemma/del_set_id.kind2

@@ -0,0 +1,11 @@
+del_set_id <A>
+- t: (QuadTree A)
+- x: Bits
+- y: Bits
+- v: A
+: (Equal (QuadTree A)
+  (QuadTree/nrm _ (QuadTree/del A (QuadTree/set A t x y) x y))
+  t)
+
+?body
+  

book/QuadTree/match.kind2

@@ -0,0 +1,27 @@
+/// Provides a way to pattern match on QuadTree values.
+///
+/// # Parameters
+///
+/// * `A` - The type of data stored in the QuadTree
+///
+/// # Inputs
+///
+/// * `P` - The motive of the elimination, a type family indexed by QuadTree A.
+/// * `n` - The case for when the QuadTree is a node.
+/// * `l` - The case for when the QuadTree is a leaf.
+/// * `t` - The QuadTree value to match on.
+///
+/// # Output
+///
+/// The result of the elimination, which has type `(P t)`.
+
+use QuadTree/{node,leaf}
+
+match <A>
+- P: (QuadTree A) -> *
+- n: ∀(nw: (QuadTree A)) ∀(ne: (QuadTree A)) ∀(sw: (QuadTree A)) ∀(se: (QuadTree A)) (P (QuadTree/node A nw ne sw se))
+- l: ∀(data: (List A)) (P (QuadTree/leaf A data))
+- t: (QuadTree A)
+: (P t)
+
+(~t P n l)

book/QuadTree/node.kind2

@@ -0,0 +1,25 @@
+/// Creates a node in a QuadTree.
+///
+/// # Parameters
+///
+/// * `A` - The type of data stored in the QuadTree
+///
+/// # Input
+///
+/// * `nw` - The northwest quadrant (QuadTree A)
+/// * `ne` - The northeast quadrant (QuadTree A)
+/// * `sw` - The southwest quadrant (QuadTree A)
+/// * `se` - The southeast quadrant (QuadTree A)
+///
+/// # Output
+///
+/// A new QuadTree node containing the four given quadrants
+
+node <A>
+- nw: (QuadTree A)
+- ne: (QuadTree A)
+- sw: (QuadTree A)
+- se: (QuadTree A)
+: (QuadTree A)
+
+~λP λnode λleaf (node nw ne sw se)

book/QuadTree/nrm.kind2

@@ -0,0 +1,25 @@
+use QuadTree/{node,leaf}
+use Bool/{and}
+use List/is_empty
+
+nrm <A>
+- tree: (QuadTree A)
+: (QuadTree A)
+
+match tree {
+  node:
+    let nw_rec = (nrm _ tree.nw)
+    let ne_rec = (nrm _ tree.ne)
+    let sw_rec = (nrm _ tree.sw)
+    let se_rec = (nrm _ tree.se)
+    let nw_emp = (QuadTree/is_empty _ nw_rec)
+    let ne_emp = (QuadTree/is_empty _ ne_rec)
+    let sw_emp = (QuadTree/is_empty _ sw_rec)
+    let se_emp = (QuadTree/is_empty _ se_rec)
+    let qt_emp = (and (and nw_emp ne_emp) (and sw_emp se_emp))
+    (Bool/if (QuadTree A) qt_emp
+      (QuadTree/leaf _ [])
+      (QuadTree/node _ nw_rec ne_rec sw_rec se_rec))
+  leaf:
+    tree
+}

book/QuadTree/set.kind2

@@ -0,0 +1,52 @@
+use QuadTree/{node,leaf}
+use Bits/{O,I,E}
+use Maybe/{some,none}
+
+set <A>
+- t: (QuadTree A)
+- x: Bits
+- y: Bits
+- v: A
+: (QuadTree A)
+
+let emp = (QuadTree/leaf _ [])
+
+match t {
+  node:
+    match x {
+      O: match y {
+        O: (QuadTree/node _ (set _ t.nw x.tail y.tail v) t.ne t.sw t.se)
+        I: (QuadTree/node _ t.nw t.ne (set _ t.sw x.tail y.tail v) t.se)
+        E: emp // unreachable
+      }
+      I: match y {
+        O: (QuadTree/node _ t.nw (set _ t.ne x.tail y.tail v) t.sw t.se)
+        I: (QuadTree/node _ t.nw t.ne t.sw (set _ t.se x.tail y.tail v))
+        E: emp // unreachable
+      }
+      E: match y {
+        O: emp // unreachable
+        I: emp // unreachable
+        E: emp // unreachable
+      }
+    }
+  leaf:
+    match x {
+      O: match y {
+        O: (QuadTree/node _ (set _ emp x.tail y.tail v) emp emp emp)
+        I: (QuadTree/node _ emp emp (set _ emp x.tail y.tail v) emp)
+        E: emp // unreachable
+      }
+      I: match y {
+        O: (QuadTree/node _ emp (set _ emp x.tail y.tail v) emp emp)
+        I: (QuadTree/node _ emp emp emp (set _ emp x.tail y.tail v))
+        E: emp // unreachable
+      }
+      E: match y {
+        O: emp // unreachable
+        I: emp // unreachable
+        E: (QuadTree/leaf _ (List/cons _ v t.xs)) // unreachable
+      }
+    }
+}
+

book/RGB/B.kind2

@@ -0,0 +1,10 @@
+/// Constructs the Blue color in the RGB color space.
+///
+/// # Output
+///
+/// The Blue color representation in RGB.
+
+B
+: RGB
+
+~λP λR λG λB B

book/RGB/G.kind2

@@ -0,0 +1,10 @@
+/// Constructs the Green color in the RGB color space.
+///
+/// # Output
+///
+/// The Green color representation in RGB.
+
+G
+: RGB
+
+~λP λR λG λB G

book/RGB/R.kind2

@@ -0,0 +1,10 @@
+/// Constructs the Red color in the RGB color space.
+///
+/// # Output
+///
+/// The Red color representation in RGB.
+
+R
+: RGB
+
+~λP λR λG λB R

book/RGB/_.kind2

@@ -0,0 +1,12 @@
+/// Defines the RGB color space with three basic colors.
+///
+/// # Constructors
+///
+/// * `R` - Represents the Red color.
+/// * `G` - Represents the Green color.
+/// * `B` - Represents the Blue color.
+
+data RGB
+| R
+| G
+| B

book/RGB/match.kind2

@@ -0,0 +1,25 @@
+/// Provides a way to pattern match on RGB colors.
+///
+/// # Inputs
+///
+/// * `P` - The motive of the elimination, a type family indexed by RGB.
+/// * `r` - The case for when the color is Red.
+/// * `g` - The case for when the color is Green.
+/// * `b` - The case for when the color is Blue.
+/// * `color` - The RGB color to match on.
+///
+/// # Output
+///
+/// The result of the elimination, which has type `(P color)`.
+
+use RGB/{R,G,B}
+
+match
+- P: RGB -> *
+- r: (P R)
+- g: (P G)
+- b: (P B)
+- color: RGB
+: (P color)
+
+(~color P r g b)

book/RGB/show.kind2

@@ -0,0 +1,21 @@
+/// Converts an RGB color to its string representation.
+///
+/// # Input
+///
+/// * `x` - The RGB color to convert.
+///
+/// # Output
+///
+/// A string representation of the RGB color.
+
+use RGB/{R,G,B}
+
+show
+- x: RGB
+: String
+
+match x {
+  R: "Red"   // Return "Red" for the Red color
+  G: "Green" // Return "Green" for the Green color
+  B: "Blue"  // Return "Blue" for the Blue color
+}

book/RGB/spin.kind2

@@ -0,0 +1,21 @@
+/// Spins the RGB color to the next one in the sequence.
+///
+/// # Input
+///
+/// * `color` - The current RGB color.
+///
+/// # Output
+///
+/// The next RGB color in the sequence (R -> G -> B -> R).
+
+use RGB/{R,G,B}
+
+spin
+- color: RGB
+: RGB
+
+match color {
+  R: G
+  G: B
+  B: R
+}

book/RGB/unspin.kind2

@@ -0,0 +1,21 @@
+/// Unspins the RGB color to the previous one in the sequence.
+///
+/// # Input
+///
+/// * `color` - The current RGB color.
+///
+/// # Output
+///
+/// The previous RGB color in the sequence (R <- G <- B <- R).
+
+use RGB/{R,G,B}
+
+unspin
+- color: RGB
+: RGB
+
+match color {
+  R: B
+  G: R
+  B: G
+}

book/RGB/unspin_spec.kind2

@@ -0,0 +1,16 @@
+use RGB/{R,G,B,spin,unspin}
+use Equal/refl
+
+unspin_spec
+- x: RGB
+: (Equal RGB (unspin (spin x)) x)
+
+match x {
+  R: (refl RGB R)
+  G: (refl RGB G)
+  B: (refl RGB B)
+}
+
+//there is no way to complete this file
+
+//unless "unspin" is correct w.r.t. the spec

book/Shape/_.kind2

@@ -0,0 +1,13 @@
+// TASK:
+// create a Shape type that allows the user
+// to create simple shapes that can be rendered
+// on HTML5 Canvas
+// including:
+// - line (from / to)
+// - circle (pos / radius)
+// (only that for now)
+// uses the V2 type
+
+data Shape
+| line (ini: V2) (end: V2)
+| circle (pos: V2) (rad: U48)

book/Shape/circle.kind2

@@ -0,0 +1,17 @@
+/// Creates a circle shape.
+///
+/// # Input
+///
+/// * `pos` - The center position of the circle (V2)
+/// * `rad` - The radius of the circle (U48)
+///
+/// # Output
+///
+/// A Shape representing a circle with center `pos` and radius `rad`
+
+circle
+- pos: V2
+- rad: U48
+: Shape
+
+~λP λline λcircle (circle pos rad)

book/Shape/line.kind2

@@ -0,0 +1,17 @@
+/// Creates a line shape.
+///
+/// # Input
+///
+/// * `ini` - The initial point of the line (V2)
+/// * `end` - The end point of the line (V2)
+///
+/// # Output
+///
+/// A Shape representing a line from `ini` to `end`
+
+line
+- ini: V2
+- end: V2
+: Shape
+
+~λP λline λcircle (line ini end)

book/Solar/draw_planet.kind2

@@ -0,0 +1,11 @@
+draw_planet
+
+- planet: (Pair V2 V2)
+: (List Shape)
+
+match planet {
+  Pair/new:
+    let pos = planet.fst
+    let vel = planet.snd
+    ?a
+}

book/Solar/main.kind2

@@ -0,0 +1,36 @@
+use Bits/{O,I,E}
+use Shape/{circle,line}
+
+main: (App (List (Pair V2 V2)))
+
+use init =
+  let sun   = (Pair/new _ _ (V2/new 256000 256000) (V2/new 0 0))
+  let earth = (Pair/new _ _ (V2/new 300000 256000) (V2/new 1000 0))
+  [ sun earth ]
+
+use tick = λstate
+  state
+  //match state {
+    //V2/new: (V2/new (+ state.x 1) state.y)
+  //}
+
+use draw = λstate []
+  //(line (V2/new 50 50) (V2/new 100 100))
+  //(circle state 12)
+
+//use draw = λstate
+  //?draw
+  //(QuadTree/draw t (V2/new 256 256) 256) 
+
+use when = λkey λstate
+  state
+  //match state {
+    //V2/new:
+      //(U48/if _ (== key 'W') (V2/new state.x (- state.y 16))
+      //(U48/if _ (== key 'S') (V2/new state.x (+ state.y 16))
+      //(U48/if _ (== key 'A') (V2/new (- state.x 16) state.y)
+      //(U48/if _ (== key 'D') (V2/new (+ state.x 16) state.y)
+      //state))))
+  //}
+
+(App/new _ init tick draw when)

book/U48/if.kind2

@@ -1,3 +1,19 @@
+/// Conditional expression for U48 values.
+///
+/// # Parameters
+///
+/// * `P` - The type of the result.
+///
+/// # Inputs
+///
+/// * `x` - The U48 condition.
+/// * `t` - The value to return if the condition is non-zero.
+/// * `f` - The value to return if the condition is zero.
+///
+/// # Output
+///
+/// Returns `t` if `x` is non-zero, otherwise returns `f`.
+
 if <P>
 - x: U48
 - t: P
@@ -5,6 +21,6 @@ if <P>
 : P
 
 switch x {
-  0: t
-  _: f
-}
+  0: f
+  _: t
+}: P

book/U48/sqrt.kind2

@@ -0,0 +1 @@
+// TODO

book/U48/sqrt/go.kind2

@@ -0,0 +1,34 @@
+/// Performs the iterative step of the integer square root calculation using Newton's method.
+///
+/// This function implements the core logic of the integer square root algorithm,
+/// using Newton's method for successive approximations.
+///
+/// # Inputs
+///
+/// * `n` - The number for which we're calculating the square root.
+/// * `guess` - The current guess for the square root.
+/// * `prev_guess` - The previous guess, used to check for convergence.
+///
+/// # Output
+///
+/// Returns the calculated integer square root of `n`.
+///
+/// # Algorithm
+///
+/// 1. Calculate a new guess using the formula: (guess + n/guess) / 2
+/// 2. If the new guess equals the previous guess, we've converged; return the guess.
+/// 3. Otherwise, recurse with the new guess as the current guess and the old guess as the previous guess.
+
+// TODO: review
+
+go
+- n: U48
+- guess: U48
+- prev_guess: U48
+: U48
+
+let new_guess = (/ (+ guess (/ n guess)) 2)
+switch x = (== guess prev_guess) {
+  0: guess
+  _: (U48/sqrt/go n new_guess guess)
+}

book/U48/to_bits.kind2

@@ -0,0 +1,26 @@
+/// Converts a U48 number to its binary representation as Bits.
+///
+/// # Input
+///
+/// * `n` - The U48 number to convert.
+///
+/// # Output
+///
+/// The Bits representation of the input number.
+
+use Bits/{O,I,E}
+
+to_bits
+- d: U48
+- n: U48
+: Bits
+
+switch d {
+  0: E
+  _: let tail = (to_bits (- d 1) (/ n 2))
+     let bit  = (% n 2)
+     switch bit {
+       0: (O tail)
+       _: (I tail)
+     }
+}: Bits

book/V2/_.kind2

@@ -0,0 +1,13 @@
+/// Defines a 2D vector with U48 coordinates.
+///
+/// # Constructor
+///
+/// * `new` - Creates a new V2 vector with given x and y coordinates.
+///
+/// # Fields
+///
+/// * `x` - The x-coordinate (U48)
+/// * `y` - The y-coordinate (U48)
+
+data V2
+| new (x: U48) (y: U48)

book/V2/add.kind2

@@ -0,0 +1,23 @@
+/// Adds two V2 vectors.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector
+/// * `b` - The second V2 vector
+///
+/// # Output
+///
+/// A new V2 vector representing the sum of `a` and `b`
+
+use V2/{new}
+
+add
+- a: V2
+- b: V2
+: V2
+
+match a {
+  new: match b {
+    new: (new (+ a.x b.x) (+ a.y b.y))
+  }
+}

book/V2/div.kind2

@@ -0,0 +1,24 @@
+/// Divides two V2 vectors component-wise.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector (dividend)
+/// * `b` - The second V2 vector (divisor)
+///
+/// # Output
+///
+/// A new V2 vector representing the component-wise division of `a` by `b`
+/// Note: This function does not handle division by zero.
+
+use V2/{new}
+
+div
+- a: V2
+- b: V2
+: V2
+
+match a {
+  new: match b {
+    new: (new (/ a.x b.x) (/ a.y b.y))
+  }
+}

book/V2/dot.kind2

@@ -0,0 +1,23 @@
+/// Computes the dot product of two V2 vectors.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector
+/// * `b` - The second V2 vector
+///
+/// # Output
+///
+/// The dot product of `a` and `b` as a U48
+
+use V2/{new}
+
+dot
+- a: V2
+- b: V2
+: U48
+
+match a {
+  new: match b {
+    new: (+ (* a.x b.x) (* a.y b.y))
+  }
+}

book/V2/get_x.kind2

@@ -0,0 +1,19 @@
+/// Gets the x-coordinate of a V2 vector.
+///
+/// # Input
+///
+/// * `v` - The V2 vector
+///
+/// # Output
+///
+/// The x-coordinate of the vector as a U48
+
+use V2/{new}
+
+get_x
+- v: V2
+: U48
+
+match v {
+  new: v.x
+}

book/V2/get_y.kind2

@@ -0,0 +1,19 @@
+/// Gets the y-coordinate of a V2 vector.
+///
+/// # Input
+///
+/// * `v` - The V2 vector
+///
+/// # Output
+///
+/// The y-coordinate of the vector as a U48
+
+use V2/{new}
+
+get_y
+- v: V2
+: U48
+
+match v {
+  new: v.y
+}

book/V2/match.kind2

@@ -0,0 +1,22 @@
+/// Provides a way to pattern match on V2 vectors.
+///
+/// # Parameters
+///
+/// * `P` - The motive of the elimination.
+///
+/// # Inputs
+///
+/// * `n` - The function to apply in the case of a V2 vector.
+/// * `v` - The V2 vector to match on.
+///
+/// # Output
+///
+/// The result of the elimination.
+
+match
+- P: V2 -> *
+- n: ∀(x: U48) ∀(y: U48) (P (V2/new x y))
+- v: V2
+: (P v)
+
+(~v P n)

book/V2/mul.kind2

@@ -0,0 +1,23 @@
+/// Multiplies two V2 vectors component-wise.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector
+/// * `b` - The second V2 vector
+///
+/// # Output
+///
+/// A new V2 vector representing the component-wise product of `a` and `b`
+
+use V2/{new}
+
+mul
+- a: V2
+- b: V2
+: V2
+
+match a {
+  new: match b {
+    new: (new (* a.x b.x) (* a.y b.y))
+  }
+}

book/V2/neg.kind2

@@ -0,0 +1,19 @@
+/// Negates a V2 vector.
+///
+/// # Input
+///
+/// * `v` - The V2 vector to negate
+///
+/// # Output
+///
+/// A new V2 vector with negated coordinates
+
+use V2/{new}
+
+neg
+- v: V2
+: V2
+
+match v {
+  new: (new (- 0 v.x) (- 0 v.y))
+}

book/V2/new.kind2

@@ -0,0 +1,17 @@
+/// Creates a new V2 vector.
+///
+/// # Input
+///
+/// * `x` - The x-coordinate (U48)
+/// * `y` - The y-coordinate (U48)
+///
+/// # Output
+///
+/// A new V2 vector with the given coordinates
+
+new
+- x: U48
+- y: U48
+: V2
+
+~λP λnew (new x y)

book/V2/sqr_dist.kind2

@@ -0,0 +1,26 @@
+/// Calculates the squared distance between two V2 vectors.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector
+/// * `b` - The second V2 vector
+///
+/// # Output
+///
+/// The squared distance between `a` and `b` as a U48
+
+use V2/{new}
+
+sqr_dist
+- a: V2
+- b: V2
+: U48
+
+match a {
+  new: match b {
+    new:
+      let dx = (- a.x b.x)
+      let dy = (- a.y b.y)
+      (+ (* dx dx) (* dy dy))
+  }
+}

book/V2/sub.kind2

@@ -0,0 +1,23 @@
+/// Subtracts two V2 vectors.
+///
+/// # Input
+///
+/// * `a` - The first V2 vector
+/// * `b` - The second V2 vector
+///
+/// # Output
+///
+/// A new V2 vector representing the difference of `a` and `b`
+
+use V2/{new}
+
+sub
+- a: V2
+- b: V2
+: V2
+
+match a {
+  new: match b {
+    new: (new (- a.x b.x) (- a.y b.y))
+  }
+}

book/hello.kind2

@@ -0,0 +1,26 @@
+// Hello Circle
+
+use Shape/{circle,line}
+
+main: (App V2)
+
+use init = (V2/new 256 256)
+use tick = λstate
+  match state {
+    V2/new: (V2/new (+ state.x 1) state.y)
+  }
+use draw = λstate [
+  (line (V2/new 50 50) (V2/new 100 100))
+  (circle state 12)
+]
+use when = λkey λstate
+  match state {
+    V2/new:
+      (U48/if _ (== key 'W') (V2/new state.x (- state.y 16))
+      (U48/if _ (== key 'S') (V2/new state.x (+ state.y 16))
+      (U48/if _ (== key 'A') (V2/new (- state.x 16) state.y)
+      (U48/if _ (== key 'D') (V2/new (+ state.x 16) state.y)
+      state))))
+  }
+
+(App/new _ init tick draw when)

book/index.html

@@ -0,0 +1,18 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+  <meta charset="UTF-8">
+  <meta name="viewport" content="width=device-width, initial-scale=1.0">
+  <script src="rt.js"></script>
+  <script src="main.js"></script>
+  <title>Canvas Drawing</title>
+</head>
+<body>
+  <canvas
+    id="canvas"
+    width="512"
+    height="512"
+    style="border: 1px solid black;">
+  </canvas>
+</body>
+</html>

book/kind4.kind2

@@ -0,0 +1,11 @@
+use V2/{new,add,mul,dot}
+
+main
+
+let a = (new 5 6)
+let b = (new 10 20)
+// 10 * 5 + 6 * 20 = 170
+
+(dot a b)
+
+

book/main.js

@@ -0,0 +1,55 @@
+const App = (S_1) => null;
+const App_new = (S_1) => (init_2) => (tick_3) => (draw_4) => (when_5) => (P_6) => (new_7) => new_7(init_2)(tick_3)(draw_4)(when_5);
+const Bits = null;
+const Bits_E = (P_1) => (O_2) => (I_3) => (E_4) => E_4;
+const Bits_I = (tail_1) => (P_2) => (O_3) => (I_4) => (E_5) => I_4(tail_1);
+const Bits_O = (tail_1) => (P_2) => (O_3) => (I_4) => (E_5) => O_3(tail_1);
+const Bits_match = (P_1) => (o_2) => (i_3) => (e_4) => (b_5) => b_5(P_1)(o_2)(i_3)(e_4);
+const Bits_reverse = (bits_1) => Bits_reverse_go(bits_1)(Bits_E);
+const Bits_reverse_go = (bits_1) => (acc_2) => (() => { const bits_P_3 = null; return (() => { const bits_O_4 = (bits_tail_4) => Bits_reverse_go(bits_tail_4)(Bits_O(acc_2)); return (() => { const bits_I_5 = (bits_tail_5) => Bits_reverse_go(bits_tail_5)(Bits_I(acc_2)); return (() => { const bits_E_6 = acc_2; return Bits_match(bits_P_3)(bits_O_4)(bits_I_5)(bits_E_6)(bits_1); })(); })(); })(); })();
+const Char = null;
+const List = (T_1) => null;
+const List_concat = (T_1) => (xs_2) => (ys_3) => (() => { const xs_P_4 = null; return (() => { const xs_cons_5 = (xs_head_5) => (xs_tail_6) => List_cons(null)(xs_head_5)(List_concat(null)(xs_tail_6)(ys_3)); return (() => { const xs_nil_6 = ys_3; return List_match(null)(xs_P_4)(xs_cons_5)(xs_nil_6)(xs_2); })(); })(); })();
+const List_cons = (T_1) => (head_2) => (tail_3) => (P_4) => (cons_5) => (nil_6) => cons_5(head_2)(tail_3);
+const List_flatten = (T_1) => (xss_2) => (() => { const xss_P_3 = null; return (() => { const xss_cons_4 = (xss_head_4) => (xss_tail_5) => List_concat(null)(xss_head_4)(List_flatten(null)(xss_tail_5)); return (() => { const xss_nil_5 = List_nil(null); return List_match(null)(xss_P_3)(xss_cons_4)(xss_nil_5)(xss_2); })(); })(); })();
+const List_fold = (A_1) => (P_2) => (c_3) => (n_4) => (xs_5) => (() => { const xs_P_6 = null; return (() => { const xs_cons_7 = (xs_head_7) => (xs_tail_8) => c_3(xs_head_7)(List_fold(null)(P_2)(c_3)(n_4)(xs_tail_8)); return (() => { const xs_nil_8 = n_4; return List_match(null)(xs_P_6)(xs_cons_7)(xs_nil_8)(xs_5); })(); })(); })();
+const List_map = (A_1) => (B_2) => (xs_3) => (fn_4) => (() => { const xs_P_5 = null; return (() => { const xs_cons_6 = (xs_head_6) => (xs_tail_7) => (() => { const head_8 = fn_4(xs_head_6); return (() => { const tail_9 = List_map(null)(null)(xs_tail_7)(fn_4); return List_cons(null)(head_8)(tail_9); })(); })(); return (() => { const xs_nil_7 = List_nil(null); return List_match(null)(xs_P_5)(xs_cons_6)(xs_nil_7)(xs_3); })(); })(); })();
+const List_match = (A_1) => (P_2) => (c_3) => (n_4) => (xs_5) => xs_5(P_2)(c_3)(n_4);
+const List_nil = (T_1) => (P_2) => (cons_3) => (nil_4) => nil_4;
+const Nat = null;
+const Nat_succ = (n_1) => (P_2) => (succ_3) => (zero_4) => succ_3(n_1);
+const Nat_zero = (P_1) => (succ_2) => (zero_3) => zero_3;
+const Planet = null;
+const Planet_draw = (planet_1) => (() => { const planet_P_2 = null; return (() => { const planet_new_3 = (planet_pos_3) => (planet_vel_4) => (planet_rad_5) => (() => { const pos_6 = V2_div(planet_pos_3)(V2_new(1000)(1000)); return (() => { const rad_7 = planet_rad_5; return List_cons(null)(Shape_circle(pos_6)(rad_7))(List_nil(null)); })(); })(); return Planet_match(planet_P_2)(planet_new_3)(planet_1); })(); })();
+const Planet_interact = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_pos_4) => (a_vel_5) => (a_rad_6) => (() => { const b_P_7 = null; return (() => { const b_new_8 = (b_pos_8) => (b_vel_9) => (b_rad_10) => (() => { const dist_11 = V2_sqr_dist(a_pos_4)(b_pos_8); return (() => { const force_12 = V2_sub(b_pos_8)(a_pos_4); return (() => { const force_13 = V2_mul(force_12)(V2_new(1000000)(1000000)); return (() => { const force_14 = V2_div(force_13)(V2_new(dist_11)(dist_11)); return (() => { const force_15 = V2_mul(force_14)(V2_new(a_rad_6)(a_rad_6)); return (() => { const force_16 = V2_div(force_15)(V2_new(b_rad_10)(b_rad_10)); return (() => { const b_vel_17 = V2_add(b_vel_9)(V2_neg(force_16)); return Planet_new(b_pos_8)(b_vel_17)(b_rad_10); })(); })(); })(); })(); })(); })(); })(); return Planet_match(b_P_7)(b_new_8)(b_2); })(); })(); return Planet_match(a_P_3)(a_new_4)(a_1); })(); })();
+const Planet_interactions = (planets_1) => (others_2) => (() => { const planets_P_3 = null; return (() => { const planets_cons_4 = (planets_head_4) => (planets_tail_5) => (() => { const head_6 = planets_head_4; return (() => { const tail_7 = planets_tail_5; return (() => { const head_8 = List_fold(null)(null)(Planet_interact)(head_6)(others_2(tail_7)); return (() => { const tail_9 = Planet_interactions(tail_7)((k_9) => others_2(List_cons(null)(head_8)(k_9))); return List_cons(null)(head_8)(tail_9); })(); })(); })(); })(); return (() => { const planets_nil_5 = List_nil(null); return List_match(null)(planets_P_3)(planets_cons_4)(planets_nil_5)(planets_1); })(); })(); })();
+const Planet_match = (P_1) => (n_2) => (p_3) => p_3(P_1)(n_2);
+const Planet_new = (pos_1) => (vel_2) => (rad_3) => (P_4) => (new_5) => new_5(pos_1)(vel_2)(rad_3);
+const Planet_tick = (planet_1) => (() => { const planet_P_2 = null; return (() => { const planet_new_3 = (planet_pos_3) => (planet_vel_4) => (planet_rad_5) => (() => { const pos_6 = V2_add(planet_pos_3)(planet_vel_4); return (() => { const vel_7 = planet_vel_4; return (() => { const rad_8 = planet_rad_5; return Planet_new(pos_6)(vel_7)(rad_8); })(); })(); })(); return Planet_match(planet_P_2)(planet_new_3)(planet_1); })(); })();
+const QuadTree = (A_1) => null;
+const QuadTree_draw = (A_1) => (qt_2) => (pos_3) => (rad_4) => (() => { const qt_P_5 = null; return (() => { const qt_node_6 = (qt_nw_6) => (qt_ne_7) => (qt_sw_8) => (qt_se_9) => (() => { const half_r_10 = Math.floor(rad_4 / 2); return (() => { const nw_pos_11 = V2_new(Math.floor(V2_get_x(pos_3) - half_r_10))(Math.floor(V2_get_y(pos_3) + half_r_10)); return (() => { const ne_pos_12 = V2_new(Math.floor(V2_get_x(pos_3) + half_r_10))(Math.floor(V2_get_y(pos_3) + half_r_10)); return (() => { const sw_pos_13 = V2_new(Math.floor(V2_get_x(pos_3) - half_r_10))(Math.floor(V2_get_y(pos_3) - half_r_10)); return (() => { const se_pos_14 = V2_new(Math.floor(V2_get_x(pos_3) + half_r_10))(Math.floor(V2_get_y(pos_3) - half_r_10)); return (() => { const nw_rec_15 = QuadTree_draw(A_1)(qt_nw_6)(nw_pos_11)(half_r_10); return (() => { const ne_rec_16 = QuadTree_draw(A_1)(qt_ne_7)(ne_pos_12)(half_r_10); return (() => { const sw_rec_17 = QuadTree_draw(A_1)(qt_sw_8)(sw_pos_13)(half_r_10); return (() => { const se_rec_18 = QuadTree_draw(A_1)(qt_se_9)(se_pos_14)(half_r_10); return (() => { const square_19 = QuadTree_draw_area(pos_3)(rad_4); return List_flatten(null)(List_cons(null)(square_19)(List_cons(null)(nw_rec_15)(List_cons(null)(ne_rec_16)(List_cons(null)(sw_rec_17)(List_cons(null)(se_rec_18)(List_nil(null))))))); })(); })(); })(); })(); })(); })(); })(); })(); })(); })(); return (() => { const qt_leaf_7 = (qt_xs_7) => QuadTree_draw_area(pos_3)(rad_4); return QuadTree_match(null)(qt_P_5)(qt_node_6)(qt_leaf_7)(qt_2); })(); })(); })();
+const QuadTree_draw_area = (pos_1) => (rad_2) => (() => { const r_3 = rad_2; return (() => { const x_4 = V2_get_x(pos_1); return (() => { const y_5 = V2_get_y(pos_1); return (() => { const top_lft_6 = V2_new(Math.floor(x_4 - r_3))(Math.floor(y_5 + r_3)); return (() => { const top_rgt_7 = V2_new(Math.floor(x_4 + r_3))(Math.floor(y_5 + r_3)); return (() => { const bot_lft_8 = V2_new(Math.floor(x_4 - r_3))(Math.floor(y_5 - r_3)); return (() => { const bot_rgt_9 = V2_new(Math.floor(x_4 + r_3))(Math.floor(y_5 - r_3)); return (() => { const top_side_10 = Shape_line(top_lft_6)(top_rgt_7); return (() => { const rgt_side_11 = Shape_line(top_rgt_7)(bot_rgt_9); return (() => { const bot_side_12 = Shape_line(bot_rgt_9)(bot_lft_8); return (() => { const lft_side_13 = Shape_line(bot_lft_8)(top_lft_6); return List_cons(null)(top_side_10)(List_cons(null)(rgt_side_11)(List_cons(null)(bot_side_12)(List_cons(null)(lft_side_13)(List_nil(null))))); })(); })(); })(); })(); })(); })(); })(); })(); })(); })(); })();
+const QuadTree_leaf = (A_1) => (xs_2) => (P_3) => (node_4) => (leaf_5) => leaf_5(xs_2);
+const QuadTree_match = (A_1) => (P_2) => (n_3) => (l_4) => (t_5) => t_5(P_2)(n_3)(l_4);
+const QuadTree_node = (A_1) => (nw_2) => (ne_3) => (sw_4) => (se_5) => (P_6) => (node_7) => (leaf_8) => node_7(nw_2)(ne_3)(sw_4)(se_5);
+const QuadTree_set = (A_1) => (t_2) => (x_3) => (y_4) => (v_5) => (() => { const emp_6 = QuadTree_leaf(null)(List_nil(null)); return (() => { const t_P_7 = null; return (() => { const t_node_8 = (t_nw_8) => (t_ne_9) => (t_sw_10) => (t_se_11) => (() => { const x_P_12 = null; return (() => { const x_O_13 = (x_tail_13) => (() => { const y_P_14 = null; return (() => { const y_O_15 = (y_tail_15) => QuadTree_node(null)(QuadTree_set(null)(t_nw_8)(x_tail_13)(y_tail_15)(v_5))(t_ne_9)(t_sw_10)(t_se_11); return (() => { const y_I_16 = (y_tail_16) => QuadTree_node(null)(t_nw_8)(t_ne_9)(QuadTree_set(null)(t_sw_10)(x_tail_13)(y_tail_16)(v_5))(t_se_11); return (() => { const y_E_17 = emp_6; return Bits_match(y_P_14)(y_O_15)(y_I_16)(y_E_17)(y_4); })(); })(); })(); })(); return (() => { const x_I_14 = (x_tail_14) => (() => { const y_P_15 = null; return (() => { const y_O_16 = (y_tail_16) => QuadTree_node(null)(t_nw_8)(QuadTree_set(null)(t_ne_9)(x_tail_14)(y_tail_16)(v_5))(t_sw_10)(t_se_11); return (() => { const y_I_17 = (y_tail_17) => QuadTree_node(null)(t_nw_8)(t_ne_9)(t_sw_10)(QuadTree_set(null)(t_se_11)(x_tail_14)(y_tail_17)(v_5)); return (() => { const y_E_18 = emp_6; return Bits_match(y_P_15)(y_O_16)(y_I_17)(y_E_18)(y_4); })(); })(); })(); })(); return (() => { const x_E_15 = (() => { const y_P_15 = null; return (() => { const y_O_16 = (y_tail_16) => emp_6; return (() => { const y_I_17 = (y_tail_17) => emp_6; return (() => { const y_E_18 = emp_6; return Bits_match(y_P_15)(y_O_16)(y_I_17)(y_E_18)(y_4); })(); })(); })(); })(); return Bits_match(x_P_12)(x_O_13)(x_I_14)(x_E_15)(x_3); })(); })(); })(); })(); return (() => { const t_leaf_9 = (t_xs_9) => (() => { const x_P_10 = null; return (() => { const x_O_11 = (x_tail_11) => (() => { const y_P_12 = null; return (() => { const y_O_13 = (y_tail_13) => QuadTree_node(null)(QuadTree_set(null)(emp_6)(x_tail_11)(y_tail_13)(v_5))(emp_6)(emp_6)(emp_6); return (() => { const y_I_14 = (y_tail_14) => QuadTree_node(null)(emp_6)(emp_6)(QuadTree_set(null)(emp_6)(x_tail_11)(y_tail_14)(v_5))(emp_6); return (() => { const y_E_15 = emp_6; return Bits_match(y_P_12)(y_O_13)(y_I_14)(y_E_15)(y_4); })(); })(); })(); })(); return (() => { const x_I_12 = (x_tail_12) => (() => { const y_P_13 = null; return (() => { const y_O_14 = (y_tail_14) => QuadTree_node(null)(emp_6)(QuadTree_set(null)(emp_6)(x_tail_12)(y_tail_14)(v_5))(emp_6)(emp_6); return (() => { const y_I_15 = (y_tail_15) => QuadTree_node(null)(emp_6)(emp_6)(emp_6)(QuadTree_set(null)(emp_6)(x_tail_12)(y_tail_15)(v_5)); return (() => { const y_E_16 = emp_6; return Bits_match(y_P_13)(y_O_14)(y_I_15)(y_E_16)(y_4); })(); })(); })(); })(); return (() => { const x_E_13 = (() => { const y_P_13 = null; return (() => { const y_O_14 = (y_tail_14) => emp_6; return (() => { const y_I_15 = (y_tail_15) => emp_6; return (() => { const y_E_16 = QuadTree_leaf(null)(List_cons(null)(v_5)(t_xs_9)); return Bits_match(y_P_13)(y_O_14)(y_I_15)(y_E_16)(y_4); })(); })(); })(); })(); return Bits_match(x_P_10)(x_O_11)(x_I_12)(x_E_13)(x_3); })(); })(); })(); })(); return QuadTree_match(null)(t_P_7)(t_node_8)(t_leaf_9)(t_2); })(); })(); })(); })();
+const Shape = null;
+const Shape_circle = (pos_1) => (rad_2) => (P_3) => (line_4) => (circle_5) => circle_5(pos_1)(rad_2);
+const Shape_line = (ini_1) => (end_2) => (P_3) => (line_4) => (circle_5) => line_4(ini_1)(end_2);
+const String = List(Char);
+const String_cons = (head_1) => (tail_2) => (P_3) => (cons_4) => (nil_5) => cons_4(head_1)(tail_2);
+const String_nil = (P_1) => (cons_2) => (nil_3) => nil_3;
+const U48_to_bits = (d_1) => (n_2) => (() => { const d_3_1 = d_1; switch (d_3_1) { case 0: return Bits_E; default: return ((d_3_1 => (() => { const d_1_4 = d_3_1; return (() => { const tail_5 = U48_to_bits(Math.floor(d_1 - 1))(Math.floor(n_2 / 2)); return (() => { const bit_6 = Math.floor(n_2 % 2); return (() => { const bit_7_1 = bit_6; switch (bit_7_1) { case 0: return Bits_O(tail_5); default: return ((bit_7_1 => (() => { const bit_1_8 = bit_7_1; return Bits_I(tail_5); })())((bit_7_1) - 1)); } })(); })(); })(); })())((d_3_1) - 1)); } })();
+const V2 = null;
+const V2_add = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_x_4) => (a_y_5) => (() => { const b_P_6 = null; return (() => { const b_new_7 = (b_x_7) => (b_y_8) => V2_new(Math.floor(a_x_4 + b_x_7))(Math.floor(a_y_5 + b_y_8)); return V2_match(b_P_6)(b_new_7)(b_2); })(); })(); return V2_match(a_P_3)(a_new_4)(a_1); })(); })();
+const V2_div = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_x_4) => (a_y_5) => (() => { const b_P_6 = null; return (() => { const b_new_7 = (b_x_7) => (b_y_8) => V2_new(Math.floor(a_x_4 / b_x_7))(Math.floor(a_y_5 / b_y_8)); return V2_match(b_P_6)(b_new_7)(b_2); })(); })(); return V2_match(a_P_3)(a_new_4)(a_1); })(); })();
+const V2_get_x = (v_1) => (() => { const v_P_2 = null; return (() => { const v_new_3 = (v_x_3) => (v_y_4) => v_x_3; return V2_match(v_P_2)(v_new_3)(v_1); })(); })();
+const V2_get_y = (v_1) => (() => { const v_P_2 = null; return (() => { const v_new_3 = (v_x_3) => (v_y_4) => v_y_4; return V2_match(v_P_2)(v_new_3)(v_1); })(); })();
+const V2_match = (P_1) => (n_2) => (v_3) => v_3(P_1)(n_2);
+const V2_mul = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_x_4) => (a_y_5) => (() => { const b_P_6 = null; return (() => { const b_new_7 = (b_x_7) => (b_y_8) => V2_new(Math.floor(a_x_4 * b_x_7))(Math.floor(a_y_5 * b_y_8)); return V2_match(b_P_6)(b_new_7)(b_2); })(); })(); return V2_match(a_P_3)(a_new_4)(a_1); })(); })();
+const V2_neg = (v_1) => (() => { const v_P_2 = null; return (() => { const v_new_3 = (v_x_3) => (v_y_4) => V2_new(Math.floor(0 - v_x_3))(Math.floor(0 - v_y_4)); return V2_match(v_P_2)(v_new_3)(v_1); })(); })();
+const V2_new = (x_1) => (y_2) => (P_3) => (new_4) => new_4(x_1)(y_2);
+const V2_sqr_dist = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_x_4) => (a_y_5) => (() => { const b_P_6 = null; return (() => { const b_new_7 = (b_x_7) => (b_y_8) => (() => { const dx_9 = Math.floor(a_x_4 - b_x_7); return (() => { const dy_10 = Math.floor(a_y_5 - b_y_8); return Math.floor(Math.floor(dx_9 * dx_9) + Math.floor(dy_10 * dy_10)); })(); })(); return V2_match(b_P_6)(b_new_7)(b_2); })(); })(); return V2_match(a_P_3)(a_new_4)(a_1); })(); })();
+const V2_sub = (a_1) => (b_2) => (() => { const a_P_3 = null; return (() => { const a_new_4 = (a_x_4) => (a_y_5) => (() => { const b_P_6 = null; return (() => { const b_new_7 = (b_x_7) => (b_y_8) => V2_new(Math.floor(a_x_4 - b_x_7))(Math.floor(a_y_5 - b_y_8)); return V2_match(b_P_6)(b_new_7)(b_2); })(); })(); return V2_match(a_P_3)(a_new_4)(a_1); })(); })();
+const main = (() => { const init_1 = (() => { const sun_1 = Planet_new(V2_new(256000)(256000))(V2_new(0)(0))(20); return (() => { const mercury_2 = Planet_new(V2_new(286000)(256000))(V2_new(0)(3700))(3); return (() => { const venus_3 = Planet_new(V2_new(296000)(256000))(V2_new(0)(3500))(3); return (() => { const earth_4 = Planet_new(V2_new(320000)(256000))(V2_new(0)(3000))(3); return (() => { const mars_5 = Planet_new(V2_new(352000)(256000))(V2_new(0)(2400))(3); return (() => { const jupiter_6 = Planet_new(V2_new(400000)(256000))(V2_new(0)(1300))(11); return (() => { const saturn_7 = Planet_new(V2_new(448000)(256000))(V2_new(0)(970))(9); return (() => { const uranus_8 = Planet_new(V2_new(488000)(256000))(V2_new(0)(680))(4); return (() => { const neptune_9 = Planet_new(V2_new(510000)(256000))(V2_new(0)(540))(4); return (() => { const moon_10 = Planet_new(V2_new(322000)(256000))(V2_new(0)(3100))(2); return List_cons(null)(sun_1)(List_cons(null)(mercury_2)(List_cons(null)(venus_3)(List_cons(null)(earth_4)(List_cons(null)(mars_5)(List_cons(null)(jupiter_6)(List_cons(null)(saturn_7)(List_cons(null)(uranus_8)(List_cons(null)(neptune_9)(List_cons(null)(moon_10)(List_nil(null))))))))))); })(); })(); })(); })(); })(); })(); })(); })(); })(); })(); return (() => { const tick_2 = (state_2) => (() => { const state_3 = List_map(null)(null)(state_2)(Planet_tick); return (() => { const state_4 = Planet_interactions(state_3)((x_4) => x_4); return state_4; })(); })(); return (() => { const draw_3 = (state_3) => (() => { const sun_pos_4 = (() => { const state_P_4 = (state_4) => V2; return (() => { const state_cons_5 = (state_head_5) => (state_tail_6) => (() => { const sun_7 = state_head_5; return (() => { const sun_P_8 = null; return (() => { const sun_new_9 = (sun_pos_9) => (sun_vel_10) => (sun_rad_11) => sun_pos_9; return Planet_match(sun_P_8)(sun_new_9)(sun_7); })(); })(); })(); return (() => { const state_nil_6 = V2_new(0)(0); return List_match(null)(state_P_4)(state_cons_5)(state_nil_6)(state_3); })(); })(); })(); return (() => { const qt_5 = QuadTree_leaf(null)(List_nil(null)); return (() => { const qt_6 = List_fold(null)(QuadTree(null))((p_6) => (qt_7) => (() => { const p_P_8 = null; return (() => { const p_new_9 = (p_pos_9) => (p_vel_10) => (p_rad_11) => (() => { const pp_12 = V2_sub(p_pos_9)(sun_pos_4); return (() => { const px_13 = Math.floor(Math.floor(V2_get_x(pp_12) / 1000) + 256); return (() => { const py_14 = Math.floor(512 - Math.floor(Math.floor(V2_get_y(pp_12) / 1000) + 256)); return (() => { const kx_15 = Bits_reverse(U48_to_bits(9)(px_13)); return (() => { const ky_16 = Bits_reverse(U48_to_bits(9)(py_14)); return (() => { const qt_17 = QuadTree_set(null)(qt_7)(kx_15)(ky_16)(42); return qt_17; })(); })(); })(); })(); })(); })(); return Planet_match(p_P_8)(p_new_9)(p_6); })(); })())(qt_5)(state_3); return (() => { const aa_7 = QuadTree_draw(null)(qt_6)(V2_new(256)(256))(256); return (() => { const pl_8 = (() => { const state_P_8 = (state_8) => List(Shape); return (() => { const state_cons_9 = (state_head_9) => (state_tail_10) => List_flatten(null)(List_map(null)(null)(state_3)((planet_11) => (() => { const planet_P_12 = null; return (() => { const planet_new_13 = (planet_pos_13) => (planet_vel_14) => (planet_rad_15) => (() => { const pos_16 = V2_sub(planet_pos_13)(sun_pos_4); return (() => { const pos_17 = V2_add(pos_16)(V2_new(256000)(256000)); return (() => { const vel_18 = planet_vel_14; return (() => { const rad_19 = planet_rad_15; return (() => { const pnt_20 = Planet_new(pos_17)(vel_18)(rad_19); return Planet_draw(pnt_20); })(); })(); })(); })(); })(); return Planet_match(planet_P_12)(planet_new_13)(planet_11); })(); })())); return (() => { const state_nil_10 = List_nil(null); return List_match(null)(state_P_8)(state_cons_9)(state_nil_10)(state_3); })(); })(); })(); return List_concat(null)(aa_7)(pl_8); })(); })(); })(); })(); })(); return (() => { const when_4 = (key_4) => (state_5) => state_5; return App_new(null)(init_1)(tick_2)(draw_3)(when_4); })(); })(); })(); })();
+

book/main.kind2

@@ -1,13 +1,124 @@
 use Bits/{O,I,E}
-use Maybe/{none,some}
+use Shape/{circle,line}
 
-main
+main: (App (List Planet))
 
-let key = (O (O E))
-let val = 123
+//use init =
+  //let sun   = (Planet/new (V2/new 256000 256000) (V2/new 0 0) 30)
+  //let earth = (Planet/new (V2/new 450000 256000) (V2/new 0 2000) 20)
+  //let moon  = (Planet/new (V2/new 350000 256000) (V2/new 0 2000) 3)
+  //[ sun earth moon ]
 
-let map = (BMap/leaf _)
-let map = (BMap/set _ map key (some _ val))
-let map = (BMap/get _ map key)
+// PROBLEM:
+// the init list above was meant to represent the solar
+// system, in a canvas with 512000 x 512000 pixels, and
+// the sun in the center (256000 256000). sadly, it is
+// wrong. the moon and earth are misplaced, the sizes
+// are incorrect and the other planes are missing. this
+// only needs to have earth's moon, no other moon and
+// no other celestial body.
+// this should be done in a way such that Neptune is around
+// the edge of the canvas. pluto should be out because
+// nobody likes pluto
+// remember: every planet should be included in the
+// segment from x=256000 to x=512000, and their radiuses
+// should be from 1 to 20 (sun)
+// implement the corrected init below:
 
-val
+use init =
+  let sun     = (Planet/new (V2/new 256000 256000) (V2/new 0 0) 20)
+  let mercury = (Planet/new (V2/new 286000 256000) (V2/new 0 3700) 3)
+  let venus   = (Planet/new (V2/new 296000 256000) (V2/new 0 3500) 3)
+  let earth   = (Planet/new (V2/new 320000 256000) (V2/new 0 3000) 3)
+  let mars    = (Planet/new (V2/new 352000 256000) (V2/new 0 2400) 3)
+  let jupiter = (Planet/new (V2/new 400000 256000) (V2/new 0 1300) 11)
+  let saturn  = (Planet/new (V2/new 448000 256000) (V2/new 0 970) 9)
+  let uranus  = (Planet/new (V2/new 488000 256000) (V2/new 0 680) 4)
+  let neptune = (Planet/new (V2/new 510000 256000) (V2/new 0 540) 4)
+  let moon    = (Planet/new (V2/new 322000 256000) (V2/new 0 3100) 2)
+  [ sun mercury venus earth mars jupiter saturn uranus neptune moon ]
+
+use tick = λstate
+  let state = (List/map _ _ state Planet/tick)
+  let state = (Planet/interactions state λx(x))
+  state
+
+// FIXME: ugly code just to center the camera around the sun
+use draw = λstate
+
+  // Gets the sun (first planet) position
+  let sun_pos = match state {
+    List/nil: (V2/new 0 0)
+    List/cons: 
+      let sun = state.head
+      match sun {
+        Planet/new: sun.pos
+      }
+  }: V2 // FIXME: why cant infer this?
+
+  // Draws the QuadTree
+  let qt = (QuadTree/leaf U48 [])
+  let qt = (List/fold _ (QuadTree U48) λpλqt(match p {
+    Planet/new:
+      let pp = (V2/sub p.pos sun_pos)
+      let px = (+ (/ (V2/get_x pp) 1000) 256)
+      let py = (- 512 (+ (/ (V2/get_y pp) 1000) 256))
+      let kx = (Bits/reverse (U48/to_bits 9 px))
+      let ky = (Bits/reverse (U48/to_bits 9 py))
+      let qt = (QuadTree/set _ qt kx ky 42)
+      qt
+  }) qt state)
+
+  //let qt = (QuadTree/leaf U48 [])
+  //let kx = (Bits/reverse (U48/to_bits 9 255))
+  //let ky = (Bits/reverse (U48/to_bits 9 256))
+  //let qt = (QuadTree/set _ qt kx ky 42)
+  let aa = (QuadTree/draw _ qt (V2/new 256 256) 256)
+
+  // Draws the planets
+  let pl = match state {
+    List/nil: [] // unreachable
+    List/cons: (List/flatten _ (List/map _ _ state λplanet(
+      match planet {
+        Planet/new:
+          let pos = (V2/sub planet.pos sun_pos)
+          let pos = (V2/add pos (V2/new 256000 256000))
+          let vel = planet.vel
+          let rad = planet.rad
+          let pnt = (Planet/new pos vel rad)
+          (Planet/draw pnt)
+      }
+    )))
+  }: (List Shape)
+
+  (List/concat _ aa pl)
+  //aa
+
+
+//use draw = λstate
+  //?draw
+  //(QuadTree/draw t (V2/new 256 256) 256) 
+
+use when = λkey λstate
+  state
+  //match state {
+    //V2/new:
+      //(U48/if _ (== key 'W') (V2/new state.x (- state.y 16))
+      //(U48/if _ (== key 'S') (V2/new state.x (+ state.y 16))
+      //(U48/if _ (== key 'A') (V2/new (- state.x 16) state.y)
+      //(U48/if _ (== key 'D') (V2/new (+ state.x 16) state.y)
+      //state))))
+  //}
+
+(App/new _ init tick draw when)
+
+
+
+
+
+
+
+
+
+
+//Bend with types -> HVM -> WebGPU

book/main1.js

@@ -0,0 +1,136 @@
+//./App/_.kind2//
+//./Shape/_.kind2//
+//./List/_.kind2//
+
+const App = (S_1) => null;
+
+const App_new = (S_1) => (tick_2) => (draw_3) => (when_4) => (P_5) => (new_6) =>
+  new_6(tick_2)(draw_3)(when_4);
+
+const Char = null;
+
+const List = (T_1) => null;
+
+const List_cons = (T_1) => (head_2) => (tail_3) => (P_4) => (cons_5) => (nil_6) =>
+  cons_5(head_2)(tail_3);
+
+const List_nil = (T_1) => (P_2) => (cons_3) => (nil_4) =>
+  nil_4;
+
+const Nat = null;
+
+const Nat_succ = (n_1) => (P_2) => (succ_3) => (zero_4) =>
+  succ_3(n_1);
+
+const Nat_zero = (P_1) => (succ_2) => (zero_3) =>
+  zero_3;
+
+const Shape = null;
+
+const Shape_circle = (pos_1) => (rad_2) => (P_3) => (line_4) => (circle_5) =>
+  circle_5(pos_1)(rad_2);
+
+const Shape_line = (ini_1) => (end_2) => (P_3) => (line_4) => (circle_5) =>
+  line_4(ini_1)(end_2);
+
+const String = List(Char);
+
+const String_cons = (head_1) => (tail_2) => (P_3) => (cons_4) => (nil_5) =>
+  cons_4(head_1)(tail_2);
+
+const String_nil = (P_1) => (cons_2) => (nil_3) =>
+  nil_3;
+
+const V2 = null;
+
+const V2_new = (x_1) => (y_2) => (P_3) => (new_4) =>
+  new_4(x_1)(y_2);
+
+const main = (() => {
+  const tick_1 = (x__1) => 0;
+  return (() => {
+    const draw_2 = (state_2) =>
+      List_cons(null)(Shape_circle(V2_new(100)(300))(12))(List_nil(null));
+    return (() => {
+      const when_3 = (state_3) => (event_4) => state_3;
+      return App_new(null)(tick_1)(draw_2)(when_3);
+    })();
+  })();
+})();
+
+require("./rt.js");
+
+// TASK: write a TypeScript type for App, Shape, etc.
+
+// type V2 = {
+//   $: "new";
+//   x: number;
+//   y: number;
+// };
+// 
+// type Shape =
+//   | {$: "line"; ini: V2; end: V2; }
+//   | {$: "circle"; pos: V2; rad: number; };
+// 
+// type List<T>
+//   = { $: "cons"; head: T; tail: List<T>; }
+//   | { $: "nil"; };
+// 
+// type App<S> = {
+//   $: "new";
+//   tick: (state: S) => S;
+//   draw: (state: S) => List<Shape>;
+//   when: (state: S) => (event: number) => S;
+// };
+
+// write a JavaScript function called fn_draw(canvas, shapes)
+// that receives a canvas and an array of shapes (as a JSON)
+// and draws every shape in the correct position in the canvas
+
+// TODO: create a fn_when function that 
+
+
+var MAIN = App_to_JSON(main);
+var DRAW = MAIN.draw;
+
+var shapes = List_to_JSON(Shape_to_JSON, DRAW(0));
+//console.log(shapes);
+
+window.onload = () => {
+  console.log("->", shapes);
+
+  var canvas = document.getElementById('canvas');
+  fn_draw(canvas, shapes);
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

book/main2.kind2

@@ -0,0 +1,12 @@
+
+use Bits/{O,I,E}
+use Maybe/{none,some}
+
+main
+
+let key = (O (O E))
+let val = 123
+let map = (BMap/leaf _)
+let map = (BMap/set _ map key (some _ val))
+
+val

book/main3.kind2

@@ -0,0 +1,13 @@
+use Bits/{O,I,E}
+use Maybe/{none,some}
+
+main
+
+let key = (O (O E))
+let val = 123
+
+let map = (BMap/leaf _)
+let map = (BMap/set _ map key (some _ val))
+let map = (BMap/get _ map key)
+
+val

book/main4.kind2

@@ -0,0 +1,153 @@
+// PLEASE FORMAT THIS FILE BETTER
+// IMPROVE ITS INDENTATION
+// don't change anything else
+// ty <3
+
+const BMap = (A_1) => null;
+
+const BMap_get = (A_1) => (map_2) => (key_3) => (() => {
+  const key_P_4 = null;
+  return (() => {
+    const key_O_5 = (key_tail_5) => (() => {
+      const map_P_6 = null;
+      return (() => {
+        const map_node_7 = (map_lft_7) => (map_val_8) => (map_rgt_9) =>
+          BMap_get(null)(map_lft_7)(key_tail_5);
+        return (() => {
+          const map_leaf_8 = Maybe_none(null);
+          return BMap_match(null)(map_P_6)(map_node_7)(map_leaf_8)(map_2);
+        })();
+      })();
+    })();
+    return (() => {
+      const key_I_6 = (key_tail_6) => (() => {
+        const map_P_7 = null;
+        return (() => {
+          const map_node_8 = (map_lft_8) => (map_val_9) => (map_rgt_10) =>
+            BMap_get(null)(map_rgt_10)(key_tail_6);
+          return (() => {
+            const map_leaf_9 = Maybe_none(null);
+            return BMap_match(null)(map_P_7)(map_node_8)(map_leaf_9)(map_2);
+          })();
+        })();
+      })();
+      return (() => {
+        const key_E_7 = (() => {
+          const map_P_7 = null;
+          return (() => {
+            const map_node_8 = (map_lft_8) => (map_val_9) => (map_rgt_10) => map_val_9;
+            return (() => {
+              const map_leaf_9 = Maybe_none(null);
+              return BMap_match(null)(map_P_7)(map_node_8)(map_leaf_9)(map_2);
+            })();
+          })();
+        })();
+        return Bits_match(key_P_4)(key_O_5)(key_I_6)(key_E_7)(key_3);
+      })();
+    })();
+  })();
+})();
+
+const BMap_leaf = (A_1) => (P_2) => (node_3) => (leaf_4) => leaf_4;
+
+const BMap_match = (A_1) => (P_2) => (n_3) => (l_4) => (bm_5) => bm_5(P_2)(n_3)(l_4);
+
+const BMap_node = (A_1) => (lft_2) => (val_3) => (rgt_4) => (P_5) => (node_6) => (leaf_7) =>
+  node_6(lft_2)(val_3)(rgt_4);
+
+const BMap_set = (A_1) => (map_2) => (key_3) => (val_4) => (() => {
+  const key_P_5 = null;
+  return (() => {
+    const key_O_6 = (key_tail_6) => (() => {
+      const map_P_7 = null;
+      return (() => {
+        const map_node_8 = (map_lft_8) => (map_val_9) => (map_rgt_10) =>
+          BMap_node(null)(BMap_set(null)(map_lft_8)(key_tail_6)(val_4))(map_val_9)(map_rgt_10);
+        return (() => {
+          const map_leaf_9 = BMap_node(null)(BMap_set(null)(BMap_leaf(null))(key_tail_6)(val_4))(Maybe_none(null))(BMap_leaf(null));
+          return BMap_match(null)(map_P_7)(map_node_8)(map_leaf_9)(map_2);
+        })();
+      })();
+    })();
+    return (() => {
+      const key_I_7 = (key_tail_7) => (() => {
+        const map_P_8 = null;
+        return (() => {
+          const map_node_9 = (map_lft_9) => (map_val_10) => (map_rgt_11) =>
+            BMap_node(null)(map_lft_9)(map_val_10)(BMap_set(null)(map_rgt_11)(key_tail_7)(val_4));
+          return (() => {
+            const map_leaf_10 = BMap_node(null)(BMap_leaf(null))(Maybe_none(null))(BMap_set(null)(BMap_leaf(null))(key_tail_7)(val_4));
+            return BMap_match(null)(map_P_8)(map_node_9)(map_leaf_10)(map_2);
+          })();
+        })();
+      })();
+      return (() => {
+        const key_E_8 = BMap_node(null)(BMap_leaf(null))(val_4)(BMap_leaf(null));
+        return Bits_match(key_P_5)(key_O_6)(key_I_7)(key_E_8)(key_3);
+      })();
+    })();
+  })();
+})();
+
+const Bits = null;
+
+const Bits_E = (P_1) => (O_2) => (I_3) => (E_4) => E_4;
+
+const Bits_I = (tail_1) => (P_2) => (O_3) => (I_4) => (E_5) => I_4(tail_1);
+
+const Bits_O = (tail_1) => (P_2) => (O_3) => (I_4) => (E_5) => O_3(tail_1);
+
+const Bits_match = (P_1) => (o_2) => (i_3) => (e_4) => (b_5) => b_5(P_1)(o_2)(i_3)(e_4);
+
+const Char = null;
+
+const List = (T_1) => null;
+
+const List_cons = (T_1) => (head_2) => (tail_3) => (P_4) => (cons_5) => (nil_6) =>
+  cons_5(head_2)(tail_3);
+
+const List_nil = (T_1) => (P_2) => (cons_3) => (nil_4) => nil_4;
+
+const Maybe = (T_1) => null;
+
+const Maybe_none = (T_1) => (P_2) => (some_3) => (none_4) => none_4;
+
+const Maybe_some = (T_1) => (value_2) => (P_3) => (some_4) => (none_5) => some_4(value_2);
+
+const Nat = null;
+
+const Nat_succ = (n_1) => (P_2) => (succ_3) => (zero_4) => succ_3(n_1);
+
+const Nat_zero = (P_1) => (succ_2) => (zero_3) => zero_3;
+
+const String = List(Char);
+
+const String_cons = (head_1) => (tail_2) => (P_3) => (cons_4) => (nil_5) =>
+  cons_4(head_1)(tail_2);
+
+const String_nil = (P_1) => (cons_2) => (nil_3) => nil_3;
+
+const main = (() => {
+  const key_1 = Bits_O(Bits_O(Bits_E));
+  return (() => {
+    const val_2 = 123;
+    return (() => {
+      const map_3 = BMap_leaf(null);
+      return (() => {
+        const map_4 = BMap_set(null)(map_3)(key_1)(Maybe_some(null)(val_2));
+        return (() => {
+          const map_5 = BMap_get(null)(map_4)(key_1);
+          return val_2;
+        })();
+      })();
+    })();
+  })();
+})();
+
+
+console.log(main);
+
+
+
+
+

book/quads.kind2

@@ -0,0 +1,58 @@
+
+use Bits/{O,I,E}
+use Shape/{circle,line}
+
+//main: (App V2)
+main
+
+// Empty QuadTree
+let t = (QuadTree/leaf _ [])
+
+// Adds an entry
+let x = (I (I (I (I (I E)))))
+let y = (I (I (I (I (I E)))))
+let t = (QuadTree/set _ t x y 12)
+
+// Adds an entry
+let x = (O (O (O (O (O E)))))
+let y = (O (O (O (O (O E)))))
+let t = (QuadTree/set _ t x y 24)
+//let t = (QuadTree/set _ t x y 42)
+
+// Dels an entry
+let t = (QuadTree/del _ t x y)
+
+// Normalize the tree
+let t = (QuadTree/nrm _ t)
+
+//let v = (QuadTree/get _ t x y)
+//v
+
+use init = (V2/new 256 256)
+use tick = λstate
+  match state {
+    V2/new: (V2/new (+ state.x 1) state.y)
+  }
+
+//use draw = λstate [
+  //(line (V2/new 50 50) (V2/new 100 100))
+  //(circle state 12)
+//]
+
+use draw = λstate
+  (QuadTree/draw t (V2/new 256 256) 256) 
+
+use when = λkey λstate
+  match state {
+    V2/new:
+      (U48/if _ (== key 'W') (V2/new state.x (- state.y 16))
+      (U48/if _ (== key 'S') (V2/new state.x (+ state.y 16))
+      (U48/if _ (== key 'A') (V2/new (- state.x 16) state.y)
+      (U48/if _ (== key 'D') (V2/new (+ state.x 16) state.y)
+      state))))
+  }
+
+(App/new _ init tick draw when)
+
+
+

book/rt.js

@@ -0,0 +1,120 @@
+// type V2 = {
+//   $: "new";
+//   x: number;
+//   y: number;
+// };
+// 
+// type Shape =
+//   | {$: "line"; ini: V2; end: V2; }
+//   | {$: "circle"; pos: V2; rad: number; };
+// 
+// type List<T>
+//   = { $: "cons"; head: T; tail: List<T>; }
+//   | { $: "nil"; };
+// 
+// type App<S> = {
+//   $: "new";
+//   tick: (state: S) => S;
+//   draw: (state: S) => List<Shape>;
+//   when: (state: S) => (event: number) => S;
+// };
+
+V2_to_JSON = (v2) => {
+  return v2(null)(x => y => ({ $: "new", x: x, y: y }));
+};
+
+Shape_to_JSON = (shape) => {
+  return (shape(null)
+    (ini => end => ({ $: "line", ini: V2_to_JSON(ini), end: V2_to_JSON(end) }))
+    (pos => rad => ({ $: "circle", pos: V2_to_JSON(pos), rad: rad })));
+};
+
+List_to_JSON = (map, list) => { 
+  const result = [];
+  let current = list;
+  while (true) {
+    var is_nil = current(null)
+      (head => tail => {
+        result.push(map(head));
+        current = tail;
+        return false;
+      })
+      (true);
+    if (is_nil) {
+      break;
+    }
+  }
+  return result;
+};
+
+App_to_JSON = (app) => {
+  return app(null)(init => tick => draw => when => ({ $: "new", init, tick, draw, when }));
+};
+
+DRAW = (canvas, shapes) => {
+  console.log("hii", canvas, shapes);
+  const ctx = canvas.getContext('2d');
+  ctx.clearRect(0, 0, canvas.width, canvas.height);
+  shapes.forEach(shape => {
+    switch (shape.$) {
+      case 'line':
+        ctx.lineWidth = 0.2;
+        ctx.beginPath();
+        ctx.moveTo(shape.ini.x, shape.ini.y);
+        ctx.lineTo(shape.end.x, shape.end.y);
+        ctx.stroke();
+        break;
+      case 'circle':
+        //ctx.lineWidth = 1;
+        //ctx.beginPath();
+        //ctx.arc(shape.pos.x, shape.pos.y, shape.rad, 0, 2 * Math.PI);
+        //ctx.stroke();
+        //TODO: fill this with a black color
+        ctx.fillStyle = 'gray';
+        ctx.beginPath();
+        ctx.arc(shape.pos.x, shape.pos.y, shape.rad, 0, 2 * Math.PI);
+        ctx.fill();
+        break;
+    }
+  });
+};
+
+RENDER = () => {
+  //console.log(main);
+  //console.log(V2_to_JSON(state));
+  //console.log(canvas);
+  DRAW(CANVAS, List_to_JSON(Shape_to_JSON, APP.draw(STATE)));
+}
+
+if (typeof window !== "undefined") {
+  window.onload = () => {
+    CANVAS = document.getElementById('canvas');
+    APP    = App_to_JSON(main);
+    STATE  = APP.init;
+    RENDER();
+  };
+
+  TICK = () => {
+    STATE = APP.tick(STATE);
+    RENDER();
+  };
+  setInterval(TICK, 1000 / 30);
+
+  // implement a keyboard event handler
+  // when the user presses a key, it will call the global APP.when
+  // function and update the global state mutably
+  document.addEventListener('keydown', (event) => {
+    // Convert the key code to a number
+    const keyCode = event.keyCode || event.which;
+
+    console.log("->", keyCode);
+    
+    // Call the 'when' function of the APP with the current state and key code
+    STATE = APP.when(keyCode)(STATE);
+    console.log(V2_to_JSON(STATE));
+    
+    // Re-render the canvas with the updated state
+    RENDER();
+  });
+
+}

book/sqr_dist_test.kind2

@@ -0,0 +1,7 @@
+sqr_dist_test
+
+let a = (V2/new 10000 10000)
+let b = (V2/new 20000 20000)
+
+(V2/sqr_dist a b)
+

book/stuff.js

@@ -0,0 +1,14 @@
+const json = (bmap) => {
+  const map_P = null;
+  const map_node = (lft) => (val) => (rgt) => ({
+    type: 'node',
+    left: json(lft),
+    value: val(
+      (v) => ({ type: 'some', value: v }),
+      { type: 'none' }
+    ),
+    right: json(rgt)
+  });
+  const map_leaf = { type: 'leaf' };
+  return BMap_match(null)(map_P)(map_node)(map_leaf)(bmap);
+};

book/test_a.kind2

@@ -0,0 +1,4 @@
+test_a
+
+let n = 123
+(U48/to_bits n)

kjfsadkfj.bend

@@ -0,0 +1,2 @@
+def render(map, pixel, pos):
+  return ...

src/term/compile.rs

@@ -1,5 +1,4 @@
 use crate::{*};
-use std::collections::BTreeMap;
 
 // Kind -> HVM2
 // ------------
@@ -212,7 +211,10 @@ impl Term {
 
   pub fn to_js(&self) -> String {
     let mut term = self.clone();
-    term.sanitize(&mut BTreeMap::new(), &mut 0);
+    //println!("OVERSHADOW:");
+    //println!("{}", term.show());
+    term.overshadow(&im::HashMap::new(), &mut 0);
+    //println!("{}", term.show());
     //term.desugar();
     //term.expand_implicits(im::Vector::new(), &BTreeMap::new());
     term.to_js_go()
@@ -286,7 +288,7 @@ impl Term {
   }
 
   pub fn to_js_name(name: &str) -> String {
-    name.replace("/", "_").replace(".","_")
+    name.replace("/", "_").replace(".","_").replace("-","_")
   }
 }
 

src/term/mod.rs

@@ -171,76 +171,167 @@ impl Term {
   // On binders, add a mapping: name => name_{depth}
   // On variables, just retrieve
   // Receive a mutable term
-  pub fn sanitize(&mut self, name_map: &mut BTreeMap<String, String>, depth: &mut u64) {
+  
+  //pub fn overshadow(&mut self, name_map: &mut BTreeMap<String, String>, depth: &mut u64) {
+    //match self {
+      //Term::All { era: _, nam, inp, bod } => {
+        //inp.overshadow(name_map, depth);
+        //*depth += 1;
+        //let new_name = format!("{}_{}", nam, depth);
+        //name_map.insert(nam.clone(), new_name.clone());
+        //*nam = new_name;
+        //bod.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::Lam { era: _, nam, bod } => {
+        //*depth += 1;
+        //let new_name = format!("{}_{}", nam, depth);
+        //name_map.insert(nam.clone(), new_name.clone());
+        //*nam = new_name;
+        //bod.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::App { era: _, fun, arg } => {
+        //fun.overshadow(name_map, depth);
+        //arg.overshadow(name_map, depth);
+      //},
+      //Term::Ann { chk: _, val, typ } => {
+        //val.overshadow(name_map, depth);
+        //typ.overshadow(name_map, depth);
+      //},
+      //Term::Slf { nam, typ, bod } => {
+        //typ.overshadow(name_map, depth);
+        //*depth += 1;
+        //let new_name = format!("{}_{}", nam, depth);
+        //name_map.insert(nam.clone(), new_name.clone());
+        //*nam = new_name;
+        //bod.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::Ins { val } => {
+        //val.overshadow(name_map, depth);
+      //},
+      //Term::Op2 { opr: _, fst, snd } => {
+        //fst.overshadow(name_map, depth);
+        //snd.overshadow(name_map, depth);
+      //},
+      //Term::Swi { nam, x, z, s, p } => {
+        //x.overshadow(name_map, depth);
+        //z.overshadow(name_map, depth);
+        //*depth += 1;
+        //let new_name = format!("{}_{}-1", nam, depth);
+        //name_map.insert(format!("{}-1",nam), new_name.clone());
+        //*nam = new_name;
+        //s.overshadow(name_map, depth);
+        //p.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::Let { nam, val, bod } => {
+        //val.overshadow(name_map, depth);
+        //*depth += 1;
+        //let new_name = format!("{}_{}", nam, depth);
+        //name_map.insert(nam.clone(), new_name.clone());
+        //*nam = new_name;
+        //bod.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::Use { nam, val, bod } => {
+        //val.overshadow(name_map, depth);
+        //*depth += 1;
+        //let new_name = format!("{}_{}", nam, depth);
+        //name_map.insert(nam.clone(), new_name.clone());
+        //*nam = new_name;
+        //bod.overshadow(name_map, depth);
+        //*depth -= 1;
+      //},
+      //Term::Var { nam } => {
+        //if let Some(new_name) = name_map.get(nam) {
+          //*nam = new_name.clone();
+        //}
+      //},
+      //Term::Src { src: _, val } => {
+        //val.overshadow(name_map, depth);
+      //},
+      //_ => {}
+    //}
+  //}
+  
+  // this function has a bug:
+  // it uses a mutable map instead of an immutable one to add new variables to the context
+  // it should use an immutable one like the expand_implicits function
+  // refactor it to fix that bug
+  // do it now
+  
+  pub fn overshadow(&mut self, name_map: &im::HashMap<String, String>, depth: &mut u64) {
     match self {
       Term::All { era: _, nam, inp, bod } => {
-        inp.sanitize(name_map, depth);
+        inp.overshadow(name_map, depth);
         *depth += 1;
         let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_map = name_map.update(nam.clone(), new_name.clone());
         *nam = new_name;
-        bod.sanitize(name_map, depth);
+        bod.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::Lam { era: _, nam, bod } => {
         *depth += 1;
         let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_map = name_map.update(nam.clone(), new_name.clone());
         *nam = new_name;
-        bod.sanitize(name_map, depth);
+        bod.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::App { era: _, fun, arg } => {
-        fun.sanitize(name_map, depth);
-        arg.sanitize(name_map, depth);
+        fun.overshadow(name_map, depth);
+        arg.overshadow(name_map, depth);
       },
       Term::Ann { chk: _, val, typ } => {
-        val.sanitize(name_map, depth);
-        typ.sanitize(name_map, depth);
+        val.overshadow(name_map, depth);
+        typ.overshadow(name_map, depth);
       },
       Term::Slf { nam, typ, bod } => {
-        typ.sanitize(name_map, depth);
+        typ.overshadow(name_map, depth);
         *depth += 1;
         let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_map = name_map.update(nam.clone(), new_name.clone());
         *nam = new_name;
-        bod.sanitize(name_map, depth);
+        bod.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::Ins { val } => {
-        val.sanitize(name_map, depth);
+        val.overshadow(name_map, depth);
       },
       Term::Op2 { opr: _, fst, snd } => {
-        fst.sanitize(name_map, depth);
-        snd.sanitize(name_map, depth);
+        fst.overshadow(name_map, depth);
+        snd.overshadow(name_map, depth);
       },
       Term::Swi { nam, x, z, s, p } => {
-        x.sanitize(name_map, depth);
-        z.sanitize(name_map, depth);
+        x.overshadow(name_map, depth);
+        z.overshadow(name_map, depth);
         *depth += 1;
-        let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_name = format!("{}_{}-1", nam, depth);
+        let new_map = name_map.update(format!("{}-1",nam), new_name.clone());
         *nam = new_name;
-        s.sanitize(name_map, depth);
-        p.sanitize(name_map, depth);
+        s.overshadow(&new_map, depth);
+        p.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::Let { nam, val, bod } => {
-        val.sanitize(name_map, depth);
+        val.overshadow(name_map, depth);
         *depth += 1;
         let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_map = name_map.update(nam.clone(), new_name.clone());
         *nam = new_name;
-        bod.sanitize(name_map, depth);
+        bod.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::Use { nam, val, bod } => {
-        val.sanitize(name_map, depth);
+        val.overshadow(name_map, depth);
         *depth += 1;
         let new_name = format!("{}_{}", nam, depth);
-        name_map.insert(nam.clone(), new_name.clone());
+        let new_map = name_map.update(nam.clone(), new_name.clone());
         *nam = new_name;
-        bod.sanitize(name_map, depth);
+        bod.overshadow(&new_map, depth);
         *depth -= 1;
       },
       Term::Var { nam } => {
@@ -249,7 +340,7 @@ impl Term {
         }
       },
       Term::Src { src: _, val } => {
-        val.sanitize(name_map, depth);
+        val.overshadow(name_map, depth);
       },
       _ => {}
     }