WIP

book/BMap/_.kind2

@@ -1,3 +1,14 @@
+/// Represents a binary map (binary search tree) data structure.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values stored in the binary map.
+///
+/// # Constructors
+///
+/// * `node` - An internal node of the binary map, containing a value and two subtrees.
+/// * `leaf` - A leaf node, representing an empty subtree.
+
 data BMap <A>
-| node (lft: (BMap A)) (val: A) (rgt: (BMap A))
+| node (lft: (BMap A)) (val: (Maybe A)) (rgt: (BMap A))
 | leaf

book/BMap/get.kind2

@@ -0,0 +1,38 @@
+/// Retrieves a value from the binary map for a given key.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values stored in the binary map.
+///
+/// # Inputs
+///
+/// * `map` - The binary map to search in.
+/// * `key` - The key represented as Bits.
+///
+/// # Output
+///
+/// A Maybe value containing the value associated with the key, or none if not found.
+
+use BMap/{node,leaf}
+use Bits/{O,I,E}
+use Maybe/{some,none}
+
+get <A>
+- map: (BMap A)
+- key: Bits
+: (Maybe A)
+
+match key {
+  O: match map {
+    node: (get _ map.lft key.tail)
+    leaf: (Maybe/none _)
+  }
+  I: match map {
+    node: (get _ map.rgt key.tail)
+    leaf: (Maybe/none _)
+  }
+  E: match map {
+    node: map.val
+    leaf: (Maybe/none _)
+  }
+}

book/BMap/leaf.kind2

@@ -1,3 +1,13 @@
+/// Represents a leaf node in the binary map (BMap) data structure.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values that would be stored in the BMap.
+///
+/// # Output
+///
+/// An empty BMap (leaf node) of type `(BMap A)`.
+
 BMap/leaf
 : ∀(A: *) (BMap A)
 

book/BMap/match.kind2

@@ -0,0 +1,27 @@
+/// Provides a way to pattern match on BMap values.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values stored in the binary map.
+///
+/// # Inputs
+///
+/// * `P` - The motive of the elimination, a type family indexed by (BMap A).
+/// * `n` - The case for when the BMap is a node.
+/// * `l` - The case for when the BMap is a leaf.
+/// * `bm` - The BMap value to match on.
+///
+/// # Output
+///
+/// The result of the elimination, which has type `(P bm)`.
+
+use BMap/{node,leaf}
+
+match <A>
+- P: (BMap A) -> *
+- n: ∀(lft: (BMap A)) ∀(val: (Maybe A)) ∀(rgt: (BMap A)) (P (BMap/node A lft val rgt))
+- l: (P (BMap/leaf A))
+- bm: (BMap A)
+: (P bm)
+
+(~bm P n l)

book/BMap/node.kind2

@@ -1,7 +1,23 @@
+/// Creates a new node in the binary map (BMap) data structure.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values stored in the binary map.
+///
+/// # Inputs
+///
+/// * `lft` - The left subtree of the node.
+/// * `val` - The value stored in the node, wrapped in a Maybe.
+/// * `rgt` - The right subtree of the node.
+///
+/// # Output
+///
+/// A new BMap node containing the given value and subtrees.
+
 BMap/node
 : ∀(A: *)
   ∀(lft: (BMap A))
-  ∀(val: A)
+  ∀(val: (Maybe A))
   ∀(rgt: (BMap A))
   (BMap A)
 

book/BMap/set.kind2

@@ -0,0 +1,37 @@
+/// Sets a value in the binary map for a given key.
+///
+/// # Type Parameters
+///
+/// * `A` - The type of values stored in the binary map.
+///
+/// # Inputs
+///
+/// * `map` - The binary map to update.
+/// * `key` - The key represented as Bits.
+/// * `val` - The value to be set, wrapped in a Maybe.
+///
+/// # Output
+///
+/// A new BMap with the value set for the given key.
+
+use BMap/{node,leaf}
+use Bits/{O,I,E}
+use Maybe/{some,none}
+
+set <A>
+- map: (BMap A)
+- key: Bits
+- val: (Maybe A)
+: (BMap A)
+
+match key {
+  O: match map {
+    node: (BMap/node _ (set _ map.lft key.tail val) map.val map.rgt)
+    leaf: (BMap/node _ (set _ (BMap/leaf _) key.tail val) (Maybe/none _) (BMap/leaf _))
+  }
+  I: match map {
+    node: (BMap/node _ map.lft map.val (set _ map.rgt key.tail val))
+    leaf: (BMap/node _ (BMap/leaf _) (Maybe/none _) (set _ (BMap/leaf _) key.tail val))
+  }
+  E: (BMap/node _ (BMap/leaf _) val (BMap/leaf _))
+}

book/Bits/E.kind2

@@ -0,0 +1,10 @@
+/// Constructs an empty Bits value.
+///
+/// # Output
+///
+/// An empty Bits value, representing the end of a bit sequence.
+
+E
+: Bits
+
+~λP λO λI λE E

book/Bits/I.kind2

@@ -0,0 +1,15 @@
+/// Constructs a Bits value with a one bit followed by more bits.
+///
+/// # Input
+///
+/// * `tail` - The remaining bits after the one bit.
+///
+/// # Output
+///
+/// A new Bits value with a one bit followed by `tail`.
+
+I
+- tail: Bits
+: Bits
+
+~λP λO λI λE (I tail)

