diff --git a/TODO b/TODO new file mode 100644 index 00000000..58a78080 --- /dev/null +++ b/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 | | | | | +-----|---|-------|-------|--------| +| | | +| | | +| | | +| | | +| | | +| | | +-----------------|----------------- diff --git a/book/App/_.kind2 b/book/App/_.kind2 new file mode 100644 index 00000000..858ea3f4 --- /dev/null +++ b/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 +| new + (init: S) + (tick: S -> S) + (draw: S -> (List Shape)) + (when: U48 -> S -> S) diff --git a/book/App/new.kind2 b/book/App/new.kind2 new file mode 100644 index 00000000..1ed23047 --- /dev/null +++ b/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 +- 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) diff --git a/book/Bits/reverse.kind2 b/book/Bits/reverse.kind2 new file mode 100644 index 00000000..06f69060 --- /dev/null +++ b/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) diff --git a/book/Bits/reverse/go.kind2 b/book/Bits/reverse/go.kind2 new file mode 100644 index 00000000..3a7b34e1 --- /dev/null +++ b/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 +} + diff --git a/book/List/concat.kind2 b/book/List/concat.kind2 index fd6fcc4c..0488a6d1 100644 --- a/book/List/concat.kind2 +++ b/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 @@ -6,6 +21,10 @@ concat : (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 } diff --git a/book/List/flatten.kind2 b/book/List/flatten.kind2 new file mode 100644 index 00000000..0ad637c8 --- /dev/null +++ b/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 +- xss: (List (List T)) +: (List T) + +match xss { + cons: (List/concat _ xss.head (flatten _ xss.tail)) + nil: (nil _) +} diff --git a/book/List/head.kind2 b/book/List/head.kind2 new file mode 100644 index 00000000..cffcbd8f --- /dev/null +++ b/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 +- xs: (List A) +: (Maybe A) + +match xs { + cons: (some _ xs.head) + nil: (none _) +} diff --git a/book/List/is_empty.kind2 b/book/List/is_empty.kind2 new file mode 100644 index 00000000..75df0e8f --- /dev/null +++ b/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 +- xs: (List A) +: Bool + +match xs { + cons: false + nil: true +} diff --git a/book/List/tail.kind2 b/book/List/tail.kind2 new file mode 100644 index 00000000..c6f63165 --- /dev/null +++ b/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 +- xs: (List A) +: (Maybe (List A)) + +match xs { + cons: (some _ xs.tail) + nil: (none _) +} diff --git a/book/Nat/half.kind2 b/book/Nat/half.kind2 index a3b04ded..a2cbfe0f 100644 --- a/book/Nat/half.kind2 +++ b/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 + + + + + + + + diff --git a/book/Planet/_.kind2 b/book/Planet/_.kind2 new file mode 100644 index 00000000..e0064632 --- /dev/null +++ b/book/Planet/_.kind2 @@ -0,0 +1,2 @@ +data Planet +| new (pos: V2) (vel: V2) (rad: U48) : Planet diff --git a/book/Planet/draw.kind2 b/book/Planet/draw.kind2 new file mode 100644 index 00000000..7fb0da08 --- /dev/null +++ b/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)] +} diff --git a/book/Planet/interact.kind2 b/book/Planet/interact.kind2 new file mode 100644 index 00000000..64c72b98 --- /dev/null +++ b/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 = + + + + + + diff --git a/book/Planet/interactions.kind2 b/book/Planet/interactions.kind2 new file mode 100644 index 00000000..e62fdf8d --- /dev/null +++ b/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: + [] +} diff --git a/book/Planet/match.kind2 b/book/Planet/match.kind2 new file mode 100644 index 00000000..24c09656 --- /dev/null +++ b/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) diff --git a/book/Planet/new.kind2 b/book/Planet/new.kind2 new file mode 100644 index 00000000..fa7f90f6 --- /dev/null +++ b/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) diff --git a/book/Planet/tick.kind2 b/book/Planet/tick.kind2 new file mode 100644 index 00000000..3098150b --- /dev/null +++ b/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) +} diff --git a/book/QuadTree/_.kind2 b/book/QuadTree/_.kind2 new file mode 100644 index 00000000..15477f4c --- /dev/null +++ b/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 +| node (nw: (QuadTree A)) (ne: (QuadTree A)) (sw: (QuadTree A)) (se: (QuadTree A)) +| leaf (xs: (List A)) diff --git a/book/QuadTree/del.kind2 b/book/QuadTree/del.kind2 new file mode 100644 index 00000000..51842037 --- /dev/null +++ b/book/QuadTree/del.kind2 @@ -0,0 +1,30 @@ +use QuadTree/{node,leaf} +use Bits/{O,I,E} +use Maybe/{some,none} + +del +- 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 +} diff --git a/book/QuadTree/draw/_.kind2 b/book/QuadTree/draw/_.kind2 new file mode 100644 index 00000000..eb85f96e --- /dev/null +++ b/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 +- 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) +} diff --git a/book/QuadTree/draw/area.kind2 b/book/QuadTree/draw/area.kind2 new file mode 100644 index 00000000..4fb27259 --- /dev/null +++ b/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 +] diff --git a/book/QuadTree/foo/_.kind2 b/book/QuadTree/foo/_.kind2 new file mode 100644 index 00000000..8f8691cb --- /dev/null +++ b/book/QuadTree/foo/_.kind2 @@ -0,0 +1,3 @@ +foo : U48 + +42 diff --git a/book/QuadTree/get.kind2 b/book/QuadTree/get.kind2 new file mode 100644 index 00000000..e3a92c18 --- /dev/null +++ b/book/QuadTree/get.kind2 @@ -0,0 +1,27 @@ +use QuadTree/{node,leaf} +use Bits/{O,I,E} +use Maybe/{some,none} + +get +- 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 +} diff --git a/book/QuadTree/is_empty.kind2 b/book/QuadTree/is_empty.kind2 new file mode 100644 index 00000000..02749670 --- /dev/null +++ b/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 +- tree: (QuadTree A) +: Bool + +match tree { + node: false + leaf: (List/is_empty _ tree.xs) +} diff --git a/book/QuadTree/leaf.kind2 b/book/QuadTree/leaf.kind2 new file mode 100644 index 00000000..7ea32eb7 --- /dev/null +++ b/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 +- xs: (List A) +: (QuadTree A) + +~λP λnode λleaf (leaf xs) diff --git a/book/QuadTree/lemma/del_set_id.kind2 b/book/QuadTree/lemma/del_set_id.kind2 new file mode 100644 index 00000000..dbdef4e5 --- /dev/null +++ b/book/QuadTree/lemma/del_set_id.kind2 @@ -0,0 +1,11 @@ +del_set_id +- 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 + diff --git a/book/QuadTree/match.kind2 b/book/QuadTree/match.kind2 new file mode 100644 index 00000000..9bc79e84 --- /dev/null +++ b/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 +- 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) diff --git a/book/QuadTree/node.kind2 b/book/QuadTree/node.kind2 new file mode 100644 index 00000000..7e337ff8 --- /dev/null +++ b/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 +- nw: (QuadTree A) +- ne: (QuadTree A) +- sw: (QuadTree A) +- se: (QuadTree A) +: (QuadTree A) + +~λP λnode λleaf (node nw ne sw se) diff --git a/book/QuadTree/nrm.kind2 b/book/QuadTree/nrm.kind2 new file mode 100644 index 00000000..ab978076 --- /dev/null +++ b/book/QuadTree/nrm.kind2 @@ -0,0 +1,25 @@ +use QuadTree/{node,leaf} +use Bool/{and} +use List/is_empty + +nrm +- 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 +} diff --git a/book/QuadTree/set.kind2 b/book/QuadTree/set.kind2 new file mode 100644 index 00000000..56fbdf5f --- /dev/null +++ b/book/QuadTree/set.kind2 @@ -0,0 +1,52 @@ +use QuadTree/{node,leaf} +use Bits/{O,I,E} +use Maybe/{some,none} + +set +- 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 + } + } +} + diff --git a/book/RGB/B.kind2 b/book/RGB/B.kind2 new file mode 100644 index 00000000..4f6f895e --- /dev/null +++ b/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 diff --git a/book/RGB/G.kind2 b/book/RGB/G.kind2 new file mode 100644 index 00000000..3296d7c1 --- /dev/null +++ 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 diff --git a/book/RGB/R.kind2 b/book/RGB/R.kind2 new file mode 100644 index 00000000..30b2ee7a --- /dev/null +++ b/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 diff --git a/book/RGB/_.kind2 b/book/RGB/_.kind2 new file mode 100644 index 00000000..0b86aeed --- /dev/null +++ b/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 diff --git a/book/RGB/match.kind2 b/book/RGB/match.kind2 new file mode 100644 index 00000000..a7dde07b --- /dev/null +++ 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) diff --git a/book/RGB/show.kind2 b/book/RGB/show.kind2 new file mode 100644 index 00000000..3f5cb89d --- /dev/null +++ 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 +} diff --git a/book/RGB/spin.kind2 b/book/RGB/spin.kind2 new file mode 100644 index 00000000..a311468d --- /dev/null +++ b/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 +} diff --git a/book/RGB/unspin.kind2 b/book/RGB/unspin.kind2 new file mode 100644 index 00000000..e106ca97 --- /dev/null +++ b/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 +} diff --git a/book/RGB/unspin_spec.kind2 b/book/RGB/unspin_spec.kind2 new file mode 100644 index 00000000..6f80ad4a --- /dev/null +++ b/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 diff --git a/book/Shape/_.kind2 b/book/Shape/_.kind2 new file mode 100644 index 00000000..e89ffe9c --- /dev/null +++ b/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) diff --git a/book/Shape/circle.kind2 b/book/Shape/circle.kind2 new file mode 100644 index 00000000..34f88bba --- /dev/null +++ b/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) diff --git a/book/Shape/line.kind2 b/book/Shape/line.kind2 new file mode 100644 index 00000000..211f03e6 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/book/Solar/draw_planet.kind2 b/book/Solar/draw_planet.kind2 new file mode 100644 index 00000000..01e956fe --- /dev/null +++ b/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 +} diff --git a/book/Solar/main.kind2 b/book/Solar/main.kind2 new file mode 100644 index 00000000..a83e6acd --- /dev/null +++ b/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) diff --git a/book/U48/if.kind2 b/book/U48/if.kind2 index fd30a335..cd0ba007 100644 --- a/book/U48/if.kind2 +++ b/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

