First pass at a scheme backend

.editorconfig

@@ -4,5 +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

@@ -13,6 +13,8 @@ mkday.py
 tmp
 min.js.gz
 src/Revision.newt
+newt.ss
+newt.so
 .calva
 .clj-kondo
 .joyride

.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

@@ -9,11 +9,8 @@ RUNJS=node
 all: newt.js
 
 
-REV=$(shell git rev-parse --short HEAD)
 src/Revision.newt: .PHONY
-	echo "module Revision\nimport Prelude\ngitRevision : String\ngitRevision = \"${REV}\"" > src/Revision.newt.new
+	sh ./scripts/mkrevision
-	cmp src/Revision.newt.new src/Revision.newt || cp src/Revision.newt.new src/Revision.newt
-	rm -f src/Revision.newt.new
 
 newt.js: ${SRCS} src/Revision.newt
 	$(RUNJS) bootstrap/newt.js src/Main.newt -o newt.js
@@ -25,6 +22,12 @@ newt3.js: newt2.js
 	time $(RUNJS) newt2.js src/Main.newt -o newt3.js
 	cmp newt2.js newt3.js
 
+newt.ss: newt.js
+	$(RUNJS) newt.js src/Main.newt -o newt.ss
+
+newt.so: newt.ss
+	chez --script scripts/compile-chez.ss
+
 test: newt.js
 	scripts/test
 
@@ -35,11 +38,11 @@ aoctest: newt.js
 # Misc
 
 # build / install old vscode extension
-vscode:
+# vscode:
-	cd newt-vscode && vsce package && code --install-extension *.vsix
+	# cd newt-vscode && vsce package && code --install-extension *.vsix
 
 # build / install new LSP vscode extension
-vscode-lsp:
+vscode-lsp vscode: lsp
 	cd newt-vscode-lsp && vsce package && code --install-extension *.vsix
 
 playground: .PHONY
@@ -68,6 +71,7 @@ playground/src/newt.js: 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 $@
 
 lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js
 

TODO.md

@@ -1,14 +1,24 @@
 
 ## TODO
 
