Add list sugar

Allow:
```newt
data Foo : U
```
as a forward declaration for data. (The `Foo : U` syntax still works for
now.)

.editorconfig

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

.gitignore

@@ -3,11 +3,19 @@ build/
 *~
 *.swp
 *.log
-*.agda
-*.agdai
-/*.js
+*.bak
 input.txt
 node_modules
 mkday.py
 tmp
 min.js.gz
+src/Revision.newt
+.calva
+.clj-kondo
+.joyride
+.lsp
+.vscode
+.helix
+bootstrap/serializer.js
+/newt-vscode-lsp/src/newt.js
+/playground/src/newt.js

.tangled/workflows/build.yml

@@ -0,0 +1,17 @@
+when:
+  - event: ["push", "manual"]
+    branch: ["main"]
+engine: "nixery"
+dependencies:
+  nixpkgs:
+    - nodejs
+    - gnumake
+    - diffutils
+    - findutils
+    - git
+    - time
+steps:
+  - name: "build newt"
+    command: "make newt3.js"
+  - name: "test"
+    command: "make test"

Makefile

@@ -1,52 +1,83 @@
 SRCS=$(shell find src -name "*.newt")
 
-# Node shaves off 40% of the time.
-# RUNJS=bun run
-RUNJS=node
-
 .PHONY:
 
-all: newt.js
+all: build/newt.js
 
-newt.js: ${SRCS}
-	-rm build/* >/dev/null
-	$(RUNJS) bootstrap/newt.js src/Main.newt -o newt.js
+newt2: build/newt2.js
 
-newt2.js: newt.js
-	-rm build/*
-	$(RUNJS) newt.js src/Main.newt -o newt2.js
+newt3: build/newt3.js
 
-newt3.js: newt2.js
-	-rm build/*
-	time $(RUNJS) newt2.js src/Main.newt -o newt3.js
-	cmp newt2.js newt3.js
-
-min.js: newt3.js scripts/pack
-	scripts/pack
-	gzip -kf min.js
-	ls -l min.js min.js.gz
-
-test: newt.js
+test: build/newt.js
 	scripts/test
 
-aoctest: newt.js
+cheztest: build/newt.so
+	make test NEWT='chez --program build/newt.so' RUNOUT="chez --script" OUTFILE=tmp/out.ss
+
+aoctest: build/newt.js
 	scripts/aoc
+	scripts/aoc25
 
-# Misc
+lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js
 
-vscode:
-	cd newt-vscode && vsce package && code --install-extension *.vsix
+# build / install new LSP vscode extension
+vscode-lsp vscode: lsp
+	cd newt-vscode-lsp && vsce package && code --install-extension *.vsix
 
 playground: .PHONY
 	cd playground && ./build
 
 profile: .PHONY
-	rm isolate* build/*; node --prof newt.js -o newt2.js src/Main.newt
+	rm isolate* build/*
+	node --prof build/newt.js -o build/newt2.js src/Main.newt
 	node --prof-process isolate* > profile.txt
 
 clean:
-	rm newt*.js iife.js min.js min.js.gz
+	rm  build/*
 
 audit: .PHONY
 	(cd playground && npm audit)
 	(cd newt-vscode && npm audit)
+	(cd newt-vscode-lsp && npm audit)
+
+##
+
+build:
+	mkdir -p build
+
+src/Revision.newt: .PHONY build
+	sh ./scripts/mkrevision
+
+build/newt.js: ${SRCS} src/Revision.newt build
+	node bootstrap/newt.js src/Main.newt -o build/newt.js
+
+build/newt2.js: build/newt.js
+	node build/newt.js src/Main.newt -o build/newt2.js
+
+build/newt3.js: build/newt2.js
+	time node build/newt2.js src/Main.newt -o build/newt3.js
+	cmp build/newt2.js build/newt3.js
+
+build/newt.ss: build/newt.js
+	node build/newt.js src/Main.newt -o build/newt.ss
+
+build/newt.so: build/newt.ss prim.ss
+	chez --script scripts/compile-chez.ss
+
+build/newt2.ss: build/newt.so
+	time chez --program build/newt.so src/Main.newt -o build/newt2.ss
+
+build/lsp.js: ${SRCS} build/newt.js
+	node build/newt.js src/LSP.newt -o build/lsp.js
+
+newt-vscode-lsp/src/newt.js: build/lsp.js
+	cp build/lsp.js $@
+
+playground/src/newt.js: build/lsp.js
+	cp build/lsp.js $@
+
+newt-vscode-lsp/dist/lsp.js: newt-vscode-lsp/src/lsp.ts newt-vscode-lsp/src/newt.js
+	(cd newt-vscode-lsp && node esbuild.js)
+	chmod +x $@
+
+

README.md

@@ -24,7 +24,7 @@ The `Makefile` will build builds `./newt.js`. There is a bootstrap version of ne
 
 Newt can also be built by running `node bootstrap/newt.js src/Main.newt -o newt.js`.
 
-The source for the vscode extension is found in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `build/exec/newt` to exist in the workspace. And `make test` will run a few black box tests. Currently it simply checks return codes, since the output format is in flux.
+The source for the vscode extension is found in `newt-vscode`. Running `make vscode` will build and install it. The extension expects `newt.js` to exist in the workspace. And `make test` will run a few black box tests. The tests have an expected succesful output in a `.golden` file or expected failure output in a `.fail` file.
 
 ## Playground
 

TODO.md

@@ -1,11 +1,82 @@
 
 ## TODO
 
-- [ ] Maybe make the editor json more compact
+- [x] Scheme backend
+- [ ] Smart encoding of lists (and cons cells?) in scheme
+- [ ] Unsolved meta in Lib.Types doesn't print when building newt.
+  - delete Show Char to test, it does surface in the LSP, we need to dump these when processing dependent modules
+- [ ] maybe `let case` instead of `let ()` (which is a little subtle)
+  - Or simply put a term in there and treat as a variable iff it is lowercase and non-app
+- [x] Use looping for TCO
+  - For single functions at least - I think this would be a performance win. I've learned that the slowness on `bun` goes away if I drop the TCO transform.
+  - Doing this manually for `lookupT23` got 3% speedup.
+  - got 12% speedup overall from this, not doing it for mutual recursion
+- [ ] Importing Prelude twice should be an error (currently it causes double hints and breaks auto)
+- [x] For errors in other files, point to the import
+- [x] Unsolved metas should be errors (user metas are fine)
+- [x] Better syntax for forward declared data (so we can distinguish from functions)
+- [ ] maybe allow "Main" module name for any file
+- [ ] preserve information on record / class / instance for LSP "document symbols" kind
+  - We will want some of this for default implementations in class
+  - It may help avoid reverse-engineering the class when processing implementation
+- [ ] Put `Def` on `Ref`
+  - It may be Axiom for forward/recursive functions, but it would get us DCon and TCon info without lookup - and may save passing around the Ref2 (+lookup) during Compilation.
+- [x] Restore "add missing cases" for LSP mode
+- [x] Case split for LSP mode
+- [x] Require lowercase pattern variables
+  - I accidentally misspell a constructor and end up with a wildcard.
+- [x] Leverage LSP code for web playground
+- [ ] Improve handling of names:
+  - We need FC on names in a lot of places
+  - [x] FC for duplicate `data`, `record`, `class` name is wrong (points to `data`)
+  - [x] FC on bad import should point to the name
+  - [x] Current module overrides imports
+  - [ ] Duplicate data constructors point to `data`
+  - [ ] Allow Qualified names in surface syntax
+  - Don't disambiguate on type for now
+- [ ] Could we disambiguate just Data constructors on type?
+- [x] change "in prefix position" and "trailing operator" errors to do sections
+- [ ] maybe add fat arrows, I keep wanting to type them, `{{...}}` is a little ugly
+  - There may be ambiguity issues at the parsing level, but we don't have typecase, so.
+  - It's less to type, too.
+- [x] get some names on add missing cases (if not too difficult)
+- [ ] Implement "add missing cases" for playground
+- [x] add optional types to case `case xxx : Maybe Int of ...`
+- [x] "Expected keyword" at `\ a ->` should be error at the `->`
+- [x] 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.
+- [x] Add Foldable
+- [ ] Maybe return constraints instead of solving metas during unification
+  - We already return non-meta constraints for work on the LHS.
+  - We might get into a situation where solving immediately would have gotten us more progress?
+- [ ] "Failed to unify %var0 and %var1" - get names in there
+  - Need fancier `Env` or the index on the type of `Tm`
+  - Or the name on the VVar?
+  - Also we should render %pi, etc more readably (bonus points for _×_)
+- Editor support:
+  - [x] add missing cases should skip indented lines
+  - [x] add missing cases should handle `_::_`
+  - [x] add missing cases should share code between vscode and playground
+  - [x] "Not in scope" should offer to import
+  - [x] Case split
+- [ ] Delay checking
+  - We have things like `foldr (\ x acc => case x : ...`, where the lambda doesn't have a good type, so we have to be explicit. If we could defer the checking of that expression until more things are solved, we might not need the annotation (e.g. checking the other arguments). Some `case` statements may have a similar situation.
+  - One idea is to throw the checks onto some sort of TODO list and run whatever works. (I think Idris may have a heuristic where it checks arguments backwards in some cases.)
+- [x] Dependent records (I guess I missed that bit)
+- [x] Arguments on records
+- [ ] Add sugar for type aliases (maybe infer arguments)
+  - Lean has this, we maybe could run infer on the RHS and call it a day? We would need a simple LHS, though.
+- [ ] see if we can get a better error if `for` is used instead of `for_` in do blocks
+- [ ] Maybe make the editor json more compact (we want to replace this with REPL / LSP though)
 - [ ] Remove erased args from primitive functions
   - But we need separate `+` functions rather than the magic `∀ a. a -> a -> a` to support other backends
 - [ ] consider moving primitive functions to a support file
-  - Downside here is that we lose some dead code elimination, but it better supports bootstrapping when calling convention changes.
+  - Downside here is that we lose some dead code elimination
+  - it better supports bootstrapping when calling convention changes.
+  - it better supports other
 - [ ] Alternate backend
   - Options are scheme, C, WASM, arm assembly. Maybe C is the next step.
 - [ ] allow declaration of primitive operators
@@ -19,6 +90,7 @@
 - [ ] See if we can split up `Elab.newt`
   - Unify, checking, and case builder have circular references.
   - Perhaps unify should return constraints instead of calling solve directly.
+  - passing a pointer to `check` in the context may suffice
 - [ ] Add error for non-linear names in pattern matching (currently it picks one)
   - We probably should handle forced values. Idris requires them to have the same name.
 - [ ] Functions with erased-only arguments still get called with `()` - do we want this or should they be constants?
@@ -28,25 +100,23 @@
 - [ ] 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.
+  - Does softening up check errors break `auto`?
+  - [ ] 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).
   - Do we want to (maybe later) keep the scope as a FC? We could do scope at point then.
-  - But ideally we'd switch to a server/repl, so we don't have to mess around with serializing stuff.
 - [ ] LSP and/or more editor support
   - [ ] refactor to query based?  E.g. importing a module
-  - [ ] would be nice to have "add missing cases" and "case split"
+  - [x] would be nice to have "add missing cases" and "case split"
   - [x] Probably need ranges for FC
-  - [ ] leave an interactive process running
+  - [x] leave an interactive process running
   - [ ] restart mid file (we could save state per top level decl)
   - [ ] rename in editor (need to accumulate all names and what they reference)
   - [ ] who calls X?  We can only do this scoped to the current context for now. Someday whole source dir. #lsp
 - [ ] Pretty print
   - Can we format code? Maybe pull nearby comments or attach them like FC to tokens?
   - We would need to address stack and laziness issues in prettier printer (or make it merely pretty)
-- [ ] Look into descriptions, etc.
-  - Can generating descriptions help with automatic "show" implementations
-  - We lost debug printing when switching to numeric tags
 - [ ] Add info to Ref/VRef (is dcon, arity, etc)
   - To save lookups during compilation and it might make eval faster
 - [x] number tags for data constructors
@@ -60,7 +130,7 @@
   - [ ] Maybe add qualified names to surface syntax and allow / detect conflicts on reference
   - [ ] Add `export` keywords
 - [x] vscode - run newt when switching editors
-- [ ] case split
+- [x] case split
   - We could fake this up:
     - given a name and a point in the editor
     - walk through the function looking for the binder
@@ -68,8 +138,11 @@
     - enumerate valid constructors (and their arity)
     - Repeat the line with each, applied to args
     - For `<-` or `let` we'd want to fudge some `|` lines
+    - [ ] `let` has issues for multiline split / add missing
+    - [ ] `derive` has phantom splits in it
 - [x] Support "Add missing cases"
   - This has been hakced together
+  - LSP version now.
   - We could possibly fake up missing cases, too. Since they're listed and  have an FC pointing at the first one
 - [x] inline struct getters during code generation (We'd like  `x.h1.h2`)
 - [ ] Better FC for parse errors (both EOF and the ones that show up just after the error)
@@ -79,18 +152,20 @@
 - [x] implement magic nat
 - [ ] Consider splitting desugar/check
   - We can only check physical syntax at the moment, which has been inconvenient in a couple of spots where we want to check generated code. E.g. solutions to auto implicits.
-- [ ] record update can't elaborate if type is unsolved meta
-  - need to postpone elab until meta is known. Create fresh meta for the term to return and have postponed elab fill it in later.
+- [x] record update can't elaborate if type is unsolved meta
+  - The issue actually was a solved meta that wasn't forced
 - [x] drop erased args on types and top level functions
 - [x] can I do some inlining without blowing up code size?
   - [x] Maybe tag some functions as inline
   - [x] Eq Nat is not tail recursive because of the call to `==`
 - [ ] Eq Nat does things the hard way, can we turn it into `==`?
+  - We could have a compile time substitution for the function
+  - Maybe this could reify how we're hard coding functions to js operators
 - [x] use hint table for auto solving. (I think walking the `toList` is a big chunk of performance in `Elab.newt`.)
 - [x] implement string enum (or number, but I'm using strings for tags at the moment)
 - [x] use monaco input method instead of lean's
 - [x] `Def` is shadowed between Types and Syntax (TCon vs DCon), detect this
-- [ ] constructor magic for Bool?
+- [x] constructor magic for Bool?
   - We'd have to make assumptions about order.
   - we could special case some translations
   - extra code.
@@ -98,16 +173,15 @@
   - Two issues
     - I'm rewriting stuff in the context, leaving it in a bad state (forward references). I think I can avoid this.
     - The variables at the end of pattern matching have types with references in the wrong order. I think we can reorder them on dependencies.
-    - should w
+    - In some cases Idris stuffs Erased into types.
 - Improve `auto`
   - [ ] Improve cases where the auto isn't solved because of a type error
   - [ ] Handle `Foo Blah`, `Foo a => Bar a` vs `Bar Blah`
 - [ ] Add some optimizations
-  - [ ] see if we can make the typeclass stuff a little leaner, e.g. inline a projection of a static record.
+  - [ ] see if we can make the typeclass stuff a little leaner, e.g. inline a projection of a static record. (Maybe done now with the inlining, but verify.)
   - It would be nice if IO looked like imperative JS, but that might be a bit of a stretch.
-
-
 - [ ] warn on unused imports?
+  - Probably have to mark on name lookup, maybe wait until we have query-based
 - [x] redo code to determine base path
 - [x] emit only one branch for default case when splitting inductives
 - [x] save/load results of processing a module
@@ -121,10 +195,11 @@
 - [x] get port to run
   - [x] something goes terribly wrong with traverse_ and for_ (related to erasure, I think)
 - [x] ~~don't use `take` - it's not stack safe~~ The newt version is stack safe
-- [ ] show user hole info even in case of error
+- [x] show user hole info even in case of error
 - [x] tokenizer that can be ported to newt
 - [ ] Add default path for library, so we don't need symlinks everywhere and can write tests for the library
   - We need this to work for tests / dev and for installed newt.
+  - The new `FileSource` mechanism might help here.
 - [x] string interpolation?
   - The tricky part here is the `}` - I need to run the normal tokenizer in a way that treats `}` specially.
   - Idris handles `putStrLn "done \{ show $ add {x=1} 2}"` - it recurses for `{` `}` pairs.  Do we want that complexity?
@@ -138,6 +213,7 @@
 - [x] record update sugar
 - [x] Change `Ord` to be more like Idris - LT / EQ / GT (and entail equality)
 - [ ] Consider making `<` independent of `Ord`, so we get the `<` oper in the javascript.
+  - Maybe a "default implementation" deal.
 - [x] Keep a `compare` function on `SortedMap` (like lean)
   - `emptyMap` helper defaults to `compare` from `Ord a`
 - [x] keymap for monaco
@@ -174,8 +250,9 @@
 - [x] Fix string printing to be js instead of weird Idris strings
 - [x] make $ special
   - Makes inference easier, cleaner output, and allows `foo $ \ x => ...`
-  - [ ] `$` no longer works inside ≡⟨ ⟩ sort out how to support both that and `$ \ x => ...` (or don't bother)
+  - [ ] `$` no longer works inside ≡⟨ ⟩ - sort out how to support both that and `$ \ x => ...` (or don't bother)
     - We'd either need to blacklist all non-initial mixfix bits at the appropriate spots or always pass around a terminating token.
+    - I'm leaning towards _no_ here, because I may want to lift mixfix processing out of the parsing step in the future.
 - [x] **Translate newt to newt**
   - [x] Support @ on the LHS
   - [x] if / then / else sugar
@@ -193,7 +270,8 @@
   - Probably fixed by trying to solve auto immediately
 - [x] Can't skip an auto. We need `{{_}}` to be auto or have a `%search` syntax.
 - [x] add filenames to FC
-- [ ] Add full ranges to FC
+- [x] Add full ranges to FC
+  - [ ] Done, but we need to fix a bunch of FC in the parser
 - [x] maybe use backtick for javascript so we don't highlight strings as JS
 - [x] dead code elimination
 - [x] imported files leak info messages everywhere
@@ -203,18 +281,20 @@
 - [x] accepting DCon for another type (skipping case, but should be an error)
 - [ ] don't allow (or dot) duplicate names on LHS
 - [x] remove metas from context, M has TopContext
-- [ ] improve test driver
-  - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
+- [ ] add unit test framework
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)
 - [x] Bad module name error has FC 0,0 instead of the module or name
 - [ ] Revisit substitution in case building
 - [x] Check for shadowing when declaring dcon
   - Handles the forward decl in `Zoo1.newt`, but we'll need different syntax if
     we have different core terms for TCon/DCon/Function
-- [ ] Require infix decl before declaring mixfix names with `_` (helps find bugs) or implicitly define as infixl something if it is missing
+- [ ] Require infix decl before declaring mixfix names with `_` (helps find bugs) or implicitly define as infixl if it is missing
 - [x] sugar for typeclasses
 - [x] maybe add implicits in core to help resugar operators?
 - [ ] consider putting binders in environment, like Idris, to better mark `let` and to provide names
+  - I might want to distinguish `let` from pattern vars from user-`let`. The latter we probably want to exist
+    in emitted code, and the former inlined.  Currently they both live in context and the inlining occurs during
+    code-gen if the definition is simple enough (other vars or projections).
 - [x] move some top-level chattiness to `debug`
 - [ ] consider optionally compiling to eliminators for a second type-checking pass to help catch bugs.
 - [x] Allow unicode operators/names
@@ -263,6 +343,8 @@
   - [x] top level
   - [x] case statements
 - [ ] Lean ⟨ ⟩ anonymous constructors
+  - This would only work for `check` and we might need to revisit how `,` is handled.
+- [ ] Lean-like `#eval`
 - [ ] Lean-like .map, etc? (resolve name in namespace of target type, etc)
 - [x] autos / typeclass resolution
   - [x] very primitive version in place, not higher order, search at end
@@ -283,13 +365,15 @@
 - [ ] remove erased top level arguments
   - maybe have something shaped like `List Bool` for `arity`
 - [x] top level at point in vscode
-- [ ] repl
+- [x] repl
 - [x] don't match forced constructors at runtime
   - I think we got this by not switching for single cases
 - [x] magic nat (codegen as number with appropriate pattern matching)
 - [ ] magic tuple? (codegen as array)
   - Seems like this would be tricky as soon as the user starts peeling off the tail or consing them
 - [ ] magic newtype? (drop them in codegen)
+  - Needed before we newtype IO, so the tail recursion still works
+  - Without handling erased values, there are only two instances in the compiler code.
 - [x] vscode: syntax highlighting for String
 - [ ] add `poper` or variant of `pfunc` that maps to an operator, giving the js operator and precedence on RHS
   - This has now been hard-coded in codegen, but a syntax or something would be better.

aoc2024/Aoc.newt

@@ -34,3 +34,8 @@ instance Sub Point where
 
 -- instance Eq Point where
 --   (a,b) == (c,d) = a == c && b == d
+
+-- Doesn't play well with scheme and was removed from prelude, a couple of days depend on it for BigInt
+pfunc jsCompare uses (EQ LT GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT`
+pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? Prelude_True : Prelude_False`
+

aoc2024/Day21.newt.golden

@@ -1,8 +1,8 @@
 aoc2024/day21/eg.txt
-[(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2))]
+[('0', (3, 1)), ('1', (2, 0)), ('2', (2, 1)), ('3', (2, 2)), ('4', (1, 0)), ('5', (1, 1)), ('6', (1, 2)), ('7', (0, 0)), ('8', (0, 1)), ('9', (0, 2)), ('A', (3, 2))]
 part1 126384
 part2 154115708116294
 aoc2024/day21/input.txt
-[(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2))]
+[('0', (3, 1)), ('1', (2, 0)), ('2', (2, 1)), ('3', (2, 2)), ('4', (1, 0)), ('5', (1, 1)), ('6', (1, 2)), ('7', (0, 0)), ('8', (0, 1)), ('9', (0, 2)), ('A', (3, 2))]
 part1 248108
 part2 303836969158972

aoc2024/Day21monad.newt.golden

@@ -1,8 +1,8 @@
 aoc2024/day21/eg.txt
-[(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2))]
+[('0', (3, 1)), ('1', (2, 0)), ('2', (2, 1)), ('3', (2, 2)), ('4', (1, 0)), ('5', (1, 1)), ('6', (1, 2)), ('7', (0, 0)), ('8', (0, 1)), ('9', (0, 2)), ('A', (3, 2))]
 part1 126384
 part2 154115708116294
 aoc2024/day21/input.txt
-[(0, (3, 1)), (1, (2, 0)), (2, (2, 1)), (3, (2, 2)), (4, (1, 0)), (5, (1, 1)), (6, (1, 2)), (7, (0, 0)), (8, (0, 1)), (9, (0, 2)), (A, (3, 2))]
+[('0', (3, 1)), ('1', (2, 0)), ('2', (2, 1)), ('3', (2, 2)), ('4', (1, 0)), ('5', (1, 1)), ('6', (1, 2)), ('7', (0, 0)), ('8', (0, 1)), ('9', (0, 2)), ('A', (3, 2))]
 part1 248108
 part2 303836969158972

aoc2024/Day23.newt

@@ -27,10 +27,6 @@ startT s = case unpack s of
   ('t' :: _) => True
   _ => False
 
-isJust : ∀ a. Maybe a → Bool
-isJust (Just x) = True
-isJust _ = False
-
 checkK3 : Graph → EdgeSet → Edge → Int
 checkK3 g es (a,b) =
   let cand = fromMaybe Nil $ snd <$> lookupMap b g

aoc2025/Day1.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day1/eg.txt
+part1 3
+part2 6
+aoc2025/day1/input.txt
+part1 1100
+part2 6358

aoc2025/Day10.newt

@@ -0,0 +1,122 @@
+module Day10
+
+import Prelude
+import Node
+import Aoc
+import Parser
+import Data.Vect
+import Data.Fin
+import Z3
+
+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/Day11.newt.golden

@@ -0,0 +1,11 @@
+aoc2025/day11/eg.txt
+part1 5
+svr missing {"tag":0}
+part2 0
+aoc2025/day11/eg2.txt
+you missing {"tag":0}
+part1 0
+part2 2
+aoc2025/day11/input.txt
+part1 636
+part2 509312913844956

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/Day12.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day12/eg.txt
+[7, 7, 7, 7, 7, 7]
+3 rows, 0 easy, 3 maybe, 0 impossible
+aoc2025/day12/input.txt
+[7, 5, 7, 6, 7, 7]
+1000 rows, 479 easy, 0 maybe, 521 impossible

aoc2025/Day2.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day2/eg.txt
+part1 1227775554
+part2 4174379265
+aoc2025/day2/input.txt
+part1 18893502033
+part2 26202168557

aoc2025/Day3.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day3/eg.txt
+part1 357
+part2 3121910778619
+aoc2025/day3/input.txt
+part1 17452
+part2 173300819005913

aoc2025/Day4.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day4/eg.txt
+part1 13
+part2 43
+aoc2025/day4/input.txt
+part1 1569
+part2 9280

aoc2025/Day5.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day5/eg.txt
+part1 3
+part2 14
+aoc2025/day5/input.txt
+part1 862
+part2 357907198933892

aoc2025/Day6.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day6/eg.txt
+part1 4277556
+part2 3263827
+aoc2025/day6/input.txt
+part1 5346286649122
+part2 10389131401929

aoc2025/Day7.newt

@@ -4,7 +4,6 @@ import Prelude
 import Node
 import Aoc
 import Data.SortedMap
-import Monad.State
 
 gridPoints : String → List (Char × Int × Int)
 gridPoints text = go 0 0 (unpack text) Nil

aoc2025/Day7.newt.golden

@@ -0,0 +1,10 @@
+aoc2025/day7/eg.txt
+rows 15
+cols 14
+part1 21
+part2 40
+aoc2025/day7/input.txt
+rows 141
+cols 140
+part1 1587
+part2 5748679033029

aoc2025/Day8.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day8/eg.txt
+part1 40
+part2 25272
+aoc2025/day8/input.txt
+part1 123234
+part2 9259958565

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/Day9.newt.golden

@@ -0,0 +1,6 @@
+aoc2025/day9/eg.txt
+part1 6 50
+part2 24
+aoc2025/day9/input.txt
+part1 1222 4777816465
+part2 1410501884

aoc2025/Monad

@@ -0,0 +1 @@
+../src/Monad

aoc2025/Node.newt

@@ -2,6 +2,30 @@ module Node
 
 import Prelude
 
-pfunc fs : JSObject := `require('fs')`
+-- 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 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 readFile uses (MkIORes) : (fn : String) -> IO String := `(fn) => (w) => Prelude_MkIORes(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/Parser.newt

@@ -0,0 +1,75 @@
+module Parser
+
+import Prelude
+import Aoc
+
+Parser : U → U
+Parser a = List Char → Either String (a × List Char)
+
+instance Monad Parser where
+  pure a = \ cs => Right (a, cs)
+  bind ma mab = \ cs => ma cs >>= uncurry mab
+
+instance Alternative Parser where
+  pa <|> pb = \ cs => case pa cs of
+    Left msg => pb cs
+    res => res
+
+instance Functor Parser where
+  map f pa = \ cs => case pa cs of
+    Left msg => Left msg
+    Right (a, cs) => Right (f a, cs)
+
+instance Applicative Parser where
+  return a = pure a
+  pa <*> pb = pa >>= (\ f => map f pb)
+
+
+fail : ∀ a. String -> Parser a
+fail msg = \ cs => Left msg
+
+-- TODO, case builder isn't expanding Parser Unit to count lambdas
+eof : Parser Unit
+eof = \case
+  Nil => Right (MkUnit, Nil)
+  _ =>  Left "expected eof"
+
+satisfy : (Char → Bool) → Parser Char
+satisfy pred = \case
+  Nil => Left "unexpected EOF"
+  (c :: cs) => if pred c then Right (c, cs) else Left ("did not expect " ++ show c ++ " - " ++ pack cs)
+
+match : Char → Parser Char
+match d = satisfy (_==_ d)
+
+any : Parser Char
+any = satisfy (λ _ => True)
+
+some many : ∀ a. Parser a → Parser (List a)
+many p = some p <|> pure Nil
+some p = do
+  v <- p
+  vs <- many p
+  pure (v :: vs)
+
+string : String → Parser Unit
+string str = go (unpack str)
+  where
+    go : List Char → Parser Unit
+    go Nil = pure MkUnit
+    go (c :: cs) = match c >> go cs
+
+number : Parser Int
+number = stringToInt ∘ pack <$> some (satisfy isDigit)
+  -- do
+  -- digs <- some (satisfy isDigit)
+  -- pure $ stringToInt $ pack digs
+
+optional : ∀ a. Parser a → Parser (Maybe a)
+optional pa = Just <$> pa <|> pure Nothing
+
+ws : Parser Unit
+ws = many (match ' ') >> pure MkUnit
+
+token : String → Parser Unit
+token str = string str >> ws

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

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

newt-vscode-lsp/.eslintrc.json

@@ -0,0 +1,30 @@
+{
+    "root": true,
+    "parser": "@typescript-eslint/parser",
+    "parserOptions": {
+        "ecmaVersion": 6,
+        "sourceType": "module"
+    },
+    "plugins": [
+        "@typescript-eslint"
+    ],
+    "rules": {
+        "@typescript-eslint/naming-convention": [
+            "warn",
+            {
+                "selector": "import",
+                "format": [ "camelCase", "PascalCase" ]
+            }
+        ],
+        "@typescript-eslint/semi": "warn",
+        "curly": "off",
+        "eqeqeq": "warn",
+        "no-throw-literal": "warn",
+        "semi": "off"
+    },
+    "ignorePatterns": [
+        "out",
+        "dist",
+        "**/*.d.ts"
+    ]
+}

