Add some stray files

.gitignore

@@ -18,3 +18,4 @@ src/Revision.newt
 .joyride
 .lsp
 .vscode
+bootstrap/serializer.js

misc/README.md

@@ -0,0 +1,2 @@
+This directory contains experiments that I did in typescript before implementing a couple of features.
+

misc/mixfix.ts

@@ -0,0 +1,114 @@
+// mixfix+pratt experiment, single expression type
+// Generates ["app", "a", "b"] nodes for app
+
+// 561 bytes w/o test cases, error messages
+
+// TODO
+// - it might be interesting to pretty print stuff back using the grammar
+
+// using a tuple makes the output two bytes bigger...
+type OpDef = { n: string; p: number; f: string; s: string[] }
+type Rules = Record<string, OpDef>
+type AST = string | AST[]
+
+function parse(str: string, grammar: string) {
+  let rval
+  let rules: Rules = {}
+  let fail = (m?: string) => {
+    throw new Error(m)
+  }
+  // Fancy tokenizer
+  let toks = str.match(/\w+|[=>+*/-]+|\d+|\S/g)!
+  let pos = 0
+  let mixfix = (ast: AST[], def: OpDef, stop: string): AST => {
+    def.s.slice(def.s[0] ? 1 : 2).forEach((step) => {
+      ast.push(step ? expr(0, step) : expr(def.f == 'L' ? def.p + 1 : def.p, stop))
+      if (step && toks[pos++] != step) fail('expected ' + step)
+    })
+    return ast
+  }
+
+  let expr = (prec: number, stop: string): AST => {
+    // this needs to be an arg for tail recursive version
+    let left: AST = toks[pos++]
+    let right: AST
+    let rule = rules[left as string]
+    if (!left) fail('EOF')
+    if (rule) left = rule.s[0] ? mixfix([rule.n], rule, stop) : fail('stray operator')
+    for (;;) {
+      right = toks[pos]
+      if (!right || right == stop) return left
+      rule = rules[right]
+      if (!rule) {
+        left = ['app', left, right]
+        pos++
+      } else if (rule.s[0]) {
+        pos++
+        left = ['app', left, mixfix([rule.n], rule, stop)]
+      } else {
+        if (rule.p < prec) return left
+        pos++
+        left = mixfix([rule.n, left], rule, stop)
+      }
+    }
+  }
+  // Parse grammar
+  grammar
+    .trim()
+    .split('\n')
+    .forEach((def) => {
+      let [fix, prec, name] = def.split(' ')
+      let parts = name.split('_')
+      rules[parts[0] || parts[1]] = { n: name, p: +prec, f: fix, s: parts }
+    })
+
+  // need to check if we've parsed everything
+  rval = expr(0, '')
+  if (toks[pos]) fail(`extra toks`)
+  return rval
+}
+
+// TESTS
+
+// For prefix, the tail gets the prec
+let grammar = `
+R 7 _++_
+L 7 _+_
+L 7 _-_
+L 8 _*_
+L 8 _/_
+L 1 _==_
+L 0 (_)
+R 0 if_then_else_
+R 0 \\_=>_
+`
+
+const check = (s: string) => console.log(s, ' -> ', parse(s, grammar))
+const failing = (s: string) => {
+  let rval
+  try {
+    rval = parse(s, grammar)
+  } catch (e) {
+    console.log(s, ' ->', e!.toString())
+  }
+  if (rval) throw new Error(`expected ${s} to fail, got ${JSON.stringify(rval)}`)
+}
+check('a b c')
+check('1+1')
+check('\\ x => x')
+check('a+b+c')
+check('a++b++c')
+check('a+b*c+d')
+check('(a+b)*c')
+check('if x == 1 + 1 then a + b else c')
+check('1 ∧ 2')
+check('a b + b c')
+check('¬ a')
+failing('a +')
+failing('a + +')
+failing('+ a')
+
+// Has to be at end because TESTS
+
+// for "minify", I'm dropping error details and using map instead of forEach
+// sed -e 's/fail([^)]*)/fail()/g;s/forEach/map/g;/TESTS/,$d' <src/mixfix.ts|esbuild --loader=ts --minify|wc -c