-- [ ] Use looping for TCO
+- [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
@@ -24,7 +34,7 @@
   - [ ] 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?
+- [ ] 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.

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`
+

newt-vscode-lsp/esbuild.js

@@ -35,6 +35,9 @@ async function main() {
 		sourcemap: !production,
 		sourcesContent: false,
 		platform: 'node',
+		banner: {
+			js: "#!/usr/bin/env node",
+		},
 		// outfile: 'dist/extension.js',
 		outdir: 'dist',
 		external: ['vscode'],

newt-vscode-lsp/src/lsp.ts

@@ -1,11 +1,9 @@
 /**
- * WIP
- *
  * 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 } from './newt.js'
+import { LSP_checkFile, LSP_updateFile, LSP_hoverInfo, LSP_codeActionInfo, LSP_docSymbols } from './newt.js'
 
 import {
   createConnection,
@@ -118,12 +116,25 @@ connection.onCodeAction(({textDocument, range}) => {
   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,
   },
 }));
 

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

@@ -1,4 +1,4 @@
-import { CodeAction, Diagnostic, Location } from "vscode-languageserver";
+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[];
@@ -8,3 +8,5 @@ interface HoverResult {
 }
 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;
+

playground/samples/DSL.newt

@@ -20,15 +20,15 @@ Z * m = Z
 
 infixr 4 _::_
 data Vec : U → Nat → U where
-  Nil : {a} → Vec a Z
+  Nil : ∀ a. Vec a Z
-  _::_ : {a k} → a → Vec a k → Vec a (S k)
+  _::_ : ∀ 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
 
@@ -57,12 +57,12 @@ data Unit : U where
   MkUnit : Unit
 
 data Either : U -> U -> U where
-  Left : {A B} → A → Either A B
+  Left : ∀ a b. a → Either a b
-  Right : {A B} → B → 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
@@ -85,11 +85,11 @@ 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
 
@@ -111,8 +111,8 @@ test4 = enumerate four
 -- for now, I'll define ≡ to check
 
 infixl 2 _≡_
-data _≡_ : {A} → A → A → U where
+data _≡_ : ∀ a. a → a → U where
-  Refl : {A} {a : A} → a ≡ a
+  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/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
+  inl : ∀ a b. a -> a + b
-  inr : {A B} -> B -> 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
+  leaf : ∀ l u. (lu : l <<= u) -> T23 l u Z
-  node2 : {l u h} (x : _)
+  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
 

prim.ss

@@ -0,0 +1,97 @@
+;; REVIEW all of this - some of it is IO and needs the IO dance
+;; maybe we make a helper? A macro?
+
+(define $Nil (lambda (nm-0) (vector 0 nm-0)))
+(define $Cons (lambda (nm-0 nm-1 nm-2) (vector 1 nm-0 nm-1 nm-2)))
+(define $IORes (lambda (nm-1 nm-2) (vector 0 #f nm-1 nm-2)))
+(define ($Left x) (vector 0 #f #f x))
+(define ($Right x) (vector 1 #f #f 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 (Node.exitFailure _ msg) (raise msg))
+(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)
+
+;; coerce scheme list to newt
+(define (list->List xs)
+  (define (go acc xs)
+    (if (null? xs) acc
+        (go ($Cons #f (car xs) acc) (cdr xs))))
+  (go ($Nil #f) (reverse xs)))
+
+(define (List->list xs)
+  (define (go acc xs)
+    (if (= 0 (vector-ref xs 0)) (reverse acc)
+        (go (cons (vector-ref xs 2) acc) (vector-ref xs 3))))
+  (go '() xs))
+
+(define (Prelude.unpack str) (list->List (string->list str)))
+(define (Prelude.pack cs) (list->string (List->list cs)))
+(define (Prelude.fastConcat strings) (apply string-append (List->list 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)
+  ($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))
+(define (Prelude.fatalError _ msg) (raise msg))
+(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 (list->List (command-line)) w))

scripts/aoc25

@@ -25,7 +25,7 @@ for fn in  aoc2025/Day*.newt; do
     if ! diff -q tmp/${bn}.out ${fn}.golden; then
       echo "Output mismatch for $fn"
       failed=$((failed + 1))
-      if [ $1 = "--fix" ]; then
+      if [ "$1" = "--fix" ]; then
         cp tmp/${bn}.out ${fn}.golden
       fi
     fi

scripts/compile-chez.ss

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

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

src/Data/List1.newt

@@ -9,8 +9,8 @@ record List1 a where
   head1 : a
   tail1 : List a
 
-split1 : String → String → List1 String
+splitBy1 : String → Char → List1 String
-split1 str by = case split str by of
+splitBy1 str by = case splitBy str by of
   Nil => str ::: Nil
   x :: xs => x ::: xs
 
@@ -22,6 +22,6 @@ unsnoc {a} (x ::: xs) = go x xs
     go x (y :: ys) = let (as, a) = go y ys in (x :: as, a)
 
 splitFileName : String → String × String
-splitFileName fn = case split1 fn "." of
+splitFileName fn = case splitBy1 fn '.' of
     part ::: Nil => (part, "")
     xs => mapFst (joinBy ".") $ unsnoc xs

src/Data/SnocList.newt

@@ -9,6 +9,13 @@ snoclen {a} xs = go xs Z
     go Lin acc = acc
     go (xs :< x) acc = go xs (S acc)
 
+snoclen' : ∀ a. SnocList a → Int
+snoclen' {a} xs = go xs 0
+  where
+    go : SnocList a → Int → Int
+    go Lin acc = acc
+    go (xs :< x) acc = go xs (1 + acc)
+
 snocelem : ∀ a. {{Eq a}} → a → SnocList a → Bool
 snocelem a Lin = False
 snocelem a (xs :< x) = if a == x then True else snocelem a xs

src/LSP.newt

@@ -16,7 +16,7 @@ import Commands
 import Lib.ProcessDecl
 import Lib.Prettier
 import Lib.Error
-import Lib.Compile
+import Lib.CompileJS
 
 pfunc js_castArray : Array JSObject → JSObject := `x => x`
 pfunc js_castInt : Int → JSObject := `x => x`
@@ -29,7 +29,6 @@ pfunc js_castObj : Array (String × JSObject) → JSObject := `(data) => {
     return rval
 }`
 
--- need case split
 jsonToJObject : Json → JSObject
 jsonToJObject (JsonInt x) = js_castInt x
 jsonToJObject (JsonNull) = js_null
@@ -173,6 +172,36 @@ errorToDiag err =
 -- These shouldn't escape
 errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg}"
 
+getSymbols : M (List Json)
+getSymbols = do
+  top <- getTop
+  let defs = listValues top.currentMod.modDefs
+  putStrLn "scan \{show $ length' defs} defs"
+  go Nil defs
+    where
+      getKind : Def → Int
+      getKind Axiom = 12
+      getKind (TCon _ _) = 23
+      getKind (DCon _ _ _ _) = 10
+      getKind (Fn _) = 12
+      getKind (PrimTCon _) = 23
+      getKind (PrimFn _ _ _) = 12
+      getKind (PrimOp _) = 12
+
+      -- highlight where hx!
+      go : List Json → List TopEntry → M (List Json)
+      go acc Nil = pure $ reverse acc
+      go acc ((MkEntry fc name type def eflags) :: rest) =
+        let range = fcToRange fc in
+        let kind = getKind def in
+        let diag = JsonObj
+              $  ("name" , JsonStr (name.baseName))
+              :: ("range", range)
+              :: ("selectionRange", range)
+              :: ("kind", JsonInt kind)
+              -- detail
+              :: Nil
+        in go (diag :: acc) rest
 
 getInfos : M (List Json)
 getInfos = do
@@ -225,6 +254,24 @@ checkFile fn = unsafePerformIO $ do
     modifyIORef state $ [ topContext := top ]
     pure $ jsonToJObject $ JsonArray json
 
+docSymbols : String → JSObject
+docSymbols fn = unsafePerformIO $ do
+    let (base, modName) = decomposeName fn
+    st <- readIORef state
+    putStrLn "Symbols for \{fn}"
+    if st.baseDir /= base
+        then resetState base
+        else pure MkUnit
+    repo <- lspFileSource
+    (Right (top, json)) <- (do
+        mod <- processModule emptyFC repo Nil modName
+        modifyTop [ currentMod := mod; ops := mod.modOps ]
+        getSymbols).runM st.topContext
+        | Left err => do
+           pure $ jsonToJObject $ JsonNull
+    modifyIORef state $ [ topContext := top ]
+    pure $ jsonToJObject $ JsonArray json
+
 compileJS : String → JSObject
 compileJS fn = unsafePerformIO $ do
   let (base, modName) = decomposeName fn
@@ -244,6 +291,4 @@ compileJS fn = unsafePerformIO $ do
   modifyIORef state [ topContext := top ]
   pure $ js_castStr src
 
-
+#export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols
-
-#export updateFile checkFile hoverInfo codeActionInfo compileJS

src/Lib/Common.newt

@@ -55,6 +55,12 @@ toHex : Int -> List Char
 toHex 0 = Nil
 toHex v = snoc (toHex (div v 16)) (hexDigit v)
 
+padding : Int → Char → String
+padding n ch = go n Nil
+  where
+    go : Int → List Char → String
+    go 0 chs = pack chs
+    go k chs = go (k - 1) (ch :: chs)
 
 quoteString : String -> String
 quoteString str = pack $ encode (unpack str) (Lin :<  '"')

src/Lib/CompileExp.newt

@@ -57,18 +57,6 @@ lamArity : Tm -> List Quant
 lamArity (Lam _ _ _ quant t) = quant :: (lamArity t)
 lamArity _ = Nil
 
--- It would be nice to be able to declare these
-compilePrimOp : String → List CExp → Maybe CExp
-compilePrimOp "Prelude.addString" (x :: y :: Nil) = Just (CPrimOp "+" x y)
-compilePrimOp "Prelude.addInt" (x :: y :: Nil) = Just (CPrimOp "+" x y)
-compilePrimOp "Prelude.mulInt" (x :: y :: Nil) = Just (CPrimOp "*" x y)
-compilePrimOp "Prelude.subInt" (x :: y :: Nil) = Just (CPrimOp "-" x y)
-compilePrimOp "Prelude._&&_" (x :: y :: Nil) = Just (CPrimOp "&&" x y)
-compilePrimOp "Prelude._||_" (x :: y :: Nil) = Just (CPrimOp "||" x y)
--- Assumes Bool is in the right order!
-compilePrimOp "Prelude.jsEq" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
-compilePrimOp "Prelude.divInt" (x :: y :: Nil) = Just (CPrimOp "|" (CPrimOp "/" x y) (CLit $ LInt 0))
-compilePrimOp _ _ = Nothing
 
 -- This is how much we want to curry at top level
 -- leading lambda Arity is used for function defs and metas
@@ -80,11 +68,11 @@ arityForName fc nm = do
     Nothing => error fc "Name \{show nm} not in scope"
     (Just Axiom) => pure Nil
     (Just (PrimOp _)) => pure $ Many :: Many :: Nil
-    (Just (TCon arity strs)) => pure $ replicate' (cast arity) Many
+    (Just (TCon arity strs)) => pure $ replicate (cast arity) Many
     (Just (DCon _ _ arity str)) => pure arity
     (Just (Fn t)) => pure $ lamArity t
-    (Just (PrimTCon arity)) => pure $ replicate' (cast arity) Many
+    (Just (PrimTCon arity)) => pure $ replicate (cast arity) Many
-    (Just (PrimFn t arity used)) => pure $ replicate' arity Many
+    (Just (PrimFn t arity used)) => pure $ replicate arity Many
   where
 
 
@@ -147,8 +135,6 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
         defs <- getRef Defs
         args' <- traverse compileTerm args
         arity <- arityForName fc nm
-        let (Nothing) = compilePrimOp (show nm) args'
-          | Just cexp => pure cexp
         case lookupMap' nm defs : Maybe Def of
           Just (DCon _ SuccCon _ _) => applySucc args'
           _ => apply nm args' arity
@@ -277,7 +263,7 @@ defToCExp (qn, (PrimOp _)) = (_,_ qn) <$> compilePop qn
 defToCExp (qn, DCon ix info arity _)   = pure (qn, compileDCon ix qn info arity)
 -- We're not using these are runtime at the moment, no typecase
 -- we need to sort out tag number if we do typecase
-defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many))
+defToCExp (qn, TCon arity conNames) = pure (qn, compileDCon Z qn NormalCon (replicate (cast arity) Many))
-defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate' (cast arity) Many))
+defToCExp (qn, PrimTCon arity) = pure (qn, compileDCon Z qn NormalCon (replicate (cast arity) Many))
 defToCExp (qn, PrimFn src _ deps) = pure (qn, CRaw src deps)
 defToCExp (qn, Fn tm)          = (_,_ qn) <$> compileFun tm

src/Lib/CompileJS.newt

@@ -1,7 +1,4 @@
--- TODO Audit how much "outside" stuff could pile up in the continuation. (How much might be repeated in case branches.)
+module Lib.CompileJS
--- TODO consider inlining constructors here (a future inline process might do this anyway).
--- TODO consider not emitting null in `LitObject` (after inlining constructors)
-module Lib.Compile
 
 import Prelude
 import Lib.Common
@@ -147,6 +144,25 @@ getEnv ix env = case getAt' ix env of
   Just e => e
   Nothing => fatalError "Bad bounds \{show ix}"
 
+-- It would be nice to be able to declare these
+compilePrimOp : String → List CExp → Maybe CExp
+compilePrimOp "Prelude.addString" (x :: y :: Nil) = Just (CPrimOp "+" x y)
+compilePrimOp "Prelude.addInt" (x :: y :: Nil) = Just (CPrimOp "+" x y)
+compilePrimOp "Prelude.mulInt" (x :: y :: Nil) = Just (CPrimOp "*" x y)
+compilePrimOp "Prelude.subInt" (x :: y :: Nil) = Just (CPrimOp "-" x y)
+compilePrimOp "Prelude._&&_" (x :: y :: Nil) = Just (CPrimOp "&&" x y)
+compilePrimOp "Prelude._||_" (x :: y :: Nil) = Just (CPrimOp "||" x y)
+-- Assumes Bool is in the right order!
+compilePrimOp "Prelude.jsEq" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
+compilePrimOp "Prelude.eqChar" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
+compilePrimOp "Prelude.ltChar" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y)
+compilePrimOp "Prelude.eqInt" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
+compilePrimOp "Prelude.ltInt" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y)
+compilePrimOp "Prelude.eqString" (_ :: x :: y :: Nil) = Just (CPrimOp "==" x y)
+compilePrimOp "Prelude.ltString" (_ :: x :: y :: Nil) = Just (CPrimOp "<" x y)
+compilePrimOp "Prelude.divInt" (x :: y :: Nil) = Just (CPrimOp "|" (CPrimOp "/" x y) (CLit $ LInt 0))
+compilePrimOp _ _ = Nothing
+
 -- This is inspired by A-normalization, look into the continuation monad
 -- There is an index on JSStmt, adopted from Stefan Hoeck's code.
 --
@@ -224,7 +240,10 @@ termToJS {e} env (CLoop args quants) f = runArgs (reverse env.jsenv) args quants
     runArgs (JUndefined :: rest) (arg :: args) (q :: qs) = runArgs rest args qs
     runArgs (wat :: rest) (arg :: args) (q :: qs) = fatalError "bad env for quant \{show q}"
     runArgs a b c = fatalError "FALLBACK \{show $ length' a} \{show $ length' b} \{show $ length' c}"
-termToJS env (CAppRef nm args quants) f = termToJS env (CRef nm) (\ t' => (argsToJS env t' args quants Lin f))
+termToJS env (CAppRef nm args quants) f =
+  case compilePrimOp (show nm) args of
+    Just cexp => termToJS env cexp f
+    Nothing => termToJS env (CRef nm) (\ t' => (argsToJS env t' args quants Lin f))
   where
     etaExpand : JSEnv -> List Quant -> SnocList JSExp -> JSExp -> JSExp
     etaExpand env Nil args tm = Apply tm (args <>> Nil)
@@ -261,11 +280,16 @@ termToJS {e} env (CCase t alts) f =
       -- TODO with inlining, we hit cases where the let gets pulled forward more than once
       -- two cases as separate args, se we need actual unique names. For now, we're calling
       -- incr when processing App, as a stopgap, we probably need a fresh names state monad
+      -- also TODO find out when the case builder pulls out sc$ for us and when we do
+      -- _sc here.  It seems like nm doesn't get used in the CDefAlt case.
+      -- possibly from inlining?
+      -- Lib.Parser.pratt has two (hence the incr)
+      -- and record updates hit _sc$
       let nm = "_sc$\{show env.depth}"
           -- increment the bit that goes into the name
           env' = incr env
       in if simpleJSExp t'
-        then (maybeCaseStmt env' t' alts)
+        then (maybeCaseStmt env t' alts)
         else JSnoc (JConst nm t') (maybeCaseStmt env' (Var nm) alts)
   where
     tertiary : JSExp → JSStmt e → JSStmt e → Cont e → JSStmt e
@@ -290,15 +314,18 @@ termToJS {e} env (CCase t alts) f =
     maybeCaseStmt env sc alts@(CLitAlt _ _  :: _) =
         (JCase sc (map (termToJSAlt env sc) alts))
     maybeCaseStmt env sc alts = case alts of
+        -- Bool alt becomes tertiary operator
         CLitAlt (LBool b) rhs :: alt :: Nil =>
           let t' = termToJS env rhs f
               e' = termToJS env (getBody alt) f
           in if b then tertiary sc t' e' f else tertiary sc e' t' f
+        -- two branch alt becomes tertiary operator
         CConAlt ix name info args t :: alt :: Nil =>
           let cond = (JPrimOp "==" (Dot sc "tag") (LitInt $ cast ix))
               t' = termToJS (conAltEnv sc 0 env args) t f
               u' = termToJS (conAltEnv sc 0 env $ getArgs alt) (getBody alt) f
           in tertiary cond t' u' f
+        -- fall back to switch statement
         alts => JCase (Dot sc "tag") (map (termToJSAlt env sc) alts)
 
 jsKeywords : List String

src/Lib/CompileScheme.newt

@@ -0,0 +1,338 @@
+module Lib.CompileScheme
+
+import Prelude
+import Lib.Common
+import Lib.Types
+import Lib.Eval
+import Lib.Prettier
+import Lib.CompileExp
+import Lib.TopContext
+import Lib.LiftWhere
+import Lib.LiftLambda
+import Lib.TCO
+import Lib.Ref2
+import Lib.Erasure
+import Data.String
+import Data.Int
+import Data.SortedMap
+import Data.IORef
+import Data.SnocList
+
+SCEnv : U
+SCEnv = List String
+
+getEnv : Int → SCEnv → String
+getEnv ix env = case getAt' ix env of
+  Just e => e
+  Nothing => fatalError "Bad bounds \{show ix}"
+
+scbind : String → SCEnv → (String × SCEnv)
+scbind nm env = let
+  x = length' env
+  nm' = "nm-\{show x}"
+  in (nm', nm' :: env)
+
+-- TODO
+scmKeywords : List String
+scmKeywords = "lambda" :: Nil
+
+scmIdent : String → String
+scmIdent id = if elem id scmKeywords then "$" ++ id else pack $ fix (unpack id)
+  where
+    fix : List Char -> List Char
+    fix Nil = Nil
+    fix (x :: xs) =
+      if isAlphaNum x || x == '_' || x == '.' then
+        x :: fix xs
+      -- make qualified names more readable
+      else if x == ',' then '_' :: fix xs
+      else if x == ' ' then '_' :: fix xs
+      else if x == '$' then
+        '$' :: '$' :: fix xs
+      else
+        '$' :: (toHex (cast x)) ++ fix xs
+
+
+scmLit : Literal → String
+scmLit (LString str) = quoteString str
+scmLit (LInt n) = show n
+scmLit (LChar c) = pack $ '#' :: '\\' :: c :: Nil -- FIXME
+scmLit (LBool b) = ite b "#t" "#f"
+
+scmName : QName → String
+scmName qn = scmIdent $ show qn
+
+cexpToScm : SCEnv → CExp → String
+
+withVar : SCEnv → CExp → (String → String) → String
+-- withVar env (CBnd _) f = ?
+-- withVar env (CLit _) f = ?
+withVar env t f = let nm = "wv$\{show $ length' env}"
+  in "(let ((\{nm} \{cexpToScm env t})) \{f nm})"
+
+cexpToScm env (CBnd n) = getEnv n env
+cexpToScm env (CLam nm t) = case scbind nm env of
+  (nm', env') => "(lambda (\{nm'}) \{cexpToScm env' t})"
+cexpToScm env (CFun args body) = case bindAll args Lin env  of
+    (nms,env') => "(lambda (\{joinBy " " nms}) \{cexpToScm env' body})"
+  where
+    bindAll : List (Quant × String) → SnocList String → SCEnv → List String × SCEnv
+    bindAll Nil acc env = (acc <>> Nil, env)
+    bindAll ((_,nm) :: rest) acc env = case scbind nm env of
+      (nm', env') => bindAll rest (acc :< nm') env'
+cexpToScm env (CApp t u) = "(\{cexpToScm env t} \{cexpToScm env u})"
+cexpToScm env (CAppRef nm args Nil) = go (scmName nm) $ map (cexpToScm env) args
+  where
+    go : String → List String → String
+    go acc Nil = acc
+    go acc (arg :: args) = go "(\{acc} \{arg})" args
+-- If we're short, we need to eta expand
+cexpToScm env (CAppRef nm args quants) =
+  go env "(\{scmName nm}" (map (cexpToScm env) args) quants
+  where
+    -- here `acc` is always missing a closing paren
+    go : SCEnv → String → List String → List Quant → String
+    go env acc Nil Nil = acc ++ ")"
+    -- extra args are applied
+    go env acc (arg :: args) Nil = go env "(\{acc}) \{arg}" args Nil
+    -- missing args get eta expanded
+    go env acc Nil (q :: qs) = case scbind "_" env of
+      (nm, env') => let acc = "\{acc} \{nm}" in "(lambda (\{nm}) \{go env' acc Nil qs})"
+    -- TODO / REVIEW Only for Many?
+    go env acc (arg :: args) (q :: qs) = go env "\{acc} \{arg}" args qs
+    -- go env acc (arg :: args) (q :: qs) = go env acc args qs
+-- so... we're not giving scrutinee a deBruijn index, but we may
+-- need to let it so we can pull data off for the CConAlt
+cexpToScm env (CCase sc alts) = do
+    -- assign sc, might need to do more to make the name unique, we only
+    -- get one of these per env at the moment
+    -- Not vector-ref for CLitAlt...
+    withVar env sc $ \ nm => doCase nm alts
+  where
+    -- add a bunch of lets then do body
+    conAlt : SCEnv → String → SnocList String → List String → CExp → String
+    conAlt env nm lets Nil body = "(let (\{joinBy " " (lets <>> Nil)}) \{cexpToScm env body})"
+    -- TODO let `vector-ref nm ..`` vs `#f` (erased) in env for erased fields
+    conAlt env nm lets (arg :: args) body = case scbind arg env of
+      (arg', env') => let ix = 1 + snoclen' lets
+        in conAlt env' nm (lets :< "(\{arg'} (vector-ref \{nm} \{show ix}))") args body
+
+    doAlt : String → CAlt → String
+    doAlt nm (CConAlt tag cname _ args body) = "((\{show tag}) \{conAlt env nm Lin args body})"
+    doAlt nm (CDefAlt body) = "(else \{cexpToScm env body})"
+    doAlt nm (CLitAlt lit body) = "((\{scmLit lit}) \{cexpToScm env body})"
+
+    doCase : String → List CAlt → String
+    doCase nm alts@(CLitAlt _ _ :: _) = "(case \{nm} \{joinBy " " $ map (doAlt nm) alts})"
+    doCase nm alts = "(case (vector-ref \{cexpToScm env sc} 0) \{joinBy " " $ map (doAlt nm) alts})"
+
+cexpToScm env (CRef nm) = scmName nm
+cexpToScm env (CMeta _) = fatalError "meta in code gen"
+cexpToScm env (CLit lit) = scmLit lit
+cexpToScm env (CLet nm t u) =
+  let (nm',env') = scbind nm env in
+  "(let ((\{nm'} \{cexpToScm env t})) \{cexpToScm env' u})"
+cexpToScm env (CLetRec nm t u) =
+  let (nm',env') = scbind nm env in
+  "(let ((\{nm'} \{cexpToScm env' t})) \{cexpToScm env' u})"
+cexpToScm env (CLetLoop _ _) = fatalError "CLetLoop in scheme codegen"
+cexpToScm env (CLoop _ _) = fatalError "CLoop in scheme codegen"
+cexpToScm env CErased = "#f"
+cexpToScm env (CConstr tag nm args quants) =
+  -- FIXME need to deal with quants
+  let args' = map (cexpToScm env) args in
+  "(vector \{show tag} \{joinBy " " args'})"
+-- TODO
+cexpToScm env (CRaw _ _) = "CRaw"
+-- TODO We still have a couple of these in CompileExp, for the magic Nat
+cexpToScm env (CPrimOp op a b) = "(\{op} \{cexpToScm env a} \{cexpToScm env b})"
+
+
+-- Collect the QNames used in a term
+getNames : Tm -> List QName -> List QName
+getNames (Ref x nm) acc = nm :: acc
+getNames (Lam x str _ _ t) acc = getNames t acc
+getNames (App x t u) acc = getNames u $ getNames t acc
+getNames (Pi x str icit y t u) acc = getNames u $ getNames t $ QN primNS "PiType" :: acc
+getNames (Let x str t u) acc = getNames u $ getNames t acc
+getNames (LetRec x str _ t u) acc = getNames u $  getNames t acc
+getNames (Case x t alts) acc = getNames t $ foldl getAltNames acc alts
+  where
+    getAltNames : List QName -> CaseAlt -> List QName
+    getAltNames acc (CaseDefault t) = getNames t acc
+    getAltNames acc (CaseCons name args t) = name :: getNames t acc
+    getAltNames acc (CaseLit lit t) = getNames t acc
+getNames _ acc = acc
+
+-- returns a QName -> Def of in-use entries
+-- This will be what we work on for optimization passes
+getEntries : SortedMap QName Def → QName → M (SortedMap QName Def)
+getEntries acc name = do
+  top <- getTop
+  case lookup name top of
+    Nothing => do
+      putStrLn "bad name \{show name}"
+      pure acc
+    Just (MkEntry _ name type def@(Fn exp) _) => case lookupMap' name acc of
+      Just _ => pure acc
+      Nothing => do
+        top <- getTop
+        exp <- zonk top 0 Nil exp
+        let acc = updateMap name (Fn exp) acc
+        foldlM getEntries acc $ getNames exp Nil
+    Just (MkEntry _ name type def@(PrimFn _ _ used) _) =>
+      let acc = updateMap name def acc in
+      foldlM getEntries acc used
+    Just entry => pure $ updateMap name entry.def acc
+
+/-
+
+## Sort names by dependencies
+
+This code is _way too subtle. The problem goes away if I wrap `() =>` around 0-ary top level functions. But I'm
+stubborn, so I'm giving it a try. Changing codegen may repeatedly break this and require switching to `() =>`.
+
+The idea here is to get a list of names to emit in order of dependencies. But top level 0-ary functions can reference
+and call names at startup. They can't reference something that hasn't been declared yet and can't call something that
+hasn't been defined.
+
+As an example, a recursive show instance:
+- References the `show` function
+- `show` function references the instance under a lambda (not inlining this yet)
+- We hit the bare function first, it depends on the instance (because of recursion), which depends on the
+  function, but loop prevention cuts.
+
+We have main at the top, it is called so we visit it deep. We do a depth-first traversal, but will distinguish whether
+we're visiting shallow or deep. We're trying to avoid hitting issues with indirect circular references.
+
+- Anything we visit deep, we ensure is visited shallow first
+- Shallow doesn't go into function bodies, but we do go into lambdas
+- Anything invoked with arguments while shallow is visited deep, anything referenced or partially applied is still shallow.
+- We keep track of both shallow and deep visits in our accumuulator
+- Shallow represents the declaration, so we filter to those at the end
+
+TODO this could be made faster by keeping a map of the done information
+REVIEW could I avoid most of this by using `function` instead of arrow functions?
+
+-/
+
+sortedNames : SortedMap QName CExp → List QName → List QName
+sortedNames defs names =
+  map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (True,) names
+  where
+    getBody : CAlt → CExp
+    getBody (CConAlt _ _ _ _ t) = t
+    getBody (CLitAlt _ t) = t
+    getBody (CDefAlt t) = t
+
+    -- deep if this qn is being applied to something
+    getNames : (deep : Bool) → List (Bool × QName) → CExp →  List (Bool × QName)
+    -- liftIO calls a lambda statically
+    getNames deep acc (CLam _ t) = getNames deep acc t
+    getNames deep acc (CLetLoop _ t) = getNames deep acc t
+    -- top level 0-ary function, doesn't happen
+    getNames deep acc (CFun _ t) = if deep then getNames deep acc t else acc
+    -- REVIEW - True or deep?
+    getNames deep acc (CLoop args qs) = foldl (getNames True) acc args
+    getNames deep acc (CAppRef nm args qs) =
+      if length' args == length' qs
+        then case args of
+          Nil => (True, nm) :: acc
+          ts => foldl (getNames True) ((True, nm) :: acc) ts
+        else
+          foldl (getNames deep) ((deep, nm) :: acc) args
+   -- TODO look at which cases generate CApp
+    getNames deep acc (CApp t u) = getNames True (getNames deep acc u) t
+    getNames deep acc (CCase t alts) = foldl (getNames deep) acc $ t :: map getBody alts
+    -- we're not calling it
+    getNames deep acc (CRef qn) = (deep, qn) :: acc
+    getNames deep acc (CLet _ t u) = getNames deep (getNames deep acc t) u
+    getNames deep acc (CLetRec _ t u) = getNames deep (getNames deep acc t) u
+    getNames deep acc (CConstr _ _ ts _) = foldl (getNames deep) acc ts
+    -- if the CRaw is called, then the deps are called
+    getNames deep acc (CRaw _ deps) = acc -- map (_,_ deep) deps ++ acc
+    -- wrote these out so I get an error when I add a new constructor
+    getNames deep acc (CLit _) = acc
+    getNames deep acc (CMeta _) = acc
+    getNames deep acc (CBnd _) = acc
+    getNames deep acc CErased = acc
+    getNames deep acc (CPrimOp op t u) = getNames deep (getNames deep acc t) u
+
+    -- recurse on all dependencies, pushing onto acc
+    go : List (Bool × QName) → List (Bool × QName) → (Bool × QName) → List (Bool × QName)
+      -- Need to force shallow if we're doing deep and haven't done shallow.
+    go loop acc this@(deep, qn) =
+      -- there is a subtle issue here with an existing (False, qn) vs (True, qn)
+      let acc = if deep && not (elem (False, qn) acc) && not (elem (False, qn) loop)
+                  then go loop acc (False, qn)
+                  else acc
+      in if elem this loop
+        then acc
+        else if elem this acc then acc
+        else
+          case lookupMap' qn defs of
+            Nothing => acc   -- only `bouncer`
+            Just exp => this :: foldl (go $ this :: loop) acc (getNames deep Nil exp)
+
+eraseEntries : {{Ref2 Defs St}} → M Unit
+eraseEntries = do
+  defs <- getRef Defs
+  ignore $ traverse go $ toList defs
+  where
+    go : {{Ref2 Defs St}} → (QName × Def) → M Unit
+    go (qn, Fn tm) = do
+      tm' <- erase Nil tm Nil
+      modifyRef Defs $ updateMap qn (Fn tm')
+    go _ = pure MkUnit
+
+-- given a initial function, return a dependency-ordered list of javascript source
+process : List QName → M (List String)
+process names = do
+  top <- getTop
+  entries <- foldlM getEntries emptyMap names
+
+  -- Maybe move this dance into liftWhere
+  ref <- newIORef entries
+  let foo = MkRef ref -- for the autos below
+  eraseEntries
+  liftWhere
+  entries <- readIORef ref
+  -- Now working with defs
+  exprs <- mapM defToCExp $ toList entries
+  let cexpMap = foldMap const emptyMap exprs
+  -- not needed for scheme
+  -- cexpMap <- tailCallOpt cexpMap
+  -- Not needed for scheme
+  -- cexpMap <- liftLambda cexpMap
+  let names = sortedNames cexpMap names
+  pure $ mapMaybe (go cexpMap) names
+  where
+    go : ExpMap → QName → Maybe String
+    go cexpMap name = do
+      (qn, cexp) <- lookupMap name cexpMap
+      case cexp of
+        CRaw _ _ => Nothing
+        _ => Just $ "(define \{scmName qn} \{cexpToScm Nil cexp})"
+
+compileScheme : M (List String)
+compileScheme = do
+  top <- getTop
+  let exports = getExports Nil $ listValues top.currentMod.modDefs
+  let mainName = (QN top.currentMod.modName "main")
+  let main = lookup mainName top
+  let todo = case main of
+    Nothing => exports
+    Just _ => mainName :: exports
+  defs <- process todo
+  case lookup mainName top of
+    Just _ => -- tack on call to main function
+      let exec = "(\{show mainName} 'world)"
+      in pure $ "(import (chezscheme))" :: "(include \"prim.ss\")" :: reverse (exec :: defs)
+    Nothing => pure $ reverse defs
+  where
+    getExports : List QName → List TopEntry → List QName
+    getExports acc Nil = acc
+    getExports acc ((MkEntry fc name@(QN ns nm) type def eflags) :: rest) =
+      let acc = if elem Export eflags then name :: acc else acc
+      in getExports acc rest
+

src/Lib/Derive.newt

@@ -127,25 +127,3 @@ deriveShow fc name = do
 
       pure (left, Just right)
 
-
-
--- -- A description would be nice.
--- deriveShow : FC → QName → M Raw
--- deriveShow fc qn = do
---     top <- getTop
---     case lookup qn top : Maybe TopEntry of
---         Nothing => error {Raw} fc "Can't find \{show qn} in derive Show"
---         -- I want case split too... I need to tie the editor into the repl.
---         (Just (MkEntry fc name type (TCon _ conNames) eflags) ) => ?
---         (Just (MkEntry fc name type (Axiom) eflags) ) => ?
---         (Just (MkEntry fc name type (DCon _ _ _ _) eflags) ) => ?
---         (Just (MkEntry fc name type (Fn _) eflags) ) => ?
---         (Just (MkEntry fc name type (PrimTCon _) eflags) ) => ?
---         (Just (MkEntry fc name type (PrimFn _ _ _) eflags) ) => ?
---         (Just (MkEntry fc name type (PrimOp _) eflags) ) => ?
-
---     error fc "TODO"
-
-
--- HasFC as example of user-defined derivation (when we get to that)
--- SetFC would be nice, too.

src/Lib/Error.newt

@@ -31,7 +31,7 @@ showError src err =
     go fc l (x :: xs) =
       if l == fcLine fc then
         let width = fc.bnds.endCol - fc.bnds.startCol in
-        "  \{x}\n  \{replicate (cast $ fcCol fc) ' '}\{replicate (cast width) '^'}\n"
+        "  \{x}\n  \{padding (fcCol fc) ' '}\{padding width '^'}\n"
       else if fcLine fc - 3 < l then "  " ++ x ++ "\n" ++ go fc (l + 1) xs
       else go fc (l + 1) xs
 

src/Lib/Parser.newt

@@ -314,7 +314,7 @@ lamExpr = do
 caseAlt : Parser RCaseAlt
 caseAlt = do
   pure MkUnit
-  pat <- typeExpr
+  pat <- term
   t <- optional (keyword "=>" >> term)
   pure $ MkAlt pat t
 
@@ -364,6 +364,7 @@ doCaseLet = do
   keyword "="
   sc <- typeExpr
   alts <- startBlock $ manySame $ symbol "|" *> caseAlt
+  -- REVIEW why am I collecting the rest here?
   bodyFC <- getPos
   body <- RDo <$> getPos <*> someSame doStmt
   pure $ DoExpr fc (RCase fc sc Nothing (MkAlt pat (Just body) :: alts))
@@ -457,9 +458,9 @@ ibind = do
   symbol "{"
   quant <- quantity
   names <- (some (addPos varname))
-  ty <- optional (symbol ":" *> typeExpr)
+  ty <- symbol ":" *> typeExpr
   symbol "}"
-  pure $ map (makeBind quant ty) names
+  pure $ map (makeBind quant (Just ty)) names
   where
     makeBind : Quant → Maybe Raw → FC × String → BindInfo × Raw
     makeBind quant ty (pos, name) = (BI pos name Implicit quant, fromMaybe (RImplicit pos) ty)

src/Lib/Parser/Impl.newt

@@ -76,7 +76,7 @@ getOps = P $ \last toks com ops col => OK ops last toks com ops
 
 addOp : String -> Int -> Fixity -> Parser Unit
 addOp nm prec fix = P $ \ last toks com ops col =>
-  let parts = split nm "_" in
+  let parts = splitBy nm '_' in
   case parts of
     "" :: key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix False rule) ops)
     key :: rule => OK MkUnit last toks com (updateMap key (MkOp nm prec fix True rule) ops)