newt-vscode-lsp/.gitignore

@@ -0,0 +1,4 @@
+dist
+node_modules
+*.vsix
+

newt-vscode-lsp/.vscodeignore

@@ -0,0 +1,5 @@
+.vscode/**
+.vscode-test/**
+.gitignore
+vsc-extension-quickstart.md
+node_modules

newt-vscode-lsp/CHANGELOG.md

@@ -0,0 +1,9 @@
+# Change Log
+
+All notable changes to the "newt-vscode" extension will be documented in this file.
+
+Check [Keep a Changelog](http://keepachangelog.com/) for recommendations on how to structure this file.
+
+## [Unreleased]
+
+- Initial release

newt-vscode-lsp/LICENSE

@@ -0,0 +1,24 @@
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to <https://unlicense.org>

newt-vscode-lsp/README.md

@@ -0,0 +1,3 @@
+# newt-vscode README
+
+newt extension for vscode

newt-vscode-lsp/esbuild.js

@@ -0,0 +1,61 @@
+const esbuild = require("esbuild");
+
+const production = process.argv.includes('--production');
+const watch = process.argv.includes('--watch');
+
+/**
+ * @type {import('esbuild').Plugin}
+ */
+const esbuildProblemMatcherPlugin = {
+	name: 'esbuild-problem-matcher',
+
+	setup(build) {
+		build.onStart(() => {
+			console.log('[watch] build started');
+		});
+		build.onEnd((result) => {
+			result.errors.forEach(({ text, location }) => {
+				console.error(`✘ [ERROR] ${text}`);
+				console.error(`    ${location.file}:${location.line}:${location.column}:`);
+			});
+			console.log('[watch] build finished');
+		});
+	},
+};
+
+async function main() {
+	const ctx = await esbuild.context({
+		entryPoints: [
+			'src/extension.ts',
+			'src/lsp.ts'
+		],
+		bundle: true,
+		format: 'cjs',
+		minify: production,
+		sourcemap: !production,
+		sourcesContent: false,
+		platform: 'node',
+		banner: {
+			js: "#!/usr/bin/env node",
+		},
+		// outfile: 'dist/extension.js',
+		outdir: 'dist',
+		external: ['vscode'],
+		logLevel: 'silent',
+		plugins: [
+			/* add to the end of plugins array */
+			esbuildProblemMatcherPlugin,
+		],
+	});
+	if (watch) {
+		await ctx.watch();
+	} else {
+		await ctx.rebuild();
+		await ctx.dispose();
+	}
+}
+
+main().catch(e => {
+	console.error(e);
+	process.exit(1);
+});

newt-vscode-lsp/language-configuration.json

@@ -0,0 +1,53 @@
+{
+  // see singleton in Tokenizer.idr
+  "wordPattern": "[^()\\{}\\[\\],.@\\s]+",
+  "comments": {
+    // symbol used for single line comment. Remove this entry if your language does not support line comments
+    "lineComment": "--",
+    // symbols used for start and end a block comment. Remove this entry if your language does not support block comments
+    "blockComment": ["/-", "-/"]
+  },
+  // symbols used as brackets
+  "brackets": [
+    ["{", "}"],
+    ["{{", "}}"],
+    ["[", "]"],
+    ["(", ")"]
+  ],
+  // symbols that are auto closed when typing
+  "autoClosingPairs": [
+    ["{", "}"],
+    ["[", "]"],
+    ["(", ")"],
+    ["\"", "\""],
+    // ["'", "'"],  causes problems with foo''
+    ["/-", "-/"]
+  ],
+  // symbols that can be used to surround a selection
+  "surroundingPairs": [
+    ["{", "}"],
+    ["[", "]"],
+    ["(", ")"],
+    ["\"", "\""],
+    ["'", "'"]
+  ],
+  "onEnterRules": [
+    {
+      "beforeText": "\\b(where|of|do)\\s*$",
+      "action": { "indent": "indent" }
+    },
+    {
+      "beforeText": "/-",
+      "afterText": "-/",
+      "action": {
+        "indent": "indentOutdent"
+      }
+    },
+    {
+      "beforeText": "^\\s+$",
+      "action": {
+        "indent": "outdent"
+      }
+    }
+  ]
+}

newt-vscode-lsp/package.json

@@ -0,0 +1,105 @@
+{
+  "name": "newt-vscode",
+  "publisher": "dunhamsteve",
+  "displayName": "newt-vscode",
+  "description": "newt language support with LSP",
+  "version": "0.0.1",
+  "license": "MIT",
+  "repository": {
+    "type": "git",
+    "url": "https://github.com/dunhamsteve/newt"
+  },
+  "engines": {
+    "vscode": "^1.91.0"
+  },
+  "categories": [
+    "Programming Languages"
+  ],
+  "activationEvents": [],
+  "main": "./dist/extension.js",
+  "contributes": {
+    "languages": [
+      {
+        "id": "newt",
+        "aliases": [
+          "newt"
+        ],
+        "extensions": [
+          "newt"
+        ],
+        "configuration": "./language-configuration.json"
+      }
+    ],
+    "grammars": [
+      {
+        "language": "newt",
+        "scopeName": "source.newt",
+        "path": "./syntaxes/newt.tmLanguage.json"
+      },
+      {
+        "path": "./syntaxes/inject.json",
+        "scopeName": "newt.injection",
+        "injectTo": [
+          "text.html.markdown"
+        ],
+        "embeddedLanguages": {
+          "meta.embedded.block.idris": "newt"
+        }
+      }
+    ],
+    "commands": [
+      {
+        "command": "newt-vscode.check",
+        "title": "Check newt file"
+      }
+    ],
+    "configuration": {
+      "type": "object",
+      "title": "Newt Configuration",
+      "properties": {
+        "newt.path": {
+          "type": "string",
+          "default": "node bootstrap/newt.js",
+          "description": "Command to run newt"
+        },
+        "newt.lspPath": {
+          "type": "string",
+          "default": null,
+          "description": "path to LSP script (run in node)"
+        }
+      }
+    }
+  },
+  "scripts": {
+    "vscode:prepublish": "npm run package",
+    "compile": "npm run check-types && npm run lint && node esbuild.js",
+    "watch": "npm-run-all -p watch:*",
+    "watch:esbuild": "node esbuild.js --watch",
+    "esbuild": "node esbuild.js",
+    "package": "echo npm run check-types && npm run lint && node esbuild.js --production",
+    "compile-tests": "tsc -p . --outDir out",
+    "watch-tests": "tsc -p . -w --outDir out",
+    "pretest": "npm run compile-tests && npm run compile && npm run lint",
+    "check-types": "tsc --noEmit",
+    "lint": "eslint src --ext ts",
+    "test": "vscode-test"
+  },
+  "devDependencies": {
+    "@types/mocha": "^10.0.7",
+    "@types/node": "25.x",
+    "@types/vscode": "^1.90.0",
+    "@typescript-eslint/eslint-plugin": "^7.14.1",
+    "@typescript-eslint/parser": "^7.11.0",
+    "@vscode/test-cli": "^0.0.9",
+    "@vscode/test-electron": "^2.4.0",
+    "esbuild": "^0.25.0",
+    "eslint": "^8.57.0",
+    "npm-run-all": "^4.1.5",
+    "typescript": "^5.4.5"
+  },
+  "dependencies": {
+    "vscode-languageclient": "^9.0.1",
+    "vscode-languageserver": "^9.0.1",
+    "vscode-languageserver-textdocument": "^1.0.12"
+  }
+}

newt-vscode-lsp/src/abbrev.ts

@@ -0,0 +1,36 @@
+// This needs to be fleshed out a lot, I've been adding them as needed
+// There is a mix of agda, lean, and my own shortcuts here
+export const ABBREV: Record<string, string> = {
+  "\\x": "×",
+  "\\r": "→",
+  "\\all": "∀",
+  "\\\\": "\\",
+  "\\==": "≡",
+  "\\circ": "∘",
+  "\\oplus": "⊕",
+  "\\otimes": "⊗",
+  // lean
+  "\\1": "₁",
+  "\\2": "₂",
+  "\\<": "⟨",
+  "\\>": "⟩",
+  // agda
+  "\\_0": "₀",
+  "\\_1": "₁",
+  "\\_2": "₂",
+  "\\_3": "₃",
+  // lean has \n here, which is a royal pain
+  "\\neg": "¬",
+  "\\bN": "ℕ",
+  "\\bZ": "ℤ",
+  "\\GG": "Γ",
+  "\\Gi": "ι",
+  "\\Gl": "λ",
+  "\\Gs": "σ",
+  "\\Gt": "τ",
+  "\\GD": "Δ",
+  "\\GS": "Σ",
+  "\\GP": "∏",
+  "\\[[": "⟦",
+  "\\]]": "⟧",
+};

newt-vscode-lsp/src/extension.ts

@@ -0,0 +1,97 @@
+import * as vscode from "vscode";
+import { ABBREV } from "./abbrev";
+import {
+  LanguageClient,
+  LanguageClientOptions,
+  ServerOptions,
+  TransportKind
+} from 'vscode-languageclient/node';
+
+function getIndent(text: string) {
+  return text.match(/\S/)?.index ?? 0
+}
+
+// They put this at module level for deactivate below.
+let client: LanguageClient
+
+export function activate(context: vscode.ExtensionContext) {
+  const serverModule = context.asAbsolutePath('./dist/lsp.js')
+  console.log('*** servervModule', serverModule)
+  const config = vscode.workspace.getConfiguration("newt");
+  const cmd = config.get<string | null>("lspPath");
+
+  let serverOptions: ServerOptions
+  if (cmd) {
+    serverOptions = {
+      run: { command: "node", args: ['--heapsnapshot-signal=SIGUSR2',cmd], transport: TransportKind.pipe },
+      debug: { command: "node", args: [cmd], transport: TransportKind.pipe },
+    }
+  } else {
+    serverOptions = {
+      run: { module: serverModule, transport: TransportKind.ipc },
+      debug: { module: serverModule, transport: TransportKind.ipc },
+    }
+  }
+
+  const clientOptions: LanguageClientOptions = {
+    documentSelector: [{ scheme: 'file', language: 'newt' }],
+    synchronize: {
+      fileEvents: vscode.workspace.createFileSystemWatcher('*.newt')
+    }
+  }
+
+  client = new LanguageClient(
+    'NewtLanguageServer',
+    'Newt Language Server',
+    serverOptions,
+    clientOptions
+  )
+
+  client.start();
+  console.log('CLIENT started')
+
+  vscode.workspace.onDidChangeTextDocument((event) => {
+    const editor = vscode.window.activeTextEditor;
+    if (!editor || event.document !== editor.document) return;
+
+    const changes = event.contentChanges;
+    if (changes.length === 0) return;
+
+    // TODO - agda input mode does the replacement as soon as possible
+    // but if the sequence is a prefix, it will change for subsequent characters
+    // The latter would require keeping state, but if we don't allow sequences to prefix
+    // each other, we could activate quicker.
+    const lastChange = changes[changes.length - 1];
+    const text = lastChange.text;
+    // Check if the last change is a potential shortcut trigger
+    if (!text || !(" ')\\_".includes(text) || text.startsWith('\n'))) return;
+
+    const document = editor.document;
+    const position = lastChange.range.end;
+    const lineText = document.lineAt(position.line).text;
+    const start = Math.max(0, position.character - 10);
+    const snippet = lineText.slice(start, position.character);
+    const m = snippet.match(/(\\[^ ]+)$/);
+    if (m) {
+      const cand = m[0];
+      console.log("cand", cand);
+      const replacement = ABBREV[cand];
+      console.log("repl", replacement);
+      if (replacement) {
+        const range = new vscode.Range(
+          position.line,
+          position.character - cand.length,
+          position.line,
+          position.character
+        );
+        editor.edit((editBuilder) => {
+          editBuilder.replace(range, replacement);
+        });
+      }
+    }
+  });
+}
+
+export function deactivate() {
+  if (client) client.stop();
+}

newt-vscode-lsp/src/lsp.ts

