Add list sugar

drop old record syntax
use new record update syntax
2026-03-29 19:54:01 -07:00 · 2026-03-29 19:54:01 -07:00 · 2026-03-29 19:54:01 -07:00 · 2026-03-29 19:53:48 -07:00 · 2026-03-29 09:56:42 -07:00 · 2026-03-29 09:56:39 -07:00
44 changed files with 1151 additions and 937 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -4,21 +4,18 @@ build/
 *.swp
 *.log
 *.bak
-*.agda
-*.agdai
-/*.js
 input.txt
 node_modules
 mkday.py
 tmp
 min.js.gz
 src/Revision.newt
-newt.ss
-newt.so
 .calva
 .clj-kondo
 .joyride
 .lsp
 .vscode
+.helix
 bootstrap/serializer.js
 /newt-vscode-lsp/src/newt.js
+/playground/src/newt.js
--- a/84
+++ b/84
@@ -1,45 +1,24 @@
 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

+newt2: build/newt2.js

-src/Revision.newt: .PHONY
-	sh ./scripts/mkrevision
+newt3: build/newt3.js

-newt.js: ${SRCS} src/Revision.newt
-	$(RUNJS) bootstrap/newt.js src/Main.newt -o newt.js
-
-newt2.js: newt.js
-	$(RUNJS) newt.js src/Main.newt -o newt2.js
-
-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
+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
-
-# build / install old vscode extension
-# vscode:
-	# cd newt-vscode && vsce package && code --install-extension *.vsix
+lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js

 # build / install new LSP vscode extension
 vscode-lsp vscode: lsp
@@ -49,29 +28,56 @@ 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)

-lsp.js: ${SRCS}
-	node newt.js src/LSP.newt -o lsp.js
+##

-newt-vscode-lsp/src/newt.js: lsp.js
-	cp lsp.js $@
+build:
+	mkdir -p build

-playground/src/newt.js: lsp.js
-	cp lsp.js $@
+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 $@

-lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js

--- a/bootstrap/newt.js
+++ b/bootstrap/newt.js
--- a/newt-vscode-lsp/src/extension.ts
+++ b/newt-vscode-lsp/src/extension.ts
@@ -23,7 +23,7 @@ export function activate(context: vscode.ExtensionContext) {
  let serverOptions: ServerOptions
  if (cmd) {
    serverOptions = {
-      run: { command: "node", args: [cmd], transport: TransportKind.pipe },
+      run: { command: "node", args: ['--heapsnapshot-signal=SIGUSR2',cmd], transport: TransportKind.pipe },
      debug: { command: "node", args: [cmd], transport: TransportKind.pipe },
    }
  } else {
--- a/newt-vscode-lsp/src/lsp.ts
+++ b/newt-vscode-lsp/src/lsp.ts
@@ -16,6 +16,8 @@ import {
  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);
@@ -70,16 +72,18 @@ async function runChange() {
        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);
 });
@@ -138,6 +142,21 @@ connection.onInitialize((_params: InitializeParams): InitializeResult => ({
  },
 }));

+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')
--- a/playground/build
+++ b/playground/build
@@ -1,8 +1,7 @@
-#!/bin/bash 
+#!/bin/bash
 mkdir -p public
-echo copy newt
-(cd .. && make lsp.js)
-cp ../lsp.js src/newt.js
+echo build lsp.js
+(cd .. && make lsp)
 echo build newt worker
 esbuild src/worker.ts --bundle --format=esm --platform=browser > public/worker.js
 esbuild src/frame.ts --bundle --format=esm --platform=browser > public/frame.js
--- a/playground/src/cmeditor.ts
+++ b/playground/src/cmeditor.ts
@@ -154,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);
 }
--- a/playground/src/ipc.ts
+++ b/playground/src/ipc.ts
@@ -49,7 +49,7 @@ export interface API {
  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):  string;
+  compile(fileName: string, language: 'javascript'|'scheme'):  string;
 }

 export interface Message<K extends keyof API> {
@@ -116,4 +116,3 @@ export class IPC {
  }
 }

-class IPCClient {}
--- a/playground/src/main.ts
+++ b/playground/src/main.ts
@@ -11,12 +11,12 @@ 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, Position } from "./ipc.ts";
 import helpText from "./help.md?raw";
-import { basicSetup, EditorView } from "codemirror";
+import { basicSetup, EditorView} from "codemirror";
 import {Compartment, EditorState} from "@codemirror/state";
 import { javascript } from "@codemirror/lang-javascript";
 import { oneDark } from "@codemirror/theme-one-dark";
@@ -82,11 +82,23 @@ if (!state.javascript.value) {
    const fileName = state.currentFile.value;
    // maybe send fileName, src?
    await ipc.sendMessage("updateFile", [fileName, src]);
-    let js = await ipc.sendMessage("compile", [fileName]);
+    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;
+  }
+}
+
 async function runOutput() {
  await refreshJS()
  const src = state.javascript.value;
@@ -153,15 +165,23 @@ 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)
@@ -263,8 +283,8 @@ const language: EditorDelegate = {
        });
      }
      setOutput(res.output)
-      // less flashy version
-      ipc.sendMessage("compile", [fileName]).then(js => state.javascript.value = bundle(js));
+      state.javascript.value = ""
+      state.scheme.value = ""
      return diags;
    } catch (e) {
      console.log("ERR", e);
@@ -287,26 +307,26 @@ function Editor({ initialValue }: EditorProps) {
  return h("div", { id: "editor", ref });
 }

-// for extra credit, we could have a read-only monaco
-function JavaScript() {
-  const text = state.javascript.value;
+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(() => {
-    console.log('JSEFFECT')
    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({})),
-        javascript(),
+        language == 'javascript' ? javascript() : scheme(),
        EditorState.readOnly.of(true),
        EditorView.editable.of(false),
      ],
@@ -347,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";
@@ -365,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, {});
@@ -398,6 +417,7 @@ function Tabs() {
      { className: "tabBar" },
      Tab(RESULTS),
      Tab(JAVASCRIPT),
+      Tab(SCHEME),
      Tab(CONSOLE),
      Tab(HELP),
    ),
--- a/playground/src/newt.d.ts
+++ b/playground/src/newt.d.ts
@@ -5,3 +5,4 @@ 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;
--- a/playground/src/worker.ts
+++ b/playground/src/worker.ts
@@ -1,7 +1,7 @@
 import { shim } from "./emul";
 import { API, Message, ResponseMSG } from "./ipc";
 import { archive, preload } from "./preload";
-import { LSP_checkFile, LSP_codeActionInfo, LSP_compileJS, LSP_hoverInfo, LSP_updateFile } from './newt';
+import { LSP_checkFile, LSP_codeActionInfo, LSP_compileJS, LSP_compileToScheme, LSP_hoverInfo, LSP_updateFile } from './newt';

 const LOG = console.log

@@ -25,7 +25,10 @@ const api: API = {
  },
  hoverInfo: LSP_hoverInfo,
  codeActionInfo: LSP_codeActionInfo,
-  compile: LSP_compileJS,
+  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> }) {
--- a/playground/style.css
+++ b/playground/style.css
@@ -7,6 +7,7 @@
 body {
  overflow: hidden;
  font-size: 12px;
+  -webkit-text-size-adjust: none;
 }
 svg.icon path {
  stroke: black;
--- a/prim.ss
+++ b/prim.ss
@@ -1,11 +1,7 @@
-;; 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 $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)
@@ -18,7 +14,6 @@
 (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)
@@ -38,22 +33,9 @@
 ;; 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.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))))
@@ -83,15 +65,24 @@
 ;; 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))
+  (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))
-(define (Prelude.fatalError _ msg) (raise msg))
+;; 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 (list->List (command-line)) w))
+(define (Node.getArgs w) ($IORes (command-line) w))
+(define (Prelude.unsafePerformIO a f)
+  (car (f 'world)))
--- a/scripts/aoc
+++ b/scripts/aoc
@@ -2,7 +2,7 @@
 mkdir -p tmp
 echo "Test AoC 2024 solutions"
 # FIXME - it turns out there are some stack issues here (including length)
-NCC="bun run newt.js"
+NCC="bun run build/newt.js"
 total=0
 failed=0
 for fn in  aoc2024/Day*.newt; do
--- a/scripts/aoc25
+++ b/scripts/aoc25
@@ -1,7 +1,7 @@
 #!/bin/sh
 mkdir -p tmp
 echo "Test AoC 2025 solutions"
-NCC="node newt.js"
+NCC="node build/newt.js"
 total=0
 failed=0
 for fn in  aoc2025/Day*.newt; do
--- a/scripts/compile-chez.ss
+++ b/scripts/compile-chez.ss
@@ -1 +1 @@
-(parameterize ([optimize-level 3]) (compile-program "newt.ss"))
+(parameterize ([optimize-level 3]) (compile-program "build/newt.ss"))
--- a/scripts/stats.py
+++ b/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]
--- a/scripts/test
+++ b/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
@@ -34,7 +37,7 @@ for fn in tests/*.newt ; do
  fi
  # if there is a golden file, run the code and compare output
  if [ -f ${fn}.golden ]; then
-    node out.js > tmp/${bn}.out
+    $RUNOUT $OUTFILE > tmp/${bn}.out
    if [ $? != "0" ]; then
      echo Run failed for $fn
      failed=$((failed + 1))
--- a/src/Commands.newt
+++ b/src/Commands.newt
@@ -38,7 +38,7 @@ switchModule repo modns = do
    top <- getTop
    -- mod <- processModule emptyFC repo Nil modns
    let (Just mod) = lookupMap' modns top.modules | Nothing => pure Nothing
-    modifyTop [ currentMod := mod; ops := mod.modOps ]
+    modifyTop { currentMod := mod; ops := mod.modOps }
    pure $ Just mod

 data HoverInfo = NoHoverInfo | NeedCheck | HasHover FC String
--- a/src/LSP.newt
+++ b/src/LSP.newt
@@ -17,6 +17,7 @@ import Lib.ProcessDecl
 import Lib.Prettier
 import Lib.Error
 import Lib.CompileJS
+import Lib.CompileScheme

 pfunc js_castArray : Array JSObject → JSObject := `x => x`
 pfunc js_castInt : Int → JSObject := `x => x`
@@ -67,13 +68,12 @@ lspFileSource = do

 updateFile : String → String → Unit
 updateFile fn src = unsafePerformIO $ do
+    modifyIORef state { files $= updateMap fn src }
    st <- readIORef state
-    modifyIORef state [ files $= updateMap fn src ]
-    let st = the LSPState $ [ files $= updateMap fn src ] st
    let (base,modName) = decomposeName fn
    Right (ctx,_) <- (invalidateModule modName).runM st.topContext
        | _ => writeIORef state st
-    modifyIORef state [ topContext := ctx ]
+    modifyIORef state { topContext := ctx }


 fcToRange : FC → Json
@@ -96,17 +96,17 @@ hoverInfo uri line col = unsafePerformIO $ do
    -- We're proactively running check if there is no module information, make sure we save it
    Right (top, HasHover fc msg) <- (getHoverInfo repo modns line col).runM st.topContext
        | Right (top, NeedCheck)  => do
-            modifyIORef state $ [ topContext := top ]
+            modifyIORef state $ { topContext := top }
            putStrLn $ "NeedsCheck"
            pure $ js_castBool True
        | Right (top, NoHoverInfo)  => do
-            modifyIORef state $ [ topContext := top ]
+            modifyIORef state $ { topContext := top }
            putStrLn $ "Nothing to see here"
            pure $ js_castBool True
        | Left err => do
            putStrLn $ showError "" err
            pure $ jsonToJObject JsonNull
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
    let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
    pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil

@@ -126,7 +126,7 @@ codeActionInfo uri line col = unsafePerformIO $ do
      putStrLn "ACTIONS ERROR"
      putStrLn $ showError "" err
      pure js_null
-  modifyIORef state $ [ topContext := top ]
+  modifyIORef state $ { topContext := top }
  pure $ jsonToJObject $ JsonArray $ map actionToJson actions
  where
    single : String → Json → Json
@@ -238,7 +238,7 @@ checkFile fn = unsafePerformIO $ do
    (Right (top, json)) <- (do
        putStrLn "processModule"
        mod <- processModule emptyFC repo Nil modName
-        modifyTop [ currentMod := mod; ops := mod.modOps ]
+        modifyTop { currentMod := mod; ops := mod.modOps }

        -- pull out errors and infos
        top <- getTop
@@ -251,7 +251,7 @@ checkFile fn = unsafePerformIO $ do
            putStrLn $ showError "" err
            pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
    -- Cache loaded modules
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
    pure $ jsonToJObject $ JsonArray json

 docSymbols : String → JSObject
@@ -265,11 +265,11 @@ docSymbols fn = unsafePerformIO $ do
    repo <- lspFileSource
    (Right (top, json)) <- (do
        mod <- processModule emptyFC repo Nil modName
-        modifyTop [ currentMod := mod; ops := mod.modOps ]
+        modifyTop { currentMod := mod; ops := mod.modOps }
        getSymbols).runM st.topContext
        | Left err => do
           pure $ jsonToJObject $ JsonNull
-    modifyIORef state $ [ topContext := top ]
+    modifyIORef state $ { topContext := top }
    pure $ jsonToJObject $ JsonArray json

 compileJS : String → JSObject
@@ -279,7 +279,6 @@ compileJS fn = unsafePerformIO $ do
  when (st.baseDir /= base) $ \ _ => resetState base
  repo <- lspFileSource
  (Right (top, src)) <- (do
-    putStrLn "woo"
    mod <- processModule emptyFC repo Nil modName
    docs <- compile
    let src = unlines $
@@ -288,7 +287,22 @@ compileJS fn = unsafePerformIO $ do
          ++ map (render 90 ∘ noAlt) docs
    pure src).runM st.topContext
    | Left err => pure $ js_castStr "// \{errorMsg err}"
-  modifyIORef state [ topContext := top ]
+  modifyIORef state { topContext := top }
  pure $ js_castStr src

-#export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols
+compileToScheme : String → JSObject
+compileToScheme fn = unsafePerformIO $ do
+  let (base, modName) = decomposeName fn
+  st <- readIORef state
+  when (st.baseDir /= base) $ \ _ => resetState base
+  repo <- lspFileSource
+  (Right (top, src)) <- (do
+    mod <- processModule emptyFC repo Nil modName
+    docs <- compileScheme
+    let src = unlines docs
+    pure src).runM st.topContext
+    | Left err => pure $ js_castStr ";; \{errorMsg err}"
+  modifyIORef state { topContext := top }
+  pure $ js_castStr src
+
+#export updateFile checkFile hoverInfo codeActionInfo compileJS docSymbols compileToScheme
--- a/src/Lib/CompileExp.newt
+++ b/src/Lib/CompileExp.newt
@@ -17,7 +17,7 @@ import Data.SortedMap
 CExp : U

 data CAlt : U where
-  CConAlt : Nat → String → ConInfo → List String → CExp → CAlt
+  CConAlt : Nat → String → ConInfo → List String → List Quant → CExp → CAlt
  -- REVIEW keep var name?
  CDefAlt : CExp -> CAlt
  -- literal
@@ -43,7 +43,7 @@ data CExp : U where
  CLoop : List CExp → List Quant → CExp
  CErased : CExp
  -- Data / type constructor
-  CConstr : Nat → Name → List CExp → List Quant → CExp
+  CConstr : Nat → Name → List CExp → List Quant → ConInfo → CExp
  -- Raw javascript for `pfunc`
  CRaw : String -> List QName -> CExp
  -- Need this for magic Nat
@@ -101,7 +101,7 @@ lookupDef fc nm = do
    Just def => pure def

 getBody : CAlt → CExp
-getBody (CConAlt _ _ _ _ t) = t
+getBody (CConAlt _ _ _ _ _ t) = t
 getBody (CLitAlt _ t) = t
 getBody (CDefAlt t) = t

@@ -137,6 +137,15 @@ compileTerm tm@(App _ _ _) = case funArgs tm of
        arity <- arityForName fc nm
        case lookupMap' nm defs : Maybe Def of
          Just (DCon _ SuccCon _ _) => applySucc args'
+          -- Inline these two, maybe all of them?
+          Just (DCon tag ConsCon qs _) =>
+            if length' qs == length' args
+              then pure $ CConstr tag nm.baseName args' qs ConsCon
+              else apply nm args' arity
+          Just (DCon tag NilCon qs _) =>
+            if length' qs == length' args
+              then pure $ CConstr tag nm.baseName args' qs NilCon
+              else apply nm args' arity
          _ => apply nm args' arity
  -- REVIEW maybe we want a different constructor for non-Ref applications?
  (t, args) => do
@@ -164,25 +173,25 @@ compileTerm (Case fc t alts) = do
      defs <- getRef Defs
      def <- lookupDef emptyFC qn
      case def of
-        DCon ix info _ _ => CConAlt ix nm info args <$> compileTerm tm
-        _ => error fc "\{show nm} is not constructor"
+        DCon ix info qs _ => CConAlt ix nm info args qs <$> compileTerm tm
+        _ => error fc "\{show nm} is not a data constructor"

    CaseLit lit tm => CLitAlt lit <$> compileTerm tm
  pure $ CCase t' $ fancyCons t' alts'
  where
    numAltP : CAlt → Bool
-    numAltP (CConAlt _ _ SuccCon _ _) = True
-    numAltP (CConAlt _ _ ZeroCon _ _) = True
+    numAltP (CConAlt _ _ SuccCon _ _ _) = True
+    numAltP (CConAlt _ _ ZeroCon _ _ _) = True
    numAltP _ = False

    enumAlt : CAlt → CAlt
-    enumAlt (CConAlt ix nm EnumCon args tm) = CLitAlt (LInt $ cast ix) tm
-    enumAlt (CConAlt ix nm FalseCon args tm) = CLitAlt (LBool False) tm
-    enumAlt (CConAlt ix nm TrueCon args tm) = CLitAlt (LBool True) tm
+    enumAlt (CConAlt ix nm EnumCon args _ tm) = CLitAlt (LInt $ cast ix) tm
+    enumAlt (CConAlt ix nm FalseCon args _ tm) = CLitAlt (LBool False) tm
+    enumAlt (CConAlt ix nm TrueCon args _ tm) = CLitAlt (LBool True) tm
    enumAlt alt = alt

    isInfo : ConInfo → CAlt → Bool
-    isInfo needle (CConAlt _ _  info _ _)  = needle == info
+    isInfo needle (CConAlt _ _  info _ _ _)  = needle == info
    isInfo _ _ = False

    isDef : CAlt → Bool
@@ -193,7 +202,7 @@ compileTerm (Case fc t alts) = do
    doNumCon : CExp → List CAlt → List CAlt
    doNumCon sc alts =
      let zeroAlt = case find (isInfo ZeroCon) alts of
-            Just (CConAlt _ _ _ _ tm) => CLitAlt (LInt 0) tm :: Nil
+            Just (CConAlt _ _ _ _ _ tm) => CLitAlt (LInt 0) tm :: Nil
            Just tm => fatalError "ERROR zeroAlt mismatch \{debugStr tm}"
            _ => case find isDef alts of
                  Just (CDefAlt tm) => CLitAlt (LInt 0) tm :: Nil
@@ -201,7 +210,7 @@ compileTerm (Case fc t alts) = do
                  _ => Nil
      in
      let succAlt = case find (isInfo SuccCon) alts of
-            Just (CConAlt _ _ _ _ tm) => CDefAlt (CLet "x" (CPrimOp "-" sc (CLit $ LInt 1)) tm) :: Nil
+            Just (CConAlt _ _ _ _ _ tm) => CDefAlt (CLet "x" (CPrimOp "-" sc (CLit $ LInt 1)) tm) :: Nil
            Just tm => fatalError "ERROR succAlt mismatch \{debugStr tm}"
            _ => case find isDef alts of
              Just alt => alt :: Nil
@@ -244,13 +253,13 @@ compileDCon : Nat → QName → ConInfo → List Quant → CExp
 compileDCon ix (QN _ nm) EnumCon Nil = CLit $ LInt $ cast ix
 compileDCon ix (QN _ nm) TrueCon Nil = CLit $ LBool True
 compileDCon ix (QN _ nm) FalseCon Nil = CLit $ LBool False
-compileDCon ix (QN _ nm) info Nil = CConstr ix nm Nil Nil
+compileDCon ix (QN _ nm) info Nil = CConstr ix nm Nil Nil info
 compileDCon ix (QN _ nm) info arity =
  -- so we're fully applying this here, but dropping the args later?
  -- The weird thing is that lambdas need the
  let args = mkArgs Z arity
      alen = length' arity
-  in CFun args $ CConstr ix nm (map (\k => CBnd $ alen - k - 1) (range 0 alen)) arity
+  in CFun args $ CConstr ix nm (map (\k => CBnd $ alen - k - 1) (range 0 alen)) arity info
  where
    mkArgs : Nat → List Quant → List (Quant × String)
    mkArgs k (quant :: args) = (quant, "h\{show k}") :: mkArgs (S k) args
--- a/src/Lib/CompileJS.newt
+++ b/src/Lib/CompileJS.newt
@@ -221,7 +221,7 @@ termToJS env (CLetRec nm t u) f =
  in case termToJS env' t (JAssign nm') of
    (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f)
    t' => JSnoc (JLet nm' t') (termToJS env' u f)
-termToJS env (CConstr ix _ args qs) f = go args qs 0 (\ args => f $ LitObject (("tag", LitInt (cast ix)) :: args))
+termToJS env (CConstr ix _ args qs info) f = go args qs 0 (\ args => f $ LitObject (("tag", LitInt (cast ix)) :: args))
  where
    go : ∀ e. List CExp -> List Quant -> Int -> (List (String × JSExp) -> JSStmt e) -> JSStmt e
    go (t :: ts) (Many :: qs) ix k = termToJS env t $ \ t' => go ts qs (ix + 1) $ \ args => k $ ("h\{show ix}", t') :: args
@@ -298,19 +298,23 @@ termToJS {e} env (CCase t alts) f =
    tertiary sc t f k = JIfThen sc t f

    termToJSAlt : JSEnv -> JSExp -> CAlt -> JAlt
-    termToJSAlt env nm (CConAlt ix name info args u) = JConAlt ix (termToJS (conAltEnv nm 0 env args) u f)
+    termToJSAlt env nm (CConAlt ix name info args qs u) = JConAlt ix (termToJS (conAltEnv nm 0 env args) u f)
    -- intentionally reusing scrutinee name here
-    termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS  (env) u f)
+    termToJSAlt env nm (CDefAlt u) = JDefAlt (termToJS (env) u f)
    termToJSAlt env nm (CLitAlt lit u) = JLitAlt (litToJS lit) (termToJS env u f)

    getArgs : CAlt → List String
    getArgs (CDefAlt _) = Nil
    getArgs (CLitAlt args _) = Nil
-    getArgs (CConAlt _ _ _ args _) = args
+    getArgs (CConAlt _ _ _ args qs _) = args

    maybeCaseStmt : JSEnv -> JSExp -> List CAlt -> JSStmt e
+    -- deleteT23 does this...
+    maybeCaseStmt env sc (CDefAlt u :: Nil) = (termToJS env u f)
    -- If there is a single alt, assume it matched
-    maybeCaseStmt env sc ((CConAlt _ _ info args u) :: Nil) = (termToJS (conAltEnv sc 0 env args) u f)
+    maybeCaseStmt env sc ((CConAlt _ _ info args qs u) :: Nil) = (termToJS (conAltEnv sc 0 env args) u f)
+    maybeCaseStmt env sc alts@(CLitAlt _ u :: Nil) = termToJS env u f
+    maybeCaseStmt env sc alts@(CDefAlt u :: Nil) = termToJS env u f
    maybeCaseStmt env sc alts@(CLitAlt _ _  :: _) =
        (JCase sc (map (termToJSAlt env sc) alts))
    maybeCaseStmt env sc alts = case alts of
@@ -320,7 +324,7 @@ termToJS {e} env (CCase t alts) 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 =>
+        CConAlt ix name info args qs 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
@@ -494,7 +498,7 @@ sortedNames defs names =
  map snd $ filter (not ∘ fst) $ foldl (go Nil) Nil $ map (True,) names
  where
    getBody : CAlt → CExp
-    getBody (CConAlt _ _ _ _ t) = t
+    getBody (CConAlt _ _ _ _ _ t) = t
    getBody (CLitAlt _ t) = t
    getBody (CDefAlt t) = t

@@ -521,7 +525,7 @@ sortedNames defs names =
    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
+    getNames deep acc (CConstr _ _ ts _ info) = foldl (getNames deep) acc ts
    -- if the CRaw is called, then the deps are called
    getNames deep acc (CRaw _ deps) = map (_,_ deep) deps ++ acc
    -- wrote these out so I get an error when I add a new constructor
--- a/src/Lib/CompileScheme.newt
+++ b/src/Lib/CompileScheme.newt
@@ -18,6 +18,7 @@ import Data.SortedMap
 import Data.IORef
 import Data.SnocList

+-- FIXME SnocList
 SCEnv : U
 SCEnv = List String

@@ -64,9 +65,15 @@ scmName qn = scmIdent $ show qn

 cexpToScm : SCEnv → CExp → String

+argsToScm : SCEnv → List CExp → List Quant → List String
+argsToScm env Nil Nil = Nil
+argsToScm env (e :: es) (Many :: qs) = cexpToScm env e :: argsToScm env es qs
+argsToScm env (e :: es) (Zero :: qs) = argsToScm env es qs
+argsToScm env _ _ = fatalError "Arg count mismatch"
+
 withVar : SCEnv → CExp → (String → String) → String
-- withVar env (CBnd _) f = ?
-- withVar env (CLit _) f = ?
+-- don't rebind a variable
+withVar env (CBnd n) f = f $ getEnv n env
 withVar env t f = let nm = "wv$\{show $ length' env}"
  in "(let ((\{nm} \{cexpToScm env t})) \{f nm})"

@@ -78,8 +85,9 @@ cexpToScm env (CFun args body) = case bindAll args Lin env  of
  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
+    bindAll ((Many,nm) :: rest) acc env = case scbind nm env of
      (nm', env') => bindAll rest (acc :< nm') env'
+    bindAll ((Zero,nm) :: rest) acc env = bindAll rest acc ("#f" :: 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
@@ -99,7 +107,8 @@ cexpToScm env (CAppRef nm args quants) =
    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) (Many :: qs) = go env "\{acc} \{arg}" args qs
+    go env acc (arg :: args) (Zero :: qs) = go env acc 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
@@ -110,19 +119,58 @@ cexpToScm env (CCase sc alts) = do
    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
+    conAlt : SCEnv → String → Int → List String → List Quant → CExp → String
+    conAlt env nm ix Nil Nil body = cexpToScm env body
+    conAlt env nm ix (arg :: args) (Many :: qs) body =
+        conAlt ("(vector-ref \{nm} \{show ix})" :: env) nm (ix + 1) args qs body
+    conAlt env nm ix (arg :: args) (Zero :: qs) body = conAlt ("#f" :: env) nm ix args qs body
+    conAlt env nm ix _ _ body = fatalError "arg/qs mismatch in conAlt"

+    nilAlt : SCEnv → List Quant → CExp → String
+    nilAlt env Nil body = cexpToScm env body
+    nilAlt env (Zero :: qs) body = nilAlt ("#f" :: env) qs body
+    nilAlt env (Many :: qs) body = fatalError "Non-empty field on nil constructor"
+
+    consAlt' : SCEnv → List String → List Quant → CExp → String
+    consAlt' env nms Nil body = cexpToScm env body
+    consAlt' env nms (Zero :: qs) body = consAlt' ("#f" :: env) nms qs body
+    consAlt' env Nil (Many :: qs) body = fatalError "Too many fields on cons constructor"
+    consAlt' env (nm :: nms) (Many :: qs) body = consAlt' (nm :: env) nms qs body
+
+    consAlt : SCEnv → String → List Quant → CExp → String
+    consAlt env nm qs body = consAlt' env ("(car \{nm})" :: "(cdr \{nm})" :: Nil) qs body
+
+    -- an alt branch in a `case` statement
+    -- for the Nil/Cons case, we're not inside a `case`.
    doAlt : String → CAlt → String
-    doAlt nm (CConAlt tag cname _ args body) = "((\{show tag}) \{conAlt env nm Lin args body})"
+    doAlt nm (CConAlt tag cname _ args qs body) = "((\{show tag}) \{conAlt env nm 1 args qs body})"
    doAlt nm (CDefAlt body) = "(else \{cexpToScm env body})"
    doAlt nm (CLitAlt lit body) = "((\{scmLit lit}) \{cexpToScm env body})"

+    -- doCase decides the top level path - case/cond/if/...
    doCase : String → List CAlt → String
+    doCase nm (CDefAlt body :: Nil) = cexpToScm env body
+    doCase nm (cons@(CConAlt tag cname ConsCon args qs body ) :: rest) =
+      let consBranch = consAlt env nm qs body in
+      case rest of
+        Nil => consBranch
+        (CDefAlt body :: Nil) => "(if (null? \{nm}) \{cexpToScm env body} \{consBranch})"
+        (CConAlt _ _ NilCon _ qs body :: _) => "(if (null? \{nm}) \{nilAlt env qs body} \{consBranch})"
+        (CConAlt _ _ info _ _ _ :: _) => fatalError "\{show info} alt after cons"
+        (CLitAlt _ _ :: _) => fatalError "lit alt after cons"
+        _ => fatalError "too many alts after cons"
+    doCase nm (cons@(CConAlt tag cname NilCon args qs body ) :: rest) =
+      let nilBranch = consAlt env nm qs body in
+      case rest of
+        Nil => nilBranch
+        (CDefAlt body :: Nil) => "(if (null? \{nm}) \{nilBranch} \{cexpToScm env body})"
+        (CConAlt _ _ ConsCon _ qs body :: _) => "(if (null? \{nm}) \{nilBranch} \{consAlt env nm qs body})"
+        (CConAlt _ _ info _ _ _ :: _) => fatalError "\{show info} alt after nil"
+        (CLitAlt _ _ :: _) => fatalError "lit alt after nil"
+        _ => fatalError "too many alts after cons"
+    doCase nm (CConAlt tag cname _ args qs body :: Nil) = conAlt env nm 1 args qs body
+    doCase nm (CLitAlt _ body :: Nil) = cexpToScm env body
+    doCase nm (CDefAlt body :: Nil) = cexpToScm env body
    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})"

@@ -138,16 +186,16 @@ cexpToScm env (CLetRec nm t 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"
+cexpToScm env (CConstr tag nm args quants NilCon) = "'()"
+cexpToScm env (CConstr tag nm args quants ConsCon) = case argsToScm env args quants of
+  (a :: b :: Nil) => "(cons \{a} \{b})"
+  _ => fatalError "Wrong number of args on a ConsCon"
+cexpToScm env (CConstr tag nm args quants info) = "(vector \{show tag} \{unwords $ argsToScm env args quants})"
+-- Should be handled by the caller
+cexpToScm env (CRaw _ _) = fatalError "Stray 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
@@ -215,13 +263,13 @@ 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?

 -/
-
+-- TODO factor out to CompilerCommon
 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 (CConAlt _ _ _ _ _ t) = t
    getBody (CLitAlt _ t) = t
    getBody (CDefAlt t) = t

@@ -248,7 +296,7 @@ sortedNames defs names =
    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
+    getNames deep acc (CConstr _ _ ts _ info) = 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
--- a/src/Lib/Elab.newt
+++ b/src/Lib/Elab.newt
@@ -80,6 +80,18 @@ lookupDef ctx name = go 0 ctx.types ctx.env
    go ix ((nm, ty) :: xs) (v :: vs) = if nm == name then Just v else go (1 + ix) xs vs
    go ix _ _ = Nothing

+expandList : FC → Maybe Raw → Raw
+expandList fc Nothing = RVar fc "Nil"
+expandList fc (Just t) = go fc t
+  where
+    cons : FC → Raw → Raw → Raw
+    cons fc t u = RApp fc (RApp fc (RVar fc "_::_") t Explicit) u Explicit
+
+    go : FC → Raw → Raw
+    go fc (RApp fc' (RApp fc'' (RVar fc "_,_") t Explicit) u Explicit) =
+      cons fc t $ go fc u
+    go fc t = cons fc t (RVar fc "Nil")
+
 forceMeta : Val -> M Val
 forceMeta (VMeta fc ix sp) = do
  meta <- lookupMeta ix
@@ -118,10 +130,10 @@ isCandidate _ _ = False

 setMetaMode : MetaMode → M Unit
 -- ideally we would support dotted paths like metaCtx.mcmode := CheckFirst
-setMetaMode mcmode = modifyTop [ currentMod $= [modMetaCtx $= [mcmode := mcmode] ] ]
+setMetaMode mcmode = modifyTop { currentMod $= {modMetaCtx $= {mcmode := mcmode} } }

 setMetaContext : MetaContext → M Unit
-setMetaContext mc = modifyTop [ currentMod $= [ modMetaCtx := mc ]]
+setMetaContext mc = modifyTop { currentMod $= { modMetaCtx := mc }}

 findMatches : Context -> Val -> List (QName × Tm) -> M (List QName)
 findMatches ctx ty Nil = pure Nil
@@ -138,7 +150,6 @@ findMatches ctx ty ((name, type) :: xs) = do
      debug $ \ _ => "TRY \{show name} : \{rpprint Nil type} for \{show ty}"
      -- This check is solving metas, so we save mc below in case we want this solution
      let (QN ns nm) = name
-      let (cod, tele) = splitTele type
      setMetaMode CheckFirst
      tm <- check ctx (RVar fc nm) ty
      debug $ \ _ => "Found \{rpprint Nil tm} for \{show ty}"
@@ -256,7 +267,7 @@ updateMeta ix f = do
  let autos = case me of
    Solved _ _ _ => filter (_/=_ ix) mc.autos
    _ => mc.autos
-  setMetaContext $ [metas $= updateMap ix me; autos := autos] mc
+  setMetaContext $ {metas $= updateMap ix me; autos := autos} mc

 -- Try to solve autos that reference the meta ix
 checkAutos : QName -> List QName -> M Unit
@@ -344,19 +355,10 @@ rename meta ren lvl (VPi fc n icit rig ty tm) = do
  pure (Pi fc n icit rig ty' scope')
 rename meta ren lvl (VU fc) = pure (UU fc)
 rename meta ren lvl (VErased fc) = pure (Erased fc)
-- for now, we don't do solutions with case in them.
-rename meta ren lvl (VCase fc sc alts) = error fc "Case in solution"
 rename meta ren lvl (VLit fc lit) = pure (Lit fc lit)
-rename meta ren lvl (VLet fc name val body) = do
-  val' <- rename meta ren lvl val
-  body' <- rename meta (lvl :: ren) (1 + lvl) body
-  pure $ Let fc name val' body'
-- these probably shouldn't show up in solutions...
-rename meta ren lvl (VLetRec fc name ty val body) = do
-  ty' <- rename meta ren lvl ty
-  val' <- rename meta (lvl :: ren) (1 + lvl) val
-  body' <- rename meta (lvl :: ren) (1 + lvl) body
-  pure $ LetRec fc name ty' val' body'
+-- for now, we don't do solutions with case, let, letrec in them
+-- If we we need this, follow the model of VLam
+rename meta ren lvl tm = error (getFC tm) "Unhandled term in `rename`: \{show tm}"

 lams : Nat -> List String -> Tm -> Tm
 lams Z _ tm = tm
@@ -628,7 +630,7 @@ freshMeta ctx fc ty kind = do
  let autos = case kind of
      AutoSolve => qn :: mc.autos
      _ => mc.autos
-  setMetaContext $ [ metas $= updateMap qn newmeta; autos := autos; next $= 1 +] mc
+  setMetaContext $ { metas $= updateMap qn newmeta; autos := autos; next $= 1 +} mc

  -- I tried checking Auto immediately if CheckAll, but there isn't enough information yet.
  pure $ applyBDs 0 (Meta fc qn) ctx.bds
@@ -749,7 +751,6 @@ substVal k v tm = go tm
  where
    go : Val -> Val
    go (VVar fc j sp) = if j == k then v else (VVar fc j (map go sp))
-    go (VLet fc nm a b) = VLet fc nm (go a) b
    go (VPi fc nm icit rig a b) = VPi fc nm icit rig (go a) b
    go (VMeta fc ix sp) = VMeta fc ix (map go sp)
    go (VRef fc nm sp) = VRef fc nm (map go sp)
@@ -988,6 +989,7 @@ mkPat (RAs fc as tm, icit) = do
    (PatCon fc icit nm args Nothing) => pure $ PatCon fc icit nm args (Just as)
    (PatCon fc icit nm args _) => error fc "Double as pattern \{show tm}"
    t => error fc "Can't put as on non-constructor \{show tm}"
+mkPat (RList fc mt, icit) = mkPat (expandList fc mt, icit)
 mkPat (tm, icit) = do
  top <- getTop
  case splitArgs tm Nil of
@@ -1549,6 +1551,8 @@ infer ctx (RVar fc nm) = go 0 ctx.types
    go i ((x, ty) :: xs) = if x == nm then pure (Bnd fc i, ty)
      else go (i + 1) xs

+infer ctx (RList fc mt) = infer ctx $ expandList fc mt
+
 infer ctx (RApp fc t u icit) = do
  -- If the app is explicit, add any necessary metas
  (icit, t, tty) <- case icit of
--- a/src/Lib/Erasure.newt
+++ b/src/Lib/Erasure.newt
@@ -96,7 +96,7 @@ erase env t sp = case t of
    eraseSpine env (LetRec fc nm ty u' v') sp Nothing
  (Bnd fc k) => do
    case getAt (cast k) env of
-      Nothing => error fc "bad index \{show k}"
+      Nothing => error fc "Erase: bad index \{show k}"
      Just (nm, Zero, ty) => error fc "used erased value \{show nm} (FIXME FC may be wrong here)"
      Just (nm, Many, ty) => eraseSpine env t sp ty
  (UU fc) => eraseSpine env t sp (Just $ UU fc)
--- a/src/Lib/Eval.newt
+++ b/src/Lib/Eval.newt
@@ -9,10 +9,11 @@ import Lib.TopContext
 import Data.IORef
 import Data.SnocList
 import Data.SortedMap
+import Lib.Error

 eval : Env -> Tm -> M Val

-- REVIEW everything is evalutated whether it's needed or not
+-- REVIEW everything is evaluated whether it's needed or not
 -- It would be nice if the environment were lazy.
 -- e.g. case is getting evaluated when passed to a function because
 -- of dependencies in pi-types, even if the dependency isn't used
@@ -27,6 +28,7 @@ vapp (VLam _ _ _ _ t) u = t $$ u
 vapp (VVar fc k sp) u = pure $ VVar fc k (sp :< u)
 vapp (VRef fc nm sp) u = pure $ VRef fc nm (sp :< u)
 vapp (VMeta fc k sp) u = pure $ VMeta fc k (sp :< u)
+-- not really impossible, could be a stuck VCase.
 vapp t u = error' "impossible in vapp \{show t} to \{show u}\n"

 vappSpine : Val -> SnocList Val -> M Val
@@ -50,7 +52,7 @@ unlet : Env -> Val -> M Val
 unlet env t@(VVar fc k sp) = case lookupVar env k of
      Just tt@(VVar fc' k' sp') => do
        debug $ \ _ =>  "lookup \{show k} is \{show tt}"
-        if k' == k then pure t else (vappSpine (VVar fc' k' sp') sp >>= unlet env)
+        if k' == k then pure t else (vappSpine tt sp >>= unlet env)
      Just t => vappSpine t sp >>= unlet env
      Nothing => do
        debug $ \ _ =>  "lookup \{show k} is Nothing in env \{show env}"
@@ -69,8 +71,9 @@ tryEval env (VRef fc k sp) = do
            vtm <- eval env tm
            debug $ \ _ =>  "tm is \{render 90 $ pprint Nil tm}"
            val <- vappSpine vtm sp
+            -- These are considered "stuck" and we back out to the nearest name application
            case val of
-              VCase _ _ _ => pure Nothing
+              VCase _ _ _ _ => pure Nothing
              VLam _ _ _ _ _ => pure Nothing
              -- For now? There is a spot in Compile.newt that has
              -- two applications of fresh that is getting unfolded even
@@ -78,7 +81,7 @@ tryEval env (VRef fc k sp) = do
              -- coming out of a let and is instantly applied
              VLetRec _ _ _ _ _ => pure Nothing
              v => pure $ Just v)
-            (\ _ => pure Nothing)
+            (const $ pure Nothing)
      _ => do
        debug $ \ _ => "tryEval blocked on undefined \{show k}"
        pure Nothing
@@ -98,7 +101,7 @@ forceType env x = do
    | _ => pure x
  forceType env x'

-- for cases applied to a value
+-- Handles cases applied to a value, return Nothing if stuck
 -- TODO this does not handle CaseLit
 evalCase : Env -> Val -> List CaseAlt -> M (Maybe Val)
 evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
@@ -112,40 +115,19 @@ evalCase env sc@(VRef _ nm sp) (cc@(CaseCons name nms t) :: xs) = do
      -- bail for a stuck function
      _ => pure Nothing
  where
+    -- put constructor args into scope
    pushArgs : Env -> List Val -> List String -> M (Maybe Val)
    pushArgs env (arg :: args) (nm :: nms) = pushArgs (arg :: env) args nms
-    pushArgs env args Nil = do
-      t' <- eval env t
-      Just <$> vappSpine t' (Lin <>< args)
+    pushArgs env Nil Nil = Just <$> eval env t
+    pushArgs env args Nil = fatalError "Extra args \{show args}"
    pushArgs env Nil rest = pure Nothing
-- REVIEW - this is handled in the caller already
-evalCase env sc@(VVar fc k sp) alts = case lookupVar env k of
-    Just tt@(VVar fc' k' sp') => do
-        debug $ \ _ =>  "lookup \{show k} is \{show tt}"
-        if k' == k
-          then pure Nothing
-          else do
-            val <- vappSpine (VVar fc' k' sp') sp
-            evalCase env val alts
-    Just t => do
-      val <- vappSpine t sp
-      evalCase env val alts
-    Nothing => do
-        debug $ \ _ =>  "lookup \{show k} is Nothing in env \{show env}"
-        pure Nothing
+
 evalCase env sc (CaseDefault u :: xs) = Just <$> eval env u
 evalCase env sc cc = do
  debug $ \ _ =>  "CASE BAIL sc \{show sc} vs " -- \{show cc}"
  debug $ \ _ =>  "env is \{show env}"
  pure Nothing

-- neutral alts
-evalAlt : Env → CaseAlt → M VCaseAlt
-evalAlt env (CaseDefault tm) = VCaseDefault <$> eval env tm
-evalAlt env (CaseLit lit tm) = VCaseLit lit <$> eval env tm
-- in the cons case, we're binding args
-evalAlt env (CaseCons nm args tm) = pure $ VCaseCons nm args env tm
-
 -- So smalltt says:
 --   Smalltt has the following approach:
 --   - Top-level and local definitions are lazy.
@@ -173,13 +155,19 @@ eval env (Pi fc x icit rig a b) = do
  pure $ VPi fc x icit rig a' (MkClosure env b)
 eval env (Let fc nm t u) = do
  t' <- eval env t
-  u' <- eval (VVar fc (length' env) Lin :: env) u
-  pure $ VLet fc nm t' u'
+  --
+  if True
+    then pure $ VLet fc nm t' (MkClosure env u)
+    else eval (t' :: env) u
 eval env (LetRec fc nm ty t u) = do
-  ty' <- eval env ty
-  t' <- eval (VVar fc (length' env) Lin :: env) t
-  u' <- eval (VVar fc (length' env) Lin :: env) u
-  pure $ VLetRec fc nm ty' t' u'
+  -- Used for `where`, we'd probably need to treat this like Lam.
+  error fc "eval letrec"
+  -- I think we need to handle this like lam/let, disabled for now.
+  -- It should be gone by the time we hit inlining, we'll see if it arises in other cases
+  -- ty' <- eval env ty
+  -- t' <- eval (VVar fc (length' env) Lin :: env) t
+  -- u' <- eval (VVar fc (length' env) Lin :: env) u
+  -- pure $ VLetRec fc nm ty' t' u'
 -- Here, we assume env has everything. We push levels onto it during type checking.
 -- I think we could pass in an l and assume everything outside env is free and
 -- translate to a level
@@ -191,15 +179,13 @@ eval env (Lit fc lit) = pure $ VLit fc lit
 eval env tm@(Case fc sc alts) = do
  -- TODO we need to be able to tell eval to expand aggressively here.
  sc' <- eval env sc
-  sc' <- unlet env sc' -- try to expand lets from pattern matching
-  -- possibly too aggressive?
+  -- inline metas and do beta reduction at head
  sc' <- forceType env sc'
  Nothing <- evalCase env sc' alts
    | Just v => pure v

  vsc <- eval env sc
-  alts' <- traverse (evalAlt env) alts
-  pure $ VCase fc vsc alts'
+  pure $ VCase fc vsc env alts

 quote : (lvl : Int) -> Val -> M Tm

@@ -210,10 +196,14 @@ quoteSp lvl t (xs :< x) = do
  x' <- quote lvl x
  pure $ App emptyFC t' x'

-quoteAlt : Int → VCaseAlt → M CaseAlt
-quoteAlt l (VCaseDefault val) = CaseDefault <$> quote l val
-quoteAlt l (VCaseLit lit val) = CaseLit lit <$> quote l val
-quoteAlt l (VCaseCons nm args env tm) = do
+normAlt : Env → Int → CaseAlt → M CaseAlt
+normAlt env l (CaseDefault tm) = do
+   val <- eval env tm
+   CaseDefault <$> quote l val
+normAlt env l (CaseLit lit tm) = do
+   val <- eval env tm
+   CaseLit lit <$> quote l val
+normAlt env l (CaseCons nm args tm) = do
  val <- eval (mkenv l env args) tm
  tm <- quote (length' args + l) val
  pure $ CaseCons nm args tm
@@ -224,7 +214,7 @@ quoteAlt l (VCaseCons nm args env tm) = do

 quote l (VVar fc k sp) = if k < l
  then quoteSp l (Bnd fc (lvl2ix l k )) sp -- level to index
-  else error fc "Bad index in quote \{show k} depth \{show l}"
+  else error fc "Bad level in quote \{show k} depth \{show l}"
 quote l (VMeta fc i sp) = do
  meta <- lookupMeta i
  case meta of
@@ -241,6 +231,7 @@ quote l (VPi fc x icit rig a b) = do
  pure $ Pi fc x icit rig a' tm
 quote l (VLet fc nm t u) = do
  t' <- quote l t
+  u <- u $$ VVar fc l Lin
  u' <- quote (1 + l) u
  pure $ Let fc nm t' u'
 quote l (VLetRec fc nm ty t u) = do
@@ -250,10 +241,11 @@ quote l (VLetRec fc nm ty t u) = do
  pure $ LetRec fc nm ty' t' u'
 quote l (VU fc) = pure (UU fc)
 quote l (VRef fc n sp) = quoteSp l (Ref fc n) sp
-quote l (VCase fc sc valts) = do
+quote l (VCase fc sc env alts) = do
  sc' <- quote l sc
-  alts <- traverse (quoteAlt l) valts
-  pure $ Case fc sc' alts
+  alts' <- traverse (normAlt env l) alts
+  pure $ Case fc sc' alts'
+
 quote l (VLit fc lit) = pure $ Lit fc lit
 quote l (VErased fc) = pure $ Erased fc

@@ -268,7 +260,6 @@ prvalCtx {{ctx}} v = do
  tm <- quote ctx.lvl v
  pure $ render 90 $ pprint (map fst ctx.types) tm

-
 -- 'zonk' is substituting metas _and_ doing inlining

 -- It is a flavor of eval, maybe we could combine them with some flags
@@ -309,23 +300,37 @@ zonkApp top l env t@(Meta fc k) sp = do
  meta <- lookupMeta k
  case meta of
    (Solved _ j v) => do
+      debug $ \ _ => "zonk for \{show k} env \{show env}"
+      debug $ \ _ => "spine \{show sp}"
      sp' <- traverse (eval env) sp
-      debug $ \ _ =>  "zonk \{show k} -> \{show v} spine \{show sp'}"
+      debug $ \ _ =>  "zonk meta \{show k} -> \{show v} spine \{show sp'}"
      foo <- vappSpine v (Lin <>< sp')
      debug $ \ _ =>  "-> result is \{show foo}"
-      tweakFC fc <$> quote l foo
+      if length' env /= l
+        then fatalError "MM2 \{show l} /= \{show $ length' env}"
+        else pure MkUnit
+      res <- tweakFC fc <$> quote l foo
+      debug $ \ _ => "quoted \{show res}"
+      pure res
    _ => pure $ appSpine t sp
 zonkApp top l env t sp = do
+  debug $ \ _ => "zonk2 for \{show t} env \{show env}"
+  debug $ \ _ => "spine \{show sp}"
  t' <- zonk top l env t
  -- inlining
  let (Just tm) = inlineDef t' | _ => pure $ appSpine t' sp
  sp' <- traverse (eval env) sp
  vtm <- eval env tm
  catchError (do
-    foo <- vappSpine vtm (Lin <>< sp')
-    t' <- quote l foo
-    zonk top l env t')
-    (\_ => pure $ appSpine t' sp)
+    debug $ \ _ =>  "zonk will app \{show t'} @ \{show sp} ~> \{show vtm} @ \{show sp'}"
+    res <- vappSpine vtm (Lin <>< sp')
+    debug $ \_ => "result is \{show res}"
+    t' <- quote l res
+    x <- zonk top l env t'
+    pure x)
+    (\err => do
+      debug $ \_ => "result err \{showError "" err}"
+      pure $ appSpine t' sp)
  where
    -- lookup name and return Def if flagged inline
    inlineDef : Tm → Maybe Tm
--- a/src/Lib/LiftLambda.newt
+++ b/src/Lib/LiftLambda.newt
@@ -38,8 +38,8 @@ liftLambdaTm name env tm@(CCase t alts) = do
    liftLambdaAlt : CAlt → State ExpMap CAlt
    liftLambdaAlt (CDefAlt tm) = CDefAlt <$> liftLambdaTm name env tm
    liftLambdaAlt (CLitAlt l tm) = CLitAlt l <$> liftLambdaTm name env tm
-    liftLambdaAlt (CConAlt ix nm info args tm) =
-      CConAlt ix nm info args <$> liftLambdaTm name (env <>< map (_,_ Many) args) tm
+    liftLambdaAlt (CConAlt ix nm info args qs tm) =
+      CConAlt ix nm info args qs <$> liftLambdaTm name (env <>< map (_,_ Many) args) tm
 liftLambdaTm name@(QN ns nm) env tm@(CLam nm t) = do
  let (nms, t) = splitLam tm Lin
  t' <- liftLambdaTm name (env <>< nms) t
--- a/src/Lib/LiftWhere.newt
+++ b/src/Lib/LiftWhere.newt
@@ -52,7 +52,7 @@ liftWhereTm name env (LetRec fc nm ty t u) = do
  modifyRef Defs (updateMap qn (Fn $ wrapLam qs t'))

  -- The rest
-  u' <- liftWhereTm qn env' u
+  u' <- liftWhereTm name env' u
  pure $ LetRec fc nm (Erased fc) (Erased fc) u'
  where
    -- TODO might be nice if we could nest the names (Foo.go.go) for nested where
--- a/src/Lib/Parser.newt
+++ b/src/Lib/Parser.newt
@@ -28,7 +28,7 @@ parenWrap pa = do
  pure t

 braces : ∀ a. Parser a -> Parser a
-braces pa = do
+braces pa = try $ do
  symbol "{"
  t <- pa
  symbol "}"
@@ -107,9 +107,17 @@ asAtom = do
    Just exp => pure $ RAs fc nm exp
    Nothing  => pure $ RVar fc nm

-- the inside of Raw
+
 recordUpdate : Parser Raw

+listTypeExp : Parser Raw
+listTypeExp = do
+  fc <- getPos
+  symbol "["
+  tm <- optional typeExpr
+  symbol "]"
+  pure $ RList fc tm
+
 parenTypeExp : Parser Raw
 parenTypeExp = do
  fc <- getPos
@@ -126,6 +134,7 @@ atom : Parser Raw
 atom = do
  pure MkUnit
  RU <$> getPos <* keyword "U"
+    <|> recordUpdate
    -- <|> RVar <$> getPos <*> ident
    <|> asAtom
    <|> RVar <$> getPos <*> uident
@@ -133,8 +142,8 @@ atom = do
    <|> lit
    <|> RImplicit <$> getPos <* keyword "_"
    <|> RHole <$> getPos <* keyword "?"
+    <|> listTypeExp
    <|> parenTypeExp
-    <|> recordUpdate

 updateClause : Parser UpdateClause
 updateClause = do
@@ -146,15 +155,15 @@ updateClause = do
    True => pure $ AssignField fc nm tm
    _    => pure $ ModifyField fc nm tm

-- ambiguity vs {a} or {a} -> ... is tough, we can do [] or put a keyword in front.
 recordUpdate = do
  fc <- getPos
-  symbol "["
+  symbol "{"
  clauses <- sepBy (symbol ";") updateClause
-  symbol "]"
+  symbol "}"
  tm <- optional atom
  pure $ RUpdateRec fc clauses tm

+
 -- Argument to a Spine
 pArg : Parser (Icit × FC × Raw)
 pArg = do
@@ -454,11 +463,14 @@ ebind = do

 ibind : Parser Telescope
 ibind = do
-  -- I've gone back and forth on this, but I think {m a b} is more useful than {Int}
-  symbol "{"
-  quant <- quantity
-  names <- (some (addPos varname))
-  ty <- symbol ":" *> typeExpr
+  -- we don't know if it's an ibind or record update until we hit the `:`
+  (quant, names) <- try $ do
+    symbol "{"
+    quant <- quantity
+    names <- (some (addPos varname))
+    symbol ":"
+    pure (quant, names)
+  ty <- typeExpr
  symbol "}"
  pure $ map (makeBind quant (Just ty)) names
  where
--- a/src/Lib/ProcessDecl.newt
+++ b/src/Lib/ProcessDecl.newt
@@ -54,6 +54,8 @@ logMetas (Unsolved fc k ctx ty User cons :: rest) = do
      let msg = "\{env}\n  -----------\n  \{render 90 $ pprint names ty'}"
      info fc "User Hole\n\{msg}"
      logMetas rest
+-- error is reported separately
+logMetas (Unsolved fc k ctx ty ErrorHole cons :: rest) = logMetas rest
 logMetas (Unsolved fc k ctx ty kind cons :: rest) = do
      ty' <- forceMeta ty
      tm <- quote ctx.lvl ty'
@@ -308,7 +310,7 @@ processInstance ns instfc ty decls = do
  vdcty@(VPi _ nm icit rig a b) <- eval Nil dcty
    | x => error (getFC x) "dcty not Pi"
  debug $ \ _ => "dcty \{render 90 $ pprint Nil dcty}"
-  let (_,args) = funArgs codomain
+  -- let (_,args) = funArgs codomain

  debug $ \ _ => "traverse \{show $ map show args}"
  -- This is a little painful because we're reverse engineering the
@@ -408,17 +410,31 @@ processShortData ns fc lhs sigs = do
    mkDecl args acc tm = error (getFC tm) "Expected contructor application, got: \{show tm}"

 -- Identify Nat-like, enum-like, etc
+-- TODO handle erased fields
 populateConInfo : List TopEntry → List TopEntry
 populateConInfo entries =
  let (Nothing) = traverse checkEnum entries
    -- Boolean
    | Just (a :: b :: Nil) => (setInfo a FalseCon :: setInfo b TrueCon :: Nil)
    | Just entries => entries in
-  let (a :: b :: Nil) = entries | _ => entries in
-  let (Just succ) = find isSucc entries | _ => entries in
-  let (Just zero) = find isZero entries | _ => entries in
-  setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil
+  case entries of
+    a :: Nil => case countFields a of
+      0 => setInfo a NilCon :: Nil
+      2 => setInfo a ConsCon :: Nil
+      _ => entries
+    a :: b :: Nil =>
+      fromMaybe entries $ checkNat entries <|> checkCons entries
+    _ => entries
  where
+    countFields : TopEntry → Int
+    countFields (MkEntry fc name type def eflags) = go type
+     where
+       go : Tm → Int
+       go (Pi fc nm _ Zero a b) = go b
+       go (Pi fc nm _ Many a b) = 1 + go b
+       go _ = 0
+    countFields _ = 0
+
    setInfo : TopEntry → ConInfo → TopEntry
    setInfo (MkEntry fc nm dty (DCon ix _ arity hn) flags) info = MkEntry fc nm dty (DCon ix info arity hn) flags
    setInfo x _ = x
@@ -431,11 +447,26 @@ populateConInfo entries =
    isZero (MkEntry fc nm dty (DCon _ _ Nil hn) flags) = True
    isZero _ = False

-    -- TODO - handle indexes, etc
+    -- TODO - handle indexes, erased fields, etc
    isSucc : TopEntry → Bool
    isSucc (MkEntry fc nm dty@(Pi _ _ _ _ (Ref _ a) (Ref _ b)) (DCon _ _ (Many :: Nil) hn) _) = a == b
    isSucc _ = False

+    -- assumes we've filtered down to two entries
+    checkNat : List TopEntry → Maybe (List TopEntry)
+    checkNat entries = do
+      succ <- find isSucc entries
+      zero <- find isZero entries
+      pure $ setInfo zero ZeroCon :: setInfo succ SuccCon :: Nil
+
+
+    -- assumes we've filtered down to two entries
+    checkCons : List TopEntry → Maybe (List TopEntry)
+    checkCons entries = do
+      nil <- find (\ x => countFields x == 0) entries
+      cons <- find (\x => countFields x == 2) entries
+      pure $ setInfo nil NilCon :: setInfo cons ConsCon :: Nil
+
 processData : String → FC → FC × String → Raw → List Decl → M Unit
 processData ns fc (nameFC, nm) ty cons = do
  log 1 $ \ _ => "-----"
@@ -516,9 +547,6 @@ processRecord ns recordFC (nameFC, nm) tele cname decls = do
    processFields : Raw → Raw → List (String × Raw) → List (FC × String × Raw) → M Unit
    processFields _ _ _ Nil = pure MkUnit
    processFields autoPat tail deps ((fc,name,ty) :: rest) = do
-      -- TODO dependency isn't handled yet
-      -- we'll need to replace stuff like `len` with `len self`.
-
      let funType = substRaw deps $ teleToPi (impTele tele) $ RPi fc (BI fc "$self" Explicit Many) tail ty

      -- `.fieldName`
--- a/src/Lib/ProcessModule.newt
+++ b/src/Lib/ProcessModule.newt
@@ -17,13 +17,13 @@ import Lib.Elab
 -- declare internal primitives
 addPrimitives : M ModContext
 addPrimitives = do
-  modifyTop [ currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap ]
+  modifyTop { currentMod := emptyModCtx "Prim" ""; hints := emptyMap; ops := emptyMap }
  processDecl primNS (PType emptyFC "Int" Nothing)
  processDecl primNS (PType emptyFC "String" Nothing)
  processDecl primNS (PType emptyFC "Char" Nothing)
  setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
  top <- getTop
-  modifyTop [ modules $= updateMap primNS top.currentMod ]
+  modifyTop { modules $= updateMap primNS top.currentMod }
  pure top.currentMod

 record FileSource where
@@ -74,12 +74,12 @@ processModule importFC repo stk modns = do

  -- Dummy for initial load/parse
  let mod = MkModCtx modns "" emptyMap freshMC emptyMap Nil Nil Nil
-  modifyTop [ currentMod := mod; hints := emptyMap; ops := emptyMap ]
+  modifyTop { currentMod := mod; hints := emptyMap; ops := emptyMap }

  -- TODO now we can pass in the module name...
  Right (fn,src) <- tryError $ repo.getFile importFC fn
    | Left err => reportError err  -- TODO maybe want a better FC.
-  modifyTop [ currentMod $= [ modSource := src ]]
+  modifyTop { currentMod $= { modSource := src }}

  let (Right toks) = tokenise fn src
    | Left err => reportError err
@@ -108,10 +108,10 @@ processModule importFC repo stk modns = do
  -- currentMod has been wiped by imports..
  let freshMC = MC emptyMap Nil 0 CheckAll
  let mod = MkModCtx modns src emptyMap freshMC emptyMap imported Nil Nil
-  modifyTop [ currentMod := mod
+  modifyTop { currentMod := mod
            ; hints := emptyMap
            ; ops := ops
-            ]
+            }

  -- top hints / ops include all directly imported modules
  top <- getTop
@@ -119,7 +119,7 @@ processModule importFC repo stk modns = do
    (MkImport fc (nameFC, ns)) => do
      let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
      importHints (listValues mod.modDefs)
-      modifyTop [ ops $= mergeOps mod.modOps ]
+      modifyTop { ops $= mergeOps mod.modOps }

      -- add error if an import contains an error
      -- maybe move this to after reporting
@@ -135,7 +135,7 @@ processModule importFC repo stk modns = do
  -- aside from reworking parsing, we could filter
  -- other options are removing updates from parsing (so we must use incremental parsing)
  -- or removing pratt from parsing (so it happens in elaboration)
-  modifyTop [ currentMod $= [ modOps := ops ] ]
+  modifyTop { currentMod $= { modOps := ops } }

  log 1 $ \ _ => "process Decls"
  traverse (tryProcessDecl src modns) (collectDecl decls)
@@ -151,7 +151,7 @@ processModule importFC repo stk modns = do
  -- update modules with result, leave the rest of context in case this is top file
  top <- getTop
  let modules = updateMap modns top.currentMod top.modules
-  modifyTop [modules := modules]
+  modifyTop {modules := modules}

  pure top.currentMod
  where
@@ -159,7 +159,7 @@ processModule importFC repo stk modns = do
    reportError err = do
      addError err
      top <- getTop
-      modifyTop [modules $= updateMap modns top.currentMod ]
+      modifyTop {modules $= updateMap modns top.currentMod }
      pure top.currentMod

    tryProcessDecl : String → String → Decl → M Unit
@@ -174,7 +174,7 @@ invalidateModule modname = do
  let modules = join $ map getDeps $ toList top.modules
  let revMap = map swap modules
  let deps = foldl accumulate emptyMap revMap
-  go deps $ modname :: Nil
+  modifyTop { modules $= go deps (modname :: Nil) }
  where
    accumulate : SortedMap String (List String) → String × String → SortedMap String (List String)
    accumulate deps (k,v) = let prev = fromMaybe Nil $ lookupMap' k deps
@@ -183,9 +183,10 @@ invalidateModule modname = do
    getDeps : String × ModContext → List (String × String)
    getDeps (nm, mod) = map (nm , ) mod.modDeps

-    go : SortedMap String (List String) → List String → M Unit
-    go deps Nil = pure MkUnit
-    go deps (name :: names) = do
-      modifyTop [modules $= deleteMap name]
-      let ds = fromMaybe Nil $ lookupMap' name deps
-      go deps $ ds ++ names
+    go : SortedMap String (List String) → List String → SortedMap String ModContext → SortedMap String ModContext
+    go deps Nil mods = mods
+    go deps (name :: names) mods =
+      -- Have we hit this name already?
+      let (Just _) = lookupMap name mods | _ => go deps names mods in
+      let ds = fromMaybe Nil $ lookupMap' name deps in
+      go deps (ds ++ names) (deleteMap name mods)
--- a/src/Lib/Syntax.newt
+++ b/src/Lib/Syntax.newt
@@ -60,6 +60,7 @@ data Raw : U where
  -- has to be applied or we have to know its type as Foo → Foo to elaborate.
  -- I can bake the arg in here, or require an app in elab.
  RUpdateRec : (fc : FC) → List UpdateClause → Maybe Raw → Raw
+  RList : (fc : FC) → Maybe Raw → Raw

 instance HasFC Raw where
  getFC (RVar fc nm) = fc
@@ -78,6 +79,7 @@ instance HasFC Raw where
  getFC (RAs fc _ _) = fc
  getFC (RUpdateRec fc _ _) = fc
  getFC (RImpossible fc) = fc
+  getFC (RList fc _) = fc

 data Import = MkImport FC (FC × Name)

@@ -189,6 +191,8 @@ instance Pretty Raw where
    asDoc p (RWhere _ dd b) = text "TODO pretty RWhere"
    asDoc p (RAs _ nm x) = text nm ++ text "@(" ++ asDoc 0 x ++ text ")"
    asDoc p (RUpdateRec _ clauses tm) = text "{" <+> text "TODO RUpdateRec" <+> text "}"
+    asDoc p (RList _ (Just t)) = text "[" <+> asDoc p t <+> text "]"
+    asDoc p (RList _ Nothing) = text "[]"

 prettyBind : (BindInfo × Raw) -> Doc
 prettyBind (BI _ nm icit quant, ty) = wrap icit (text (show quant ++ nm) <+> text ":" <+> pretty ty)
@@ -246,6 +250,8 @@ substRaw ss t = case t of
  (RWhere fc ds body) => RWhere fc (map substDecl ds) (substRaw ss body)
  (RDo fc stmts) => RDo fc (substStmts ss stmts)
  (RCase fc scrut mdef alts) => RCase fc (substRaw ss scrut) (map (substRaw ss) mdef) (map substAlt alts)
+  (RList fc (Just t)) => RList fc (Just $ substRaw ss t)
+  (RList fc Nothing) => RList fc Nothing
  -- Enumerate to force consideration of new cases
  t@(RImpossible _) => t
  t@(RU _) => t
--- a/src/Lib/TCO.newt
+++ b/src/Lib/TCO.newt
@@ -26,12 +26,12 @@ tailNames (CLetLoop _ _) = Nil
 tailNames (CCase _ alts) = join $ map altTailNames alts
  where
    altTailNames : CAlt → List QName
-    altTailNames (CConAlt _ _ _ _ exp) = tailNames exp
+    altTailNames (CConAlt _ _ _ _ _ exp) = tailNames exp
    altTailNames (CDefAlt exp) = tailNames exp
    altTailNames (CLitAlt _ exp) = tailNames exp
 tailNames (CLet _ _ t) = tailNames t
 tailNames (CLetRec _ _ t) = tailNames t
-tailNames (CConstr _ _ args _) = Nil
+tailNames (CConstr _ _ args _ _) = Nil
 tailNames (CBnd _) = Nil
 tailNames (CFun _ tm) = tailNames tm
 tailNames (CLam _ _) = Nil
@@ -50,20 +50,20 @@ rewriteTailCalls nms tm = case tm of
  CAppRef nm args qs =>
      if length' args == length' qs
      then case getTag (S Z) nm nms of
-        Just ix => CConstr ix (show nm) args $ map (const Many) args
-        Nothing => CConstr Z "return" (tm :: Nil) (Many :: Nil)
-      else CConstr Z "return" (tm :: Nil) (Many :: Nil)
+        Just ix => CConstr ix (show nm) args (map (const Many) args) NormalCon
+        Nothing => CConstr Z "return" (tm :: Nil) (Many :: Nil) NormalCon
+      else CConstr Z "return" (tm :: Nil) (Many :: Nil) NormalCon
  CLetRec nm t u => CLetRec nm t $ rewriteTailCalls nms u
  CLet nm t u => CLet nm t $ rewriteTailCalls nms u
  CCase sc alts => CCase sc $ map rewriteAlt alts
-  tm => CConstr Z "return" (tm :: Nil) (Many :: Nil)
+  tm => CConstr Z "return" (tm :: Nil) (Many :: Nil) NormalCon
  where
      getTag : Nat → QName → List QName → Maybe Nat
      getTag t nm Nil = Nothing
      getTag t nm (n :: ns) = if n == nm then Just t else getTag (S t) nm ns

      rewriteAlt : CAlt -> CAlt
-      rewriteAlt (CConAlt ix nm info args t) = CConAlt ix nm info args $ rewriteTailCalls nms t
+      rewriteAlt (CConAlt ix nm info args qs t) = CConAlt ix nm info args qs $ rewriteTailCalls nms t
      rewriteAlt (CDefAlt t) = CDefAlt $ rewriteTailCalls nms t
      rewriteAlt (CLitAlt lit t) = CLitAlt lit $ rewriteTailCalls nms t

@@ -81,7 +81,7 @@ rewriteLoop qn tm = case tm of
    tm => tm
  where
    rewriteAlt : CAlt → CAlt
-    rewriteAlt (CConAlt ix nm info args t) = CConAlt ix nm info args $ rewriteLoop qn t
+    rewriteAlt (CConAlt ix nm info args qs t) = CConAlt ix nm info args qs $ rewriteLoop qn t
    rewriteAlt (CDefAlt t) = CDefAlt $ rewriteLoop qn t
    rewriteAlt (CLitAlt lit t) = CLitAlt lit $ rewriteLoop qn t

@@ -109,7 +109,7 @@ doOptimize fns = do
      let arglen = length' args
      let conargs = map (\k => CBnd (arglen - k - 1)) (range 0 arglen)
      let conquant = map (const Many) conargs
-      let arg = CConstr (S ix) (show qn) conargs conquant
+      let arg = CConstr (S ix) (show qn) conargs conquant NormalCon
      let body = CAppRef bouncer (CRef recName :: arg :: Nil) (Many :: Many :: Nil)
      pure (qn, CFun args body)
    mkWrap _ (qn, _) = error emptyFC "error in mkWrap: \{show qn} not a CFun"
@@ -119,7 +119,7 @@ doOptimize fns = do
    mkRecName (QN ns nm :: _) = pure $ QN ns "REC_\{nm}"

    mkAlt : List QName → (Nat × QName × List (Quant × Name) × CExp) -> CAlt
-    mkAlt nms (ix, qn, args, tm) = CConAlt (S ix) (show qn) NormalCon (map snd args) (rewriteTailCalls nms tm)
+    mkAlt nms (ix, qn, args, tm) = CConAlt (S ix) (show qn) NormalCon (map snd args) (map fst args) (rewriteTailCalls nms tm)

    splitFun : (QName × CExp) → M (QName × List (Quant × Name) × CExp)
    splitFun (qn, CFun args body) = pure (qn, args, body)
--- a/src/Lib/Tokenizer.newt
+++ b/src/Lib/Tokenizer.newt
@@ -165,7 +165,8 @@ rawTokenise ts@(TS sl sc toks chars) = case chars of
    doChar : Char -> List Char ->  Either Error TState
    doChar c cs = if elem c standalone
      then rawTokenise (TS sl (sc + 1) (toks :< mktok True sl (sc + 1) Symbol (pack $ c :: Nil)) cs)
-      else let kind = if isDigit c then Number else if isUpper c then UIdent else Ident in
+      else if isDigit c then doRest (TS sl sc toks (c :: cs)) Number isDigit Lin
+      else let kind = if isUpper c then UIdent else Ident in
        doRest (TS sl sc toks (c :: cs)) kind isIdent Lin


--- a/src/Lib/TopContext.newt
+++ b/src/Lib/TopContext.newt
@@ -53,7 +53,7 @@ setFlag name fc flag = do
  top <- getTop
  let (Just (MkEntry fc nm ty def flags)) = lookupMap' name top.currentMod.modDefs
    | Nothing => error fc "\{show name} not declared"
-  modifyTop [ currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))] ]
+  modifyTop { currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def (flag :: flags)))} }

 setDef : QName -> FC -> Tm -> Def → List EFlag -> M Unit
 setDef name fc ty def flags = do
@@ -61,14 +61,14 @@ setDef name fc ty def flags = do
  let (Nothing) = lookupMap' name top.currentMod.modDefs
    | Just (MkEntry fc' nm' ty' def' _) => error fc "\{show name} is already defined at \{show fc'}"

-  modifyTop [currentMod $= [ modDefs $= (updateMap name (MkEntry fc name ty def flags))] ]
+  modifyTop {currentMod $= { modDefs $= (updateMap name (MkEntry fc name ty def flags))} }

 updateDef : QName -> FC -> Tm -> Def -> M Unit
 updateDef name fc ty def = do
  top <- getTop
  let (Just (MkEntry fc' nm' ty' def' flags)) = lookupMap' name top.currentMod.modDefs
    | Nothing => error fc "\{show name} not declared"
-  modifyTop [ currentMod $= [ modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs ] ]
+  modifyTop { currentMod $= { modDefs := updateMap name (MkEntry fc' name ty def flags) top.currentMod.modDefs } }

 typeName : Tm → Maybe QName
 typeName (Pi fc nm Explicit rig t u) = Nothing
@@ -86,18 +86,18 @@ addHint qn = do
        | Nothing => error entry.fc "can't find tcon name for \{show qn}"
      let xs = fromMaybe Nil $ lookupMap' tyname top.hints
      let hints = updateMap tyname ((qn, entry.type) :: xs) top.hints
-      modifyTop [ hints := hints ]
+      modifyTop { hints := hints }
    Nothing => pure MkUnit

 addError : Error -> M Unit
-addError err = modifyTop [ currentMod $= [ modErrors $= (err ::) ] ]
+addError err = modifyTop { currentMod $= { modErrors $= (err ::) } }

 addInfo : EditorInfo → M Unit
-addInfo info = modifyTop [ currentMod $= [modInfos $= (info ::) ] ]
+addInfo info = modifyTop { currentMod $= {modInfos $= (info ::) } }

 -- temporary? used in derive for now
 freshName : String → M String
 freshName nm = do
  top <- getTop
-  modifyTop [ freshIx $= 1 + ]
+  modifyTop { freshIx $= 1 + }
  pure $ "f$" ++ nm ++ show top.freshIx
--- a/src/Lib/Types.newt
+++ b/src/Lib/Types.newt
@@ -23,7 +23,10 @@ derive Show BD

 data Quant = Zero | Many
 derive Eq Quant
-derive Show Quant
+
+instance Show Quant where
+  show Zero = "0 "
+  show Many = ""

 -- We could make this polymorphic and use for environment...

@@ -169,20 +172,15 @@ Val : U
 Closure : U
 Env : U

-data VCaseAlt : U where
-  -- Like a Closure, but with a lot of args
-  VCaseCons : (name : QName) -> (args : List String) -> Env -> Tm ->  VCaseAlt
-  VCaseLit : Literal -> Val -> VCaseAlt
-  VCaseDefault : Val -> VCaseAlt
-
 data Val : U where
  VVar : FC -> (k : Int) -> (sp : SnocList Val) -> Val
  VRef : FC -> (nm : QName) -> (sp : SnocList Val) -> Val
-  VCase : FC -> (sc : Val) -> List VCaseAlt -> Val
+  VCase : FC -> (sc : Val) -> Env -> List CaseAlt -> Val
  VMeta : FC -> QName -> (sp : SnocList Val) -> Val
  VLam : FC -> Name -> Icit -> Quant -> Closure -> Val
  VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val
-  VLet : FC -> Name -> Val -> Val -> Val
+  -- not substing let, like idris
+  VLet : FC -> Name -> Val -> Closure -> Val
  VLetRec : FC -> Name -> Val -> Val -> Val -> Val
  VU : FC -> Val
  VErased : FC -> Val
@@ -196,7 +194,7 @@ data Closure = MkClosure Env Tm
 getValFC : Val -> FC
 getValFC (VVar fc _ _) = fc
 getValFC (VRef fc _ _) = fc
-getValFC (VCase fc _ _) = fc
+getValFC (VCase fc _ _ _) = fc
 getValFC (VMeta fc _ _) = fc
 getValFC (VLam fc _ _ _ _) = fc
 getValFC (VPi fc _ _ _ a b) = fc
@@ -220,15 +218,10 @@ instance Show Val where
  show (VPi fc str Implicit rig x y) = "(%pi {\{show rig} \{str} : \{show  x}}. \{showClosure  y})"
  show (VPi fc str Explicit rig x y) = "(%pi (\{show rig} \{str} : \{show  x}). \{showClosure  y})"
  show (VPi fc str Auto rig x y) = "(%pi {{\{show rig} \{str} : \{show  x}}}. \{showClosure  y})"
-  show (VCase fc sc alts) = "(%case \{show sc} \{unwords $ map showAlt alts})"
-    where
-      showAlt : VCaseAlt → String
-      showAlt (VCaseDefault v) = "(%cdef \{show v})"
-      showAlt (VCaseLit lit v) = "(%clit \{show v})"
-      showAlt (VCaseCons nm args env v) = "(%ccon \{show nm} \{unwords $ map show args} [\{show $ length env} env] \{show v}"
+  show (VCase fc sc env alts) = "(%case \{show sc} \{unwords $ map show alts})"
  show (VU _) = "U"
  show (VLit _ lit) = show lit
-  show (VLet _ nm a b) = "(%let \{show nm} = \{show a} in \{show b}"
+  show (VLet _ nm a (MkClosure env b)) = "(%let \{show nm} = \{show a} in \{show b}"
  show (VLetRec _ nm ty a b) = "(%letrec \{show nm} : \{show ty} = \{show a} in \{show b}"
  show (VErased _) = "ERASED"

@@ -269,12 +262,17 @@ record MetaContext where

 derive Eq MetaMode

-data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon
+data ConInfo = NormalCon
+             | SuccCon | ZeroCon
+             | EnumCon | TrueCon | FalseCon
+             | NilCon | ConsCon

 derive Eq ConInfo

 instance Show ConInfo where
  show NormalCon = ""
+  show ConsCon = "[C]"
+  show NilCon = "[N]"
  show FalseCon = "[F]"
  show TrueCon = "[T]"
  show SuccCon = "[S]"
--- a/src/Main.newt
+++ b/src/Main.newt
@@ -114,7 +114,7 @@ cmdLine : List String -> M (Maybe String × List String)
 cmdLine Nil = pure (Nothing, Nil)
 cmdLine ("--top" :: args) = cmdLine args -- handled later
 cmdLine ("-v" :: args) = do
-  modifyTop [ verbose $= _+_ 1 ]
+  modifyTop { verbose $= _+_ 1 }
  cmdLine args
 cmdLine ("-o" :: fn :: args) = do
  (out, files) <- cmdLine args
@@ -166,8 +166,8 @@ runCommand (Load fn) = processFile fn
 runCommand (HelpCmd) = replHelp
 runCommand (BrowseCmd qn) = browseTop qn
 runCommand (GetDoc name) = getDoc name
-runCommand (Verbose Nothing) = modifyTop [ verbose $= _+_ 1 ]
-runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
+runCommand (Verbose Nothing) = modifyTop { verbose $= _+_ 1 }
+runCommand (Verbose (Just v)) = modifyTop { verbose := v }
 runCommand (OutputJS fn) = writeSource fn
 runCommand DumpTop = do
  json <- jsonTopContext
--- a/src/Prelude.newt
+++ b/src/Prelude.newt
@@ -456,8 +456,7 @@ debugLog a = putStrLn (debugStr a)

 pfunc stringToInt : String → Int := `(s) => {
  let rval = Number(s)
-  if (isNaN(rval)) throw new Error(s + " is NaN")
-  return rval
+  return isNaN(rval) ? 0 : rval
 }`

 class Foldable (m : U → U) where
--- a/tests/ListSugar.newt
+++ b/tests/ListSugar.newt
@@ -0,0 +1,19 @@
+module ListSugar
+
+import Prelude
+
+
+blah : List Int
+blah = [ 1, 2, 3]
+
+bar : List Int → Int
+bar [ ] = 0
+bar [x] = 1
+bar _ = 42
+
+main : IO Unit
+main = do
+  printLn blah
+  printLn $ bar []
+  printLn $ bar [ 42 ]
+  printLn $ bar blah
--- a/tests/ListSugar.newt.golden
+++ b/tests/ListSugar.newt.golden
@@ -0,0 +1,4 @@
+[1, 2, 3]
+0
+1
+42
--- a/tests/NestedUpdate.newt
+++ b/tests/NestedUpdate.newt
@@ -9,4 +9,4 @@ record Bar where
    foo : Foo

 blah : Bar → Bar
-blah x = [ foo $= [ bar := 1]] x
+blah x = { foo $= { bar := 1}} x
--- a/tests/Number.newt
+++ b/tests/Number.newt
@@ -0,0 +1,9 @@
+module Number
+
+import Prelude
+
+add : Int → Int → Int
+add a b = a + b
+
+main : IO Unit
+main = printLn $ add 2$ 40
--- a/tests/Number.newt.golden
+++ b/tests/Number.newt.golden
@@ -0,0 +1 @@
+42
--- a/tests/RUTest.newt
+++ b/tests/RUTest.newt
@@ -8,12 +8,12 @@ record Foo where
  baz : Nat

 blah : Foo → Foo
-blah x = [ bar := Z ] x
+blah x = { bar := Z } x

 main : IO Unit
 main = do
  let x = blah $ MkFoo (S Z) (S (S Z))
  printLn x.bar
  -- this is unfortunate, it can't get record type from a meta
-  let x' = the Foo $ [ baz := Z ] x
+  let x' = the Foo $ { baz := Z } x
  printLn x'.baz
Author	SHA1	Message	Date
Steve Dunham	4814682712	Add list sugar Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-29 19:54:01 -07:00
Steve Dunham	2f1185bf4c	drop old record syntax	2026-03-29 19:54:01 -07:00
Steve Dunham	ee9664838f	use new record update syntax	2026-03-29 19:54:01 -07:00
Steve Dunham	ba519bdc7f	update bootstrap	2026-03-29 19:53:48 -07:00
Steve Dunham	cb394d3cc2	change record update syntax	2026-03-29 09:56:42 -07:00
Steve Dunham	3338a617cc	Move build products to `build` directory	2026-03-29 09:56:39 -07:00
Steve Dunham	ac231173ed	lit case was accidentally removed	2026-03-28 19:36:50 -07:00
Steve Dunham	f42f4aecbe	don't let constructor args in scheme backend	2026-03-28 19:32:11 -07:00
Steve Dunham	766eb69313	fix font size issue on MobileSafari	2026-03-28 17:38:34 -07:00
Steve Dunham	e2dfe4ec04	fixes to eval Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-28 16:16:06 -07:00
Steve Dunham	697c5f2641	fix updating of javascript/scheme in playground Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-28 09:36:05 -07:00
Steve Dunham	babbd01975	Fix LSP crash and tokenizer issue	2026-03-27 20:21:57 -07:00
Steve Dunham	c014233987	debug lsp crashes	2026-03-27 20:20:08 -07:00
Steve Dunham	aa6604038b	cleanup	2026-03-27 20:19:27 -07:00
Steve Dunham	a40956a4cc	fix names growing in liftWhere and redundant error for ErrorHole Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-21 20:45:28 -07:00
Steve Dunham	c6835b9dfe	scheme types need not store their indices	2026-03-21 16:50:53 -07:00
Steve Dunham	9b8a7953dd	fixes to scheme in playground	2026-03-21 11:54:14 -07:00
Steve Dunham	f5a9aae070	also show scheme code in web playground Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-21 11:39:29 -07:00
Steve Dunham	9652903df1	enable tests on scheme, fix error handling on scheme	2026-03-21 10:27:45 -07:00
Steve Dunham	da1f2705ee	Remove erased function args in scheme	2026-03-21 08:25:00 -07:00
Steve Dunham	f3f9d737cf	also drop singleton cases for lit / default	2026-03-20 08:01:31 -07:00
Steve Dunham	cfdddbb002	cons/nil for pair/unit in scheme backend Some checks failed Publish Playground / build (push) Has been cancelled Details Publish Playground / deploy (push) Has been cancelled Details	2026-03-18 17:30:28 -07:00
Steve Dunham	5eb43f6252	Cons/Nil optimization for scheme backend	2026-03-18 17:30:17 -07:00
Steve Dunham	4ce5d470ba	streamline generated code a little	2026-03-16 21:56:03 -07:00