src/Lib/Prettier.newt

@@ -2,6 +2,7 @@
 -- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf
 module Lib.Prettier
 import Prelude
+import Lib.Common
 import Data.Int
 
 -- TODO I broke this when I converted from Nat to Int, and we're disabling it
@@ -44,7 +45,7 @@ group x = Alt (flatten x) x
 -- TODO - we can accumulate snoc and cat all at once
 layout : List Item -> SnocList String -> String
 layout Nil acc = fastConcat $ acc <>> Nil
-layout (LINE k :: x) acc = layout x (acc :< "\n" :< replicate (cast k) ' ')
+layout (LINE k :: x) acc = layout x (acc :< "\n" :< padding k ' ')
 layout (TEXT str :: x) acc = layout x (acc :< str)
 
 -- Whether a documents first line fits.

src/Lib/ProcessDecl.newt

@@ -28,15 +28,19 @@ dumpEnv ctx =
 
     go : List String -> Int -> List (Val × String × Val) -> List String -> M (List String)
     go _ _ Nil acc = pure acc
-    go names k ((v, n, ty) :: xs) acc = if isVar k v
+    -- don't show the = bit for now. Lean folds it.
-      -- TODO - use Doc and add <+/> as appropriate to printing
+    go names k ((v, n, ty) :: xs) acc = do
-      then do
         ty' <- quote ctx.lvl ty
         go names (1 + k) xs ("  \{n} : \{render 90 $ pprint names ty'}":: acc)