@@ -0,0 +1,162 @@
+/**
+ * Wraps newt.js (compiled from src/LSP.newt with some tweaks to `export`) with the
+ * vscode LSP server module.
+ */
+
+import { LSP_checkFile, LSP_updateFile, LSP_hoverInfo, LSP_codeActionInfo, LSP_docSymbols } from './newt.js'
+
+import {
+  createConnection,
+  TextDocuments,
+  ProposedFeatures,
+  Hover,
+  InitializeParams,
+  InitializeResult,
+  TextDocumentSyncKind,
+  Location,
+  TextDocumentIdentifier,
+} from "vscode-languageserver/node";
+import fs from 'node:fs';
+import path from 'node:path';
+import { TextDocument } from "vscode-languageserver-textdocument";
+
+const connection = createConnection(ProposedFeatures.all);
+const documents = new TextDocuments(TextDocument);
+
+// the last is the most important to the user, but we run FIFO
+// to ensure dependencies are seen in causal order
+let changes: (TextDocument|TextDocumentIdentifier)[] = []
+let running = false
+let lastChange = 0
+function addChange(doc: TextDocument | TextDocumentIdentifier) {
+  console.log('enqueue', doc.uri)
+  // drop stale pending changes
+  let before = changes.length
+  changes = changes.filter(ch => ch.uri != doc.uri)
+  console.log('DROPPED', before - changes.length);
+  changes.push(doc)
+  lastChange = +new Date()
+  if (!running) runChange()
+}
+
+const sleep = (ms: number) => new Promise(resolve => setTimeout(resolve, ms));
+
+async function runChange() {
+  try {
+    running = true;
+    while (changes.length) {
+      console.log('LOOP TOP')
+      // Wait until things stop changing
+      let prev = lastChange
+      while (1) {
+        await sleep(100)
+        if (prev == lastChange) break
+        prev = lastChange
+        console.log('DELAY')
+      }
+      let doc = changes.shift()
+      if (!doc) {
+        running = false
+        return
+      }
+      const uri = doc.uri
+      const start = +new Date()
+      const diagnostics = LSP_checkFile(doc.uri)
+      const end = +new Date()
+      console.log('CHECK', doc.uri, 'in', end - start);
+      await sleep(1);
+      if (!changes.find(ch => ch.uri === uri)) {
+        console.log('SEND', diagnostics.length, 'for', uri)
+        connection.sendDiagnostics({ uri, diagnostics })
+      } else {
+        console.log('STALE result not sent for', uri)
+      }
+    }
+  } catch (e) {
+    console.error(e);
+  } finally {
+    running = false;
+  }
+}
+documents.onDidChangeContent(async (change) => {
+  console.log('DIDCHANGE', change.document.uri)
+  const uri = change.document.uri;
+  const text = change.document.getText();
+  // update/invalidate happens now, check happens on quiesce.
+  writeCache(path.basename(uri), text);
+  LSP_updateFile(uri, text);
+  addChange(change.document);
+});
+
+connection.onHover((params): Hover | null => {
+  // wait until quiesced (REVIEW after query-based)
+  if (running) return null
+
+  const uri = params.textDocument.uri;
+  const pos = params.position;
+  console.log('HOVER', uri, pos)
+  let res = LSP_hoverInfo(uri, pos.line, pos.character)
+  if (!res) return null
+  if (res == true) {
+    addChange(params.textDocument)
+    return null
+  } else {
+    console.log('HOVER is ', res)
+    return { contents: { kind: "plaintext", value: res.info } };
+  }
+});
+
+connection.onDefinition((params): Location | null => {
+  const uri = params.textDocument.uri;
+  const pos = params.position;
+  let value = LSP_hoverInfo(uri, pos.line, pos.character)
+  if (!value || value == true) return null;
+  return value.location
+})
+
+connection.onCodeAction(({textDocument, range}) => {
+  let actions = LSP_codeActionInfo(textDocument.uri, range.start.line, range.start.character);
+  console.log('ACTIONS is ', JSON.stringify(actions,null,'  '))
+  return actions
+})
+
+connection.onDocumentSymbol((params) => {
+  try {
+
+  const uri = params.textDocument.uri;
+  let symbols = LSP_docSymbols(uri);
+  console.log("docs got", symbols)
+  return symbols;
+  } catch (e) {
+    console.error('ERROR in onDocumentSymbol', e);
+  }
+})
+
+connection.onInitialize((_params: InitializeParams): InitializeResult => ({
+  capabilities: {
+    textDocumentSync: TextDocumentSyncKind.Incremental,
+    hoverProvider: true,
+    definitionProvider: true,
+    codeActionProvider: true,
+    documentSymbolProvider: true,
+  },
+}));
+
+function writeCache(fn: string, content: string) {
+  const home = process.env.HOME;
+  if (!home) return;
+  const dname = path.join(home, '.cache/newt-lsp');
+  const fname = path.join(dname, fn);
+  try {
+    fs.mkdirSync(dname, {recursive: true});
+  } catch (e) {
+  }
+  try {
+    fs.writeFileSync(fname, content, 'utf8');
+  } catch (e) {
+    console.error(e);
+  }
+}
+documents.listen(connection);
+connection.listen();
+console.log('STARTED')

newt-vscode-lsp/src/newt.d.ts

@@ -0,0 +1,12 @@
+import { CodeAction, Diagnostic, DocumentSymbol, Location } from "vscode-languageserver";
+
+export function LSP_updateFile(name: string, content: string): (eta: any) => any;
+export function LSP_checkFile(name: string): Diagnostic[];
+interface HoverResult {
+    info: string
+    location: Location
+}
+export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult|boolean|null;
+export function LSP_codeActionInfo(name: string, row: number, col: number): CodeAction[]|null;
+export function LSP_docSymbols(name: string): DocumentSymbol[] | null;
+

newt-vscode-lsp/syntaxes/inject.json

@@ -0,0 +1,44 @@
+{
+  "scopeName": "newt.injection",
+  "injectionSelector": "L:text.html.markdown",
+  "patterns": [
+    {
+      "include": "#fenced_code_block_newt"
+    }
+  ],
+  "repository": {
+    "fenced_code_block_newt": {
+      "begin": "(^|\\G)(\\s*)(`{3,}|~{3,})\\s*(?i:(newt)((\\s+|:|,|\\{|\\?)[^`]*)?$)",
+      "name": "markup.fenced_code.block.markdown",
+      "end": "(^|\\G)(\\2|\\s{0,3})(\\3)\\s*$",
+      "beginCaptures": {
+        "3": {
+          "name": "punctuation.definition.markdown"
+        },
+        "4": {
+          "name": "fenced_code.block.language.markdown"
+        },
+        "5": {
+          "name": "fenced_code.block.language.attributes.markdown"
+        }
+      },
+      "endCaptures": {
+        "3": {
+          "name": "punctuation.definition.markdown"
+        }
+      },
+      "patterns": [
+        {
+          "begin": "(^|\\G)(\\s*)(.*)",
+          "while": "(^|\\G)(?!\\s*([`~]{3,})\\s*$)",
+          "contentName": "meta.embedded.block.newt",
+          "patterns": [
+            {
+              "include": "source.newt"
+            }
+          ]
+        }
+      ]
+    }
+  }
+}

newt-vscode-lsp/syntaxes/newt.tmLanguage.json

@@ -0,0 +1,47 @@
+{
+  "$schema": "https://raw.githubusercontent.com/martinring/tmlanguage/master/tmlanguage.json",
+  "name": "newt",
+  "scopeName": "source.newt",
+  "patterns": [
+    {
+      "name": "invalid.illegal.trace",
+      "match": "\\b(trace|strace|fatalError)\\b"
+    },
+    {
+      "name": "comment.block.newt",
+      "begin": "/-",
+      "end": "-/",
+      "contentName": "comment.block.newt"
+    },
+    {
+      "name": "comment.line.newt",
+      "begin": "--",
+      "end": "\\n"
+    },
+    {
+      "name": "keyword.newt",
+      "match": "\\b(λ|=>|<-|->|→|:=|\\$|data|record|constructor|where|do|derive|class|uses|instance|case|of|let|if|then|else|forall|∀|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
+    },
+    {
+      "name": "string.js",
+      "begin": "`",
+      "end": "`",
+      "patterns": [{ "include": "source.js" }]
+    },
+    {
+      "name": "character",
+      "match": "'\\\\?.'"
+    },
+    {
+      "name": "string.double.newt",
+      "begin": "\"",
+      "end": "\"",
+      "patterns": [
+        {
+          "name": "constant.character.escape.newt",
+          "match": "\\\\[^{]"
+        }
+      ]
+    }
+  ]
+}

newt-vscode-lsp/tsconfig.json

@@ -0,0 +1,18 @@
+{
+	"compilerOptions": {
+		"module": "Node16",
+		"target": "ES2022",
+		"lib": [ "ES2022" ],
+		"sourceMap": true,
+		// so node can run this stuff
+		"allowImportingTsExtensions": true,
+		// required by previous, but we use esbuild anyway
+		"noEmit": true,
+		"rootDir": "src",
+		"strict": true   /* enable all strict type-checking options */
+		/* Additional Checks */
+		// "noImplicitReturns": true, /* Report error when not all code paths in function return a value. */
+		// "noFallthroughCasesInSwitch": true, /* Report errors for fallthrough cases in switch statement. */
+		// "noUnusedParameters": true,  /* Report errors on unused parameters. */
+	}
+}

newt-vscode/README.md

@@ -1,3 +1,3 @@
 # newt-vscode README
 
-newt extension for vscode
+newt extension for vscode. This is the older, non-LSP one that runs the compiler one-shot and scrapes the result. Use newt-vscode-lsp instead.

newt-vscode/package-lock.json

@@ -10,7 +10,7 @@
       "license": "MIT",
       "devDependencies": {
         "@types/mocha": "^10.0.7",
-        "@types/node": "20.x",
+        "@types/node": "25.x",
         "@types/vscode": "^1.90.0",
         "@typescript-eslint/eslint-plugin": "^7.14.1",
         "@typescript-eslint/parser": "^7.11.0",
@@ -772,13 +772,13 @@
       "license": "MIT"
     },
     "node_modules/@types/node": {
-      "version": "20.19.25",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.25.tgz",
-      "integrity": "sha512-ZsJzA5thDQMSQO788d7IocwwQbI8B5OPzmqNvpf3NY/+MHDAS759Wo0gd2WQeXYt5AAAQjzcrTVC6SKCuYgoCQ==",
+      "version": "25.2.2",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-25.2.2.tgz",
+      "integrity": "sha512-BkmoP5/FhRYek5izySdkOneRyXYN35I860MFAGupTdebyE66uZaR+bXLHq8k4DirE5DwQi3NuhvRU1jqTVwUrQ==",
       "dev": true,
       "license": "MIT",
       "dependencies": {
-        "undici-types": "~6.21.0"
+        "undici-types": "~7.16.0"
       }
     },
     "node_modules/@types/vscode": {
@@ -5605,9 +5605,9 @@
       }
     },
     "node_modules/undici-types": {
-      "version": "6.21.0",
-      "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz",
-      "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==",
+      "version": "7.16.0",
+      "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-7.16.0.tgz",
+      "integrity": "sha512-Zz+aZWSj8LE6zoxD+xrjh4VfkIG8Ya6LvYkZqtUQGJPZjYl53ypCaUwWqo7eI0x66KBGeRo+mlBEkMSeSZ38Nw==",
       "dev": true,
       "license": "MIT"
     },

newt-vscode/package.json

