Add list sugar

.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

Makefile

@@ -1,51 +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
+newt3: build/newt3.js
-	sh ./scripts/mkrevision
 
-newt.js: ${SRCS} src/Revision.newt
+test: build/newt.js
-	$(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 prim.ss
-	chez --script scripts/compile-chez.ss
-
-newt2.ss: newt.so
-	chez --program newt.ss src/Main.newt -o newt2.ss
-
-test: newt.js
 	scripts/test
 
-cheztest: newt.so
+cheztest: build/newt.so
-	make test NEWT='chez --program newt.so' RUNOUT="chez --script" OUTFILE=tmp/out.ss
+	make test NEWT='chez --program build/newt.so' RUNOUT="chez --script" OUTFILE=tmp/out.ss
 
-aoctest: newt.js
+aoctest: build/newt.js
 	scripts/aoc
 	scripts/aoc25
 
-# Misc
+lsp: newt-vscode-lsp/dist/lsp.js playground/src/newt.js
-
-# build / install old vscode extension
-# vscode:
-	# cd newt-vscode && vsce package && code --install-extension *.vsix
 
 # build / install new LSP vscode extension
 vscode-lsp vscode: lsp
@@ -55,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
+build:
-	cp lsp.js $@
+	mkdir -p build
 
-playground/src/newt.js: lsp.js
+src/Revision.newt: .PHONY build
-	cp lsp.js $@
+	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
 

playground/build

@@ -1,8 +1,7 @@
 #!/bin/bash
 mkdir -p public
-echo copy newt
+echo build lsp.js
-(cd .. && make lsp.js)
+(cd .. && make lsp)
-cp ../lsp.js src/newt.js
 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

playground/style.css

@@ -7,6 +7,7 @@
 body {
   overflow: hidden;
   font-size: 12px;
+  -webkit-text-size-adjust: none;
 }
 svg.icon path {
   stroke: black;

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

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

scripts/compile-chez.ss

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

scripts/test

@@ -1,7 +1,7 @@
 #!/bin/sh
 SAMPLES=$(find playground/samples -name "*.newt")
-# NEWT ="bun run newt.js"
+# NEWT ="bun run build/newt.js"
-NEWT=${NEWT:="node newt.js"}
+NEWT=${NEWT:="node build/newt.js"}
 OUTFILE=${OUTFILE:="tmp/out.js"}
 RUNOUT=${RUNOUT:="node"}
 mkdir -p tmp

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

src/LSP.newt

@@ -68,12 +68,12 @@ lspFileSource = do
 
 updateFile : String → String → Unit
 updateFile fn src = unsafePerformIO $ do
-    modifyIORef state [ files $= updateMap fn src ]
+    modifyIORef state { files $= updateMap fn src }
     st <- readIORef state
     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
@@ -287,7 +287,7 @@ 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
 
 compileToScheme : String → JSObject
@@ -302,7 +302,7 @@ compileToScheme fn = unsafePerformIO $ do
     let src = unlines 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

src/Lib/CompileScheme.newt

@@ -119,14 +119,12 @@ 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 → List Quant → CExp → String
+    conAlt : SCEnv → String → Int → List String → List Quant → CExp → String
-    conAlt env nm lets Nil Nil body = "(let (\{joinBy " " (lets <>> Nil)}) \{cexpToScm env body})"
+    conAlt env nm ix Nil Nil body = cexpToScm env body
-    -- TODO let `vector-ref nm ..`` vs `#f` (erased) in env for erased fields
+    conAlt env nm ix (arg :: args) (Many :: qs) body =
-    conAlt env nm lets (arg :: args) (Many :: qs) body = case scbind arg env of
+        conAlt ("(vector-ref \{nm} \{show ix})" :: env) nm (ix + 1) args qs body
-      (arg', env') => let ix = 1 + snoclen' lets
+    conAlt env nm ix (arg :: args) (Zero :: qs) body = conAlt ("#f" :: env) nm ix args qs body
-        in conAlt env' nm (lets :< "(\{arg'} (vector-ref \{nm} \{show ix}))") args qs body
+    conAlt env nm ix _ _ body = fatalError "arg/qs mismatch in conAlt"
-    conAlt env nm lets (arg :: args) (Zero :: qs) body = conAlt ("#f" :: env) nm lets args qs body
-    conAlt env nm lets _ _ body = fatalError "arg/qs mismatch in conAlt"
 
     nilAlt : SCEnv → List Quant → CExp → String
     nilAlt env Nil body = cexpToScm env body