-      else do
+
-        v' <- quote ctx.lvl v
+    -- go names k ((v, n, ty) :: xs) acc = if isVar k v
-        ty' <- quote ctx.lvl ty
+    --   then do
-        go names (1 + k) xs ("  \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc)
+    --     ty' <- quote ctx.lvl ty
+    --     go names (1 + k) xs ("  \{n} : \{render 90 $ pprint names ty'}":: acc)
+    --   else do
+    --     v' <- quote ctx.lvl v
+    --     ty' <- quote ctx.lvl ty
+    --     go names (1 + k) xs ("  \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc)
 
 
 logMetas : List MetaEntry -> M Unit

src/Lib/ProcessModule.newt

@@ -47,7 +47,7 @@ parseDecls fn ops toks@(first :: _) acc =
       else recover toks
 
 importToName : Import → List String
-importToName  (MkImport fc (_,name)) = split name "."
+importToName  (MkImport fc (_,name)) = splitBy name '.'
 
 importHints : List TopEntry → M Unit
 importHints Nil = pure MkUnit
@@ -69,7 +69,7 @@ processModule importFC repo stk modns = do
 
   let (False) = modns == primNS | _ => addPrimitives
   let freshMC = MC emptyMap Nil 0 CheckAll
-  let parts = split modns "."
+  let parts = splitBy modns '.'
   let fn = joinBy "/" parts ++ ".newt"
 
   -- Dummy for initial load/parse
@@ -144,6 +144,7 @@ processModule importFC repo stk modns = do
   -- This has addErrors as a side-effect
   logMetas $ reverse $ listValues top.currentMod.modMetaCtx.metas
 
+  top <- getTop
   -- print errors (for batch processing case)
   for_ (reverse top.currentMod.modErrors) $ \ err => putStrLn $ showError src err
 

src/Lib/ReplParser.newt

@@ -36,7 +36,7 @@ replQN = do
   ident <- uident
   rest <- many $ token Projection
   let name = joinBy "" (ident :: rest)
-  let (ns,nm) = unsnoc $ split1 name "."
+  let (ns,nm) = unsnoc $ splitBy1 name '.'
   pure $ QN (joinBy "." ns) nm
 
 data ArgType = ArgNone | ArgString | ArgIdent | ArgOptInt | ArgQName

src/Lib/Util.newt

@@ -34,7 +34,7 @@ splitTele = go Nil
 getBaseDir : String → FC → List String → M String
 getBaseDir fn fc modName = do
   let path = fst $ splitFileName fn
-  let dirs = split path "/"
+  let dirs = splitBy path '/'
   let (Right base) = baseDir (Lin <>< dirs) (Lin <>< modName)
     | Left err => error fc err
   let base = if base == "" then "." else base

src/Main.newt

@@ -4,7 +4,8 @@ import Prelude
 import Data.List1
 import Data.SortedMap
 import Lib.Common
-import Lib.Compile
+import Lib.CompileJS
+import Lib.CompileScheme
 import Lib.Parser
 import Lib.Elab
 import Lib.Util
@@ -43,6 +44,14 @@ jsonTopContext = do
       :: ("type", toJson (render 80 $ pprint Nil type) )
       :: Nil)
 
+writeScheme : String → M Unit
+writeScheme fn = do
+  lines <- compileScheme
+  let src = unlines lines
+  (Right _) <- liftIO {M} $ writeFile fn src
+    | Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err
+  pure MkUnit
+
 writeSource : String -> M Unit
 writeSource fn = do
   docs <- compile
@@ -77,7 +86,7 @@ showErrors fn src = do
 processFile : String -> M Unit
 processFile fn = do
   putStrLn "*** Process \{fn}"
-  let parts = split1 fn "/"
+  let parts = splitBy1 fn '/'
   let (dirs,file) = unsnoc parts
   let dir = if dirs == Nil then "." else joinBy "/" dirs
   let (name, ext) = splitFileName file
@@ -90,7 +99,7 @@ processFile fn = do
   let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
     | Left (err,toks) => throwError err
 
-  let modns = split modName "."
+  let modns = splitBy modName '.'
   base <- getBaseDir fn nameFC modns
 
   invalidateModule modName
@@ -201,7 +210,10 @@ main' = do
 
   case out of
     Nothing => pure MkUnit
-    Just name => writeSource name
+    Just name =>
+      if isSuffixOf ".ss" name then writeScheme name
+      else if isSuffixOf ".js" name then writeSource name
+      else exitFailure "Unknown extension for output file \{show name} - I only know .js and .ss"
 
 main : IO Unit
 main = do

src/Prelude.newt

@@ -146,7 +146,7 @@ class Functor (m : U → U) where
   map : ∀ a b. (a → b) → m a → m b
 
 infixr 4 _<$>_ _<$_
-_<$>_ : ∀ f. {{Functor f}} {0 a b} → (a → b) → f a → f b
+_<$>_ : ∀ f. {{Functor f}} {0 a b : _} → (a → b) → f a → f b
 f <$> ma = map f ma
 
 _<$_ : ∀ f a b. {{Functor f}} → b → f a → f b
@@ -214,7 +214,7 @@ instance Applicative Maybe where
 
 infixr 2 _<|>_
 class Alternative (m : U → U) where
-  _<|>_ : {0 a} → m a → m a → m a
+  _<|>_ : ∀ a. m a → m a → m a
 
 instance Alternative Maybe where
   Nothing <|> x = x
@@ -265,18 +265,22 @@ instance Concat String where
   _++_ = addString
 
 
-pfunc jsEq uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a == b ? Prelude_True : Prelude_False`
+pfunc ltInt : Int → Int → Bool := `(a,b) => a < b`
-pfunc jsLT uses (True False) : ∀ a. a → a → Bool := `(_, a, b) => a < b ? Prelude_True : Prelude_False`
+pfunc eqInt : Int → Int → Bool := `(a,b) => a == b`
+pfunc ltChar : Char → Char → Bool := `(a,b) => a < b`
+pfunc eqChar : Char → Char → Bool := `(a,b) => a == b`
+pfunc ltString : String → String → Bool := `(a,b) => a < b`
+pfunc eqString : String → String → Bool := `(a,b) => a == b`
 
 pfunc jsShow : ∀ a . a → String := `(_,a) => ''+a`
 instance Eq Int where
-  a == b = jsEq a b
+  a == b = eqInt a b
 
 instance Eq String where
-  a == b = jsEq a b
+  a == b = eqString a b
 
 instance Eq Char where
-  a == b = jsEq a b
+  a == b = eqChar a b
 
 
 
@@ -304,11 +308,6 @@ pfunc arrayToList uses (Nil _::_) : ∀ a. Array a → List a := `(a,arr) => {
   return rval
 }`
 
-
-
--- for now I'll run this in JS
-pfunc lines uses (arrayToList) : String → List String := `(s) => Prelude_arrayToList(null,s.split('\n'))`
-
 pfunc p_strHead : (s : String) → Char := `(s) => s[0]`
 pfunc p_strTail : (s : String) → String := `(s) => s[0]`
 
@@ -328,11 +327,9 @@ pfunc natToInt : Nat → Int := `(n) => n`
 pfunc intToNat : Int → Nat := `(n) => n>0?n:0`
 
 pfunc fastConcat uses (listToArray) : List String → String := `(xs) => Prelude_listToArray(null, xs).join('')`
-pfunc replicate uses (natToInt) : Nat → Char → String := `(n,c) => c.repeat(Prelude_natToInt(n))`
 
--- TODO this should be replicate and the chars thing should have a different name
+replicate : ∀ a. Nat → a → List a
-replicate' : ∀ a. Nat → a → List a
+replicate {a} n x = go n Nil
-replicate' {a} n x = go n Nil
   where
     go : Nat → List a → List a
     go Z xs = xs
@@ -370,12 +367,12 @@ instance Monad List where
 
 
 -- This is traverse, but we haven't defined Traversable yet
-mapA : ∀ m. {{Applicative m}} {0 a b} → (a → m b) → List a → m (List b)
+mapA : ∀ m. {{Applicative m}} {0 a b : _} → (a → m b) → List a → m (List b)
 mapA f Nil = return Nil
 mapA f (x :: xs) = return _::_ <*> f x <*> mapA f xs
 
 
-mapM : ∀ m. {{Monad m}} {0 a b} → (a → m b) → List a → m (List b)
+mapM : ∀ m. {{Monad m}} {0 a b : _} → (a → m b) → List a → m (List b)
 mapM f Nil = pure Nil
 mapM f (x :: xs) = do
   b <- f x
@@ -435,40 +432,23 @@ pfunc pack : List Char → String := `(cs) => {
 }
 `
 
-pfunc debugStr uses (natToInt listToArray) : ∀ a. a → String := `(_, obj) => {
+
-  const go = (obj) => {
+splitBy : String → Char → List String
-    if (obj === null) return "_"
+splitBy str ch = go Lin Lin (unpack str)
-    if (typeof obj == 'bigint') return ''+obj
+  where
-    if (obj.tag === '_,_') {
+    go : SnocList String → SnocList Char → List Char → List String
-      let rval = '('
+    go strs chs Nil = strs <>> (pack (chs <>> Nil) :: Nil)
-      while (obj?.tag === '_,_') {
+    go strs chs (c :: rest) =
-        rval += go(obj.h2) + ', '
+      if c == ch then go (strs :< pack (chs <>> Nil)) Lin rest
-        obj = obj.h3
+      else go strs (chs :< c) rest
-      }
+
-      return rval + go(obj) + ')'
+lines : String → List String
-    }
+lines str = splitBy str '\n'
-    if (obj?.tag === '_::_' || obj?.tag === 'Nil') {
+
-      let stuff = Prelude_listToArray(null,obj)
+
-      return '['+(stuff.map(go).join(', '))+']'
+-- Not as useful as it used to be, we no longer have constructor names
-    }
+pfunc debugStr : ∀ a. a → String := `(_, obj) => {
-    if (obj instanceof Array) {
-      return 'io['+(obj.map(go).join(', '))+']'
-    }
-    if (obj?.tag === 'S' || obj?.tag === 'Z') {
-      return ''+Prelude_natToInt(obj)
-    } else if (obj?.tag) {
-      let rval = '('+obj.tag
-      for(let i=0;;i++) {
-        let key = 'h'+i
-        if (!(key in obj)) break
-        rval += ' ' + go(obj[key])
-      }
-      return rval+')'
-    } else {
  return JSON.stringify(obj)
-    }
-  }
-  return go(obj)
 }`
 
 debugLog : ∀ a. a → IO Unit
@@ -507,7 +487,6 @@ pfunc addInt : Int → Int → Int := `(x,y) => x + y`
 pfunc mulInt : Int → Int → Int := `(x,y) => x * y`
 pfunc divInt : Int → Int → Int := `(x,y) => x / y | 0`
 pfunc subInt : Int → Int → Int := `(x,y) => x - y`
-pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? Prelude_True : Prelude_False`
 
 instance Mul Int where
   x * y = mulInt x y
@@ -725,6 +704,10 @@ instance Bifunctor _×_ where
 instance Functor IO where
   map f a = bind a $ \ a => pure (f a)
 
+instance ∀ a. Functor (Either a) where
+  map f (Left x) = Left x
+  map f (Right y) = Right (f y)
+
 uncurry : ∀ a b c. (a → b → c) → (a × b) → c
 uncurry f (a,b) = f a b
 
@@ -748,8 +731,6 @@ tail (x :: xs) = xs
 data Ordering = LT | EQ | GT
 derive Eq Ordering
 
-pfunc jsCompare uses (EQ LT GT) : ∀ a. a → a → Ordering := `(_, a, b) => a == b ? Prelude_EQ : a < b ? Prelude_LT : Prelude_GT`
-
 infixl 6 _<_ _<=_ _>_
 class Ord a where
   compare : a → a → Ordering
@@ -771,10 +752,10 @@ instance Ord Nat where
   compare (S n) (S m) = compare n m
 
 instance Ord Int where
-  compare a b = jsCompare a b
+  compare a b = if eqInt a b then EQ else if ltInt a b then LT else GT
 
 instance Ord Char where
-  compare a b = jsCompare a b
+  compare a b = if eqChar a b then EQ else if ltChar a b then LT else GT
 
 flip : ∀ a b c. (a → b → c) → (b → a → c)
 flip f b a = f a b
@@ -808,13 +789,13 @@ ite : ∀ a. Bool → a → a → a
 ite c t e = if c then t else e
 
 instance Ord String where
-  compare a b = jsCompare a b
+  compare a b = if eqString a b then EQ else if ltString a b then LT else GT
 
 instance Cast Int Nat where
   cast n = intToNat n
 
 instance Show Char where
-  show c = "'\{jsShow c}'"
+  show c = pack $ '\'' :: c :: '\'' :: Nil
 
 swap : ∀ a b. a × b → b × a
 swap (a,b) = (b,a)
@@ -841,8 +822,7 @@ find : ∀ a. (a → Bool) → List a → Maybe a
 find f Nil = Nothing
 find f (x :: xs) = if f x then Just x else find f xs
 
--- TODO this would be faster, but less pure as a primitive
+-- TODO maybe use fastConcat
--- fastConcat might be a good compromise
 joinBy : String → List String → String
 joinBy _ Nil = ""
 joinBy _ (x :: Nil) = x

tests/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
+  inl : ∀ a b. a -> a + b
-  inr : {A B} -> B -> 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
+  leaf : ∀ l u. (lu : l <<= u) -> T23 l u Z
-  node2 : {l u h} (x : _)
+  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)
 
@@ -71,7 +70,7 @@ 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