@@ -82,7 +82,7 @@
   },
   "devDependencies": {
     "@types/mocha": "^10.0.7",
-    "@types/node": "20.x",
+    "@types/node": "25.x",
     "@types/vscode": "^1.90.0",
     "@typescript-eslint/eslint-plugin": "^7.14.1",
     "@typescript-eslint/parser": "^7.11.0",

newt-vscode/src/abbrev.ts

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

newt-vscode/src/extension.ts

@@ -18,11 +18,16 @@ interface TopData {
   context: TopEntry[];
 }
 
+function getIndent(text: string) {
+  return text.match(/\S/)?.index ?? 0
+}
+
 export function activate(context: vscode.ExtensionContext) {
   let topData: undefined | TopData;
   const diagnosticCollection =
     vscode.languages.createDiagnosticCollection("newt");
 
+
   vscode.workspace.onDidChangeTextDocument((event) => {
     const editor = vscode.window.activeTextEditor;
     if (!editor || event.document !== editor.document) return;
@@ -128,6 +133,7 @@ export function activate(context: vscode.ExtensionContext) {
             let range = new vscode.Range(start, end);
             if (file !== fileName) {
               range = new vscode.Range(new vscode.Position(0,0), new vscode.Position(0,0));
+              message = `Error in ${file}: ${message}`
             }
             // anything indented after the ERROR/INFO line are part of
             // the message
@@ -289,12 +295,15 @@ export function activate(context: vscode.ExtensionContext) {
           const actions: vscode.CodeAction[] = [];
           for (const diagnostic of context.diagnostics) {
             let {message,range} = diagnostic;
-            let m = message.match(/missing cases: (.*)/);
+            let m = message.match(/missing cases: \[(.*)\]/);
             if (m) {
               // A lot of this logic would also apply to case split.
               let cons = m[1].split(', ');
-              const line = range.start.line;
-              const lineText = document.lineAt(line).text;
+              let line = range.start.line;
+              let lineText = document.lineAt(line).text;
+              // this isn't going to work for let.
+              // and I think I relaxed the indent for `|`
+              const indent = getIndent(lineText)
               let m2 = lineText.match(/(.*=>?)/);
               if (!m2) continue;
               let s = range.start.character;
@@ -311,13 +320,43 @@ export function activate(context: vscode.ExtensionContext) {
                   vscode.CodeActionKind.QuickFix
                 );
                 fix.edit = new vscode.WorkspaceEdit();
-                // TODO - we should skip over subsequent lines that are indented more than the current.
-                const insertPos = new vscode.Position(line + 1, 0);
-                fix.edit.insert(document.uri, insertPos, lines.join('\n') + '\n');
+                // skip indented lines
+                while (1) {
+                  line = line + 1
+                  lineText = document.lineAt(line).text
+                  if (!lineText.trim() || getIndent(lineText) <= indent) break
+                }
+                const insertPos = new vscode.Position(line, 0);
+                let text = lines.join('\n') + '\n';
+                if (insertPos.line === document.lineCount) {
+                  text = "\n" + text;
+                }
+                fix.edit.insert(document.uri, insertPos, text);
                 fix.diagnostics = [diagnostic];
                 fix.isPreferred = true;
                 actions.push(fix);
             }
+            m = message.match(/try importing: (.*)/);
+            if (m) {
+              let mods = m[1].split(', ')
+              let insertLine = 0;
+              for (let i = 0; i < document.lineCount; i++) {
+                const line = document.lineAt(i).text;
+                if (/^(import|module)\b/.test(line)) insertLine = i + 1;
+              }
+              const insertPos = new vscode.Position(insertLine, 0);
+              for (let mod of mods) {
+                const fix = new vscode.CodeAction(
+                  `Import ${mod}`,
+                  vscode.CodeActionKind.QuickFix
+                );
+                fix.edit = new vscode.WorkspaceEdit();
+                fix.edit.insert(document.uri, insertPos, `import ${mod}\n`);
+                fix.diagnostics = [diagnostic];
+                // fix.isPreferred = true;  // they're all preferred?
+                actions.push(fix);
+              }
+            }
           }
           return actions;
         }

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": "/-",

newt-vscode/tsconfig.json

@@ -2,10 +2,12 @@
 	"compilerOptions": {
 		"module": "Node16",
 		"target": "ES2022",
-		"lib": [
-			"ES2022"
-		],
+		"lib": [ "ES2022" ],
 		"sourceMap": true,
+		// so node can run this stuff
+		"allowImportingTsExtensions": true,
+		// required by previous, but we use esbuild anyway
+		"noEmit": true,
 		"rootDir": "src",
 		"strict": true   /* enable all strict type-checking options */
 		/* Additional Checks */

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/build

@@ -1,9 +1,9 @@
-#!/bin/sh
+#!/bin/bash
 mkdir -p public
+echo build lsp.js
+(cd .. && make lsp)
 echo build newt worker
-esbuild src/worker.ts --bundle --format=esm > public/worker.js
-esbuild src/frame.ts --bundle --format=esm > public/frame.js
-echo copy newt
-cp ../newt.js public
+esbuild src/worker.ts --bundle --format=esm --platform=browser > public/worker.js
+esbuild src/frame.ts --bundle --format=esm --platform=browser > public/frame.js
 cp -r static/* public
 (cd samples && zip -r ../public/files.zip .)

playground/index.html

@@ -3,10 +3,16 @@
   <head>
     <meta charset="UTF-8" />
     <link rel="stylesheet" href="style.css">
+    <link rel="shortcut icon" href="newt.png" type="image/png">
     <meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=1" />
     <title>Newt Playground</title>
   </head>
   <body>
+    <svg xmlns="http://www.w3.org/2000/svg">
+      <symbol id="github" viewBox="0 0 496 512"><path fill="currentColor" d="M165.9 397.4c0 2-2.3 3.6-5.2 3.6-3.3.3-5.6-1.3-5.6-3.6 0-2 2.3-3.6 5.2-3.6 3-.3 5.6 1.3 5.6 3.6zm-31.1-4.5c-.7 2 1.3 4.3 4.3 4.9 2.6 1 5.6 0 6.2-2s-1.3-4.3-4.3-5.2c-2.6-.7-5.5.3-6.2 2.3zm44.2-1.7c-2.9.7-4.9 2.6-4.6 4.9.3 2 2.9 3.3 5.9 2.6 2.9-.7 4.9-2.6 4.6-4.6-.3-1.9-3-3.2-5.9-2.9zM244.8 8C106.1 8 0 113.3 0 252c0 110.9 69.8 205.8 169.5 239.2 12.8 2.3 17.3-5.6 17.3-12.1 0-6.2-.3-40.4-.3-61.4 0 0-70 15-84.7-29.8 0 0-11.4-29.1-27.8-36.6 0 0-22.9-15.7 1.6-15.4 0 0 24.9 2 38.6 25.8 21.9 38.6 58.6 27.5 72.9 20.9 2.3-16 8.8-27.1 16-33.7-55.9-6.2-112.3-14.3-112.3-110.5 0-27.5 7.6-41.3 23.6-58.9-2.6-6.5-11.1-33.3 2.6-67.9 20.9-6.5 69 27 69 27 20-5.6 41.5-8.5 62.8-8.5s42.8 2.9 62.8 8.5c0 0 48.1-33.6 69-27 13.7 34.7 5.2 61.4 2.6 67.9 16 17.7 25.8 31.5 25.8 58.9 0 96.5-58.9 104.2-114.8 110.5 9.2 7.9 17 22.9 17 46.4 0 33.7-.3 75.4-.3 83.6 0 6.5 4.6 14.4 17.3 12.1C428.2 457.8 496 362.9 496 252 496 113.3 383.5 8 244.8 8zM97.2 352.9c-1.3 1-1 3.3.7 5.2 1.6 1.6 3.9 2.3 5.2 1 1.3-1 1-3.3-.7-5.2-1.6-1.6-3.9-2.3-5.2-1zm-10.8-8.1c-.7 1.3.3 2.9 2.3 3.9 1.6 1 3.6.7 4.3-.7.7-1.3-.3-2.9-2.3-3.9-2-.6-3.6-.3-4.3.7zm32.4 35.6c-1.6 1.3-1 4.3 1.3 6.2 2.3 2.3 5.2 2.6 6.5 1 1.3-1.3.7-4.3-1.3-6.2-2.2-2.3-5.2-2.6-6.5-1zm-11.4-14.7c-1.6 1-1.6 3.6 0 5.9 1.6 2.3 4.3 3.3 5.6 2.3 1.6-1.3 1.6-3.9 0-6.2-1.4-2.3-4-3.3-5.6-2z"/></symbol>
+      <symbol id="share" viewBox="0 -960 960 960" fill="currentColor"><path d="M240-80q-33 0-56.5-23.5T160-160v-400q0-33 23.5-56.5T240-640h120v80H240v400h480v-400H600v-80h120q33 0 56.5 23.5T800-560v400q0 33-23.5 56.5T720-80H240Zm200-240v-447l-64 64-56-57 160-160 160 160-56 57-64-64v447h-80Z"/></symbol>
+      <symbol id="play" viewBox="0 -960 960 960" fill="currentColor"><path d="M320-200v-560l440 280-440 280Zm80-280Zm0 134 210-134-210-134v268Z"/></symbol>
+    </svg>
     <div id="app">
       <div class="wrapper">
         <div id="editor"></div>

playground/package-lock.json

@@ -8,6 +8,7 @@
       "name": "playground",
       "version": "0.0.0",
       "dependencies": {
+        "@codemirror/lang-javascript": "^6.2.4",
         "@preact/signals": "^1.3.0",
         "codemirror": "^6.0.1",
         "preact": "^10.24.3"
@@ -20,9 +21,9 @@
       }
     },
     "node_modules/@codemirror/autocomplete": {
-      "version": "6.19.1",
-      "resolved": "https://registry.npmjs.org/@codemirror/autocomplete/-/autocomplete-6.19.1.tgz",
-      "integrity": "sha512-q6NenYkEy2fn9+JyjIxMWcNjzTL/IhwqfzOut1/G3PrIFkrbl4AL7Wkse5tLrQUUyqGoAKU5+Pi5jnnXxH5HGw==",
+      "version": "6.20.0",
+      "resolved": "https://registry.npmjs.org/@codemirror/autocomplete/-/autocomplete-6.20.0.tgz",
+      "integrity": "sha512-bOwvTOIJcG5FVo5gUUupiwYh8MioPLQ4UcqbcRf7UQ98X90tCa9E1kZ3Z7tqwpZxYyOvh1YTYbmZE9RTfTp5hg==",
       "license": "MIT",
       "dependencies": {
         "@codemirror/language": "^6.0.0",
@@ -32,9 +33,9 @@
       }
     },
     "node_modules/@codemirror/commands": {
-      "version": "6.10.0",
-      "resolved": "https://registry.npmjs.org/@codemirror/commands/-/commands-6.10.0.tgz",
-      "integrity": "sha512-2xUIc5mHXQzT16JnyOFkh8PvfeXuIut3pslWGfsGOhxP/lpgRm9HOl/mpzLErgt5mXDovqA0d11P21gofRLb9w==",
+      "version": "6.10.1",
+      "resolved": "https://registry.npmjs.org/@codemirror/commands/-/commands-6.10.1.tgz",
+      "integrity": "sha512-uWDWFypNdQmz2y1LaNJzK7fL7TYKLeUAU0npEC685OKTF3KcQ2Vu3klIM78D7I6wGhktme0lh3CuQLv0ZCrD9Q==",
       "license": "MIT",
       "dependencies": {
         "@codemirror/language": "^6.0.0",
@@ -43,15 +44,30 @@
         "@lezer/common": "^1.1.0"
       }
     },
+    "node_modules/@codemirror/lang-javascript": {
+      "version": "6.2.4",
+      "resolved": "https://registry.npmjs.org/@codemirror/lang-javascript/-/lang-javascript-6.2.4.tgz",
+      "integrity": "sha512-0WVmhp1QOqZ4Rt6GlVGwKJN3KW7Xh4H2q8ZZNGZaP6lRdxXJzmjm4FqvmOojVj6khWJHIb9sp7U/72W7xQgqAA==",
+      "license": "MIT",
+      "dependencies": {
+        "@codemirror/autocomplete": "^6.0.0",
+        "@codemirror/language": "^6.6.0",
+        "@codemirror/lint": "^6.0.0",
+        "@codemirror/state": "^6.0.0",
+        "@codemirror/view": "^6.17.0",
+        "@lezer/common": "^1.0.0",
+        "@lezer/javascript": "^1.0.0"
+      }
+    },
     "node_modules/@codemirror/language": {
-      "version": "6.11.3",
-      "resolved": "https://registry.npmjs.org/@codemirror/language/-/language-6.11.3.tgz",
-      "integrity": "sha512-9HBM2XnwDj7fnu0551HkGdrUrrqmYq/WC5iv6nbY2WdicXdGbhR/gfbZOH73Aqj4351alY1+aoG9rCNfiwS1RA==",
+      "version": "6.12.1",
+      "resolved": "https://registry.npmjs.org/@codemirror/language/-/language-6.12.1.tgz",
+      "integrity": "sha512-Fa6xkSiuGKc8XC8Cn96T+TQHYj4ZZ7RdFmXA3i9xe/3hLHfwPZdM+dqfX0Cp0zQklBKhVD8Yzc8LS45rkqcwpQ==",
       "license": "MIT",
       "dependencies": {
         "@codemirror/state": "^6.0.0",
         "@codemirror/view": "^6.23.0",
-        "@lezer/common": "^1.1.0",
+        "@lezer/common": "^1.5.0",
         "@lezer/highlight": "^1.0.0",
         "@lezer/lr": "^1.0.0",
         "style-mod": "^4.0.0"
@@ -80,9 +96,9 @@
       }
     },
     "node_modules/@codemirror/state": {
-      "version": "6.5.2",
-      "resolved": "https://registry.npmjs.org/@codemirror/state/-/state-6.5.2.tgz",
-      "integrity": "sha512-FVqsPqtPWKVVL3dPSxy8wEF/ymIEuVzF1PK3VbUgrxXpJUSHQWWZz4JMToquRxnkw+36LTamCZG2iua2Ptq0fA==",
+      "version": "6.5.3",
+      "resolved": "https://registry.npmjs.org/@codemirror/state/-/state-6.5.3.tgz",
+      "integrity": "sha512-MerMzJzlXogk2fxWFU1nKp36bY5orBG59HnPiz0G9nLRebWa0zXuv2siH6PLIHBvv5TH8CkQRqjBs0MlxCZu+A==",
       "license": "MIT",
       "dependencies": {
         "@marijn/find-cluster-break": "^1.0.0"
@@ -102,9 +118,9 @@
       }
     },
     "node_modules/@codemirror/view": {
-      "version": "6.38.8",
-      "resolved": "https://registry.npmjs.org/@codemirror/view/-/view-6.38.8.tgz",
-      "integrity": "sha512-XcE9fcnkHCbWkjeKyi0lllwXmBLtyYb5dt89dJyx23I9+LSh5vZDIuk7OLG4VM1lgrXZQcY6cxyZyk5WVPRv/A==",
+      "version": "6.39.7",
+      "resolved": "https://registry.npmjs.org/@codemirror/view/-/view-6.39.7.tgz",
+      "integrity": "sha512-3Vif9hnNHJnl2YgOtkR/wzGzhYcQ8gy3LGdUhkLUU8xSBbgsTxrE8he/CMTpeINm5TgxLe2FmzvF6IYQL/BSAg==",
       "license": "MIT",
       "dependencies": {
         "@codemirror/state": "^6.5.0",
@@ -556,9 +572,9 @@
       }
     },
     "node_modules/@lezer/common": {
-      "version": "1.3.0",
-      "resolved": "https://registry.npmjs.org/@lezer/common/-/common-1.3.0.tgz",
-      "integrity": "sha512-L9X8uHCYU310o99L3/MpJKYxPzXPOS7S0NmBaM7UO/x2Kb2WbmMLSkfvdr1KxRIFYOpbY0Jhn7CfLSUDzL8arQ==",
+      "version": "1.5.0",
+      "resolved": "https://registry.npmjs.org/@lezer/common/-/common-1.5.0.tgz",
+      "integrity": "sha512-PNGcolp9hr4PJdXR4ix7XtixDrClScvtSCYW3rQG106oVMOOI+jFb+0+J3mbeL/53g1Zd6s0kJzaw6Ri68GmAA==",
       "license": "MIT"
     },
     "node_modules/@lezer/highlight": {
@@ -570,10 +586,21 @@
         "@lezer/common": "^1.3.0"
       }
     },
+    "node_modules/@lezer/javascript": {
+      "version": "1.5.4",
+      "resolved": "https://registry.npmjs.org/@lezer/javascript/-/javascript-1.5.4.tgz",
+      "integrity": "sha512-vvYx3MhWqeZtGPwDStM2dwgljd5smolYD2lR2UyFcHfxbBQebqx8yjmFmxtJ/E6nN6u1D9srOiVWm3Rb4tmcUA==",
+      "license": "MIT",
+      "dependencies": {
+        "@lezer/common": "^1.2.0",
+        "@lezer/highlight": "^1.1.3",
+        "@lezer/lr": "^1.3.0"
+      }
+    },
     "node_modules/@lezer/lr": {
-      "version": "1.4.3",
-      "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.4.3.tgz",
-      "integrity": "sha512-yenN5SqAxAPv/qMnpWW0AT7l+SxVrgG+u0tNsRQWqbrz66HIl8DnEbBObvy21J5K7+I1v7gsAnlE2VQ5yYVSeA==",
+      "version": "1.4.5",
+      "resolved": "https://registry.npmjs.org/@lezer/lr/-/lr-1.4.5.tgz",
+      "integrity": "sha512-/YTRKP5yPPSo1xImYQk7AZZMAgap0kegzqCSYHjAL9x1AZ0ZQW+IpcEzMKagCsbTsLnVeWkxYrCNeXG8xEPrjg==",
       "license": "MIT",
       "dependencies": {
         "@lezer/common": "^1.0.0"
@@ -612,9 +639,9 @@
       }
     },
     "node_modules/@rollup/rollup-android-arm-eabi": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm-eabi/-/rollup-android-arm-eabi-4.53.2.tgz",
-      "integrity": "sha512-yDPzwsgiFO26RJA4nZo8I+xqzh7sJTZIWQOxn+/XOdPE31lAvLIYCKqjV+lNH/vxE2L2iH3plKxDCRK6i+CwhA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm-eabi/-/rollup-android-arm-eabi-4.54.0.tgz",
+      "integrity": "sha512-OywsdRHrFvCdvsewAInDKCNyR3laPA2mc9bRYJ6LBp5IyvF3fvXbbNR0bSzHlZVFtn6E0xw2oZlyjg4rKCVcng==",
       "cpu": [
         "arm"
       ],
@@ -626,9 +653,9 @@
       ]
     },
     "node_modules/@rollup/rollup-android-arm64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm64/-/rollup-android-arm64-4.53.2.tgz",
-      "integrity": "sha512-k8FontTxIE7b0/OGKeSN5B6j25EuppBcWM33Z19JoVT7UTXFSo3D9CdU39wGTeb29NO3XxpMNauh09B+Ibw+9g==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-android-arm64/-/rollup-android-arm64-4.54.0.tgz",
+      "integrity": "sha512-Skx39Uv+u7H224Af+bDgNinitlmHyQX1K/atIA32JP3JQw6hVODX5tkbi2zof/E69M1qH2UoN3Xdxgs90mmNYw==",
       "cpu": [
         "arm64"
       ],
@@ -640,9 +667,9 @@
       ]
     },
     "node_modules/@rollup/rollup-darwin-arm64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-darwin-arm64/-/rollup-darwin-arm64-4.53.2.tgz",
-      "integrity": "sha512-A6s4gJpomNBtJ2yioj8bflM2oogDwzUiMl2yNJ2v9E7++sHrSrsQ29fOfn5DM/iCzpWcebNYEdXpaK4tr2RhfQ==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-darwin-arm64/-/rollup-darwin-arm64-4.54.0.tgz",
+      "integrity": "sha512-k43D4qta/+6Fq+nCDhhv9yP2HdeKeP56QrUUTW7E6PhZP1US6NDqpJj4MY0jBHlJivVJD5P8NxrjuobZBJTCRw==",
       "cpu": [
         "arm64"
       ],
@@ -654,9 +681,9 @@
       ]
     },
     "node_modules/@rollup/rollup-darwin-x64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-darwin-x64/-/rollup-darwin-x64-4.53.2.tgz",
-      "integrity": "sha512-e6XqVmXlHrBlG56obu9gDRPW3O3hLxpwHpLsBJvuI8qqnsrtSZ9ERoWUXtPOkY8c78WghyPHZdmPhHLWNdAGEw==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-darwin-x64/-/rollup-darwin-x64-4.54.0.tgz",
+      "integrity": "sha512-cOo7biqwkpawslEfox5Vs8/qj83M/aZCSSNIWpVzfU2CYHa2G3P1UN5WF01RdTHSgCkri7XOlTdtk17BezlV3A==",
       "cpu": [
         "x64"
       ],
@@ -668,9 +695,9 @@
       ]
     },
     "node_modules/@rollup/rollup-freebsd-arm64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-freebsd-arm64/-/rollup-freebsd-arm64-4.53.2.tgz",
-      "integrity": "sha512-v0E9lJW8VsrwPux5Qe5CwmH/CF/2mQs6xU1MF3nmUxmZUCHazCjLgYvToOk+YuuUqLQBio1qkkREhxhc656ViA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-freebsd-arm64/-/rollup-freebsd-arm64-4.54.0.tgz",
+      "integrity": "sha512-miSvuFkmvFbgJ1BevMa4CPCFt5MPGw094knM64W9I0giUIMMmRYcGW/JWZDriaw/k1kOBtsWh1z6nIFV1vPNtA==",
       "cpu": [
         "arm64"
       ],
@@ -682,9 +709,9 @@
       ]
     },
     "node_modules/@rollup/rollup-freebsd-x64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-freebsd-x64/-/rollup-freebsd-x64-4.53.2.tgz",
-      "integrity": "sha512-ClAmAPx3ZCHtp6ysl4XEhWU69GUB1D+s7G9YjHGhIGCSrsg00nEGRRZHmINYxkdoJehde8VIsDC5t9C0gb6yqA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-freebsd-x64/-/rollup-freebsd-x64-4.54.0.tgz",
+      "integrity": "sha512-KGXIs55+b/ZfZsq9aR026tmr/+7tq6VG6MsnrvF4H8VhwflTIuYh+LFUlIsRdQSgrgmtM3fVATzEAj4hBQlaqQ==",
       "cpu": [
         "x64"
       ],
@@ -696,9 +723,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-arm-gnueabihf": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm-gnueabihf/-/rollup-linux-arm-gnueabihf-4.53.2.tgz",
-      "integrity": "sha512-EPlb95nUsz6Dd9Qy13fI5kUPXNSljaG9FiJ4YUGU1O/Q77i5DYFW5KR8g1OzTcdZUqQQ1KdDqsTohdFVwCwjqg==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm-gnueabihf/-/rollup-linux-arm-gnueabihf-4.54.0.tgz",
+      "integrity": "sha512-EHMUcDwhtdRGlXZsGSIuXSYwD5kOT9NVnx9sqzYiwAc91wfYOE1g1djOEDseZJKKqtHAHGwnGPQu3kytmfaXLQ==",
       "cpu": [
         "arm"
       ],
@@ -710,9 +737,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-arm-musleabihf": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm-musleabihf/-/rollup-linux-arm-musleabihf-4.53.2.tgz",
-      "integrity": "sha512-BOmnVW+khAUX+YZvNfa0tGTEMVVEerOxN0pDk2E6N6DsEIa2Ctj48FOMfNDdrwinocKaC7YXUZ1pHlKpnkja/Q==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm-musleabihf/-/rollup-linux-arm-musleabihf-4.54.0.tgz",
+      "integrity": "sha512-+pBrqEjaakN2ySv5RVrj/qLytYhPKEUwk+e3SFU5jTLHIcAtqh2rLrd/OkbNuHJpsBgxsD8ccJt5ga/SeG0JmA==",
       "cpu": [
         "arm"
       ],
@@ -724,9 +751,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-arm64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm64-gnu/-/rollup-linux-arm64-gnu-4.53.2.tgz",
-      "integrity": "sha512-Xt2byDZ+6OVNuREgBXr4+CZDJtrVso5woFtpKdGPhpTPHcNG7D8YXeQzpNbFRxzTVqJf7kvPMCub/pcGUWgBjA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm64-gnu/-/rollup-linux-arm64-gnu-4.54.0.tgz",
+      "integrity": "sha512-NSqc7rE9wuUaRBsBp5ckQ5CVz5aIRKCwsoa6WMF7G01sX3/qHUw/z4pv+D+ahL1EIKy6Enpcnz1RY8pf7bjwng==",
       "cpu": [
         "arm64"
       ],
@@ -738,9 +765,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-arm64-musl": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm64-musl/-/rollup-linux-arm64-musl-4.53.2.tgz",
-      "integrity": "sha512-+LdZSldy/I9N8+klim/Y1HsKbJ3BbInHav5qE9Iy77dtHC/pibw1SR/fXlWyAk0ThnpRKoODwnAuSjqxFRDHUQ==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-arm64-musl/-/rollup-linux-arm64-musl-4.54.0.tgz",
+      "integrity": "sha512-gr5vDbg3Bakga5kbdpqx81m2n9IX8M6gIMlQQIXiLTNeQW6CucvuInJ91EuCJ/JYvc+rcLLsDFcfAD1K7fMofg==",
       "cpu": [
         "arm64"
       ],
@@ -752,9 +779,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-loong64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-loong64-gnu/-/rollup-linux-loong64-gnu-4.53.2.tgz",
-      "integrity": "sha512-8ms8sjmyc1jWJS6WdNSA23rEfdjWB30LH8Wqj0Cqvv7qSHnvw6kgMMXRdop6hkmGPlyYBdRPkjJnj3KCUHV/uQ==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-loong64-gnu/-/rollup-linux-loong64-gnu-4.54.0.tgz",
+      "integrity": "sha512-gsrtB1NA3ZYj2vq0Rzkylo9ylCtW/PhpLEivlgWe0bpgtX5+9j9EZa0wtZiCjgu6zmSeZWyI/e2YRX1URozpIw==",
       "cpu": [
         "loong64"
       ],
@@ -766,9 +793,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-ppc64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-ppc64-gnu/-/rollup-linux-ppc64-gnu-4.53.2.tgz",
-      "integrity": "sha512-3HRQLUQbpBDMmzoxPJYd3W6vrVHOo2cVW8RUo87Xz0JPJcBLBr5kZ1pGcQAhdZgX9VV7NbGNipah1omKKe23/g==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-ppc64-gnu/-/rollup-linux-ppc64-gnu-4.54.0.tgz",
+      "integrity": "sha512-y3qNOfTBStmFNq+t4s7Tmc9hW2ENtPg8FeUD/VShI7rKxNW7O4fFeaYbMsd3tpFlIg1Q8IapFgy7Q9i2BqeBvA==",
       "cpu": [
         "ppc64"
       ],
@@ -780,9 +807,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-riscv64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-riscv64-gnu/-/rollup-linux-riscv64-gnu-4.53.2.tgz",
-      "integrity": "sha512-fMjKi+ojnmIvhk34gZP94vjogXNNUKMEYs+EDaB/5TG/wUkoeua7p7VCHnE6T2Tx+iaghAqQX8teQzcvrYpaQA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-riscv64-gnu/-/rollup-linux-riscv64-gnu-4.54.0.tgz",
+      "integrity": "sha512-89sepv7h2lIVPsFma8iwmccN7Yjjtgz0Rj/Ou6fEqg3HDhpCa+Et+YSufy27i6b0Wav69Qv4WBNl3Rs6pwhebQ==",
       "cpu": [
         "riscv64"
       ],
@@ -794,9 +821,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-riscv64-musl": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-riscv64-musl/-/rollup-linux-riscv64-musl-4.53.2.tgz",
-      "integrity": "sha512-XuGFGU+VwUUV5kLvoAdi0Wz5Xbh2SrjIxCtZj6Wq8MDp4bflb/+ThZsVxokM7n0pcbkEr2h5/pzqzDYI7cCgLQ==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-riscv64-musl/-/rollup-linux-riscv64-musl-4.54.0.tgz",
+      "integrity": "sha512-ZcU77ieh0M2Q8Ur7D5X7KvK+UxbXeDHwiOt/CPSBTI1fBmeDMivW0dPkdqkT4rOgDjrDDBUed9x4EgraIKoR2A==",
       "cpu": [
         "riscv64"
       ],
@@ -808,9 +835,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-s390x-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-s390x-gnu/-/rollup-linux-s390x-gnu-4.53.2.tgz",
-      "integrity": "sha512-w6yjZF0P+NGzWR3AXWX9zc0DNEGdtvykB03uhonSHMRa+oWA6novflo2WaJr6JZakG2ucsyb+rvhrKac6NIy+w==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-s390x-gnu/-/rollup-linux-s390x-gnu-4.54.0.tgz",
+      "integrity": "sha512-2AdWy5RdDF5+4YfG/YesGDDtbyJlC9LHmL6rZw6FurBJ5n4vFGupsOBGfwMRjBYH7qRQowT8D/U4LoSvVwOhSQ==",
       "cpu": [
         "s390x"
       ],
@@ -822,9 +849,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-x64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-x64-gnu/-/rollup-linux-x64-gnu-4.53.2.tgz",
-      "integrity": "sha512-yo8d6tdfdeBArzC7T/PnHd7OypfI9cbuZzPnzLJIyKYFhAQ8SvlkKtKBMbXDxe1h03Rcr7u++nFS7tqXz87Gtw==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-x64-gnu/-/rollup-linux-x64-gnu-4.54.0.tgz",
+      "integrity": "sha512-WGt5J8Ij/rvyqpFexxk3ffKqqbLf9AqrTBbWDk7ApGUzaIs6V+s2s84kAxklFwmMF/vBNGrVdYgbblCOFFezMQ==",
       "cpu": [
         "x64"
       ],
@@ -836,9 +863,9 @@
       ]
     },
     "node_modules/@rollup/rollup-linux-x64-musl": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-x64-musl/-/rollup-linux-x64-musl-4.53.2.tgz",
-      "integrity": "sha512-ah59c1YkCxKExPP8O9PwOvs+XRLKwh/mV+3YdKqQ5AMQ0r4M4ZDuOrpWkUaqO7fzAHdINzV9tEVu8vNw48z0lA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-linux-x64-musl/-/rollup-linux-x64-musl-4.54.0.tgz",
+      "integrity": "sha512-JzQmb38ATzHjxlPHuTH6tE7ojnMKM2kYNzt44LO/jJi8BpceEC8QuXYA908n8r3CNuG/B3BV8VR3Hi1rYtmPiw==",
       "cpu": [
         "x64"
       ],
@@ -850,9 +877,9 @@
       ]
     },
     "node_modules/@rollup/rollup-openharmony-arm64": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-openharmony-arm64/-/rollup-openharmony-arm64-4.53.2.tgz",
-      "integrity": "sha512-4VEd19Wmhr+Zy7hbUsFZ6YXEiP48hE//KPLCSVNY5RMGX2/7HZ+QkN55a3atM1C/BZCGIgqN+xrVgtdak2S9+A==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-openharmony-arm64/-/rollup-openharmony-arm64-4.54.0.tgz",
+      "integrity": "sha512-huT3fd0iC7jigGh7n3q/+lfPcXxBi+om/Rs3yiFxjvSxbSB6aohDFXbWvlspaqjeOh+hx7DDHS+5Es5qRkWkZg==",
       "cpu": [
         "arm64"
       ],
@@ -864,9 +891,9 @@
       ]
     },
     "node_modules/@rollup/rollup-win32-arm64-msvc": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-arm64-msvc/-/rollup-win32-arm64-msvc-4.53.2.tgz",
-      "integrity": "sha512-IlbHFYc/pQCgew/d5fslcy1KEaYVCJ44G8pajugd8VoOEI8ODhtb/j8XMhLpwHCMB3yk2J07ctup10gpw2nyMA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-arm64-msvc/-/rollup-win32-arm64-msvc-4.54.0.tgz",
+      "integrity": "sha512-c2V0W1bsKIKfbLMBu/WGBz6Yci8nJ/ZJdheE0EwB73N3MvHYKiKGs3mVilX4Gs70eGeDaMqEob25Tw2Gb9Nqyw==",
       "cpu": [
         "arm64"
       ],
@@ -878,9 +905,9 @@
       ]
     },
     "node_modules/@rollup/rollup-win32-ia32-msvc": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-ia32-msvc/-/rollup-win32-ia32-msvc-4.53.2.tgz",
-      "integrity": "sha512-lNlPEGgdUfSzdCWU176ku/dQRnA7W+Gp8d+cWv73jYrb8uT7HTVVxq62DUYxjbaByuf1Yk0RIIAbDzp+CnOTFg==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-ia32-msvc/-/rollup-win32-ia32-msvc-4.54.0.tgz",
+      "integrity": "sha512-woEHgqQqDCkAzrDhvDipnSirm5vxUXtSKDYTVpZG3nUdW/VVB5VdCYA2iReSj/u3yCZzXID4kuKG7OynPnB3WQ==",
       "cpu": [
         "ia32"
       ],
@@ -892,9 +919,9 @@
       ]
     },
     "node_modules/@rollup/rollup-win32-x64-gnu": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-x64-gnu/-/rollup-win32-x64-gnu-4.53.2.tgz",
-      "integrity": "sha512-S6YojNVrHybQis2lYov1sd+uj7K0Q05NxHcGktuMMdIQ2VixGwAfbJ23NnlvvVV1bdpR2m5MsNBViHJKcA4ADw==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-x64-gnu/-/rollup-win32-x64-gnu-4.54.0.tgz",
+      "integrity": "sha512-dzAc53LOuFvHwbCEOS0rPbXp6SIhAf2txMP5p6mGyOXXw5mWY8NGGbPMPrs4P1WItkfApDathBj/NzMLUZ9rtQ==",
       "cpu": [
         "x64"
       ],
@@ -906,9 +933,9 @@
       ]
     },
     "node_modules/@rollup/rollup-win32-x64-msvc": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-x64-msvc/-/rollup-win32-x64-msvc-4.53.2.tgz",
-      "integrity": "sha512-k+/Rkcyx//P6fetPoLMb8pBeqJBNGx81uuf7iljX9++yNBVRDQgD04L+SVXmXmh5ZP4/WOp4mWF0kmi06PW2tA==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/@rollup/rollup-win32-x64-msvc/-/rollup-win32-x64-msvc-4.54.0.tgz",
+      "integrity": "sha512-hYT5d3YNdSh3mbCU1gwQyPgQd3T2ne0A3KG8KSBdav5TiBg6eInVmV+TeR5uHufiIgSFg0XsOWGW5/RhNcSvPg==",
       "cpu": [
         "x64"
       ],
@@ -1092,9 +1119,9 @@
       }
     },
     "node_modules/preact": {
-      "version": "10.27.2",
-      "resolved": "https://registry.npmjs.org/preact/-/preact-10.27.2.tgz",
-      "integrity": "sha512-5SYSgFKSyhCbk6SrXyMpqjb5+MQBgfvEKE/OC+PujcY34sOpqtr+0AZQtPYx5IA6VxynQ7rUPCtKzyovpj9Bpg==",
+      "version": "10.28.2",
+      "resolved": "https://registry.npmjs.org/preact/-/preact-10.28.2.tgz",
+      "integrity": "sha512-lbteaWGzGHdlIuiJ0l2Jq454m6kcpI1zNje6d8MlGAFlYvP2GO4ibnat7P74Esfz4sPTdM6UxtTwh/d3pwM9JA==",
       "license": "MIT",
       "peer": true,
       "funding": {
@@ -1103,9 +1130,9 @@
       }
     },
     "node_modules/rollup": {
-      "version": "4.53.2",
-      "resolved": "https://registry.npmjs.org/rollup/-/rollup-4.53.2.tgz",
-      "integrity": "sha512-MHngMYwGJVi6Fmnk6ISmnk7JAHRNF0UkuucA0CUW3N3a4KnONPEZz+vUanQP/ZC/iY1Qkf3bwPWzyY84wEks1g==",
+      "version": "4.54.0",
+      "resolved": "https://registry.npmjs.org/rollup/-/rollup-4.54.0.tgz",
+      "integrity": "sha512-3nk8Y3a9Ea8szgKhinMlGMhGMw89mqule3KWczxhIzqudyHdCIOHw8WJlj/r329fACjKLEh13ZSk7oE22kyeIw==",
       "dev": true,
       "license": "MIT",
       "dependencies": {
@@ -1119,28 +1146,28 @@
         "npm": ">=8.0.0"
       },
       "optionalDependencies": {
-        "@rollup/rollup-android-arm-eabi": "4.53.2",
-        "@rollup/rollup-android-arm64": "4.53.2",
-        "@rollup/rollup-darwin-arm64": "4.53.2",
-        "@rollup/rollup-darwin-x64": "4.53.2",
-        "@rollup/rollup-freebsd-arm64": "4.53.2",
-        "@rollup/rollup-freebsd-x64": "4.53.2",
-        "@rollup/rollup-linux-arm-gnueabihf": "4.53.2",
-        "@rollup/rollup-linux-arm-musleabihf": "4.53.2",
-        "@rollup/rollup-linux-arm64-gnu": "4.53.2",
-        "@rollup/rollup-linux-arm64-musl": "4.53.2",
-        "@rollup/rollup-linux-loong64-gnu": "4.53.2",
-        "@rollup/rollup-linux-ppc64-gnu": "4.53.2",
-        "@rollup/rollup-linux-riscv64-gnu": "4.53.2",
-        "@rollup/rollup-linux-riscv64-musl": "4.53.2",
-        "@rollup/rollup-linux-s390x-gnu": "4.53.2",
-        "@rollup/rollup-linux-x64-gnu": "4.53.2",
-        "@rollup/rollup-linux-x64-musl": "4.53.2",
-        "@rollup/rollup-openharmony-arm64": "4.53.2",
-        "@rollup/rollup-win32-arm64-msvc": "4.53.2",
-        "@rollup/rollup-win32-ia32-msvc": "4.53.2",
-        "@rollup/rollup-win32-x64-gnu": "4.53.2",
-        "@rollup/rollup-win32-x64-msvc": "4.53.2",
+        "@rollup/rollup-android-arm-eabi": "4.54.0",
+        "@rollup/rollup-android-arm64": "4.54.0",
+        "@rollup/rollup-darwin-arm64": "4.54.0",
+        "@rollup/rollup-darwin-x64": "4.54.0",
+        "@rollup/rollup-freebsd-arm64": "4.54.0",
+        "@rollup/rollup-freebsd-x64": "4.54.0",
+        "@rollup/rollup-linux-arm-gnueabihf": "4.54.0",
+        "@rollup/rollup-linux-arm-musleabihf": "4.54.0",
+        "@rollup/rollup-linux-arm64-gnu": "4.54.0",
+        "@rollup/rollup-linux-arm64-musl": "4.54.0",
+        "@rollup/rollup-linux-loong64-gnu": "4.54.0",
+        "@rollup/rollup-linux-ppc64-gnu": "4.54.0",
+        "@rollup/rollup-linux-riscv64-gnu": "4.54.0",
+        "@rollup/rollup-linux-riscv64-musl": "4.54.0",
+        "@rollup/rollup-linux-s390x-gnu": "4.54.0",
+        "@rollup/rollup-linux-x64-gnu": "4.54.0",
+        "@rollup/rollup-linux-x64-musl": "4.54.0",
+        "@rollup/rollup-openharmony-arm64": "4.54.0",
+        "@rollup/rollup-win32-arm64-msvc": "4.54.0",
+        "@rollup/rollup-win32-ia32-msvc": "4.54.0",
+        "@rollup/rollup-win32-x64-gnu": "4.54.0",
+        "@rollup/rollup-win32-x64-msvc": "4.54.0",
         "fsevents": "~2.3.2"
       }
     },

playground/package.json

@@ -8,6 +8,9 @@
     "build": "tsc && vite build",
     "preview": "vite preview"
   },
+  "browser": {
+    "fs": "./src/fs.ts"
+  },
   "devDependencies": {
     "@codemirror/theme-one-dark": "^6.1.2",
     "esbuild": "^0.25.0",
@@ -15,6 +18,7 @@
     "vite": "^6.1.0"
   },
   "dependencies": {
+    "@codemirror/lang-javascript": "^6.2.4",
     "@preact/signals": "^1.3.0",
     "codemirror": "^6.0.1",
     "preact": "^10.24.3"

playground/samples/Combinatory.newt

@@ -1,6 +1,7 @@
 module Combinatory
 
 -- "A correct-by-construction conversion from lambda calculus to combinatory logic", Wouter Swierstra
+-- prj/menagerie/papers/combinatory
 
 data Unit : U where
   MkUnit : Unit
@@ -10,8 +11,6 @@ data List : U -> U where
   Nil : {A : U} -> List A
   _::_ : {A : U} -> A -> List A -> List A
 
--- prj/menagerie/papers/combinatory
-
 infixr 6 _~>_
 data Type : U where
   ι : Type
@@ -41,23 +40,17 @@ data Env : Ctx -> U where
   ENil : Env Nil
   _:::_ : {Γ : Ctx} {σ : Type} → Val σ → Env Γ → Env (σ :: Γ)
 
--- TODO there is a problem here with coverage checking
--- I suspect something is being split before it's ready
+lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
+lookup Here (x ::: y) = x
+lookup () ENil
+lookup (There i) (x ::: env) = lookup i env
 
--- lookup : {σ : Type} {Γ : Ctx} → Ref σ Γ → Env Γ → Val σ
--- lookup Here (x ::: y) = x
--- lookup (There i) (x ::: env) = lookup i env
-
-lookup2 : {σ : Type} {Γ : Ctx} → Env Γ → Ref σ Γ → Val σ
-lookup2 (x ::: y) Here = x
-lookup2 (x ::: env) (There i) = lookup2 env i
-
--- TODO MixFix - this was ⟦_⟧
-eval : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
+infixl 1 ⟦_⟧
+⟦_⟧ : {Γ : Ctx} {σ : Type} → Term Γ σ → (Env Γ → Val σ)
 -- there was a unification error in direct application
-eval (App t u) env = (eval t env) (eval u env)
-eval (Lam t) env = \ x => eval t (x ::: env)
-eval (Var i) env = lookup2 env i
+⟦ App t u ⟧ env = (⟦ t ⟧ env) (⟦ u ⟧ env)
+⟦ Lam t ⟧ env = \ x => ⟦ t ⟧ (x ::: env)
+⟦ Var i ⟧ env = lookup i env
 
 data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   S : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => (f x) (g x))
@@ -65,7 +58,7 @@ data Comb : (Γ : Ctx) → (u : Type) → (Env Γ → Val u) → U where
   I : {Γ : Ctx} {σ : Type} → Comb Γ (σ ~> σ) (\ env => \ x => x)
   B : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((τ ~> τ') ~> (σ ~> τ) ~> (σ ~> τ')) (\ env => \ f g x => f (g x))
   C : {Γ : Ctx} {σ τ τ' : Type} → Comb Γ ((σ ~> τ ~> τ') ~> τ ~> (σ ~> τ')) (\ env => \ f g x => (f x) g)
-  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup2 env i)
+  CVar : {Γ : Ctx} {σ : Type} → (i : Ref σ Γ) → Comb Γ σ (\ env => lookup i env)
   CApp : {Γ : Ctx} {σ τ : Type} {f : _} {x : _} → Comb Γ (σ ~> τ) f → Comb Γ σ x → Comb Γ τ (\ env => (f env) (x env))
 
 sapp : {Γ : Ctx} {σ τ ρ : Type} {f : _} {x : _} →
@@ -86,11 +79,12 @@ abs I = CApp K I
 abs B = CApp K B
 abs C = CApp K C
 abs (CApp t u) = sapp (abs t) (abs u)
--- lookup2 was getting stuck, needed to re-eval the types in the rewritten env.
+-- lookup was getting stuck, needed to re-eval the types in the rewritten env.
 abs (CVar Here) = I
 abs (CVar (There i)) = CApp K (CVar i)
 
-translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ (eval tm)
+-- Was a bug in pratt parser when argument `⟦ tm ⟧` had a prefix operator
+translate : {Γ : Ctx} {σ : Type} → (tm : Term Γ σ) → Comb Γ σ ⟦ tm ⟧
 translate (App t u) = CApp (translate t) (translate u)
 translate (Lam t) = abs (translate t)
 translate (Var i) = CVar i

playground/samples/DSL.newt

@@ -1,33 +1,34 @@
 module DSL
 
+-- "A DSL for finite types and enumeration"
 -- https://www.youtube.com/watch?v=sFyy9sssK50
 
-data ℕ : U where
-  Z : ℕ
-  S : ℕ → ℕ
+data Nat : U where
+  Z : Nat
+  S : Nat → Nat
 
 infixl 7 _+_
 infixl 8 _*_
 
-_+_ : ℕ → ℕ → ℕ
+_+_ : Nat → Nat → Nat
 Z + m = m
 (S k) + m = S (k + m)
 
-_*_ : ℕ → ℕ → ℕ
+_*_ : Nat → Nat → Nat
 Z * m = Z
 (S k) * m = m + k * m
 
 infixr 4 _::_
-data Vec : U → ℕ → U where
-  Nil : {a} → Vec a Z
-  _::_ : {a k} → a → Vec a k → Vec a (S k)
+data Vec : U → Nat → U where
+  Nil : ∀ a. Vec a Z
+  _::_ : ∀ a k. a → Vec a k → Vec a (S k)
 
 infixl 5 _++_
-_++_ : {a n m} → Vec a n → Vec a m → Vec a (n + m)
+_++_ : ∀ a n m. Vec a n → Vec a m → Vec a (n + m)
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-map : {a b n} → (a → b) → Vec a n → Vec b n
+map : ∀ a b n. (a → b) → Vec a n → Vec b n
 map f Nil = Nil
 map f (x :: xs) = f x :: map f xs
 
@@ -43,7 +44,7 @@ two = Add One One
 four : E
 four = Mul two two
 
-card : E → ℕ
+card : E → Nat
 card Zero = Z
 card One = S Z
 card (Add x y) = card x + card y
@@ -53,15 +54,15 @@ data Empty : U where
 
 data Unit : U where
   -- unit accepted but case building thinks its a var
-  unit : Unit
+  MkUnit : Unit
 
 data Either : U -> U -> U where
-  Left : {A B} → A → Either A B
-  Right : {A B} → B → Either A B
+  Left : ∀ a b. a → Either a b
+  Right :  ∀ a b. b → Either a b
 
 infixr 4 _,_
 data Both : U → U → U where
-  _,_ : {A B} → A → B → Both A B
+  _,_ :  ∀ a b. a → b → Both a b
 
 typ : E → U
 typ Zero = Empty
@@ -73,10 +74,10 @@ Bool : U
 Bool = typ two
 
 false : Bool
-false = Left unit
+false = Left MkUnit
 
 true : Bool
-true = Right unit
+true = Right MkUnit
 
 BothBoolBool : U
 BothBoolBool = typ four
@@ -84,17 +85,17 @@ BothBoolBool = typ four
 ex1 : BothBoolBool
 ex1 = (false, true)
 
-enumAdd : {a b m n} → Vec a m → Vec b n → Vec (Either a b) (m + n)
+enumAdd : ∀ a b m n. Vec a m → Vec b n → Vec (Either a b) (m + n)
 enumAdd xs ys = map Left xs ++ map Right ys
 
 -- for this I followed the shape of _*_, the lecture was slightly different
-enumMul : {a b m n} → Vec a m → Vec b n → Vec (Both a b) (m * n)
+enumMul : ∀ a b m n. Vec a m → Vec b n → Vec (Both a b) (m * n)
 enumMul Nil ys = Nil
 enumMul (x :: xs) ys = map (_,_ x) ys ++ enumMul xs ys
 
 enumerate : (t : E) → Vec (typ t) (card t)
 enumerate Zero = Nil
-enumerate One = unit :: Nil
+enumerate One = MkUnit :: Nil
 enumerate (Add x y) = enumAdd (enumerate x) (enumerate y)
 enumerate (Mul x y) = enumMul (enumerate x) (enumerate y)
 
@@ -110,8 +111,8 @@ test4 = enumerate four
 -- for now, I'll define ≡ to check
 
 infixl 2 _≡_
-data _≡_ : {A} → A → A → U where
-  Refl : {A} {a : A} → a ≡ a
+data _≡_ : ∀ a. a → a → U where
+  Refl : ∀ a. {x : a} → x ≡ x
 
 test2' : test2 ≡ false :: true :: Nil
 test2' = Refl

playground/samples/Lists.newt

@@ -87,7 +87,7 @@ reverse-++-distrib (x :: xs) ys =
 -- same thing, but using `replace` in the proof
 reverse-++-distrib' : ∀ A. (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
 reverse-++-distrib' Nil ys = sym (++-identity (reverse ys))
-reverse-++-distrib' {A} (x :: xs) ys =
+reverse-++-distrib' {a} (x :: xs) ys =
   replace (\ z => (reverse (xs ++ ys) ++ (x :: Nil)) ≡ z)
           (sym (++-associative (reverse ys) (reverse xs) (x :: Nil)))
           (replace (\ z => (reverse (xs ++ ys)) ++ (x :: Nil) ≡ z ++ (x :: Nil)) (reverse-++-distrib' xs ys) Refl)

playground/samples/Reasoning.newt

@@ -1,48 +1,47 @@
 module Reasoning
 
-infix 4 _≡_
-data _≡_ : {A : U} → A → A → U where
-  Refl : ∀ A. {x : A} → x ≡ x
+-- From the "Lists" chapter of Programming Language Foundations in Agda
+-- https://plfa.github.io/Lists/
 
-sym : ∀ A. {x y : A} → x ≡ y → y ≡ x
+-- We define a few types and functions on lists and prove a couple of properties
+-- about them. This example demonstrates mixfix operators.
+
+infix 4 _≡_
+data _≡_ : ∀ A. A → A → U where
+  Refl : ∀ A. {0 x : A} → x ≡ x
+
+sym : ∀ A. {0 x y : A} → x ≡ y → y ≡ x
 sym Refl = Refl
 
-trans : ∀ A. {x y z : A} → x ≡ y → y ≡ z → x ≡ z
+trans : ∀ A. {0 x y z : A} → x ≡ y → y ≡ z → x ≡ z
 trans Refl eq = eq
 
-cong : ∀ A B. (f : A → B) {x y : A}
+cong : ∀ A B. (0 f : A → B) {0 x y : A}
   → x ≡ y
   → f x ≡ f y
 cong f Refl = Refl
 
-cong-app : ∀ A B. {f g : A → B}
+cong-app : ∀ A B. {0 f g : A → B}
   → f ≡ g
-  → (x : A) →  f x ≡ g x
+  → (0 x : A) →  f x ≡ g x
 cong-app Refl = λ y => Refl
 
 infixl 1 begin_
 infixr 2 _≡⟨⟩_ _≡⟨_⟩_
 infixl 3 _∎
 
-begin_ : ∀ A. {x y : A} → x ≡ y → x ≡ y
+begin_ : ∀ A. {0 x y : A} → x ≡ y → x ≡ y
 begin x≡y = x≡y
 
-_≡⟨⟩_  : ∀ A. (x : A) {y : A} → x ≡ y → x ≡ y
+_≡⟨⟩_  : ∀ A. (0 x : A) {0 y : A} → x ≡ y → x ≡ y
 x ≡⟨⟩ x≡y = x≡y
 
-_≡⟨_⟩_ : ∀ A. (x : A) {y z : A} → x ≡ y → y ≡ z → x ≡ z
+_≡⟨_⟩_ : ∀ A. (0 x : A) {0 y z : A} → x ≡ y → y ≡ z → x ≡ z
 x ≡⟨ x≡y ⟩ y≡z = trans x≡y y≡z
 
-_∎ : ∀ A. (x : A) → x ≡ x
+_∎ : ∀ A. (0 x : A) → x ≡ x
 x ∎ = Refl
 
-
--- From the "Lists" chapter of Programming Language Foundations in Agda
--- https://plfa.github.io/Lists/
-
--- We define a few types and functions on lists and prove a couple of properties
--- about them
-
 -- Natural numbers are zero (Z) or the successor (S) of a natural number
 -- We'll use these to represent the length of lists
 data Nat : U where

playground/samples/Tour.newt

@@ -1,7 +1,5 @@
-
-
 /-
-  This is newt, a self-hosted, dependent typed programming language that
+  Newt is a self-hosted, dependent typed programming language that
   compiles to javascript and borrows a lot of syntax from Idris and Agda.
 
   This page is a very simple web playground based on the codemirror editor.
@@ -18,27 +16,45 @@
 -- it must match the filename
 module Tour
 
--- We can import other modules, with a flat namespace and no cycles,
--- diamonds are ok, Prelude is not imported by default, only explicitly
--- imported modules are in scope
+-- We can import other modules with no cycles, diamonds are ok, cycles
+-- are an error. Prelude is not imported by default. Only explicitly
+-- imported modules are in scope. Duplicate names are not allowed.
 
--- commented out because we redefine parts of Prelude in this file.
--- import Prelude
+-- Example import is commented out because we redefine Prelude
+-- functions below.
 
--- We're calling the universe U and are doing type in type for now
+/-
+
+import Prelude
+
+-/
+
+
+-- The universe is U and are doing type in type for now.
+
+-- INDUCTIVE TYPES
 
 -- Inductive type definitions are similar to Idris, Agda, or Haskell
 data Nat : U where
   Z : Nat
   S : Nat -> Nat
 
--- Nat-shaped data is turned into numbers in codegen.
+-- Like in Idris, Nat-shaped data is turned into numbers at runtime.
+-- We are not yet ignoring erased fields though.
 
 -- Multiple names are allowed on the left:
 data Bool : U where
   True False : Bool
 
--- Enum shaped data becomes a bare string (the constructor name) in codegen.
+-- There also is an abbreviated syntactic sugar for simple types:
+
+data Tree a = Node a (Tree a) (Tree a) | Leaf
+
+-- Enum shaped data becomes a number at runtime (the constructor tag).
+
+data Answer = Yes | No | Maybe
+
+-- FUNCTIONS
 
 -- function definitions are equations using dependent pattern matching
 plus : Nat -> Nat -> Nat
@@ -111,19 +127,22 @@ isVowel _ = False
 
 -- And primitive functions have a type and a javascript definition:
 
-pfunc plusInt : Int -> Int -> Int := `(x,y) => x + y`
-pfunc plusString : String -> String -> String := `(x,y) => x + y`
+pfunc addInt : Int -> Int -> Int := `(x,y) => x + y`
+pfunc addString : String -> String -> String := `(x,y) => x + y`
 
--- We can make them Plus instances:
 
 instance Add Int where
-  _+_ = plusInt
+  _+_ = addInt
+
+
+infixr 7 _++_
+class Concat a where
+  _++_ : a → a → a
+
+instance Concat String where
+  _++_ = addString
 
-instance Add String where
-  _+_ = plusString
 
-concat : String -> String -> String
-concat a b = a + b
 
 -- Now we define Monad
 class Monad (m : U -> U) where
@@ -156,40 +175,32 @@ _>>=_ ma amb = bind ma amb
 _>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
 ma >> mb = ma >>= (λ _ => mb)
 
--- Now we define list and show it is a monad. At the moment, I don't
--- have sugar for Lists,
+-- Now we define list and show it is a monad.
 
 infixr 3 _::_
 data List : U -> U where
   Nil : ∀ A.  List A
   _::_ : ∀ A. A -> List A -> List A
 
-infixr 7 _++_
-_++_ : ∀ a.  List a -> List a -> List a
-Nil ++ ys = ys
-(x :: xs) ++ ys = x :: (xs ++ ys)
-
 instance Monad List where
   pure a = a :: Nil
   bind Nil f = Nil
   bind (x :: xs) f = f x ++ bind xs f
 
-/-
-This desugars to: (the names in guillemots are not user-accessible)
+-- and has the _++_ operator
 
-«Monad List,pure» : { a : U } -> a:0 -> List a:1
-pure a = _::_ a Nil
+instance ∀ a. Concat (List a) where
+  Nil ++ ys = ys
+  (x :: xs) ++ ys = x :: (xs ++ ys)
 
-«Monad List,bind» : { a : U } -> { b : U } -> (List a) -> (a -> List b) -> List b
-bind Nil f = Nil bind (_::_ x xs) f = _++_ (f x) (bind xs f)
+-- A utility function used in generating Show instances below:
 
-«Monad List» : Monad List
-«Monad List» = MkMonad «Monad List,pure» «Monad List,bind»
+joinBy : String → List String → String
+joinBy _ Nil = ""
+joinBy _ (x :: Nil) = x
+joinBy s (x :: y :: xs) = joinBy s ((x ++ s ++ y) :: xs)
 
--/
-
--- We'll want Pair below.  `,` has been left for use as an operator.
--- Also we see that → can be used in lieu of ->
+-- We define a product of two types (→ can be used in lieu of ->)
 infixr 1 _,_ _×_
 data _×_ : U → U → U where
   _,_ : ∀ A B. A → B → A × B
@@ -202,6 +213,18 @@ prod xs ys = do
   y <- ys
   pure (x, y)
 
+-- The prelude defines Eq and Show, which can be derived
+
+infixl 6 _==_
+class Eq a where
+  _==_ : a → a → Bool
+
+derive Eq Nat
+
+class Show a where
+  show : a → String
+
+derive Show Nat
 
 data Unit = MkUnit
 
@@ -219,8 +242,10 @@ instance Monad IO where
 
 pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => {
   console.log(s)
-  return Prelude_MkIORes(null,Prelude_MkUnit,w)
+  return Tour_MkIORes(Tour_MkUnit, w)
 }`
 
 main : IO Unit
-main = putStrLn "Hello, World!"
+main = do
+  putStrLn "Hello, World!"
+  putStrLn $ show (S (S Z))

playground/samples/Tree.newt

@@ -3,7 +3,6 @@ module Tree
 -- adapted from Conor McBride's 2-3 tree example
 -- youtube video: https://youtu.be/v2yXrOkzt5w?t=3013
 
-
 data Nat : U where
   Z : Nat
   S : Nat -> Nat
@@ -16,8 +15,8 @@ data Void : U where
 infixl 4 _+_
 
 data _+_ : U -> U -> U where
-  inl : {A B} -> A -> A + B
-  inr : {A B} -> B -> A + B
+  inl : ∀ a b. a -> a + b
+  inr : ∀ a b. b -> a + b
 
 infix 4 _<=_
 
@@ -47,14 +46,14 @@ _ <<= Top = Unit
 _ <<= _ = Void
 
 data Intv : Bnd -> Bnd -> U where
-  intv : {l u} (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
+  intv : ∀ l u. (x : Nat) (lx : l <<= N x) (xu : N x <<= u) -> Intv l u
 
 data T23 : Bnd -> Bnd -> Nat -> U where
-  leaf : {l u} (lu : l <<= u) -> T23 l u Z
-  node2 : {l u h} (x : _)
+  leaf : ∀ l u. (lu : l <<= u) -> T23 l u Z
+  node2 : ∀ l u h. (x : _)
     (tlx : T23 l (N x) h) (txu : T23 (N x) u h) ->
     T23 l u (S h)
-  node3 : {l u h} (x y : _)
+  node3 : ∀ l u h. (x y : _)
     (tlx : T23 l (N x) h) (txy : T23 (N x) (N y) h) (tyu : T23 (N y) u h) ->
     T23 l u (S h)
 
@@ -66,12 +65,12 @@ data Sg : (A : U) -> (A -> U) -> U where
   _,_ : {A : U} {B : A -> U} -> (a : A) -> B a -> Sg A B
 
 _*_ : U -> U -> U
-A * B = Sg A (\ _ => B)
+a * b = Sg a (\ _ => b)
 
 TooBig : Bnd -> Bnd -> Nat -> U
 TooBig l u h = Sg Nat (\ x => T23 l (N x) h * T23 (N x) u h)
 
-insert : {l u h} -> Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
+insert : ∀ l u h. Intv l u -> T23 l u h -> TooBig l u h + T23 l u h
 insert (intv x lx xu) (leaf lu) = inl (x , (leaf lx , leaf xu))
 insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
   -- u := N y is not solved at this time

playground/samples/TypeClass.newt

@@ -5,7 +5,7 @@ class Monad (m : U → U) where
   pure : ∀ a. a → m a
 
 infixl 1 _>>=_ _>>_
-_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b
+_>>=_ : ∀ m. {{Monad m}} {0 a b : _} -> (m a) -> (a -> m b) -> m b
 ma >>= amb = bind ma amb
 
 _>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
@@ -15,7 +15,7 @@ data Either : U -> U -> U where
   Left : ∀ A B. A -> Either A B
   Right : ∀ A B. B -> Either A B
 
-instance {a} -> Monad (Either a) where
+instance ∀ a. Monad (Either a) where
   bind (Left a) amb = Left a
   bind (Right b) amb = amb b
 

playground/src/cmeditor.ts

@@ -26,6 +26,7 @@ const keywords = [
   "case",
   "of",
   "data",
+  "derive",
   "U",
   "do",
   "ptype",
@@ -153,6 +154,36 @@ const newtLanguage2: StreamLanguage<State> = StreamLanguage.define({
   },
 });
 
+export function scheme() {
+  return new LanguageSupport(schemeLanguage);
+}
+
+const schemeLanguage: StreamLanguage<State> = StreamLanguage.define({
+  startState: () => null,
+  token(stream, st) {
+    const keywords = ["define", "let", "case", "cond", "import", "include", "lambda", "else"];
+    if (stream.eatSpace()) return null;
+    if (stream.match("--")) {
+      stream.skipToEnd();
+      return "comment";
+    }
+    if (stream.match(/[0-9A-Za-z!%&*+./:<=>?@^_~-]+/)) {
+      let word = stream.current();
+      if (keywords.includes(word)) return "keyword";
+      return null;
+    }
+    // unhandled
+    stream.next();
+    return null
+  },
+  languageData: {
+    commentTokens: {
+      line: ";;",
+    },
+    wordChars: "!%&*+-./:<=>?@^_~",
+  },
+});
+
 function newt() {
   return new LanguageSupport(newtLanguage2);
 }
@@ -233,32 +264,29 @@ export class CMEditor implements AbstractEditor {
           });
         }),
           this.theme.of(EditorView.baseTheme({})),
-          hoverTooltip((view, pos) => {
+          hoverTooltip(async (view, pos) => {
             let cursor = this.view.state.doc.lineAt(pos);
-            let line = cursor.number;
-            let range = this.view.state.wordAt(pos);
-            console.log(range);
-            if (range) {
-              let col = range.from - cursor.from;
-              let word = this.view.state.doc.sliceString(range.from, range.to);
-              let entry = this.delegate.getEntry(word, line, col);
-              if (!entry)
-                entry = this.delegate.getEntry("_" + word + "_", line, col);
-              console.log("entry for", word, "is", entry);
-              if (entry) {
-                let rval: Tooltip = {
-                  pos: range.head,
-                  above: true,
-                  create: () => {
-                    let dom = document.createElement("div");
-                    dom.className = "tooltip";
-                    dom.textContent = entry.type;
-                    return { dom };
-                  },
-                };
-                return rval;
-              }
+            let line = cursor.number - 1;
+            let col = pos - cursor.from;
+            // let range = this.view.state.wordAt(pos);
+            console.log('getting hover for ',line, col);
+            let entry = await this.delegate.getEntry('', line, col)
+
+            if (entry) {
+              let rval: Tooltip = {
+                // TODO pull in position from LSP (currently it only has the jump-to FC)
+                pos,
+                above: true,
+                create: () => {
+                  let dom = document.createElement("div");
+                  dom.className = "tooltip";
+                  dom.textContent = entry.info;
+                  return { dom };
+                },
+              };
+              return rval;
             }
+
             // we'll iterate the syntax tree for word.
             // let entry = delegate.getEntry(word, line, col)
             return null;

playground/src/emul.ts

@@ -7,6 +7,8 @@ export interface Handle {
   buf: Uint8Array;
 }
 
+// Some of this was written for Idris and is not used by newt
+
 interface Process {
   argv: string[];
   platform: string;
@@ -47,6 +49,12 @@ export let shim: NodeShim = {
     writeFileSync(name: string, data: string, enc?: string) {
       shim.files[name] = new TextEncoder().encode(data)
     },
+    writeSync(fd: number, data: string) {
+      shim.stdout += data;
+    },
+    readSync() {
+      return 0;
+    }
   },
   process: {
     argv: ["", ""],

playground/src/frame.ts

@@ -14,15 +14,18 @@ const shim = {
         throw new Error(`${fn} not found`);
       }
     },
+    writeSync: (fd: number, msg: string) => console.log(msg)
   },
 };
 // we intercept require to return our fake node modules
 declare global {
   interface Window {
     require: (x: string) => any;
+    fs: any;
   }
 }
 const requireStub: any = (x: string) => (shim as any)[x];
+self.fs = shim.fs;
 self.require = requireStub;
 self.process = {
   platform: "linux",

playground/src/fs.ts

@@ -0,0 +1,6 @@
+import {shim} from './emul';
+
+// Shim was dumping stuff globally and we've shifted to imports, so I'm adapting it here for now.
+
+export const {readFileSync, writeFileSync, writeFile, writeSync, readSync } = shim.fs;
+export default {readFileSync, writeFileSync, writeFile, writeSync, readSync };

playground/src/help.md

@@ -2,7 +2,7 @@
 
 Newt is a dependent typed programming language that compiles to javascript. This playground embeds the newt compiler and a codemirror based editor.
 
-The editor will typecheck the file with newt and render errors as the file is changed. The current file is saved to localStorage and will be restored if there is no data in the URL. Cmd-s or Ctrl-s will create a url embedding the file contents. There is a layout toggle for phone use.
+The editor will typecheck the file with newt and render errors as the file is changed. The current file is saved to localStorage and will be restored if there is no data in the URL. Cmd-s or Ctrl-s will create a url embedding the file contents.
 
 ## Tabs
 
@@ -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/ipc.ts

@@ -1,11 +1,55 @@
+
+//// Copy of LSP types
+
+export interface Location { uri: string; range: Range; }
+export interface Position { line: number; character: number; }
+export interface Range { start: Position; end: Position; }
+export interface HoverResult { info: string; location: Location; }
+export interface TextEdit { range: Range; newText: string; }
+export type DiagnosticSeverity = 1 | 2 | 3 | 4
+export interface DiagnosticRelatedInformation { location: Location; message: string; }
+export interface Diagnostic {
+    range: Range
+    message: string
+    severity?: DiagnosticSeverity
+    source?: string
+    // we don't emit this yet, but I think we will
+    relatedInformation?: DiagnosticRelatedInformation[]
+}
+
+export interface WorkspaceEdit {
+  changes?: {
+    [uri: string]: TextEdit[];
+  }
+}
+
+export interface CodeAction {
+  title: string;
+  edit?: WorkspaceEdit;
+}
+
+export interface BuildResult {
+  diags: Diagnostic[]
+  output: string
+}
+
+//// IPC Thinger
+
 export type Result<A> =
   | { status: "ok"; value: A }
   | { status: "err"; error: string };
 
 export interface API {
-  save(fileName: string, content: string): string;
-  typeCheck(fileName: string): string;
-  compile(fileName: string): string;
+  // Invalidates stuff and writes to an internal cache that overlays the "filesystem"
+  updateFile(fileName: string, content: string): unknown;
+  // Run checking, return diagnostics
+  typeCheck(fileName: string): BuildResult;
+  // returns True if we need to recheck - usually for files invalidating other files
+  // The playground rarely hits this situation at the moment
+  hoverInfo(fileName: string, row: number, col: number): HoverResult | boolean | null;
+  codeActionInfo(fileName: string, row: number, col: number): CodeAction[] | null;
+  // we need to add this to the LSP build
+  compile(fileName: string, language: 'javascript'|'scheme'):  string;
 }
 
 export interface Message<K extends keyof API> {
@@ -14,9 +58,9 @@ export interface Message<K extends keyof API> {
   args: Parameters<API[K]>;
 }
 
-export interface ResponseMSG {
+export interface ResponseMSG<K extends keyof API> {
   id: number;
-  result: string;
+  result: Awaited<ReturnType<API[K]>>;
 }
 
 type Suspense = {
@@ -33,7 +77,8 @@ export class IPC {
     this._postMessage = <K extends keyof API>(msg: Message<K>) =>
       newtWorker.postMessage(msg);
     // Safari/MobileSafari have small stacks in webworkers.
-    if (navigator.vendor.includes("Apple")) {
+    // But support for the frame needs to be fixed
+    if (navigator.vendor.includes("Apple") && false) {
       const workerFrame = document.createElement("iframe");
       workerFrame.src = "worker.html";
       workerFrame.style.display = "none";
@@ -46,7 +91,7 @@ export class IPC {
     }
     // Need to handle messages from the other iframe too? Or at least ignore them.
   }
-  onmessage = (ev: MessageEvent<ResponseMSG>) => {
+  onmessage = <K extends keyof API>(ev: MessageEvent<ResponseMSG<K>>) => {
     console.log("GET", ev.data);
     // Maybe key off of type
     if (ev.data.id) {
@@ -71,4 +116,3 @@ export class IPC {
   }
 }
 
-class IPCClient {}

playground/src/main.ts

@@ -11,32 +11,40 @@ import {
   TopData,
   Marker,
 } from "./types.ts";
-import { CMEditor } from "./cmeditor.ts";
+import { CMEditor, scheme } from "./cmeditor.ts";
 import { deflate } from "./deflate.ts";
 import { inflate } from "./inflate.ts";
-import { IPC } from "./ipc.ts";
+import { IPC, Position } from "./ipc.ts";
 import helpText from "./help.md?raw";
-import share from "./share.svg"
-import share_light from "./share_light.svg"
-import play from "./play.svg"
-import play_light from "./play_light.svg"
+import { basicSetup, EditorView} from "codemirror";
+import {Compartment, EditorState} from "@codemirror/state";
+import { javascript } from "@codemirror/lang-javascript";
+import { oneDark } from "@codemirror/theme-one-dark";
 
 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
 }
 
+function bundle(js: string) {
+  js = js.replace(/^import.*\n/g, '');
+  js = js.replace(/\nexport /g, '\n');
+  return js;
+}
+
 function md2nodes(md: string)  {
   let rval: VNode[] = []
   let list: VNode[] | undefined
@@ -73,9 +81,21 @@ if (!state.javascript.value) {
     console.log("SEND TO", iframe.contentWindow);
     const fileName = state.currentFile.value;
     // maybe send fileName, src?
-    await ipc.sendMessage("save", [fileName, src]);
-    let js = await ipc.sendMessage("compile", [fileName]);
-    state.javascript.value = js;
+    await ipc.sendMessage("updateFile", [fileName, src]);
+    let js = await ipc.sendMessage("compile", [fileName, "javascript"]);
+    state.javascript.value = bundle(js);
+  }
+}
+
+async function refreshScheme() {
+if (!state.scheme.value) {
+    let src = state.editor.value!.getValue();
+    console.log("SEND TO", iframe.contentWindow);
+    const fileName = state.currentFile.value;
+    // maybe send fileName, src?
+    await ipc.sendMessage("updateFile", [fileName, src]);
+    let scheme = await ipc.sendMessage("compile", [fileName, "scheme"]);
+    state.scheme.value = scheme;
   }
 }
 
@@ -145,21 +165,29 @@ function getSavedCode() {
   return value;
 }
 
+const RESULTS = "Output";
+const JAVASCRIPT = "JS";
+const SCHEME = "Scheme";
+const CONSOLE = "Console";
+const HELP = "Help";
+
 const state = {
   output: signal(""),
   toast: signal(""),
   javascript: signal(""),
+  scheme: signal(""),
   messages: signal<string[]>([]),
   editor: signal<AbstractEditor | null>(null),
   dark: signal(false),
   files: signal<string[]>(["Tour.newt"]),
   currentFile: signal<string>(localStorage.currentFile ?? "Tour.newt"),
+  selected: signal(localStorage.tab ?? RESULTS),
 };
 
 // Monitor dark mode state (TODO - let user override system setting)
 if (window.matchMedia) {
   function checkDark(ev: { matches: boolean }) {
-    console.log("CHANGE", ev);
+    console.log("CHANGE", ev.matches, ev);
     if (ev.matches) {
       document.body.className = "dark";
       state.dark.value = true;
@@ -202,8 +230,12 @@ interface EditorProps {
   initialValue: string;
 }
 const language: EditorDelegate = {
-  getEntry(word, _row, _col) {
-    return topData?.context.find((entry) => entry.name === word);
+  async getEntry(word, row, col) {
+    let fileName = state.currentFile.value
+    let res = await ipc.sendMessage("hoverInfo", [fileName, row, col])
+    console.log('HOVER', res, 'for', row, col)
+    if (res == true) return null
+    return res || null
   },
   onChange(_value) {
     // we're using lint() now
@@ -220,30 +252,39 @@ const language: EditorDelegate = {
     let module = src.match(/module\s+([^\s]+)/)?.[1];
     if (module) {
       // This causes problems with stuff like aoc/...
-      state.currentFile.value = module.replace(".", "/") + ".newt";
+      state.currentFile.value = './' + module.replace(".", "/") + ".newt";
     }
-    state.javascript.value = ''
+    // This is a little flashy
+    // state.javascript.value = ''
     let fileName = state.currentFile.value;
     console.log("FN", fileName);
     try {
-      await ipc.sendMessage("save", [fileName, src]);
-      let out = await ipc.sendMessage("typeCheck", [fileName]);
-      setOutput(out);
-      let markers = processOutput(out);
+      await ipc.sendMessage("updateFile", [fileName, src]);
+      let res = await ipc.sendMessage("typeCheck", [fileName]);
       let diags: Diagnostic[] = [];
-      for (let marker of markers) {
-        let col = marker.startColumn;
+      for (let marker of res.diags) {
+        let {start,end} = marker.range
+        let xlate = (pos: Position): number =>
+          view.state.doc.line(pos.line + 1).from + pos.character
 
-        let line = view.state.doc.line(marker.startLineNumber);
-        const pos = line.from + col - 1;
-        let word = view.state.wordAt(pos);
+        // TODO double check the last two are right
+        const SEVERITY: Diagnostic["severity"][] = [ "error", "error", "warning", "info", "hint"]
+        console.error({
+          from: xlate(start),
+          to: xlate(end),
+          severity: SEVERITY[marker.severity ?? 1],
+          message: marker.message,
+        })
         diags.push({
-          from: word?.from ?? pos,
-          to: word?.to ?? pos + 1,
-          severity: marker.severity,
+          from: xlate(start),
+          to: xlate(end),
+          severity: SEVERITY[marker.severity ?? 1],
           message: marker.message,
         });
       }
+      setOutput(res.output)
+      state.javascript.value = ""
+      state.scheme.value = ""
       return diags;
     } catch (e) {
       console.log("ERR", e);
@@ -259,19 +300,53 @@ function Editor({ initialValue }: EditorProps) {
   useEffect(() => {
     const container = ref.current!;
     const editor = new CMEditor(container, value, language);
-    // const editor = new MonacoEditor(container, value, language)
     state.editor.value = editor;
     editor.setDark(state.dark.value);
     if (initialValue === LOADING) loadFile("Tour.newt");
   }, []);
-
   return h("div", { id: "editor", ref });
 }
 
-// for extra credit, we could have a read-only monaco
-function JavaScript() {
-  const text = state.javascript.value;
-  return h("div", { id: "javascript" }, text);
+interface ViewerProps {
+  language: 'javascript' | 'scheme'
+}
+function SourceViewer({language}: ViewerProps) {
+  const text = state[language].value;
+
+  // return h("div", { id: "javascript" }, text);
+  const ref = useRef<HTMLDivElement>(null);
+  const editorView = useRef<EditorView>(null);
+  const themeRef = useRef<Compartment>(null);
+  useEffect(() => {
+    const container = ref.current!;
+    themeRef.current = new Compartment();
+    const editor = new EditorView({
+      doc: text,
+      parent: container,
+      extensions: [
+        basicSetup,
+        themeRef.current.of(state.dark.value ? oneDark : EditorView.baseTheme({})),
+        language == 'javascript' ? javascript() : scheme(),
+        EditorState.readOnly.of(true),
+        EditorView.editable.of(false),
+      ],
+    });
+    // const editor = new CMEditor(container, text, language);
+    // state.editor.value = editor;
+    // editor.setDark(state.dark.value);
+    editorView.current = editor;
+  }, []);
+  let isDark = state.dark.value;
+  let ev = editorView.current;
+  if (ev) {
+    ev.dispatch({
+      effects: themeRef.current?.reconfigure(
+        isDark ? oneDark : EditorView.baseTheme({})
+      ),
+      changes: { from: 0, to: ev.state.doc.length, insert: text },
+    });
+  }
+  return h("div", { id: "javascript", ref });
 }
 
 function Result() {
@@ -292,16 +367,11 @@ function Console() {
   );
 }
 
-const RESULTS = "Output";
-const JAVASCRIPT = "JS";
-const CONSOLE = "Console";
-const HELP = "Help";
-
 function Tabs() {
-  const [selected, setSelected] = useState(localStorage.tab ?? RESULTS);
+  const selected = state.selected.value
   const Tab = (label: string) => {
     let onClick = () => {
-      setSelected(label);
+      state.selected.value = label;
       localStorage.tab = label;
     };
     let className = "tab";
@@ -310,20 +380,24 @@ function Tabs() {
   };
 
   useEffect(() => {
-    if (state.messages.value.length) setSelected(CONSOLE);
+    if (state.messages.value.length) state.selected.value = CONSOLE;
   }, [state.messages.value]);
 
   useEffect(() => {
     if (selected === JAVASCRIPT && !state.javascript.value) refreshJS();
-  }, [selected, state.javascript.value]);
+    if (selected === SCHEME && !state.scheme.value) refreshScheme();
+  }, [selected, state.javascript.value, state.scheme.value]);
 
   let body;
   switch (selected) {
     case RESULTS:
       body = h(Result, {});
       break;
+    case SCHEME:
+      body = h(SourceViewer, {language: 'scheme'});
+      break;
     case JAVASCRIPT:
-      body = h(JavaScript, {});
+      body = h(SourceViewer, {language:'javascript'});
       break;
     case CONSOLE:
       body = h(Console, {});
@@ -343,6 +417,7 @@ function Tabs() {
       { className: "tabBar" },
       Tab(RESULTS),
       Tab(JAVASCRIPT),
+      Tab(SCHEME),
       Tab(CONSOLE),
       Tab(HELP),
     ),
@@ -361,6 +436,10 @@ preload.then(() => {
   }
 });
 
+function Icon({name}: {name: string}) {
+  return h('svg', {'class':'icon'}, h('use', {href:`#${name}`}))
+}
+
 function EditWrap() {
   const options = state.files.value.map((value) =>
     h("option", { value }, value)
@@ -386,10 +465,12 @@ function EditWrap() {
         h("option", { value: "" }, "-- load sample --"),
         options
       ),
+      // h("a", { href: 'https://github.com/dunhamsteve/newt', target: '_blank', title: "github" }, h('img', {src: state.dark.value ? github : github_light})),
+      h("a", { href: 'https://github.com/dunhamsteve/newt', target: '_blank', title: "github" }, h('svg', {'class':'icon'}, h('use', {href:'#github'}))),
       h("div", { style: { flex: "1 1" } }),
       h("div", {},
-        h("button", { onClick: copyToClipboard, title: "copy url" }, h('img', {src: state.dark.value ? share : share_light})),
-        h("button", { onClick: runOutput, title: "run program" }, h('img', {src: state.dark.value ? play : play_light})),
+        h("button", { onClick: copyToClipboard, title: "copy url" },  h('svg', {'class':'icon'}, h('use', {href:'#share'}))),
+        h("button", { onClick: runOutput, title: "run program" }, h('svg', {'class':'icon'}, h('use', {href:'#play'}))),
       )
     ),
     h("div", { className: "tabBody" }, h(Editor, { initialValue: value }))
@@ -439,6 +520,7 @@ const processOutput = (
       let endLineNumber = +eline;
       let endColumn = +ecol
       // FIXME - pass the real path in
+      if (file.startsWith("./")) file = file.slice(2);
       if (fn && fn !== file) {
         startLineNumber = startColumn = 0;
       }

playground/src/newt.d.ts

@@ -0,0 +1,8 @@
+import { Diagnostic, HoverResult, CodeAction } from './ipc'
+
+export function LSP_updateFile(name: string, content: string): any;
+export function LSP_checkFile(name: string): Diagnostic[];
+export function LSP_hoverInfo(name: string, row: number, col: number): HoverResult | boolean | null;
+export function LSP_codeActionInfo(name: string, row: number, col: number): CodeAction[] | null;
+export function LSP_compileJS(name: string): string;
+export function LSP_compileToScheme(name: string): string;

playground/src/play.svg

@@ -1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" height="24px" viewBox="0 -960 960 960" width="24px" fill="#e3e3e3"><path d="M320-200v-560l440 280-440 280Zm80-280Zm0 134 210-134-210-134v268Z"/></svg>

playground/src/play_light.svg

@@ -1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" height="24px" viewBox="0 -960 960 960" width="24px" fill="#1f1f1f"><path d="M320-200v-560l440 280-440 280Zm80-280Zm0 134 210-134-210-134v268Z"/></svg>

playground/src/share.svg

@@ -1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" height="24px" viewBox="0 -960 960 960" width="24px" fill="#e3e3e3"><path d="M240-80q-33 0-56.5-23.5T160-160v-400q0-33 23.5-56.5T240-640h120v80H240v400h480v-400H600v-80h120q33 0 56.5 23.5T800-560v400q0 33-23.5 56.5T720-80H240Zm200-240v-447l-64 64-56-57 160-160 160 160-56 57-64-64v447h-80Z"/></svg>

playground/src/share_light.svg

@@ -1 +0,0 @@
-<svg xmlns="http://www.w3.org/2000/svg" height="24px" viewBox="0 -960 960 960" width="24px" fill="#1f1f1f"><path d="M240-80q-33 0-56.5-23.5T160-160v-400q0-33 23.5-56.5T240-640h120v80H240v400h480v-400H600v-80h120q33 0 56.5 23.5T800-560v400q0 33-23.5 56.5T720-80H240Zm200-240v-447l-64 64-56-57 160-160 160 160-56 57-64-64v447h-80Z"/></svg>

playground/src/types.ts

@@ -1,7 +1,6 @@
 import { EditorView } from "codemirror";
-import { linter, Diagnostic } from "@codemirror/lint";
-
-
+import { Diagnostic } from "@codemirror/lint";
+import { HoverResult } from "./ipc";
 
 export interface CompileReq {
   id: string
@@ -55,7 +54,7 @@ export interface TopData {
   context: TopEntry[];
 }
 export interface EditorDelegate {
-  getEntry(word: string, row: number, col: number): TopEntry | undefined
+  getEntry(word: string, row: number, col: number): Promise<HoverResult | null>
   onChange(value: string): unknown
   getFileName(): string
   lint(view: EditorView): Promise<Diagnostic[]> | Diagnostic[]

playground/src/worker.ts

@@ -1,50 +1,53 @@
 import { shim } from "./emul";
 import { API, Message, ResponseMSG } from "./ipc";
 import { archive, preload } from "./preload";
+import { LSP_checkFile, LSP_codeActionInfo, LSP_compileJS, LSP_compileToScheme, LSP_hoverInfo, LSP_updateFile } from './newt';
 
 const LOG = console.log
-console.log = (m) => {
-  shim.stdout += "\n" + m;
-};
+
+// console.log = (m) => {
+//   LOG(m)
+//   shim.stdout += "\n" + m;
+// };
+
+const invoke = <T extends (...args: any[]) => any>(fun:T, args: Parameters<T>): ReturnType<T> => {
+  return fun.apply(undefined, args)
+}
+
+const api: API = {
+  // none of these are promises...
+  updateFile: LSP_updateFile,
+  typeCheck(filename) {
+    shim.stdout = ""
+    let diags = LSP_checkFile(filename);
+    let output = shim.stdout
+    return {diags,output}
+  },
+  hoverInfo: LSP_hoverInfo,
+  codeActionInfo: LSP_codeActionInfo,
+  compile: (fn, lang) => {
+    if (lang == 'scheme') return LSP_compileToScheme(fn);
+    return LSP_compileJS(fn);
+  }
+}
 
 const handleMessage = async function <K extends keyof API>(ev: { data: Message<K> }) {
   LOG("HANDLE", ev.data);
   await preload;
   shim.archive = archive;
-  let key = ev.data.key
-  if (key === 'typeCheck' || key === 'compile') {
-    let {id, args: [fileName]} = ev.data
-    LOG(key, fileName)
-    const outfile = "out.js";
-    const isCompile = key === 'compile';
-    if (isCompile)
-      shim.process.argv = ["browser", "newt", fileName, "-o", outfile, "--top"];
-    else
-      shim.process.argv = ["browser", "newt", fileName, "--top"];
-    shim.stdout = "";
-    shim.files[outfile] = new TextEncoder().encode("No JS output");
-
-    try {
-      Main_main();
-    } catch (e) {
-      // make it clickable in console
-      console.error(e);
-      // make it visable on page
-      shim.stdout += "\n" + String(e);
-    }
-    let result = isCompile ? new TextDecoder().decode(shim.files[outfile]) : shim.stdout
-    sendResponse({id, result})
-  } else if (key === 'save') {
-    let {id, args: [fileName, content]} = ev.data
-    LOG(`SAVE ${content?.length} to ${fileName}`)
-    shim.files[fileName] = new TextEncoder().encode(content)
-    LOG('send', {id, result: ''})
-    sendResponse({id, result: ''})
+  try {
+    shim.stdout = ''
+    let {id, key, args} = ev.data
+    let result = await invoke(api[key], args)
+    LOG('got', result)
+    sendResponse<typeof key>({id, result})
+  } catch (e) {
+    console.error(e)
   }
+  console.log(shim.stdout)
 
 };
 
 // hooks for worker.html to override
-let sendResponse: <K extends keyof API>(_: ResponseMSG) => void = postMessage;
+let sendResponse: <K extends keyof API>(_: ResponseMSG<K>) => void = postMessage;
 onmessage = handleMessage;
-importScripts("newt.js");

playground/style.css

@@ -1,15 +1,55 @@
+:root {
+  --border-color: #888;
+  --tab-select-color: #555;
+  --text-color: black;
+  --tab-text-color: #555;
+}
 body {
   overflow: hidden;
   font-size: 12px;
+  -webkit-text-size-adjust: none;
 }
 svg.icon path {
   stroke: black;
   fill: none;
 }
+a>img {
+  width: 20px;
+}
+svg.icon {
+  color: var(--text-color);
+  width: 24px;
+  height: 24px;
+}
+@media (prefers-color-scheme: dark) {
+  :root {
+    --tab-select-color: #eee;
+    --tab-text-color: #aaa;
+    --text-color: white;
+    background-color: black;
+    color-scheme: dark;
+  }
+
+	body {
+    color: var(--text-color);
+
+  }
+  svg.icon path {
+    stroke: white;
+    fill: none;
+  }
+  .tabBody {
+    /* match editor */
+    color: #abb2bf;
+    background-color: #282c34;
+  }
+}
 
 #help {
   padding: 5px;
   font-family: 'Comic Code', monospace;
+  overflow: auto;
+  height: 100%;
 }
 
 #help>div {
@@ -32,17 +72,13 @@ svg.icon path {
   background: white;
   text-align: center;
 }
-@media (prefers-color-scheme: dark) {
-	body {
-    color: white;
-    background-color: black;
-  }
-  svg.icon path {
-    stroke: white;
-    fill: none;
-  }
-}
 
+#javascript {
+  height: 100%;
+}
+.right .tabBody {
+  border-left: solid 1px var(--border-color);
+}
 #app {
   top: 0;
   bottom: 0;
@@ -97,7 +133,7 @@ svg.icon path {
   flex-direction: row;
   gap: 10px;
   margin: 10px 0 0 0;
-  border-bottom: solid 1px black;
+  border-bottom: solid 1px var(--border-color);
   height: 30px;
 }
 .tabBar>select {
@@ -105,17 +141,18 @@ svg.icon path {
 }
 .tab {
   padding: 4px;
-  border: solid 1px transparent;
+  border-bottom: solid 2px transparent;
+  color: var(--tab-text-color);
 }
 .tab.selected {
-  border: solid 1px black;
-  border-bottom: 0px
+  border-bottom: solid 2px var(--tab-select-color);
+  color: var(--text-color);
 }
 .tabBody {
-  overflow: auto;
   flex: 1 1;
+  height: 0; /* min height */
 }
-#result, #javascript {
+#result {
   font-family: 'Comic Code', monospace;
   font-size: 12px;
   white-space: pre;

prim.ss

@@ -0,0 +1,88 @@
+; (define $IORes (lambda (nm-1 nm-2) (vector 0 #f nm-1 nm-2)))
+(define $IORes (lambda (nm-1 nm-2) (cons nm-1 nm-2)))
+(define ($Left x) (vector 0 x))
+(define ($Right x) (vector 1 x))
+(define $LT 0)
+(define $EQ 1)
+(define $GT 2)
+(define (Prelude.addString a b) (string-append a b))
+(define (Prelude.addInt a b) (+ a b))
+(define (Prelude.ltInt a b) (< a b))
+(define (Prelude.eqInt a b) (= a b))
+(define (Prelude.ltChar a b) (char<? a b))
+(define (Prelude.eqChar a b) (char=? a b))
+(define (Prelude.ltString a b) (string<? a b))
+(define (Prelude.eqString a b) (string=? a b))
+(define Prelude.showInt number->string)
+(define (Prelude.primPutStrLn msg)
+  (lambda (w)
+    (display msg)
+    (newline)
+    ($IORes #f w)))
+(define Prelude.chr integer->char)
+(define Prelude.ord char->integer)
+(define (Prelude.intToNat x) x)
+(define (Prelude.natToInt x) x)
+(define (Prelude.slen s) (string-length s))
+(define (Prelude.debugStr _ x) (format #f "~s" x))
+;; REVIEW if this works for all of the cases that it is used for
+;; maybe they should all go away for specific instances
+(define (Prelude.jsShow x) (format #f "~s" x))
+(define (Node.putStr s)  (lambda (w) (display s) ($IORes #f w)))
+(define (Prelude.mod x y) (mod x y))
+;; REVIEW returns #f for failure
+(define Prelude.stringToInt string->number)
+
+(define (Prelude.unpack str) (string->list str))
+(define (Prelude.pack cs) (list->string cs))
+(define (Prelude.fastConcat strings) (apply string-append strings))
+
+(define (Prelude.isPrefixOf pfx str)
+        (string=? pfx (substring str 0 (string-length pfx))))
+;; Only used by getArgs(define Prelude.arrayToList #f)
+;; fastConcat uses it in js
+(define Prelude.listToArray #f)
+(define (Node.readFile fn)
+  (lambda (w)
+          (guard (x [else ($IORes ($Left (if (condition? x)
+                                             ; (condition-message x)
+                                             (with-output-to-string (lambda() (display-condition x)))
+                                             "Error")) w)])
+          ($IORes ($Right (call-with-input-file fn get-string-all)) w))))
+(define (Node.writeFile fn content)
+  (lambda (w)
+    (guard (x [else ($IORes ($Left (if (condition? x)
+                                       ; (condition-message x)
+                                       (with-output-to-string (lambda() (display-condition x)))
+                                       "Error")) w)])
+      (with-output-to-file fn
+        (lambda () (display content))
+        'replace)
+      ($IORes ($Right #f) w))))
+(define Prelude.strIndex string-ref)
+(define (Data.IORef.primNewIORef _ a) (lambda (w) ($IORes (box a) w)))
+(define (Data.IORef.primReadIORef _ ref) (lambda (w) ($IORes (unbox ref) w)))
+;; Actually should return unit..
+(define (Data.IORef.primWriteIORef _ ref a) (lambda (w) ($IORes (set-box! ref a) w)))
+(define (Node.readLine w)
+  (case (get-line (current-input-port))
+        (#!eof ($IORes ($Left "EOF") w))
+        (else ($IORes ($Right (get-line (current-input-port))) w))))
+(define (Prelude.subInt a b) (- a b))
+(define (Prelude.jsEq _ a b) (= a b))
+(define (Prelude.divInt a b) (fx/ a b))
+;; In node this throws and the next one exits cleanly
+(define (Prelude.fatalError _ msg) (raise (error #f msg)))
+(define (Node.exitFailure _ msg)
+  (display msg)
+  (newline)
+  (exit 1))
+(define (Prelude.isSuffixOf sfx s)
+  (let ((n (string-length sfx))
+        (m (string-length s)))
+    (if (<= n m)
+        (string=? sfx (substring s (- m n) m))
+        #f)))
+(define (Node.getArgs w) ($IORes (command-line) w))
+(define (Prelude.unsafePerformIO a f)
+  (car (f 'world)))

scripts/aoc

@@ -1,7 +1,8 @@
 #!/bin/sh
 mkdir -p tmp
 echo "Test AoC 2024 solutions"
-NCC="bun run newt.js"
+# FIXME - it turns out there are some stack issues here (including length)
+NCC="bun run build/newt.js"
 total=0
 failed=0
 for fn in  aoc2024/Day*.newt; do

scripts/aoc25

@@ -0,0 +1,36 @@
+#!/bin/sh
+mkdir -p tmp
+echo "Test AoC 2025 solutions"
+NCC="node build/newt.js"
+total=0
+failed=0
+for fn in  aoc2025/Day*.newt; do
+  total=$((total + 1))
+  echo Test $fn
+  bn=$(basename $fn)
+  $NCC $fn -o out.js > tmp/${bn}.compile
+  if [ $? != "0" ]; then
+    echo Compile failed for $fn
+    failed=$((failed + 1))
+    continue
+  fi
+  # if there is a golden file, run the code and compare output
+  if [ -f ${fn}.golden ]; then
+    node out.js > tmp/${bn}.out
+    if [ $? != "0" ]; then
+      echo Run failed for $fn
+      failed=$((failed + 1))
+      continue
+    fi
+    if ! diff -q tmp/${bn}.out ${fn}.golden; then
+      echo "Output mismatch for $fn"
+      failed=$((failed + 1))
+      if [ "$1" = "--fix" ]; then
+        cp tmp/${bn}.out ${fn}.golden
+      fi
+    fi
+  fi
+done
+
+echo "Total tests: $total"
+echo "Failed tests: $failed"

scripts/compile-chez.ss

@@ -0,0 +1 @@
+(parameterize ([optimize-level 3]) (compile-program "build/newt.ss"))

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"

scripts/mkrevision

@@ -0,0 +1,12 @@
+#!/bin/sh -e
+REV=$(git rev-parse --short HEAD)
+cat >> src/Revision.newt.new <<EOF
+module Revision
+
+import Prelude
+
+gitRevision : String
+gitRevision = "$REV"
+EOF
+cmp src/Revision.newt.new src/Revision.newt || cp src/Revision.newt.new src/Revision.newt
+rm -f src/Revision.newt.new

scripts/stats.py

@@ -5,7 +5,7 @@ stats = {}
 acc = ''
 name = ''
 for line in open(fn):
-    if line.startswith('const'):
+    if line.startswith('const') or line.startswith('let'):
         if name: stats[name] = len(acc)
         acc = line
         name = line.split()[1]

scripts/test

@@ -1,7 +1,10 @@
 #!/bin/sh
 SAMPLES=$(find playground/samples -name "*.newt")
-# NCC="bun run newt.js"
-NCC="node newt.js"
+# NEWT ="bun run build/newt.js"
+NEWT=${NEWT:="node build/newt.js"}
+OUTFILE=${OUTFILE:="tmp/out.js"}
+RUNOUT=${RUNOUT:="node"}
+mkdir -p tmp
 total=0
 failed=0
 for fn in tests/*.newt ; do
@@ -9,10 +12,10 @@ for fn in tests/*.newt ; do
   echo Test $fn
   bn=$(basename $fn)
   if [ -f ${fn}.golden ]; then
-    $NCC $fn -o out.js > tmp/${bn}.compile
+    $NEWT $fn -o $OUTFILE > tmp/${bn}.compile
   else
     # we've dropped support for compiling things without main for now.
-    $NCC $fn > tmp/${bn}.compile
+    $NEWT $fn > tmp/${bn}.compile
   fi
   cerr=$?
   if [ -f ${fn}.fail ]; then
@@ -20,17 +23,21 @@ for fn in tests/*.newt ; do
         echo "Compile failure mismatch for $fn"
         diff ${fn}.fail tmp/${bn}.compile
         failed=$((failed + 1))
+        if [ x$1 = "x--fix" ]; then
+          cp tmp/${bn}.compile ${fn}.fail
+        fi
         continue
     fi
   elif [ $cerr != "0" ]; then
     echo Compile failed for $fn
     failed=$((failed + 1))
     cat tmp/${bn}.compile
+
     continue
   fi
   # if there is a golden file, run the code and compare output
   if [ -f ${fn}.golden ]; then
-    bun run out.js > tmp/${bn}.out
+    $RUNOUT $OUTFILE > tmp/${bn}.out
     if [ $? != "0" ]; then
       echo Run failed for $fn
       failed=$((failed + 1))
@@ -40,6 +47,9 @@ for fn in tests/*.newt ; do
       echo "Output mismatch for $fn"
       diff ${fn}.golden tmp/${bn}.out
       failed=$((failed + 1))
+      if [ x$1 = "x--fix" ]; then
+        cp tmp/${bn}.out ${fn}.golden
+      fi
     fi
   fi
 done

serializer.ts

@@ -1,269 +0,0 @@
-// Experimental serializer / deserializer for modules
-// not completely wired in yet, serialization is running, deserialization is not
-
-const END = 0;
-const LIST = 1;
-const TUPLE = 2;
-const INDUCT = 3;
-const STRING = 4;
-const NUMBER = 5;
-const NULL = 6;
-const TRUE = 7;
-const FALSE = 8;
-const te = new TextEncoder();
-
-class DeserializationStream {
-  pos = 0;
-  buf: Uint8Array;
-
-  constructor(buf: Uint8Array) {
-    this.buf = buf;
-  }
-
-  readByte() {
-    return this.buf[this.pos++];
-  }
-
-  readVarint() {
-    let shift = 0;
-    let result = 0;
-    while (true) {
-      const byte = this.readByte();
-      result |= (byte & 0x7f) << shift;
-      if ((byte & 0x80) === 0) break;
-      shift += 7;
-    }
-    return result;
-  }
-
-  readSignedVarint() {
-    const n = this.readVarint();
-    return (n >>> 1) ^ -(n & 1);
-  }
-
-  readString() {
-    const length = this.readVarint();
-    const bytes = this.buf.slice(this.pos, this.pos + length);
-    this.pos += length;
-    return new TextDecoder().decode(bytes);
-  }
-}
-
-export class DecFile {
-  pool: string[] = [""];
-  buf: DeserializationStream;
-  static decode(encoded: Uint8Array) {
-    return new DecFile(encoded).read()
-  }
-  constructor(data: Uint8Array) {
-    this.buf = new DeserializationStream(data);
-    this.readPool();
-  }
-
-  readPool() {
-    while (true) {
-      let str = this.buf.readString();
-      if (!str.length) break
-      this.pool.push(str);
-    }
-  }
-
-  read(): any {
-    const type = this.buf.readByte();
-    switch (type) {
-      case NULL:
-        return null;
-      case LIST: {
-        const list: any[] = [];
-        while (this.buf.buf[this.buf.pos] !== END) {
-          list.push(this.read());
-        }
-        this.buf.pos++;
-        let rval: any = { tag: "Nil", 'h0': null };
-        while (list.length)
-          rval = { tag: "_::_", h0: null, h1: list.pop(), h2: rval };
-        return rval;
-      }
-      case TUPLE: {
-        const tuple: any[] = [];
-        while (this.buf.buf[this.buf.pos] !== END) {
-          tuple.push(this.read());
-        }
-        this.buf.pos++;
-        let rval: any = tuple.pop();
-        while (tuple.length)
-          rval = { tag: "_,_", h0: null, h1: null, h2: tuple.pop(), h3: rval };
-        return rval;
-      }
-      case STRING:
-        return this.pool[this.buf.readVarint()];
-      case NUMBER:
-        return this.buf.readSignedVarint();
-      case INDUCT:
-        const tag = this.buf.readVarint()
-        const obj: any = { tag };
-        let i = 0;
-        while (this.buf.buf[this.buf.pos] !== END) {
-          obj[`h${i++}`] = this.read();
-        }
-        this.buf.pos++;
-        return obj;
-      case TRUE:
-        return true;
-      case FALSE:
-        return false;
-      default:
-        debugger
-        throw new Error(`Unknown type: ${type}`);
-    }
-  }
-}
-
-class SerializationStream {
-  pos = 0;
-  buf = new Uint8Array(1024 * 1024);
-
-  ensure(size: number) {
-    if (this.buf.length - this.pos < size) {
-      const tmp = new Uint8Array(this.buf.length * 1.5);
-      tmp.set(this.buf);
-      this.buf = tmp;
-    }
-  }
-
-  writeByte(n: number) {
-    this.ensure(1);
-    this.buf[this.pos++] = n % 256;
-  }
-
-  writeVarint(n: number) {
-    while (n > 127) {
-      this.writeByte((n & 0x7f) | 0x80);
-      n >>= 7;
-    }
-    this.writeByte(n & 0x7f);
-  }
-
-  writeSignedVarint(n: number) {
-    const zigzag = (n << 1) ^ (n >> 31);
-    this.writeVarint(zigzag);
-  }
-
-  writeString(s: string) {
-    let data = te.encode(s);
-    this.ensure(data.byteLength + 4);
-    this.writeVarint(data.byteLength);
-    this.buf.set(data, this.pos);
-    this.pos += data.byteLength;
-  }
-  toUint8Array() {
-    return this.buf.slice(0, this.pos);
-  }
-}
-
-export class EncFile {
-  poollen = 1;
-  pool = new SerializationStream();
-  buf = new SerializationStream();
-  pmap: Map<string, number> = new Map();
-
-  constructor() {
-    this.pmap.set("",0);
-  }
-  static encode(data: any) {
-    let f = new EncFile()
-    f.write(data)
-    f.pool.writeVarint(0)
-    return f.toUint8Array()
-  }
-
-  writeString(s: string) {
-    let n = this.pmap.get(s);
-    if (n === undefined) {
-      n = this.poollen++;
-      this.pool.writeString(s);
-      this.pmap.set(s,n);
-    }
-    this.buf.writeVarint(n);
-  }
-
-  write(a: any) {
-    // shouldn't happen?
-    if (a == null) {
-      this.buf.writeByte(NULL);
-    } else if (a.tag == "_::_") {
-      this.buf.writeByte(LIST);
-      for (; a.tag === "_::_"; a = a.h2) {
-        this.write(a.h1);
-      }
-      this.buf.writeByte(END);
-    } else if (a.tag == "_,_") {
-      this.buf.writeByte(TUPLE);
-      for (; a.tag === "_,_"; a = a.h3) {
-        this.write(a.h2);
-      }
-      this.write(a);
-      this.buf.writeByte(END);
-    } else if (typeof a === "string") {
-      this.buf.writeByte(STRING);
-      this.writeString(a);
-    } else if (typeof a === "number") {
-      this.buf.writeByte(NUMBER);
-      this.buf.writeSignedVarint(a);
-    } else if (a === true) {
-      this.buf.writeByte(TRUE);
-    } else if (a === false) {
-      this.buf.writeByte(FALSE);
-    } else if (a.tag !== undefined) {
-      this.buf.writeByte(INDUCT);
-      this.buf.writeVarint(a.tag);
-      // Sometimes keys are skipped
-      let end = 0
-      for (let k in a) {
-        if (k[0] == 'h') end = Math.max(end, +k.slice(1))
-      }
-      for (let i = 0; i <= end; i++) {
-        let key = 'h' + i
-        let v = a[key] ?? null
-        this.write(v);
-      }
-    this.buf.writeByte(END);
-    } else {
-      throw new Error(`handle ${typeof a} ${a} ${Object.keys(a)}`);
-    }
-  }
-  toUint8Array() {
-    const poolArray = this.pool.toUint8Array();
-    const bufArray = this.buf.toUint8Array();
-    const rval = new Uint8Array(poolArray.length + bufArray.length);
-    rval.set(poolArray);
-    rval.set(bufArray, poolArray.length);
-    return rval;
-  }
-}
-
-// This was for testing
-function deepEqual(a: any, b: any): boolean {
-  if (a === b) return true;
-  if (typeof a !== typeof b) return false;
-  if (a == null || b == null) return false;
-  if (typeof a !== "object") return false;
-
-  if (Array.isArray(a)) {
-    if (!Array.isArray(b) || a.length !== b.length) return false;
-    for (let i = 0; i < a.length; i++) {
-      if (!deepEqual(a[i], b[i])) return false;
-    }
-    return true;
-  }
-
-  const keysA = Object.keys(a);
-  const keysB = Object.keys(b);
-  if (keysA.length !== keysB.length) return false;
-
-  for (const key of keysA) {
-    if (!deepEqual(a[key], b[key])) return false;
-  }
-
-  return true;
-}

src/Commands.newt

@@ -0,0 +1,299 @@
+-- For shared code between REPL and LSP
+module Commands
+
+import Prelude
+import Lib.ProcessModule
+import Lib.Types
+import Lib.TopContext
+import Lib.Common
+import Data.List1
+import Lib.Tokenizer
+import Lib.Token
+import Lib.Elab
+import Data.String
+import Lib.Eval
+import Data.SortedMap
+import Lib.Parser
+import Lib.Syntax
+import Lib.Parser.Impl
+import Lib.Error
+
+-- For now we cheat and assume capitalized directories are a module component
+decomposeName : String → String × String
+decomposeName fn =
+    go Nil $ Lin <>< split (fst $ splitFileName fn) "/"
+    where
+        go : List String → SnocList String → String × String
+        go acc Lin = (".", joinBy "." acc)
+        go acc (xs :< x) = if isUpper $ strIndex x 0
+            then go (x :: acc) xs
+            else (joinBy "/" (xs :< x <>> Nil), joinBy "." acc)
+
+switchModule : FileSource → String → M (Maybe ModContext)
+switchModule repo modns = do
+    -- TODO processing on hover is expensive, but info is not always there
+    -- I suspect this picks up the case where a file has been invalidated by a change to
+    -- another file and we switch editors. Handle that (enqueue a check) and switch this back.
+    -- this is also broken, because diagnostics don't get updated..
+    top <- getTop
+    -- mod <- processModule emptyFC repo Nil modns
+    let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
+    modifyTop { currentMod := mod; ops := mod.modOps }
+    pure $ Just mod
+
+data HoverInfo = NoHoverInfo | NeedCheck | HasHover FC String
+
+-- The cheap version of type at point, find the token, lookup in global context
+-- Later we will either get good FC for entries or scan them all and build a cache.
+getHoverInfo : FileSource → String → Int → Int → M HoverInfo
+getHoverInfo repo modns row col = do
+    Just mod <- switchModule repo modns | _ => pure NeedCheck
+    top <- getTop
+
+    -- Find the token at the point
+    let lines = split mod.modSource "\n"
+    let line = fromMaybe "" (getAt' row lines)
+    let (Right toks) = tokenise "" line | Left _ => pure NoHoverInfo
+    let (Just name) = getTok toks       | _ => pure NoHoverInfo
+
+    let (Left _) = partialParse "" parseImport emptyMap toks
+      | Right ((MkImport _ (fc, nm)), _, _) => do
+        let (baseDir, _) = splitFileName fc.file
+        let fc = MkFC ("\{repo.baseDir}/\{joinBy "/" (split nm ".")}.newt") (MkBounds 0 0 0 0)
+        pure $ HasHover fc "module \{nm}"
+    putStrLn "Hover name is \{show name}"
+    -- Lookup the name
+    let (Just e) = lookupRaw name top   | _ => pure NoHoverInfo
+    ty <- nf Nil e.type
+    pure $ HasHover e.fc ("\{show e.name} : \{rpprint Nil ty}")
+
+    where
+        -- We don't want to pick up the paren token when on the border
+        isIdent : BTok → Bool
+        isIdent (MkBounded (Tok Ident _) _) = True
+        isIdent (MkBounded (Tok UIdent _) _) = True
+        isIdent (MkBounded (Tok MixFix _) _) = True
+        isIdent (MkBounded (Tok Projection _) _) = True
+        isIdent _ = False
+
+        getTok : List BTok → Maybe String
+        getTok Nil = Nothing
+        getTok (tok :: toks) =
+            if tok.bounds.startCol <= col && col <= tok.bounds.endCol && isIdent tok
+            then Just $ value tok else getTok toks
+
+data FileEdit = MkEdit FC String
+data CodeAction
+  = CaseSplitAction (List FileEdit)
+  | AddMissingAction (List FileEdit)
+  | Intro String FileEdit
+  | ImportAction String FileEdit
+
+
+applyDCon : QName × Int × Tm → List String
+applyDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
+  where
+    go : SnocList String → Tm → List String
+    go acc (Pi _ nm Explicit _ _ u) = go (acc :< nm) u
+    go acc (Pi _ _ _ _ _ u) = go acc u
+    go acc _ = acc <>> Nil
+
+data Flavor = EqSplit | FatArrowSplit | MonadSplit
+
+-- Not quite right, we also need to check for let...
+-- But it's a first pass
+splitEquals : SnocList Char → List Char → (Flavor × String × String)
+splitEquals acc Nil = (EqSplit, pack (acc <>> Nil), "")
+splitEquals acc xs@('=' :: '>' :: _) = (FatArrowSplit, pack (acc <>> Nil), pack xs)
+splitEquals acc xs@('=' :: _) = (EqSplit, pack (acc <>> Nil), pack xs)
+splitEquals acc xs@('<' :: '-' :: _) = (MonadSplit, pack (acc <>> Nil), pack xs)
+splitEquals acc (x :: xs) = splitEquals (acc :< x) xs
+
+needParens : SnocList Char → List Char → Bool
+needParens (xs :< ' ') ys = needParens xs ys
+needParens xs (' ' :: ys) = needParens xs ys
+needParens (xs :< '(') (')' :: ys) = False
+needParens _ _ = True
+
+addParens : Bool → List String → String
+addParens _ (x :: Nil) = x
+addParens False s = unwords s
+addParens True s = "(\{unwords s})"
+
+-- resugar operator applications
+-- assumes the components are simple identifiers
+resugarOper : List String → List String
+resugarOper Nil = Nil
+resugarOper (x :: xs) = go Lin (split x "_") xs
+  where
+    go : SnocList String → List String → List String → List String
+    go acc Nil xs = acc <>> xs
+    go acc ("" :: rest) (x :: xs) = go (acc :< x) rest xs
+    -- If there are not enough parts, bail and fall back to `_+_ x`
+    go acc ("" :: rest) Nil = (x :: xs)
+    go acc (x :: xs) ys = go (acc :< x) xs ys
+
+-- REVIEW - maybe pass in QName and use applyDCon in here, especially if we want to get better names?
+makeEdits : FC → List QName → Bool → M (List FileEdit)
+makeEdits fc@(MkFC uri (MkBounds sr sc er ec)) names inPlace = do
+  cons <- map applyDCon <$> traverse lookupDCon names
+  top <- getTop
+  let (Just mod) = lookupMap' top.currentMod.modName top.modules | _ => pure Nil
+  let lines = split mod.modSource "\n"
+  let (Just line) = getAt' sr lines | _ => pure Nil
+  let cs = unpack line
+  let head = take (cast sc) cs
+  let tail = drop (S $ cast (ec - 1)) cs
+  let (splitKind, before, after) = splitEquals Lin tail
+  let np = needParens (Lin <>< head) tail
+  let cons = map (addParens np ∘ resugarOper) cons
+  let phead = pack head
+  let indent = getIndent 0 head
+  let nextrow = scan indent lines (sr + 1)
+  -- FIXME - doesn't handle `let`, but that's a little messy
+  -- need to remove let and add `|`, but also indent.
+  -- Existing `|` would have their own indent, indent of let matters. etc.
+  -- No init or first :: rest for add missing case
+  let (edits, rest) = doFirst inPlace cons
+
+  let phead = pack head
+  let fc' = MkFC uri (MkBounds nextrow 0 nextrow 0)
+  let srest =
+    case splitKind of
+      EqSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "= ?\n") rest
+      FatArrowSplit => joinBy "" $ map (\ap => phead ++ ap ++ before ++ "=> ?\n") rest
+      MonadSplit => joinBy "" $ map (\ap => "  | \{pack head}\{ap}\{before}=> ?\n") rest
+
+  putStrLn "Split \{show line} HD '\{show head}' TL '\{show tail}'"
+  putStrLn srest
+  let edits = MkEdit fc' (srest) :: edits
+  putStrLn "edits \{debugStr edits}"
+  pure edits
+  where
+    getIndent : Int → List Char → Int
+    getIndent acc (' ' :: rest) = getIndent (1 + acc) rest
+    getIndent acc _ = acc
+
+    scan : Int → List String → Int → Int
+    scan indent lines row =
+      let x = getIndent 0 $ unpack $ fromMaybe "" $ getAt' row lines in
+      if x <= indent then row else scan indent lines (row + 1)
+
+    doFirst : Bool → List String → (List FileEdit × List String)
+    doFirst True (first :: rest) = (MkEdit fc first :: Nil, rest)
+    doFirst _ cons = (Nil, cons)
+
+addMissingCases : Int → Int → FC → Context → List QName → M (Maybe CodeAction)
+addMissingCases _ _ fc@(MkFC uri (MkBounds sr sc er ec)) ctx names = do
+  top <- getTop
+  edits <- makeEdits fc names False
+  putStrLn "Add Missing \{show fc} \{show names}"
+  pure $ Just $ AddMissingAction edits
+
+getCaseSplit : Int → Int → FC → Context → String → Val → M (Maybe CodeAction)
+getCaseSplit row col fc@(MkFC uri (MkBounds sr sc er ec)) ctx nm scty = do
+  top <- getTop
+  -- It's getting vars for the type
+  scty <- unlet ctx.env scty
+  cons <- getConstructors ctx fc scty
+  ty <- quote (length' ctx.env) scty
+  cons <- filterM (checkCase ctx nm scty) cons
+  let names = map fst cons
+  putStrLn "Make splits for \{show names}"
+  edits <- makeEdits fc names True
+  -- TODO if constructor is not in scope, add import too.
+  pure $ Just $ CaseSplitAction edits
+
+posInFC : Int → Int → FC → Bool
+posInFC row col (MkFC _ (MkBounds 0 0 0 0)) = False
+posInFC row col (MkFC _ (MkBounds sr sc er ec)) = (sr <= row && row <= er) && (sc <= col && col <= ec)
+
+getHole : ModContext → Int → Int → Maybe MetaEntry
+getHole mod row col =
+  find isUserMeta $ listValues mod.modMetaCtx.metas
+  where
+    isUserMeta : MetaEntry → Bool
+    isUserMeta (Unsolved fc _ _ _ User _) = posInFC row col fc
+    isUserMeta _ = False
+
+introActions : Maybe MetaEntry → M (List CodeAction)
+introActions (Just $ Unsolved fc qn ctx vty User constraints) =
+  catchError (do
+    -- Are there ever any constraints?
+    top <- getTop
+    vty <- forceMeta vty
+    putStrLn "intros for \{show vty}"
+    case vty of
+      VPi _ nm Explicit _ a b => do
+        let str = "(\\ \{nm} => ?)"
+        pure $ Intro str (MkEdit fc str) :: Nil
+      _ => do
+        -- Prelude.Nat not a vref?
+        -- also need to handle pi types
+        cons <- getConstructors ctx fc vty
+        putStrLn "constructors \{show cons}"
+        pure $ map makeEdit cons
+  ) $ \ err => do
+      putStrLn "Got error in introActions:"
+      putStrLn $ showError "" err
+      pure Nil
+  where
+    introDCon : QName × Int × Tm → List String
+    introDCon (QN _ nm, _, tm) = go (Lin :< nm) tm
+      where
+        go : SnocList String → Tm → List String
+        go acc (Pi _ nm Explicit _ _ u) = go (acc :< "?") u
+        go acc (Pi _ _ _ _ _ u) = go acc u
+        go acc _ = acc <>> Nil
+
+    makeEdit : (QName × Int × Tm) → CodeAction
+    makeEdit con@(QN _ nm, _, _) =
+      let str = addParens True $ resugarOper $ introDCon con
+      in Intro str $ MkEdit fc $ str
+
+introActions _ = pure Nil
+
+errorActions : Int → Int → Error → M (List CodeAction)
+errorActions row col err = do
+  let (ENotInScope fc nm) = err | _ => pure Nil
+  let (True) = posInFC row col fc | _ => pure Nil
+  top <- getTop
+  let mods = map (\e => e.name.qns) $ lookupAll nm top
+  case mods of
+    Nil => pure Nil
+    _ => do
+      top <- getTop
+      let row = getInsertRow 0 1 $ split top.currentMod.modSource "\n"
+      let fc = MkFC fc.file (MkBounds row 0 row 0)
+      pure $ map (\nm => ImportAction nm (MkEdit fc "import \{nm}\n")) mods
+  where
+    getInsertRow : Int → Int → List String → Int
+    getInsertRow row cur Nil = row
+    getInsertRow row cur (l :: ls) =
+      let row =  ite (isPrefixOf "module" l || isPrefixOf "import" l) cur row
+      in getInsertRow row (cur + 1) ls
+
+getActions : FileSource → String → Int → Int → M (List CodeAction)
+getActions repo modns row col = do
+  Just mod <- switchModule repo modns | _ => pure Nil
+  top <- getTop
+  let infos = filter (posInFC row col ∘ getFC) top.currentMod.modInfos
+  putStrLn "Filter got \{show $ length' infos}"
+  actions <- go Nil $ infos
+  let hole = getHole mod row col
+  putStrLn "Hole \{debugStr hole}"
+  intros <- introActions $ getHole mod row col
+  eactions <- join <$> traverse (errorActions row col) mod.modErrors
+  pure $ actions ++ intros ++ eactions
+  where
+    getAction : EditorInfo → M (Maybe CodeAction)
+    getAction (CaseSplit fc ctx nm scty) = getCaseSplit row col fc ctx nm scty
+    getAction (MissingCases fc ctx names) = addMissingCases row col fc ctx names
+
+    go : List CodeAction → List EditorInfo → M (List CodeAction)
+    go acc Nil = pure acc
+    go acc (x :: xs) = do
+      Right (Just res) <- tryError $ getAction x
+        | _ => go acc xs
+      go (res :: acc) xs
+