scripts/import_graph.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+
+# The first pass of this was LLM generated for expediency
+
+# scan the src directory for *.newt files
+# match lines like `import Foo.Bar.Baz`
+# use graphviz to create a dependency graph in a pdf file
+
+SRC_DIR="/Users/dunham/prj/newt/src"
+OUTPUT_FILE="/Users/dunham/prj/newt/dependency_graph.pdf"
+
+TEMP_FILE=$(mktemp)
+trap 'rm -f "$TEMP_FILE"' EXIT
+
+echo "digraph dependencies {" > "$TEMP_FILE"
+
+# GPT4 did the first version of this, I wasn't familiar with "read"
+find "$SRC_DIR" -name "*.newt" | while read -r file; do
+  grep -Eo '^import [A-Za-z0-9.]+' "$file" | egrep -v 'Prelude|Data' | while read -r line; do
+    module=$(echo "$file" | sed "s|$SRC_DIR/||; s|/|.|g; s|.newt$||")
+    imported_module=$(echo "$line" | awk '{print $2}')
+    echo "  \"$module\" -> \"$imported_module\";" >> "$TEMP_FILE"
+  done
+done
+
+# End the graphviz dot file
+echo "}" >> "$TEMP_FILE"
+
+# Generate the PDF using dot
+dot -Tpdf "$TEMP_FILE" -o "$OUTPUT_FILE"
+
+echo "Dependency graph created at $OUTPUT_FILE"

src/Data/DSortedMap.newt