@@ -145,7 +143,7 @@ cexpToScm env (CCase sc alts) = do
     -- 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 qs body) = "((\{show tag}) \{conAlt env nm Lin args qs 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})"
 
@@ -170,7 +168,7 @@ cexpToScm env (CCase sc alts) = do
         (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 Lin args qs body
+    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})"

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
+-- for now, we don't do solutions with case, let, letrec in them
-  val' <- rename meta ren lvl val
+-- If we we need this, follow the model of VLam
-  body' <- rename meta (lvl :: ren) (1 + lvl) body
+rename meta ren lvl tm = error (getFC tm) "Unhandled term in `rename`: \{show tm}"
-  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'
 
 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

src/Lib/Eval.newt

@@ -9,6 +9,7 @@ import Lib.TopContext
 import Data.IORef
 import Data.SnocList
 import Data.SortedMap
+import Lib.Error
 
 eval : Env -> Tm -> M Val
 
@@ -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
@@ -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
+    pushArgs env Nil Nil = Just <$> eval env t
-      t' <- eval env t
+    pushArgs env args Nil = fatalError "Extra args \{show args}"
-      Just <$> vappSpine t' (Lin <>< 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
+  -- Used for `where`, we'd probably need to treat this like Lam.
-  t' <- eval (VVar fc (length' env) Lin :: env) t
+  error fc "eval letrec"
-  u' <- eval (VVar fc (length' env) Lin :: env) u
+  -- I think we need to handle this like lam/let, disabled for now.
-  pure $ VLetRec fc nm ty' t' u'
+  -- 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
+  -- inline metas and do beta reduction at head
-  -- possibly too aggressive?
   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 env alts
-  pure $ VCase fc vsc 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
+normAlt : Env → Int → CaseAlt → M CaseAlt
-quoteAlt l (VCaseDefault val) = CaseDefault <$> quote l val
+normAlt env l (CaseDefault tm) = do
-quoteAlt l (VCaseLit lit val) = CaseLit lit <$> quote l val
+   val <- eval env tm
-quoteAlt l (VCaseCons nm args env tm) = do
+   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
+  alts' <- traverse (normAlt env l) alts
-  pure $ Case fc sc' 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')
+    debug $ \ _ =>  "zonk will app \{show t'} @ \{show sp} ~> \{show vtm} @ \{show sp'}"
-    t' <- quote l foo
+    res <- vappSpine vtm (Lin <>< sp')
-    zonk top l env t')
+    debug $ \_ => "result is \{show res}"
-    (\_ => pure $ appSpine t' sp)
+    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

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}
+  -- 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))
-  ty <- symbol ":" *> typeExpr
+    symbol ":"
+    pure (quant, names)
+  ty <- typeExpr
   symbol "}"
   pure $ map (makeBind quant (Just ty)) names
   where

src/Lib/ProcessDecl.newt

@@ -310,6 +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
 
   debug $ \ _ => "traverse \{show $ map show args}"
   -- This is a little painful because we're reverse engineering the
@@ -546,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`

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
-  modifyTop [ modules $= 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

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

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

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})"
+  show (VCase fc sc env alts) = "(%case \{show sc} \{unwords $ map show 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 (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,7 +262,10 @@ record MetaContext where
 
 derive Eq MetaMode
 
-data ConInfo = NormalCon | SuccCon | ZeroCon | EnumCon | TrueCon | FalseCon | NilCon | ConsCon
+data ConInfo = NormalCon
+             | SuccCon | ZeroCon
+             | EnumCon | TrueCon | FalseCon
+             | NilCon | ConsCon
 
 derive Eq ConInfo
 

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 Nothing) = modifyTop { verbose $= _+_ 1 }
-runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
+runCommand (Verbose (Just v)) = modifyTop { verbose := v }
 runCommand (OutputJS fn) = writeSource fn
 runCommand DumpTop = do
   json <- jsonTopContext

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

tests/ListSugar.newt.golden

@@ -0,0 +1,4 @@
+[1, 2, 3]
+0
+1
+42

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

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