additional cast from AoC

.editorconfig

@@ -4,3 +4,5 @@ end_of_line = lf
 insert_final_newline = true
 indent_size = 2
 indent_style = space
+[Makefile]
+indent_style = tab

TODO.md

@@ -1,6 +1,22 @@
 
 ## TODO
 
+- [ ] "Expected keyword" at `\ a ->` should be error at the `->`
+- [ ] Show Either
+- [ ] `local` for `where`-like `let` clauses? (I want a `where` that closes over more stuff)
+  - I can do `let f : ... = \ a b c => ...`. But it doesn't work for recursion and cases are awkward.
+- [x] Erasure checking happens at compile time and isn't surfaced to editor..
+- [ ] Erasure issue during AoC from case building replacing a non-erased value with erased.
+- [ ] Add Foldable?
+- [ ] "Failed to unify %var0 and %var1" - get names in there
+  - Need fancier `Env`
+- [ ] add missing cases should skip indented lines
+- [ ] add missing cases should handle `_::_`
+- [ ] "Not in scope" should offer to import
+- [ ] Dependent records (I guess I missed that bit)
+- [ ] Arguments on records
+- [ ] Add sugar for type aliases (maybe infer arguments)
+- [ ] see if we can get a better error on `for` instead of `for_` in do blocks
 - [ ] Maybe make the editor json more compact
 - [ ] Remove erased args from primitive functions
   - But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends
@@ -28,6 +44,7 @@
 - [ ] Look into using holes for errors (https://types.pl/@AndrasKovacs/115401455046442009)
   - This would let us hit more cases in a function when we hit an error.
   - I've been wanting to try holes for parse errors too.
+  - [ ] Missing `∀ k` in type is error -> no declaration for, if we insert a hole, we can get the declaration.
 - [ ] in-scope type at point in vscode
   - So the idea here is that the references will be via FC, we remember the type at declaration and then point the usage back to the declaration (FC -> FC). We could dump all of this. (If we're still doing json.)
   - This information _could_ support renaming, too (but there may be indentation issues).

aoc2025/Day10.newt

@@ -0,0 +1,126 @@
+module Day10
+
+import Prelude
+import Node
+import Aoc
+import Parser
+import Data.Vect
+import Data.Fin
+import Z3
+
+instance ∀ a b. {{Show a}} → {{Show b}} → Show (Either a b) where
+  show (Left a) = "Left \{show a}"
+  show (Right b) = "Right \{show b}"
+
+record Machine where
+  goal : Int
+  buttons : List Int
+  jolts : List Int
+
+infixr 2 _**_
+
+abs : Int → Int
+abs x = if x < 0 then 0 - x else x
+
+data Σ : (a : U) → (a → U) → U where
+  _**_ : ∀ A. {0 B : A → U} → (x : A) →  (_ : B x) → Σ A B
+
+instance Show Machine where
+  show m  = "Mach{goal=\{show m.goal}, buttons=\{show m.buttons}, goal=\{show m.jolts}}"
+
+parseGroup : Char → Char → Parser (List Int)
+parseGroup start end = do
+  match start
+  nums <- some $ number <* optional (match ',')
+  match end
+  ws
+  pure nums
+
+pfunc pow : Int → Int → Int := `(x,y) => x ** y`
+pfunc xor : Int → Int → Int := `(x,y) => x ^ y`
+
+parseMachine : Parser Machine
+parseMachine = do
+  match '['
+  marks <- some $ match '.' <|> match '#'
+  match ']'
+  ws
+  buttons <- some $ parseGroup '(' ')'
+  costs <- parseGroup '{' '}'
+  pure $ MkMachine (mkgoal marks) (map mkbutton buttons) costs
+  where
+    mkbutton : List Int → Int
+    mkbutton (n :: ns) = pow 2 n + mkbutton ns
+    mkbutton Nil = 0
+
+    mkgoal : List Char → Int
+    mkgoal ('#' :: xs) = 1 + 2 * mkgoal xs
+    mkgoal (_ :: xs) = 2 * mkgoal xs
+    mkgoal Nil = 0
+
+parseFile : Parser (List Machine)
+parseFile = some $ parseMachine <* match '\n'
+
+solve : Machine → Int
+solve m = go 0 m.buttons
+  where
+    go : Int → List Int → Int
+    go st Nil = if st == m.goal then 0 else 999
+    go st (b :: bs) =
+      if st == m.goal
+        then 0
+        else min (1 + go (xor st b) bs) (go st bs)
+
+infixl 7 _&_
+pfunc _&_ : Int → Int → Int := `(x,y) => x & y`
+
+part2z3 : {{Context}} → Machine → Promise Int
+part2z3 {{context}} mach = do
+  let rows = length mach.jolts
+  let (Just todo) = toVect rows mach.jolts | _ => fatalError "jolt/rows length"
+  let vars = map (\i => z3const "x\{show $ fst i}") $ enumerate mach.buttons
+  let solver = newOptimizer context
+
+  traverse_ (constrain solver $ zip vars mach.buttons) (enumerate mach.jolts)
+  for_ vars $ \v => z3add solver $ z3ge v (z3int 0)
+  z3minimize solver $ sum vars
+  "sat" <- z3check solver | res => fatalError "GOT \{res}"
+  model <- getModel solver
+  pure $ foldl _+_ 0 $ map getInt vars
+  where
+    sum : List Arith → Arith
+    sum Nil = z3int 0
+    sum (a :: as) = foldl _+_ a as
+
+    constrain : ∀ b. Solver b → List (Arith × Int) → (Nat × Int) → Promise Unit
+    constrain solver bs (ix, goal) =
+      let mask = pow 2 $ cast ix in
+      z3add solver $ z3eq (z3int goal) $ row mask bs (z3int 0)
+      where
+        row : Int → List (Arith × Int) → Arith → Arith
+        row mask Nil acc = acc
+        row mask ((x , b) :: bs) acc = if b & mask == 0 then row mask bs acc else row mask bs (acc + x)
+
+    button2List : ∀ rows. Vect rows Int → Int → Int → Vect rows Int
+    button2List VNil _ _ = VNil
+    button2List (_ :- rest) mask b =
+      (if (b & mask) == 0 then 0 else 1) :- button2List rest (mask * 2) b
+
+run : String -> Promise Unit
+run fn = do
+  putStrLn {Promise} fn
+  text <- liftIO {Promise} $ readFile fn
+  let (Right (probs,_)) = parseFile (unpack text)
+    | Left msg => putStrLn "ERR: \{msg}"
+  let part1 = foldl _+_ 0 $ map solve probs
+  putStrLn $ "part1 \{show part1}"
+  z3 <- initZ3
+  let context = initContext z3 "main"
+  p2s <- traverse part2z3 probs
+  let p2 = foldl _+_ 0 p2s
+  putStrLn "part2 \{show p2}"
+
+main : IO Unit
+main = runPromise $ do
+  run "aoc2025/day10/eg.txt"
+  run "aoc2025/day10/input.txt"

aoc2025/Day11.newt

@@ -0,0 +1,78 @@
+module Day11
+
+import Prelude
+import Node
+import Aoc
+import Data.SortedMap
+import Monad.State
+
+Graph : U
+Graph = SortedMap String (List String)
+
+part1 : Graph →  Int
+part1 g = fst $ (count "you").runState emptyMap
+  where
+    count : String → State (SortedMap String Int) Int
+    count "out" = pure 1
+    count node = do
+      st <- get
+      case lookupMap' node st of
+        Just v => pure v
+        Nothing => do
+          let (Just nodes) = lookupMap' node g | _ => trace "\{show node} missing" $ pure 0
+          counts <- traverse count nodes
+          let total = foldl _+_ 0 counts
+          modify $ updateMap node total
+          pure total
+
+data Result = MkRes Int Int Int Int
+
+emptyResult : Result
+emptyResult = MkRes 0 0 0 0
+
+part2 : Graph →  Int
+part2 g =
+  let (MkRes none dac fft both) = fst $ (count "svr").runState emptyMap in both
+  where
+    addCount : String → Result → Result → Result
+    addCount "fft" (MkRes n d f b) (MkRes n' d' f' b') = MkRes n (d) (f + f' + n') (b + b' + d')
+    addCount "dac" (MkRes n d f b) (MkRes n' d' f' b') = MkRes n (d + d' + n') (f) (b + b' + f')
+    addCount _ (MkRes n d f b) (MkRes n' d' f' b') = MkRes (n + n') (d + d') (f + f') (b + b')
+
+    count : String → State (SortedMap String Result) Result
+    count "out" = pure $ MkRes 1 0 0 0
+    count node = do
+      st <- get
+      case lookupMap' node st of
+        Just v => pure v
+        Nothing => do
+          let (Just nodes) = lookupMap' node g | _ => trace "\{show node} missing" $ pure $ MkRes 0 0 0 0
+          counts <- traverse count nodes
+          let total = foldl (addCount node) emptyResult counts
+          modify $ updateMap node total
+          pure total
+
+parse : String → Either String Graph
+parse text = do
+  let lines = split (trim text) "\n"
+  nodes <- traverse parseNode lines
+  pure $ mapFromList $ nodes
+  where
+    parseNode : String → Either String (String × List String)
+    parseNode txt = case split txt ": " of
+      (a :: b :: Nil) => Right (a, split b " ")
+      x => Left "\{show $ length x} parts"
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  let (Right graph) = parse text | Left err => putStrLn err
+  putStrLn $ "part1 " ++ show (part1 graph)
+  putStrLn $ "part2 " ++ show (part2 graph)
+
+main : IO Unit
+main = do
+  run "aoc2025/day11/eg.txt"
+  run "aoc2025/day11/eg2.txt"
+  run "aoc2025/day11/input.txt"

aoc2025/Day12.newt

@@ -0,0 +1,73 @@
+module Day12
+
+import Prelude
+import Node
+import Aoc
+import Parser
+import Data.List1
+
+data Row = MkR Int Int (List Int)
+data Gift = MkG Int
+
+
+record Problem where
+  gifts : List Int
+  rows : List Row
+
+
+
+parse : String → Either String Problem
+parse txt = do
+  let chunks = split (trim txt) "\n\n"
+  let (c :: cs) = chunks | _ => Left "no chunks"
+  let (gifts, prob) = unsnoc (c ::: cs)
+  let lines = split prob "\n"
+  rows <- traverse parseRow lines
+  Right $ MkProblem (map weight gifts) rows
+  where
+    weight : String → Int
+    weight line = length' $ filter (_==_ '#') $ unpack line
+
+    parseRow : String → Either String Row
+    parseRow line = do
+      let (a :: b :: Nil) = split line ": " | _ => Left "no colon: \{show line}"
+      let ns = nums b
+      let (w :: h :: Nil) = nums' "x" a | _ => Left "bad dims \{show a}"
+      Right $ MkR w h ns
+
+part1 : String → IO Unit
+part1 text = do
+  let (Right prob) = parse text
+    | Left err => putStrLn {IO} err
+  printLn prob.gifts
+  let rows = prob.rows
+  let (easy, rest) = partition isEasy rows
+  let (maybe, imp) = partition (isPossible prob.gifts) rest
+  printLn "\{show $ length rows} rows, \{show $ length' easy} easy, \{show $ length' maybe} maybe, \{show $ length' imp} impossible"
+  -- and there is nothing to do for the input, the "maybe" group is empty.
+  pure MkUnit
+  where
+    isEasy : Row → Bool
+    isEasy (MkR w h boxes) =
+      let bw = w / 3
+          bh = h / 3
+          tbox = foldl _+_ 0 boxes
+       in tbox <= bw * bh
+
+    isPossible : List Int → Row → Bool
+    isPossible gifts (MkR w h boxes) =
+      let weight = foldl _+_ 0 $ map (uncurry _*_) $ zip boxes gifts
+       in weight <= w * h
+
+part2 : String → Int
+
+run : String -> IO Unit
+run fn = do
+  putStrLn fn
+  text <- readFile fn
+  part1 text
+
+main : IO Unit
+main = do
+  run "aoc2025/day12/eg.txt"
+  run "aoc2025/day12/input.txt"

aoc2025/Day9.newt

@@ -34,8 +34,8 @@ area (B l r t b) = (abs (l - r) + 1) * (abs (t - b) + 1)
 mkbox : Point → Point → Box
 mkbox (a,b) (c,d) = B (min a c) (max a c) (min b d) (max b d)
 
-boxes : List Point → List Box
-boxes pts = go pts Nil
+makeBoxes : List Point → List Box
+makeBoxes pts = go pts Nil
   where
     go2 : Point → List Point → List Box → List Box
     go2 pt (x :: xs) acc = go2 pt xs (mkbox pt x :: acc)
@@ -63,8 +63,7 @@ getLines points = go points Nil
 
 -- I'm assuming the winner isn't a single row/column
 part2 : List (Int × Box) → List Line → Int
-part2 Nil _ = 0
-part2 ((size, box) :: rest) lines = if checkRec box then size else part2 rest lines
+part2 boxes lines = go boxes lines 0
   where
     winds : Box → Line → Bool
     winds (B l r t b) (VL x y1 y2) =
@@ -77,17 +76,24 @@ part2 ((size, box) :: rest) lines = if checkRec box then size else part2 rest li
       let (Nothing) = find (isect box) lines | _ => False in
       let winding = length' $ filter (winds box) lines in mod winding 2 == 1
 
+    go : List (Int × Box) → List Line → Int → Int
+    go Nil _ acc = acc
+    go ((size, box) :: rest) lines acc =
+      if size < acc then go rest lines acc
+      else if checkRec box then go rest lines size
+      else go rest lines acc
+
 run : String -> IO Unit
 run fn = do
   putStrLn fn
   text <- readFile fn
   let (pts@(a :: _)) = parse text | _ => putStrLn "empty input"
-  -- printLn pts
-  let sortBoxes = qsort (\ a b => fst a > fst b) $ map (\box => (area box, box)) $ boxes pts
-  let ((p1,_) :: _ ) = sortBoxes | _ => printLn "no boxes"
-  putStrLn $ "part1 \{show p1}"
+  let boxes = map (\box => (area box, box)) $ makeBoxes pts
+  let ((p1,_) :: _ ) = boxes | _ => printLn "no boxes"
+  let x = foldl (\ acc x => if fst x > acc then fst x else acc) 0 boxes
+  putStrLn $ "part1 \{show p1} \{show x}"
   let vl = getLines $ a :: reverse pts
-  putStrLn $ "part2 " ++ show (part2 sortBoxes vl)
+  putStrLn $ "part2 " ++ show (part2 boxes vl)
 
 main : IO Unit
 main = do

aoc2025/Node.newt

@@ -2,6 +2,31 @@ module Node
 
 import Prelude
 
+-- Promise has some sequencing issues with IO
+ptype Promise : U → U
+pfunc promise_bind : ∀ a b. Promise a → (a → Promise b) → Promise b := `(a,b, ma, mab) => ma.then(v => mab(v))`
+pfunc promise_pure : ∀ a. a → Promise a := `(_, a) => Promise.resolve(a)`
+-- The potential issue here is that fa runs before it is even passed in!
+pfunc promise_app : ∀ a b. → Promise (a → b) → Promise a → Promise b := `(a,b,fab,fa) => fab.then(ab => fa.then(a => Promise.resolve(ab(a))))`
+-- This runs everything immediately...
+pfunc promise_lift : ∀ a. IO a → Promise a := `(a,f) => Promise.resolve(f('WORLD').h1)`
+
+instance Monad Promise where
+  bind = promise_bind
+  pure = promise_pure
+
+instance Applicative Promise where
+  return = pure
+  fab <*> fa = promise_app fab fa
+
+instance HasIO Promise where
+  liftIO = promise_lift
+
 pfunc fs : JSObject := `require('fs')`
 pfunc getArgs : List String := `arrayToList(String, process.argv)`
 pfunc readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(require('fs').readFileSync(fn, 'utf8'), w)`
+
+pfunc runPromise uses (MkIORes MkUnit) : ∀ a. Promise a → IO Unit := `(a,p) => (w) => {
+  // p(w)
+  return Prelude_MkIORes(Prelude_MkUnit, w)
+}`

aoc2025/Z3.newt

@@ -0,0 +1,46 @@
+module Z3
+
+import Prelude
+import Node
+
+ptype Context
+-- Flag if optimizer or solver
+ptype Solver : Bool → U
+ptype Arith
+ptype Z3Bool
+ptype Model
+ptype Z3
+
+pfunc initZ3 : Promise Z3 := `require('z3-solver').init()`
+pfunc z3ResetMemory : Promise Z3 := `(z3) => z3.Z3.reset_memory()`
+pfunc initContext : Z3 → String → Context := `(z3, name) => z3.Context(name)`
+
+pfunc newSolver : Context → Solver False := `(Context) => new Context.Solver()`
+pfunc newOptimizer : Context → Solver True := `(Context) => new Context.Optimize()`
+
+
+-- These probably should be IO or Promise
+pfunc freshInt : {{Context}} → Promise Arith := `(Context) => Promise.resolve(Context.Int.fresh())`
+pfunc z3const : {{Context}} → String → Arith := `(Context, name) => Context.Int.const(name)`
+pfunc arith_add : Arith → Arith → Arith := `(a,b) => a.add(b)`
+pfunc z3int : {{Context}} → Int → Arith := `(Context,a) => Context.Int.val(a)`
+
+-- We can't overload operators for these because of the return type
+
+pfunc z3eq : Arith → Arith → Z3Bool := `(a,b) => a.eq(b)`
+pfunc z3ge : Arith → Arith → Z3Bool := `(a,b) => a.ge(b)`
+
+pfunc z3add : ∀ b. Solver b → Z3Bool → Promise Unit := `(_, solver, exp) => Promise.resolve(solver.add(exp))`
+pfunc z3minimize : Solver True → Arith → Promise Unit := `(solver, exp) => Promise.resolve(solver.minimize(exp))`
+
+pfunc z3check : ∀ b. Solver b → Promise String := `(b, solver) => solver.check()`
+
+pfunc getModel : ∀ b. Solver b → Promise Model := `(b, solver) => Promise.resolve(solver.model())`
+
+pfunc getInt : {{Model}} → Arith → Int := `(model, exp) => {
+  let n = +(model.eval(exp).toString())
+  return isNaN(n) ? 0 : n
+}`
+
+instance Add Arith where
+  a + b = arith_add a b

aoc2025/Z3Test.newt

@@ -0,0 +1,38 @@
+module Z3Test
+
+import Prelude
+import Node
+import Z3
+
+test : Promise Unit
+test = do
+  context <- initZ3 "main"
+  x0 <- freshInt
+  x1 <- freshInt
+  x2 <- freshInt
+  x3 <- freshInt
+  x4 <- freshInt
+  x5 <- freshInt
+  let solver = newOptimizer context
+
+  z3add solver $ z3ge x0 $ z3int 0
+  z3add solver $ z3ge x1 $ z3int 0
+  z3add solver $ z3ge x2 $ z3int 0
+  z3add solver $ z3ge x3 $ z3int 0
+  z3add solver $ z3ge x4 $ z3int 0
+  z3add solver $ z3ge x5 $ z3int 0
+
+  z3add solver $ z3eq (x4 + x5) (z3int 3)
+  z3add solver $ z3eq (x1 + x5) (z3int 5)
+  z3add solver $ z3eq (x2 + x3 + x4) (z3int 4)
+  z3add solver $ z3eq (x0 + x1 + x3) (z3int 7)
+
+  z3minimize solver $ x0 + x1 + x2 + x3 + x4 + x5
+
+  res <- z3check solver
+  liftIO $ putStrLn "GOT \{res}"
+
+
+-- switch to promise mode
+main : IO (Promise Unit)
+main = pure test

aoc2025/day10/eg.txt

@@ -0,0 +1,3 @@
+[.##.] (3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
+[...#.] (0,2,3,4) (2,3) (0,4) (0,1,2) (1,2,3,4) {7,5,12,7,2}
+[.###.#] (0,1,2,3,4) (0,3,4) (0,1,2,4,5) (1,2) {10,11,11,5,10,5}

aoc2025/day11/eg.txt

@@ -0,0 +1,10 @@
+aaa: you hhh
+you: bbb ccc
+bbb: ddd eee
+ccc: ddd eee fff
+ddd: ggg
+eee: out
+fff: out
+ggg: out
+hhh: ccc fff iii
+iii: out

aoc2025/day11/eg2.txt

@@ -0,0 +1,13 @@
+svr: aaa bbb
+aaa: fft
+fft: ccc
+bbb: tty
+tty: ccc
+ccc: ddd eee
+ddd: hub
+hub: fff
+eee: dac
+dac: fff
+fff: ggg hhh
+ggg: out
+hhh: out

aoc2025/day12/eg.txt

@@ -0,0 +1,33 @@
+0:
+###
+##.
+##.
+
+1:
+###
+##.
+.##
+
+2:
+.##
+###
+##.
+
+3:
+##.
+###
+##.
+
+4:
+###
+#..
+###
+
+5:
+###
+.#.
+###
+
+4x4: 0 0 0 0 2 0
+12x5: 1 0 1 0 2 2
+12x5: 1 0 1 0 3 2

newt-vscode/src/abbrev.ts

@@ -29,6 +29,8 @@ export const ABBREV: Record<string, string> = {
   "\\Gs": "σ",
   "\\Gt": "τ",
   "\\GD": "Δ",
+  "\\GS": "Σ",
+  "\\GP": "∏",
   "\\[[": "⟦",
   "\\]]": "⟧",
 };

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -3,6 +3,10 @@
   "name": "newt",
   "scopeName": "source.newt",
   "patterns": [
+    {
+      "name": "invalid.illegal.trace",
+      "match": "\\b(trace|strace|fatalError)\\b"
+    },
     {
       "name": "comment.block.newt",
       "begin": "/-",

playground/TODO.md

@@ -7,20 +7,17 @@
 - [ ] make sample files available for import
   - workaround is to visit the file first
   - we can put them in the zip file and pull them over the IPC
-- [ ] make phone layout automatic
-- [ ] case split &c
+- [x] make phone layout automatic
+- [x] case split &c
 - [x] move newt to a worker (shim + newt + listener)
 - [x] tabs for source, compiler output
 - [x] Show errors in editor
 - [x] show tabs on rhs
-  - [ ] make editor a tab on mobile
-    - (or possibly put the tab bar under the keyboard)
 - [x] publish / host on github
 - [ ] multiple persistent files
 - [x] kill return for autocomplete
 - [x] save to url (copy from idris2-playground)
 - [ ] click on url
-- [ ] settings
+- [ ] settings pane
   - compilation is now optional, what else do we need for newt?
-
-
+- [ ] update docs for new icons (how do we get them in there...)

playground/src/help.md

@@ -16,11 +16,9 @@ The editor will typecheck the file with newt and render errors as the file is ch
 
 ## Buttons
 
-▶ Compile and run the current file in an iframe, console output is collected to the console tab.
+:play: Compile and run the current file in an iframe, console output is collected to the console tab.
 
-📋 Embed the current file in the URL and copy to clipboard
-
-↕ or ↔ Toggle vertical or horziontal layout (for mobile)
+:share: Embed the current file in the URL and copy to clipboard.
 
 ## Keyboard
 

playground/src/main.ts

@@ -26,13 +26,15 @@ let topData: undefined | TopData;
 const ipc = new IPC();
 
 function mdline2nodes(s: string) {
-  let cs: (VNode|string)[] = []
-  let toks = s.matchAll(/(\*\*.*?\*\*)|(\*.*?\*)|(_.*?_)|[^*]+|\*/g)
+  let cs: (VNode<any>|string)[] = []
+  let toks = s.matchAll(/\*\*(.*?)\*\*|\*(.*?)\*|_(.*?)_|!\[(.*?)\]\((.*?)\)|:(\w+):|[^*]+|\*/g);
   for (let tok of toks) {
-    if (tok[1]) cs.push(h('b',{},tok[0].slice(2,-2)))
-    else if (tok[2]) cs.push(h('em',{},tok[0].slice(1,-1)))
-    else if (tok[3]) cs.push(h('em',{},tok[0].slice(1,-1)))
-    else cs.push(tok[0])
+       tok[1] && cs.push(h('b',{},tok[1]))
+    || tok[2] && cs.push(h('em',{},tok[2]))
+    || tok[3] && cs.push(h('em',{},tok[0].slice(1,-1)))
+    || tok[5] && cs.push(h('img',{src: tok[5], alt: tok[4]}))
+    || tok[6] && cs.push(h(Icon, {name: tok[6]}))
+    || cs.push(tok[0])
   }
   return cs
 }
@@ -361,6 +363,19 @@ preload.then(() => {
   }
 });
 
+const icons: Record<string,string> = {
+  'play-dark': play,
+  'play-light': play_light,
+  'share-dark': share,
+  'share-light': share_light,
+};
+
+function Icon({name}: {name: string}) {
+  let dark = state.dark.value ? 'dark' : 'light'
+  let src = icons[name + '-' + dark];
+  return h('img', {src});
+}
+
 function EditWrap() {
   const options = state.files.value.map((value) =>
     h("option", { value }, value)

src/Data/Fin.newt

@@ -0,0 +1,38 @@
+module Data.Fin
+import Prelude
+
+-- TODO - handle erased params in Nat transform.
+-- TODO - double check we erase params to type constructors
+data Fin : Nat → U where
+  FZ : ∀ k. Fin (S k)
+  FS : ∀ k. Fin k → Fin (S k)
+
+allFins : (n : Nat) → List (Fin n)
+allFins Z = Nil
+allFins (S k) = FZ :: map FS (allFins k)
+
+-- TODO maybe teach compiler to recognize and make magic Nat Eq fast?
+instance ∀ n. Eq (Fin n) where
+  FZ == FZ = True
+  FS l == FS n = l == n
+  _ == _ = False
+
+-- TODO - recognize identity functions
+weaken : ∀ k. Fin k → Fin (S k)
+weaken FZ = FZ
+weaken (FS k) = FS $ weaken k
+
+instance ∀ n. Cast (Fin n) Nat where
+  cast FZ = Z
+  cast (FS x) = S (cast x)
+
+instance ∀ n. Cast (Fin n) Int where
+  cast FZ = 0
+  cast (FS x) = 1 + (cast x)
+
+instance ∀ k. Show (Fin k) where
+  show x = show {Nat} $ cast x
+
+lastFin : {n : _} -> Fin (S n)
+lastFin {Z} = FZ
+lastFin {S _} = FS lastFin

src/Data/Vect.newt

@@ -0,0 +1,52 @@
+module Data.Vect
+
+import Prelude
+import Data.Fin
+
+infixr 6 _:-_
+data Vect : (0 n : Nat) → (0 a : U) → U where
+  VNil :  ∀ a. Vect Z a
+  _:-_ : ∀ k a. a → Vect k a → Vect (S k) a
+
+vindex : ∀ n a. Fin n → Vect n a → a
+vindex FZ (x :- _) = x
+vindex (FS k) (x :- rest) = vindex k rest
+vindex () VNil -- Idris doesn't need this hint.
+
+instance ∀ k. Functor (Vect k) where
+  map f VNil = VNil
+  map f (x :- xs) = f x :- map f xs
+
+toVect : ∀ a. (n : Nat) -> List a -> Maybe (Vect n a)
+toVect (S k) (x :: xs) = _:-_ x <$> toVect k xs
+toVect Z Nil = Just VNil
+toVect _ _ = Nothing
+
+instance ∀ n a. Cast (Vect n a) (List a) where
+  cast VNil = Nil
+  cast (x :- xs) = x :: cast xs
+
+instance ∀ n a. {{Show a}} → Show (Vect n a) where
+  show {n} {a} xs = show $ cast {_} {List a} xs
+
+vIndexes : (n : Nat) → Vect n (Fin n)
+vIndexes Z = VNil
+vIndexes (S k) = FZ :- map FS (vIndexes k)
+
+vIndexes' : ∀ n a. Vect n a → Vect n (Fin n)
+vIndexes' VNil = VNil
+vIndexes' ( _ :- xs) = FZ :- map FS (vIndexes' xs)
+
+venum : ∀ n a. Vect n a → Vect n (Fin n × a)
+venum VNil = VNil
+venum (x :- xs) = (FZ, x) :- map (mapFst FS) (venum xs)
+
+zipVect : ∀ n a b. Vect n a → Vect n b → Vect n (a × b)
+zipVect VNil VNil = VNil
+zipVect (x :- xs) (y :- ys) = (x,y) :- zipVect xs ys
+
+vset : ∀ n a. Fin n → a → Vect n a → Vect n a
+vset () el VNil
+vset FZ el (x :- xs) = el :- xs
+vset (FS k) el (x :- xs) = x :- vset k el xs
+

src/Lib/Elab.newt

@@ -526,6 +526,7 @@ unify env mode t u = do
     unifyVar : Val -> Val -> M UnifyResult
     unifyVar t'@(VVar fc k sp)  u'@(VVar fc' k' sp')  =
       if k == k' then unifySpine env mode (k == k') sp sp'
+      -- FIXME - get some names in here.
       else error fc "Failed to unify \{show t'} and \{show u'}"
 
     unifyVar t'@(VVar fc k Lin) u = do

src/Lib/Erasure.newt

@@ -44,8 +44,10 @@ eraseSpine env t ((fc, arg) :: args) _ = do
   eraseSpine env (App fc t u) args Nothing
 
 doAlt : EEnv -> CaseAlt -> M CaseAlt
--- REVIEW do we extend env?
+-- REVIEW we're sticking Erased on RHS for impossible, might want a runtime error or elide the case.
+doAlt env (CaseDefault (Erased fc)) = pure $ CaseDefault (Erased fc)
 doAlt env (CaseDefault t) = CaseDefault <$> erase env t Nil
+doAlt env (CaseCons name args (Erased fc)) = pure (CaseCons name args (Erased fc))
 doAlt env (CaseCons name args t) = do
   top <- getTop
   let (Just (MkEntry _ str type def _)) = lookup name top

src/Lib/ProcessDecl.newt

@@ -181,12 +181,17 @@ processDef ns fc nm clauses = do
   -- moved to Compile.newt because it was interfering with type checking (Zoo4eg.newt) via over-reduction
   -- tm' <- zonk top 0 Nil tm
 
+  -- for effect, so we see errors in the editor
+  -- We need to keep the _unerased_ term for checking
+  _ <- erase Nil tm Nil
+
   debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm} : \{render 90 $ pprint Nil ty}"
   updateDef (QN ns nm) fc ty (Fn tm)
   -- putStrLn "complexity \{show (QN ns nm)} \{show $ complexity tm}"
   -- putStrLn $ show tm
   -- TODO we need some protection against inlining a function calling itself.
   -- We need better heuristics, maybe fuel and deciding while inlining.
+  -- someday users will tag functions as inline, so maybe an explicit loop check
   -- IO,bind is explicit here because the complexity has a 100 in it.
   let name = show $ QN ns nm
   if complexity tm < 15 || name == "Prelude.Prelude.Monad Prelude.IO,bind" || name == "Prelude._>>=_"

src/Lib/Tokenizer.newt

@@ -56,6 +56,7 @@ quoteTokenise ts@(TS el ec toks chars) startl startc acc = case chars of
   -- TODO newline in string should be an error
   '\n' :: cs => Left $ E (MkFC "" (MkBounds el ec el ec)) "Newline in string"
   '\\' :: 'n' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< '\n')
+  '\\' :: 't' :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< chr 9)
   '\\' :: c :: cs => quoteTokenise (TS el (ec + 2) toks cs) startl startc (acc :< c)
   c :: cs => quoteTokenise (TS el (ec + 1) toks cs) startl startc (acc :< c)
   Nil => Left $ E (MkFC "" (MkBounds el ec el ec)) "Expected '\"' at EOF"
@@ -103,7 +104,10 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
   '_' :: ',' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_,_") cs)
   '_' :: '.' :: '_' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) MixFix "_._") cs)
   '\'' :: '\\' :: c :: '\'' :: cs =>
-    let ch = ite (c == 'n') '\n' c
+    let ch = case c of
+              'n' => '\n'
+              't' => chr 9
+              c => c
     in rawTokenise (TS sl (sc + 4) (toks :< mktok False sl (sc + 4) Character (singleton ch)) cs)
   '\'' :: c :: '\'' :: cs => rawTokenise (TS sl (sc + 3) (toks :< mktok False sl (sc + 3) Character (singleton c)) cs)
   '#' :: cs => doRest (TS sl (sc + 1) toks cs) Pragma isIdent (Lin :< '#')

src/Lib/TopContext.newt

@@ -43,8 +43,7 @@ instance Show TopContext where
 emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext
 emptyTop = do
   let mcctx = MC emptyMap Nil 0 CheckAll
-  errs <- newIORef $ the (List Error) Nil
-  pure $ MkTop emptyMap Nil emptyMap Nil emptyMap mcctx 0 errs emptyMap
+  pure $ MkTop emptyMap Nil emptyMap Nil emptyMap mcctx 0 Nil emptyMap
 
 
 setFlag : QName → FC → EFlag → M Unit
@@ -91,4 +90,4 @@ addHint qn = do
 addError : Error -> M Unit
 addError err = do
   top <- getTop
-  modifyIORef top.errors (_::_ err)
+  modifyTop [ errors $= _::_ err ]

src/Lib/Types.newt

@@ -433,7 +433,7 @@ record TopContext where
 
   -- Global values
   verbose : Int -- command line flag
-  errors : IORef (List Error)
+  errors : List Error
   ops : Operators
 
 -- we'll use this for typechecking, but need to keep a TopContext around too.

src/Main.newt

@@ -165,19 +165,15 @@ processModule importFC base stk qn@(QN ns nm) = do
   top <- getTop
 
   let mod = MkModCtx csum top.defs top.metaCtx top.ops
-  errors <- liftIO {M} $ readIORef top.errors
-  if stk /= Nil && length' errors == 0
+  if stk /= Nil && length' top.errors == 0
     then dumpModule qn src mod
     else pure MkUnit
 
   let modules = updateMap modns mod top.modules
   modifyTop [modules := modules]
 
-  (Nil) <- liftIO {M} $ readIORef top.errors
-    | errors => do
-        -- we're now showing errors when they occur, so they're next to debug messages
-        -- traverse (putStrLn ∘ showError src) errors
-        exitFailure "Compile failed"
+  let (Nil) = top.errors
+    | errors => exitFailure "Compile failed"
   logMetas $ reverse $ listValues top.metaCtx.metas
   pure src
   where
@@ -199,7 +195,7 @@ showErrors : String -> String -> M Unit
 showErrors fn src = do
   top <- getTop
   -- TODO {M} needed to sort out scrutinee
-  (Nil) <- liftIO {M} $ readIORef top.errors
+  let (Nil) = top.errors
     | errors => do
         traverse (putStrLn ∘ showError src) errors
         exitFailure "Compile failed"

src/Prelude.newt

@@ -607,8 +607,15 @@ elem v (x :: xs) = if v == x then True else elem v xs
 -- TODO no empty value on my `Add`, I need a group..
 -- sum : ∀ a. {{Add a}} → List a → a
 -- sum xs = foldl _+_
+
+-- TODO debugStr is not super useful any more.
 pfunc trace uses (debugStr) : ∀ a. String → a → a := `(_, msg, a) => { console.log(msg,Prelude_debugStr(_,a)); return a }`
 
+pfunc prim_strace : String → String → String := `(msg, a) => { console.log(msg,a); return a }`
+
+strace : ∀ a. {{Show a}} → String → a → a
+strace msg a = let x = prim_strace msg (show a) in a
+
 mapMaybe : ∀ a b. (a → Maybe b) → List a → List b
 mapMaybe {a} {b} f xs = go Lin xs
   where
@@ -695,6 +702,11 @@ isNothing : ∀ a. Maybe a → Bool
 isNothing Nothing = True
 isNothing _ = False
 
+isJust : ∀ a. Maybe a → Bool
+isJust Nothing = False
+isJust _ = True
+
+
 instance Bifunctor _×_ where
   bimap f g (a,b) = (f a, g b)
 
@@ -787,7 +799,7 @@ instance Cast Int Nat where
   cast n = intToNat n
 
 instance Show Char where
-  show c = jsShow c
+  show c = "'\{jsShow c}'"
 
 swap : ∀ a b. a × b → b × a
 swap (a,b) = (b,a)
@@ -885,7 +897,7 @@ ignore = map (const MkUnit)
 
 instance ∀ a. {{Show a}} → Show (Maybe a) where
   show Nothing = "Nothing"
-  show (Just a) = "Just {show a}"
+  show (Just a) = "Just \{show a}"
 
 pfunc isPrefixOf uses (True False): String → String → Bool := `(pfx, s) => s.startsWith(pfx) ? Prelude_True : Prelude_False`
 pfunc isSuffixOf uses (True False): String → String → Bool := `(pfx, s) => s.endsWith(pfx) ? Prelude_True : Prelude_False`

tests/Quantity.newt.fail

@@ -0,0 +1,10 @@
+*** Process tests/Quantity.newt
+module Prelude
+module Quantity
+ERROR at tests/Quantity.newt:11:15--11:16: used erased value x$0 (FIXME FC may be wrong here)
+  -- This should fail to compile
+  bar : ∀ x. Nat
+  bar {x} = foo x
+                ^
+
+Compile failed