book/Bits/O.kind2

@@ -0,0 +1,15 @@
+/// Constructs a Bits value with a zero bit followed by more bits.
+///
+/// # Input
+///
+/// * `tail` - The remaining bits after the zero bit.
+///
+/// # Output
+///
+/// A new Bits value with a zero bit followed by `tail`.
+
+O
+- tail: Bits
+: Bits
+
+~λP λO λI λE (O tail)

book/Bits/_.kind2

@@ -0,0 +1,12 @@
+/// Defines a binary representation of numbers using bits.
+///
+/// # Constructors
+///
+/// * `O` - Represents a zero bit followed by more bits.
+/// * `I` - Represents a one bit followed by more bits.
+/// * `E` - Represents the end of the bit sequence (empty).
+
+data Bits
+| O (tail: Bits)
+| I (tail: Bits)
+| E

book/Bits/match.kind2

@@ -0,0 +1,28 @@
+/// Provides a way to pattern match on Bits values.
+///
+/// # Parameters
+///
+/// * `P` - The motive of the elimination, a type family indexed by Bits.
+///
+/// # Inputs
+///
+/// * `o` - The case for when the Bits value starts with a zero bit.
+/// * `i` - The case for when the Bits value starts with a one bit.
+/// * `e` - The case for when the Bits value is empty.
+/// * `b` - The Bits value to match on.
+///
+/// # Output
+///
+/// The result of the elimination, which has type `(P b)`.
+
+use Bits/{O,I,E}
+
+match
+- P: Bits -> *
+- o: ∀(tail: Bits) (P (O tail))
+- i: ∀(tail: Bits) (P (I tail))
+- e: (P E)
+- b: Bits
+: (P b)
+
+(~b P o i e)

book/_check_all.sh

@@ -1,13 +0,0 @@
-#for file in $(ls *.kind2 | grep -v '^_'); do
-  #echo "checking ${file}"
-  #kind2 check "${file%.*}"
-#done
-
-# TODO: make this script check all kind2 files recursively, not just top-dir ones
-
-#!/bin/bash
-
-find . -name "*.kind2" -not -name "_*" | while read -r file; do
-  echo "checking ${file}"
-  kind2 check "${file%.*}"
-done

book/foo.ts

@@ -1,9 +0,0 @@
-// create a function in typescript with
-
-function foo(n: number) : string {
-  return "foo";
-}
-
-let x : any = "bar";
-
-console.log(foo(x));

book/main.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/script.js

@@ -1,32 +0,0 @@
-const fs = require('fs');
-const path = require('path');
-
-// Read all .kind2 files in the current directory
-fs.readdir('.', (err, files) => {
-  if (err) {
-    console.error('Error reading directory:', err);
-    return;
-  }
-
-  files.filter(file => file.endsWith('.kind2')).forEach(file => {
-    // Construct new path by replacing dots with slashes, except for the extension
-    const newName = file.slice(0, -6).replace(/\./g, '/') + file.slice(-6);
-    const newPath = path.join('.', newName);
-    const newDir = path.dirname(newPath);
-
-    // Create the directory structure if it doesn't exist
-    fs.mkdir(newDir, { recursive: true }, (err) => {
-      if (err) {
-        console.error('Error creating directories:', err);
-        return;
-      }
-
-      // Move the file to the new location
-      fs.rename(file, newPath, (err) => {
-        if (err) {
-          console.error('Error moving file:', err);
-        }
-      });
-    });
-  });
-});

book/test.kind2

@@ -1,4 +0,0 @@
-test
-: (List U48)
-
-[50, 60]

src/kindc.hs

@@ -1180,19 +1180,19 @@ main = do
     ["check", file] -> do
       content <- readFile file
       let book = doParseBook content
-      case M.lookup "main" book of
-        Just term -> apiCheck book (Ref "main")
+      case M.lookup "MAIN" book of
+        Just term -> apiCheck book (Ref "MAIN")
         Nothing -> putStrLn "Error: No 'main' definition found in the file."
     ["run", file] -> do
       content <- readFile file
       let book = doParseBook content
-      case M.lookup "main" book of
+      case M.lookup "MAIN" book of
         Just term -> apiNormal book term
         Nothing -> putStrLn "Error: No 'main' definition found in the file."
     ["show", file] -> do
       content <- readFile file
       let book = doParseBook content
-      case M.lookup "main" book of
+      case M.lookup "MAIN" book of
         Just term -> putStrLn $ termStr term 0
         Nothing -> putStrLn "Error: No 'main' definition found in the file."
     ["help"] -> printHelp

src/main.rs

@@ -22,7 +22,7 @@ TSPL::new_parser!(KindParser);
 
 fn generate_kindc(book: &Book, arg: &str) -> String {
   let book_kindc = book.to_kindc();
-  let main_kindc = format!("main = {};\n", Term::to_kindc_name(arg));
+  let main_kindc = format!("MAIN = {};\n", Term::to_kindc_name(arg));
   format!("{}{}", book_kindc, main_kindc)
 }