fix names growing in liftWhere and redundant error for ErrorHole

playground/src/main.ts

@@ -95,7 +95,7 @@ if (!state.scheme.value) {
     // maybe send fileName, src?
     await ipc.sendMessage("updateFile", [fileName, src]);
     let scheme = await ipc.sendMessage("compile", [fileName, "scheme"]);
-    state.scheme.value = bundle(scheme);
+    state.scheme.value = scheme;
   }
 }
 
@@ -288,8 +288,6 @@ const language: EditorDelegate = {
         ipc.sendMessage("compile", [fileName, "javascript"]).then(js => state.javascript.value = bundle(js));
       if (state.selected.value === SCHEME)
         ipc.sendMessage("compile", [fileName, "scheme"]).then(scheme=> state.scheme.value = scheme);
-      // UI will update
-      state.scheme.value = "";
       return diags;
     } catch (e) {
       console.log("ERR", e);

prim.ss

@@ -1,7 +1,7 @@
 ; (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 #f #f x))
-(define ($Right x) (vector 1 #f #f x))
+(define ($Left x) (vector 0 x))
+(define ($Right x) (vector 1 x))
 (define $LT 0)
 (define $EQ 1)
 (define $GT 2)
@@ -65,7 +65,9 @@
 ;; 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))

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]

src/Lib/CompileScheme.newt

@@ -119,12 +119,14 @@ 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})"
+    conAlt : SCEnv → String → SnocList String → List String → List Quant → CExp → String
+    conAlt env nm lets Nil 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
+    conAlt env nm lets (arg :: args) (Many :: qs) 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
+        in conAlt env' nm (lets :< "(\{arg'} (vector-ref \{nm} \{show ix}))") args qs body
+    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
@@ -143,16 +145,13 @@ 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 body})"
+    doAlt nm (CConAlt tag cname _ args qs body) = "((\{show tag}) \{conAlt env nm Lin 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
-    -- I'm not sure the case tree should be generating this, c.f. deleteT23 (probably from doNumCon)
     doCase nm (CDefAlt body :: Nil) = cexpToScm env body
-    -- TODO singleton ConsCon for pair, too. (Need to detect)
-    -- oh, but what if it's default?
     doCase nm (cons@(CConAlt tag cname ConsCon args qs body ) :: rest) =
       let consBranch = consAlt env nm qs body in
       case rest of
@@ -171,11 +170,10 @@ 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 body
+    doCase nm (CConAlt tag cname _ args qs body :: Nil) = conAlt env nm Lin 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})"
 
 cexpToScm env (CRef nm) = scmName nm
@@ -194,16 +192,12 @@ 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) =
-  -- FIXME need to deal with quants (on both sides!)
-  let args' = map (cexpToScm env) args in
-  "(vector \{show tag} \{joinBy " " args'})"
--- TODO
+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

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

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'