@@ -0,0 +1,230 @@
+module Data.DSortedMap
+
+import Prelude
+
+infixr 1 _**_
+
+data Sg : (A : U) -> (A -> U) -> U where
+  _**_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
+
+data T23 : Nat -> (a : U) -> (a -> U) -> U where
+  Leaf : ∀ k. {0 v : k → U} → (x : k) -> v x -> T23 Z k v
+  Node2 : ∀ h k v. T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+  Node3 : ∀ h k v. T23 h k v -> k -> T23 h k v -> k -> T23 h k v -> T23 (S h) k v
+
+lookupT23 : ∀ h k v. (k → k → Ordering) -> (x : k) -> T23 h k v -> Maybe (Sg k v)
+lookupT23 compare key (Leaf k v)= case compare k key of
+  -- TODO - too smart for its own good...
+  -- um, we need to know compare/EQ works..
+    EQ => Just (k ** v)
+    _ => Nothing
+lookupT23 compare key (Node2 t1 k1 t2) =
+  case compare key k1 of
+    GT => lookupT23 compare key t2
+    _ => lookupT23 compare key t1
+lookupT23 compare key (Node3 t1 k1 t2 k2 t3) =
+  case compare key k1 of
+    GT => case compare key k2 of
+      GT => lookupT23 compare key t3
+      _ => lookupT23 compare key t2
+    _ => lookupT23 compare key t1
+
+insertT23 : ∀ h k. {0 v : k → U} → (k → k → Ordering) -> (x : k) -> v x -> T23 h k v -> Either (T23 h k v) (T23 h k v × k × T23 h k v)
+insertT23 compare key value (Leaf k v) = case compare key k of
+  EQ => Left (Leaf key value)
+  LT => Right (Leaf key value, key, Leaf k v)
+  GT => Right (Leaf k v, k, Leaf key value)
+insertT23 compare key value (Node2 t1 k1 t2) =
+  case compare key k1 of
+    GT => case insertT23 compare key value t2 of
+      Left t2' => Left (Node2 t1 k1 t2')
+      Right (a,b,c) => Left (Node3 t1 k1 a b c)
+    _ => case insertT23 compare key value t1 of
+      Left t1' => Left (Node2 t1' k1 t2)
+      Right (a,b,c) => Left (Node3 a b c k1 t2)
+insertT23 compare key value (Node3 t1 k1 t2 k2 t3) =
+  case compare key k1 of
+    GT => case compare key k2 of
+      GT => case insertT23 compare key value t3 of
+        Left t3' => Left (Node3 t1 k1 t2 k2 t3')
+        Right (a,b,c) => Right (Node2 t1 k1 t2, k2, Node2 a b c)
+      _ => case insertT23 compare key value t2 of
+        Left t2' => Left (Node3 t1 k1 t2' k2 t3)
+        Right (a,b,c) => Right (Node2 t1 k1 a, b, Node2 c k2 t3)
+    _ =>
+      case insertT23 compare key value t1 of
+        Left t1' => Left (Node3 t1' k1 t2 k2 t3)
+        Right (a,b,c) => Right (Node2 a b c, k1, Node2 t2 k2 t3)
+
+-- This is cribbed from Idris. Deleting nodes takes a bit of code.
+Hole : Nat → (a : U) → (a → U) → U
+Hole Z k v = Unit
+Hole (S n) k v = T23 n k v
+
+Node4 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node4 t1 k1 t2 k2 t3 k3 t4 = Node2 (Node2 t1 k1 t2) k2 (Node2 t3 k3 t4)
+
+Node5 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node5 a b c d e f g h i = Node2 (Node2 a b c) d (Node3 e f g h i)
+
+Node6 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node6 a b c d e f g h i j k = Node2 (Node3 a b c d e) f (Node3 g h i j k)
+
+Node7 : ∀ k v h. T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → k → T23 h k v → T23 (S (S h)) k v
+Node7 a b c d e f g h i j k l m = Node3 (Node3 a b c d e) f (Node2 g h i) j (Node2 k l m)
+
+merge1 : ∀ k v h. T23 h k v → k → T23 (S h) k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge1 a b (Node2 c d e) f (Node2 g h i) = Node5 a b c d e f g h i
+merge1 a b (Node2 c d e) f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge1 a b (Node3 c d e f g) h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge2 : ∀ k v h. T23 (S h) k v → k → T23 h k v → k → T23 (S h) k v → T23 (S (S h)) k v
+merge2 (Node2 a b c) d e f (Node2 g h i) = Node5 a b c d e f g h i
+merge2 (Node2 a b c) d e f (Node3 g h i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node2 i j k) = Node6 a b c d e f g h i j k
+merge2 (Node3 a b c d e) f g h (Node3 i j k l m) = Node7 a b c d e f g h i j k l m
+
+merge3 : ∀ k v h. T23 (S h) k v → k → T23 (S h) k v → k → T23 h k v → T23 (S (S h)) k v
+merge3 (Node2 a b c) d (Node2 e f g) h i = Node5 a b c d e f g h i
+merge3 (Node2 a b c) d (Node3 e f g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node2 g h i) j k = Node6 a b c d e f g h i j k
+merge3 (Node3 a b c d e) f (Node3 g h i j k) l m = Node7 a b c d e f g h i j k l m
+
+-- height is erased in the data everywhere but the top, but needed for case
+-- I wonder if we could use a 1 + 1 + 1 type instead of Either Tree Hole and condense this
+deleteT23 : ∀ k v. (k → k → Ordering) → (h : Nat) -> k -> T23 h k v -> Either (T23 h k v) (Hole h k v)
+deleteT23 compare Z key (Leaf k v) = case compare k key of
+  EQ => Right MkUnit
+  _ => Left (Leaf k v)
+deleteT23 compare (S Z) key (Node2 t1 k1 t2) =
+  case compare key k1 of
+    GT => case deleteT23 compare Z key t2 of
+      Left t2 => Left (Node2 t1 k1 t2)
+      Right MkUnit => Right t1
+    _ => case deleteT23 compare Z key t1 of
+      Left t1 => Left (Node2 t1 k1 t2)
+      Right _ => Right t2
+deleteT23 compare (S Z) key (Node3 t1 k1 t2 k2 t3) =
+  case compare key k1 of
+    GT => case compare key k2 of
+      GT => case deleteT23 compare _ key t3 of
+        Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+        Right _ => Left (Node2 t1 k1 t2)
+      _ => case deleteT23 compare _ key t2 of
+        Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+        Right _ => Left (Node2 t1 k1 t3)
+    _ => case deleteT23 compare _ key t1 of
+      Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+      Right MkUnit => Left (Node2 t2 k2 t3)
+deleteT23 compare (S (S h)) key (Node2 t1 k1 t2) =
+  case compare key k1 of
+    GT => case deleteT23 compare _ key t2 of
+      Left t2 => Left (Node2 t1 k1 t2)
+      Right t2 => case t1 of
+        Node2 a b c => Right (Node3 a b c k1 t2)
+        Node3 a b c d e => Left (Node4 a b c d e k1 t2)
+    _ => case deleteT23 compare (S h) key t1 of
+      Left t1 => Left (Node2 t1 k1 t2)
+      Right t1 => case t2 of
+        Node2 t2' k2' t3' => Right (Node3 t1 k1 t2' k2' t3')
+        Node3 t2 k2 t3 k3 t4 => Left $ Node4 t1 k1 t2 k2 t3 k3 t4
+
+deleteT23 compare (S (S h)) key (Node3 t1 k1 t2 k2 t3) =
+  case compare key k1 of
+    GT => case compare key k2 of
+      GT => case deleteT23 compare _ key t3 of
+        Left t3 => Left (Node3 t1 k1 t2 k2 t3)
+        Right t3 => Left (merge3 t1 k1 t2 k2 t3)
+      _ => case deleteT23 compare _ key t2 of
+        Left t2 => Left (Node3 t1 k1 t2 k2 t3)
+        Right t2 => Left (merge2 t1 k1 t2 k2 t3)
+    _ => case deleteT23 compare _ key t1 of
+      Left t1 => Left (Node3 t1 k1 t2 k2 t3)
+      Right t1 => Left (merge1 t1 k1 t2 k2 t3)
+
+treeLeft : ∀ h k v. T23 h k v → (Sg k v)
+treeLeft (Leaf k v) = (k ** v)
+treeLeft (Node2 t1 _ _) = treeLeft t1
+treeLeft (Node3 t1 _ _ _ _) = treeLeft t1
+
+treeRight : ∀ h k v. T23 h k v → (Sg k v)
+treeRight (Leaf k v) = (k ** v)
+treeRight (Node2 _ _ t2) = treeRight t2
+treeRight (Node3 _ _ _ _ t3) = treeRight t3
+
+data SortedMap : (a : U) -> (a -> U) -> U where
+  EmptyMap : ∀ k v. (k → k → Ordering) → SortedMap k v
+  -- h not erased so we know what happens in delete
+  MapOf : ∀ k v. {h : Nat} → (k → k → Ordering) → T23 h k v → SortedMap k v
+
+deleteMap : ∀ k v. k → SortedMap k v → SortedMap k v
+deleteMap key m@(EmptyMap _) = m
+-- REVIEW if I split h separately in a nested case, it doesn't sort out Hole
+deleteMap key (MapOf {k} {v} {Z} compare tree) = case deleteT23 compare Z key tree of
+  Left t => MapOf compare t
+  Right t => EmptyMap compare
+deleteMap key (MapOf {k} {v} {S n} compare tree) = case deleteT23 compare (S n) key tree of
+  Left t => MapOf compare t
+  Right t => MapOf compare t
+
+leftMost : ∀ k v. SortedMap k v → Maybe (Sg k v)
+leftMost (MapOf compare m) = Just (treeLeft m)
+leftMost _ = Nothing
+
+rightMost : ∀ k v. SortedMap k v → Maybe (Sg k v)
+rightMost (MapOf compare m) = Just (treeRight m)
+rightMost _ = Nothing
+
+-- TODO issue with metas and case if written as `do` block
+pop : ∀ k v. SortedMap k v → Maybe ((Sg k v) × SortedMap k v)
+pop m = case leftMost m of
+    Just (k ** v) => Just ((k ** v), deleteMap k m)
+    Nothing => Nothing
+
+lookupMap : ∀ k v. k -> SortedMap k v -> Maybe (Sg k v)
+lookupMap k (MapOf compare map) = lookupT23 compare k map
+lookupMap k _ = Nothing
+
+-- We're kind of in a corner here. The type checker knows EQ might not be right, so
+-- we have to hit up DecEq both to be sure and make the type checker happy.
+lookupMap' : ∀ k. {{DecEq k}} {0 v : k → U} → (x : k) -> SortedMap k v -> Maybe (v x)
+lookupMap' k (MapOf compare map) = case lookupT23 compare k map of
+  Nothing => Nothing
+  Just (k' ** b) => case decEq k k' of
+    Yes Refl => Just b
+    _ => Nothing
+lookupMap' k _ = Nothing
+
+updateMap : ∀ k. {0 v : k → U} → (x : k) -> v x -> SortedMap k v -> SortedMap k v
+updateMap k v (EmptyMap compare) = MapOf compare $ Leaf k v
+updateMap k v (MapOf compare map) = case insertT23 compare k v map of
+  Left map' => MapOf compare map'
+  Right (a, b, c) => MapOf compare (Node2 a b c)
+
+toList : ∀ k v. SortedMap k v → List (Sg k v)
+toList {k} {v} (MapOf compare smap) = reverse $ go smap Nil
+  where
+    go : ∀ h. T23 h k v → List (Sg k v) → List (Sg k v)
+    go (Leaf k v) acc = (k ** v) :: acc
+    go (Node2 t1 k1 t2) acc = go t2 (go t1 acc)
+    go (Node3 t1 k1 t2 k2 t3) acc = go t3 $ go t2 $ go t1 acc
+toList _ = Nil
+
+emptyMap :  ∀ k v. {{Ord k}} → SortedMap k v
+emptyMap = EmptyMap compare
+
+mapFromList : ∀ k v. {{Ord k}} → List (Sg k v) → SortedMap k v
+mapFromList {k} {v} stuff = foldl go emptyMap stuff
+  where
+    go : SortedMap k v → Sg k v → SortedMap k v
+    go map (k ** v) = updateMap k v map
+
+foldMap : ∀ a. {{DecEq a}} {0 b : a → U} → ((x : a) → b x → b x → b x) → SortedMap a b → List (Sg a b) → SortedMap a b
+foldMap f m Nil = m
+foldMap {k} {v} f m ((a ** b) :: xs) = case lookupMap' a m : Maybe $ v a of
+  Nothing => foldMap f (updateMap a b m) xs
+  Just b' => foldMap f (updateMap _ (f a b' b) m) xs
+
+-- listValues : ∀ k v. SortedMap k v → List v
+-- listValues sm = map snd $ toList sm