- x: U48 - t: P @@ -5,6 +21,6 @@ if

: P switch x { - 0: t - _: f -} + 0: f + _: t +}: P diff --git a/book/U48/sqrt.kind2 b/book/U48/sqrt.kind2 new file mode 100644 index 00000000..70b786d1 --- /dev/null +++ b/book/U48/sqrt.kind2 @@ -0,0 +1 @@ +// TODO diff --git a/book/U48/sqrt/go.kind2 b/book/U48/sqrt/go.kind2 new file mode 100644 index 00000000..aa962437 --- /dev/null +++ b/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) +} diff --git a/book/U48/to_bits.kind2 b/book/U48/to_bits.kind2 new file mode 100644 index 00000000..282bc239 --- /dev/null +++ b/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 diff --git a/book/V2/_.kind2 b/book/V2/_.kind2 new file mode 100644 index 00000000..f18cefd2 --- /dev/null +++ b/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) diff --git a/book/V2/add.kind2 b/book/V2/add.kind2 new file mode 100644 index 00000000..d6682374 --- /dev/null +++ b/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)) + } +} diff --git a/book/V2/div.kind2 b/book/V2/div.kind2 new file mode 100644 index 00000000..e7923fdc --- /dev/null +++ b/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)) + } +} diff --git a/book/V2/dot.kind2 b/book/V2/dot.kind2 new file mode 100644 index 00000000..ee6b458c --- /dev/null +++ b/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)) + } +} diff --git a/book/V2/get_x.kind2 b/book/V2/get_x.kind2 new file mode 100644 index 00000000..a145e5cc --- /dev/null +++ b/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 +} diff --git a/book/V2/get_y.kind2 b/book/V2/get_y.kind2 new file mode 100644 index 00000000..c4420673 --- /dev/null +++ b/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 +} diff --git a/book/V2/match.kind2 b/book/V2/match.kind2 new file mode 100644 index 00000000..3720b430 --- /dev/null +++ b/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) diff --git a/book/V2/mul.kind2 b/book/V2/mul.kind2 new file mode 100644 index 00000000..224d32fd --- /dev/null +++ b/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)) + } +} diff --git a/book/V2/neg.kind2 b/book/V2/neg.kind2 new file mode 100644 index 00000000..9df8e2c5 --- /dev/null +++ b/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)) +} diff --git a/book/V2/new.kind2 b/book/V2/new.kind2 new file mode 100644 index 00000000..a1941bbd --- /dev/null +++ b/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) diff --git a/book/V2/sqr_dist.kind2 b/book/V2/sqr_dist.kind2 new file mode 100644 index 00000000..883bcf3b --- /dev/null +++ b/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)) + } +} diff --git a/book/V2/sub.kind2 b/book/V2/sub.kind2 new file mode 100644 index 00000000..155b219d --- /dev/null +++ b/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)) + } +} diff --git a/book/hello.kind2 b/book/hello.kind2 new file mode 100644 index 00000000..82926b8c --- /dev/null +++ b/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) diff --git a/book/index.html b/book/index.html new file mode 100644 index 00000000..0b483aff --- /dev/null +++ b/book/index.html @@ -0,0 +1,18 @@ + + + + + + + + Canvas Drawing + + + + + + diff --git a/book/kind4.kind2 b/book/kind4.kind2 new file mode 100644 index 00000000..7e393188 --- /dev/null +++ b/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) + + diff --git a/book/main.js b/book/main.js new file mode 100644 index 00000000..03486099 --- /dev/null +++ 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); })(); })(); })(); })(); + diff --git a/book/main.kind2 b/book/main.kind2 index 1c5b9286..81242ca2 100644 --- a/book/main.kind2 +++ b/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 diff --git a/book/main1.js b/book/main1.js new file mode 100644 index 00000000..7d9d7f35 --- /dev/null +++ b/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 +// = { $: "cons"; head: T; tail: List; } +// | { $: "nil"; }; +// +// type App = { +// $: "new"; +// tick: (state: S) => S; +// draw: (state: S) => List; +// 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); +} + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/book/main2.kind2 b/book/main2.kind2 new file mode 100644 index 00000000..9d7ff544 --- /dev/null +++ b/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 diff --git a/book/main3.kind2 b/book/main3.kind2 new file mode 100644 index 00000000..1c5b9286 --- /dev/null +++ b/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 diff --git a/book/main4.kind2 b/book/main4.kind2 new file mode 100644 index 00000000..8be02048 --- /dev/null +++ b/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); + + + + + diff --git a/book/quads.kind2 b/book/quads.kind2 new file mode 100644 index 00000000..d2db6292 --- /dev/null +++ b/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) + + + diff --git a/book/rt.js b/book/rt.js new file mode 100644 index 00000000..c7e5bd53 --- /dev/null +++ b/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 +// = { $: "cons"; head: T; tail: List; } +// | { $: "nil"; }; +// +// type App = { +// $: "new"; +// tick: (state: S) => S; +// draw: (state: S) => List; +// 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(); + }); + +} diff --git a/book/sqr_dist_test.kind2 b/book/sqr_dist_test.kind2 new file mode 100644 index 00000000..fd3168a4 --- /dev/null +++ b/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) + diff --git a/book/stuff.js b/book/stuff.js new file mode 100644 index 00000000..df0a6411 --- /dev/null +++ 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); +}; diff --git a/book/test_a.kind2 b/book/test_a.kind2 new file mode 100644 index 00000000..fc7a71a1 --- /dev/null +++ b/book/test_a.kind2 @@ -0,0 +1,4 @@ +test_a + +let n = 123 +(U48/to_bits n) diff --git a/kjfsadkfj.bend b/kjfsadkfj.bend new file mode 100644 index 00000000..5a61e644 --- /dev/null +++ b/kjfsadkfj.bend @@ -0,0 +1,2 @@ +def render(map, pixel, pos): + return ... diff --git a/src/term/compile.rs b/src/term/compile.rs index 869384bb..ac227122 100644 --- a/src/term/compile.rs +++ b/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("-","_") } } diff --git a/src/term/mod.rs b/src/term/mod.rs index 7738956f..94b34695 100644 --- a/src/term/mod.rs +++ b/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, depth: &mut u64) { + + //pub fn overshadow(&mut self, name_map: &mut BTreeMap, 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, 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); }, _ => {} }