better name for metas

playground/src/emul.ts

@@ -47,6 +47,9 @@ export let shim: NodeShim = {
     writeFileSync(name: string, data: string, enc?: string) {
       shim.files[name] = new TextEncoder().encode(data)
     },
+    writeSync(fd: number, data: string) {
+      shim.stdout += data;
+    }
   },
   process: {
     argv: ["", ""],

playground/src/main.ts

@@ -484,6 +484,7 @@ const processOutput = (
       let endLineNumber = +eline;
       let endColumn = +ecol
       // FIXME - pass the real path in
+      if (file.startsWith("./")) file = file.slice(2);
       if (fn && fn !== file) {
         startLineNumber = startColumn = 0;
       }

scripts/test

@@ -20,12 +20,16 @@ for fn in tests/*.newt ; do
         echo "Compile failure mismatch for $fn"
         diff ${fn}.fail tmp/${bn}.compile
         failed=$((failed + 1))
+        if [ $1 = "--fix" ]; then
+          cp tmp/${bn}.compile ${fn}.fail
+        fi
         continue
     fi
   elif [ $cerr != "0" ]; then
     echo Compile failed for $fn
     failed=$((failed + 1))
     cat tmp/${bn}.compile
+
     continue
   fi
   # if there is a golden file, run the code and compare output
@@ -40,6 +44,9 @@ for fn in tests/*.newt ; do
       echo "Output mismatch for $fn"
       diff ${fn}.golden tmp/${bn}.out
       failed=$((failed + 1))
+      if [ $1 = "--fix" ]; then
+        cp tmp/${bn}.out ${fn}.golden
+      fi
     fi
   fi
 done

src/Lib/Common.newt

@@ -15,9 +15,15 @@ record Bounds where
 -- FIXME we should handle overlap and out of order..
 instance Add Bounds where
   a + b =
+    if empty a then b
+    else if empty b then a else
     let a' = if a.startLine < b.startLine  || a.startLine == b.startLine && a.startCol < b.startCol then a else b
         b' = if a.endLine < b.endLine || a.endLine == b.endLine && a.endCol < b.endCol then b else a
     in MkBounds a'.startLine a'.startCol b'.endLine b'.endCol
+    where
+      empty : Bounds → Bool
+      empty (MkBounds 0 0 0 0) = True
+      empty _ = False
 
 instance Eq Bounds where
   (MkBounds sl sc el ec) == (MkBounds sl' sc' el' ec') =

src/Lib/Elab.newt

@@ -363,6 +363,8 @@ lams Z _ tm = tm
 lams (S k) Nil tm = Lam emptyFC "arg_\{show k}" Explicit Many (lams k Nil tm)
 lams (S k) (x :: xs) tm = Lam emptyFC x Explicit Many (lams k xs tm)
 
+
+
 unify : Env -> UnifyMode -> Val -> Val  -> M UnifyResult
 
 .boundNames : Context -> List String
@@ -626,7 +628,7 @@ freshMeta ctx fc ty kind = do
   debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})"
   -- need the ns here
   -- we were fudging this for v1
-  let qn = QN top.ns "\{show mc.next}"
+  let qn = QN top.ns "$m\{show mc.next}"
   let newmeta = Unsolved fc qn ctx ty kind Nil
   let autos = case kind of
       AutoSolve => qn :: mc.autos
@@ -1525,6 +1527,7 @@ check ctx tm ty = do
 
     (tm,ty) => do
       (tm', ty') <- infer ctx tm
+      -- REVIEW - should we look at `tm` to know how many to insert? Is there a case where this helps?
       (tm', ty') <- insert ctx tm' ty'
 
       let names = map fst ctx.types

src/Lib/ReplParser.newt

@@ -14,6 +14,7 @@ data ReplCommand
     | GetDoc String
     | BrowseCmd QName
     | HelpCmd
+    | DumpTop
 
 kw : String → Parser String
 kw s = satisfy (\t => t.val.text == s) "Expected \{show s}"
@@ -61,6 +62,7 @@ commands
     :: MkCmd ":d" "document function" ArgIdent GetDoc
     :: MkCmd ":doc" "document function" ArgIdent GetDoc
     :: MkCmd ":b" "browse namespace" ArgQName BrowseCmd
+    :: MkCmd ":top" "dump top context as json" ArgNone DumpTop
     -- type at point
     -- solve hole
     -- search by prefix (for autocomplete - ideally include types at point, but we'd need recovery)

src/Main.newt

@@ -54,8 +54,7 @@ writeSource fn = do
         :: Nil)
         ++ map (render 90 ∘ noAlt) docs
   (Right _) <- liftIO {M} $ writeFile fn src
-    | Left err => exitFailure (show err)
+    | Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err
-  -- (Right _) <- chmodRaw fn 493 | Left err => exitFailure (show err)
   pure MkUnit
 
 
@@ -105,22 +104,22 @@ processModule importFC base stk qn@(QN ns nm) = do
   modifyTop [modules := updateMap modns (emptyModCtx "") top.modules]
   let fn = (joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt"
   (Right src) <- liftIO {M} $ readFile fn
-    | Left err => exitFailure "ERROR at \{show importFC}: error reading \{fn}: \{show err}"
+    | Left err => throwError $ E importFC "error reading \{fn}: \{show err}"
   let (Right toks) = tokenise fn src
-    | Left err => exitFailure (showError src err)
+    | Left err => throwError err
 
   let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks
-    | Left (err, toks) => exitFailure (showError src err)
+    | Left (err, toks) => throwError err
 
   log 1 $ \ _ => "scan imports for module \{modName}"
   let ns = split modName "."
   let (path, modName') = unsnoc $ split1 modName "."
   -- let bparts = split base "/"
   let (True) = qn == QN path modName'
-    | _ => exitFailure "ERROR at \{show nameFC}: module name \{show modName} doesn't match file name \{show fn}"
+    | _ => throwError $ E nameFC "module name \{show modName} doesn't match file name \{show fn}"
 
   let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks
-    | Left (err, toks) => exitFailure (showError src err)
+    | Left (err, toks) => throwError err
 
   let importNames = map importToQN imports
 
@@ -155,7 +154,13 @@ processModule importFC base stk qn@(QN ns nm) = do
   top <- getTop
   let freshMC = MC emptyMap Nil 0 CheckAll
   -- set imported, mod, freshMC, ops  before processing
-  modifyTop (\ top => MkTop top.modules imported emptyMap modns emptyMap freshMC top.verbose top.errors ops)
+  modifyTop [ imported := imported
+            ; hints := emptyMap
+            ; ns := modns
+            ; defs := emptyMap
+            ; metaCtx := freshMC
+            ; ops := ops
+            ]
   for imported $ \ ns => do
     let (Just mod) = lookupMap' ns top.modules | _ => error emptyFC "namespace \{show ns} missing"
     importHints (listValues mod.modDefs)
@@ -176,7 +181,7 @@ processModule importFC base stk qn@(QN ns nm) = do
 
   logMetas $ reverse $ listValues top.metaCtx.metas
   let (Nil) = top.errors
-    | errors => exitFailure "Compile failed"
+    | errors => throwError $ E importFC "Failed to compile module \{show qn}"
   pure src
   where
     tryProcessDecl : String -> List String → Decl -> M Unit
@@ -200,7 +205,7 @@ showErrors fn src = do
   let (Nil) = top.errors
     | errors => do
         traverse (putStrLn ∘ showError src) errors
-        exitFailure "Compile failed"
+        throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed"
   pure MkUnit
 
 invalidateModule : QName -> M Unit
@@ -235,7 +240,12 @@ processFile fn = do
 
   top <- getTop
   let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules
-  modifyTop (\ top => MkTop modules (primNS :: Nil) emptyMap Nil emptyMap top.metaCtx top.verbose top.errors top.ops)
+  modifyTop [ modules := modules
+            ; imported := primNS :: Nil
+            ; hints := emptyMap
+            ; ns := Nil
+            ; defs := emptyMap
+            ]
 
   invalidateModule qn
 
@@ -304,6 +314,9 @@ runCommand (GetDoc name) = getDoc name
 runCommand (Verbose Nothing) = modifyTop [ verbose $= _+_ 1 ]
 runCommand (Verbose (Just v)) = modifyTop [ verbose := v ]
 runCommand (OutputJS fn) = writeSource fn
+runCommand DumpTop = do
+  json <- jsonTopContext
+  putStrLn "TOP:\{renderJson json}"
 
 -- Broken out to a separate function so I can hook it.
 runString : String → M Unit

src/Prelude.newt

@@ -389,7 +389,7 @@ instance HasIO IO where
   liftIO a = a
 
 pfunc primPutStrLn uses (MkIORes MkUnit) : String → IO Unit := `(s) => (w) => {
-  console.log(s)
+  require('fs').writeSync(1, s + '\n')
   return Prelude_MkIORes(Prelude_MkUnit,w)
 }`
 

tests/BadAlt.newt.fail

@@ -7,4 +7,4 @@ ERROR at tests/BadAlt.newt:6:6--6:13: Prelude._:<_ not a constructor for (Prelud
   foo (xs :< x) = x
        ^^^^^^^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module BadAlt

tests/Duplicate.newt.fail

@@ -6,4 +6,4 @@ ERROR at tests/Duplicate.newt:4:1--4:5: Duplicate.Left is already defined at tes
   data Either : U -> U -> U where
   ^^^^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module Duplicate

tests/ErrMsg2.newt.fail

@@ -3,4 +3,4 @@ module Prelude
 module ErrMsg2
 ERROR at tests/ErrMsg2.newt:6:13--6:15: Expected '=>' at Keyword:->
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module ErrMsg2

tests/ErrorDup.newt.fail

@@ -18,4 +18,4 @@ ERROR at tests/ErrorDup.newt:9:7--9:10: Nat already declared
   class Nat where
         ^^^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module ErrorDup

tests/LitConCase.newt.fail

@@ -6,4 +6,4 @@ ERROR at tests/LitConCase.newt:7:5--7:11: expected Prim.Int
   foo MkUnit = MkUnit
       ^^^^^^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module LitConCase

tests/Possible.newt.fail

@@ -7,4 +7,4 @@ ERROR at tests/Possible.newt:6:5--6:8: possible constructors: [Prelude.Z, Prelud
   foo ()
       ^^^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module Possible

tests/Quantity.newt.fail

@@ -7,4 +7,4 @@ ERROR at tests/Quantity.newt:11:15--11:16: used erased value x$0 (FIXME FC may b
   bar {x} = foo x
                 ^
 
-Compile failed
+ERROR at :1:1--1:2: Failed to compile module Quantity