Use List String for module name, add abstraction for loading files (prep for LSP)

TODO.md

@@ -1,7 +1,9 @@
 
 ## TODO
 
-- [ ] For errors in other files, point to import
+- [ ] Inject markdown highlighter into /- -/ comments in vscode
+- [ ] For errors in other files, point to the import
+  - put a try in there and remove exitFailure
 - [x] Unsolved metas should be errors (user metas are fine)
 - [x] Better syntax for forward declared data (so we can distinguish from functions)
 - [ ] maybe allow "Main" module name for any file
@@ -316,6 +318,8 @@
   - [x] top level
   - [x] case statements
 - [ ] Lean ⟨ ⟩ anonymous constructors
+  - This would only work for `check` and we might need to revisit how `,` is handled.
+- [ ] Lean-like `#eval`
 - [ ] Lean-like .map, etc? (resolve name in namespace of target type, etc)
 - [x] autos / typeclass resolution
   - [x] very primitive version in place, not higher order, search at end

newt-vscode/package-lock.json

@@ -10,7 +10,7 @@
       "license": "MIT",
       "devDependencies": {
         "@types/mocha": "^10.0.7",
-        "@types/node": "20.x",
+        "@types/node": "25.x",
         "@types/vscode": "^1.90.0",
         "@typescript-eslint/eslint-plugin": "^7.14.1",
         "@typescript-eslint/parser": "^7.11.0",
@@ -772,13 +772,13 @@
       "license": "MIT"
     },
     "node_modules/@types/node": {
-      "version": "20.19.25",
+      "version": "25.2.2",
-      "resolved": "https://registry.npmjs.org/@types/node/-/node-20.19.25.tgz",
+      "resolved": "https://registry.npmjs.org/@types/node/-/node-25.2.2.tgz",
-      "integrity": "sha512-ZsJzA5thDQMSQO788d7IocwwQbI8B5OPzmqNvpf3NY/+MHDAS759Wo0gd2WQeXYt5AAAQjzcrTVC6SKCuYgoCQ==",
+      "integrity": "sha512-BkmoP5/FhRYek5izySdkOneRyXYN35I860MFAGupTdebyE66uZaR+bXLHq8k4DirE5DwQi3NuhvRU1jqTVwUrQ==",
       "dev": true,
       "license": "MIT",
       "dependencies": {
-        "undici-types": "~6.21.0"
+        "undici-types": "~7.16.0"
       }
     },
     "node_modules/@types/vscode": {
@@ -5605,9 +5605,9 @@
       }
     },
     "node_modules/undici-types": {
-      "version": "6.21.0",
+      "version": "7.16.0",
-      "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-6.21.0.tgz",
+      "resolved": "https://registry.npmjs.org/undici-types/-/undici-types-7.16.0.tgz",
-      "integrity": "sha512-iwDZqg0QAGrg9Rav5H4n0M64c3mkR59cJ6wQp+7C4nI0gsmExaedaYLNO44eT4AtBBwjbTiGPMlt2Md0T9H9JQ==",
+      "integrity": "sha512-Zz+aZWSj8LE6zoxD+xrjh4VfkIG8Ya6LvYkZqtUQGJPZjYl53ypCaUwWqo7eI0x66KBGeRo+mlBEkMSeSZ38Nw==",
       "dev": true,
       "license": "MIT"
     },

newt-vscode/package.json

@@ -82,7 +82,7 @@
   },
   "devDependencies": {
     "@types/mocha": "^10.0.7",
-    "@types/node": "20.x",
+    "@types/node": "25.x",
     "@types/vscode": "^1.90.0",
     "@typescript-eslint/eslint-plugin": "^7.14.1",
     "@typescript-eslint/parser": "^7.11.0",

newt-vscode/tsconfig.json

@@ -2,10 +2,12 @@
 	"compilerOptions": {
 		"module": "Node16",
 		"target": "ES2022",
-		"lib": [
+		"lib": [ "ES2022" ],
-			"ES2022"
-		],
 		"sourceMap": true,
+		// so node can run this stuff
+		"allowImportingTsExtensions": true,
+		// required by previous, but we use esbuild anyway
+		"noEmit": true,
 		"rootDir": "src",
 		"strict": true   /* enable all strict type-checking options */
 		/* Additional Checks */

src/Lib/ProcessModule.newt

@@ -0,0 +1,154 @@
+module Lib.ProcessModule
+
+import Prelude
+import Serialize
+import Lib.Types
+import Lib.Common
+import Lib.Syntax
+import Lib.ProcessDecl
+import Lib.TopContext
+import Lib.Tokenizer
+import Data.SortedMap
+import Lib.Parser.Impl
+import Lib.Parser
+import Data.List1
+import Lib.Elab
+
+-- declare internal primitives
+addPrimitives : M Unit
+addPrimitives = do
+  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
+
+
+record FileSource where
+  getFile : FC → String → M (String × String)
+
+parseDecls : String → Operators → TokenList → SnocList Decl → M (List Decl × Operators)
+parseDecls fn ops Nil acc = pure (acc <>> Nil, ops)
+parseDecls fn ops toks@(first :: _) acc =
+  case partialParse fn (sameLevel parseDecl) ops toks of
+    Left (err, toks) => do
+      putStrLn $ showError "" err
+      addError err
+      parseDecls fn ops (recover toks) acc
+    Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl)
+  where
+    recover : TokenList → TokenList
+    recover Nil = Nil
+    -- skip to top token, but make sure there is progress
+    recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds
+      then (tok :: toks)
+      else recover toks
+
+moduleHash : String → List (List String) → M String
+moduleHash src imports = do
+  srcHash <- liftIO $ checksum src
+  top <- getTop
+  let mods = mapMaybe (\x => lookupMap' x top.modules) imports
+  let modHashes = map (\x => x.csum) mods
+  liftIO $ checksum $ fastConcat $ srcHash :: modHashes
+
+importToName : Import → List String
+importToName  (MkImport fc (_,name)) = split name "."
+
+importHints : List TopEntry → M Unit
+importHints Nil = pure MkUnit
+importHints (entry :: entries) = do
+  when (elem Hint entry.eflags) $ \ _ => addHint entry.name
+  importHints entries
+
+processModule : FC → FileSource → List String → List String → M String
+processModule importFC repo stk modns = do
+  top <- getTop
+  -- let modns = (snoc ns nm)
+  let name = joinBy "." modns
+  let (Nothing) = lookupMap modns top.modules | _ => pure ""
+  -- dummy entry for processing
+  modifyTop [modules := updateMap modns (emptyModCtx "") top.modules]
+
+  let fn = joinBy "/" modns ++ ".newt"
+  -- TODO now we can pass in the module name...
+  (fn,src) <- repo.getFile importFC fn
+  let (Right toks) = tokenise fn src
+    | Left err => throwError err
+
+  let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks
+    | Left (err, toks) => throwError err
+
+  log 1 $ \ _ => "scan imports for module \{modName}"
+  let (True) = modns == split modName "."
+    | _ => 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) => throwError err
+
+  let importNames = map importToName imports
+
+  imported <- for imports $ \case
+    MkImport fc (nameFC,name') => do
+      let imp = split name' "."
+      when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} → \{show name'}"
+      processModule nameFC repo (name :: stk) imp
+      pure $ imp
+  let imported = snoc imported primNS
+  srcSum <- liftIO $ checksum src
+  csum <- moduleHash srcSum imported
+
+  putStrLn "module \{modName}"
+  top <- getTop
+  -- TODO we need a flag on this so `make newt3.js` properly tests self-compile
+  (Nothing) <- loadModule modns csum
+    | Just mod => do
+      let modules = updateMap modns mod top.modules
+
+      -- FIXME - we don't want stray operators in a module.
+      -- inject module ops into top
+      let ops = foldMap const top.ops $ toList mod.ctxOps
+      modifyTop [modules := modules; ops := ops ]
+      pure src  -- why am I returning this?
+
+  log 1 $ \ _ => "MODNS " ++ show modns
+  top <- getTop
+  (decls, ops) <- parseDecls fn top.ops toks Lin
+
+  top <- getTop
+  let freshMC = MC emptyMap Nil 0 CheckAll
+  -- set imported, mod, freshMC, ops  before processing
+  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)
+
+  log 1 $ \ _ => "process Decls"
+  traverse (tryProcessDecl src modns) (collectDecl decls)
+
+  -- update modules with result, leave the rest of context in case this is top file
+  top <- getTop
+
+  let mod = MkModCtx csum top.defs top.metaCtx top.ops importNames
+  if stk /= Nil && length' top.errors == 0
+    then dumpModule modns src mod
+    else pure MkUnit
+
+  let modules = updateMap modns mod top.modules
+  modifyTop [modules := modules]
+
+  logMetas $ reverse $ listValues top.metaCtx.metas
+  let (Nil) = top.errors
+    | errors => throwError $ E importFC "Failed to compile module \{joinBy "." modns}"
+  pure src
+  where
+    tryProcessDecl : String → List String → Decl → M Unit
+    tryProcessDecl src ns decl = do
+      (Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
+      putStrLn $ showError src err
+      addError err

src/Lib/Types.newt

@@ -402,7 +402,7 @@ record ModContext where
   modMetaCtx : MetaContext
   -- longer term maybe drop this, put the operator decls in ctxDefs and collect them on import
   ctxOps : Operators
-  modDeps : List QName
+  modDeps : List (List String)
 
 -- Top level context.
 -- Most of the reason this is separate is to have a different type

src/Lib/Util.newt

@@ -32,27 +32,20 @@ splitTele = go Nil
     go ts (Pi fc nm icit quant t u) = go (MkBinder fc nm icit quant t :: ts) u
     go ts tm = (tm, reverse ts)
 
-
+-- given a filename and split module name, return the base path or an error
-
+getBaseDir : String → FC → List String → M String
-getBaseDir : String → FC → String → M (String × QName)
 getBaseDir fn fc modName = do
-  let (path, modName') = unsnoc $ split1 modName "."
+  let path = fst $ splitFileName fn
-  let parts = split1 fn "/"
+  let dirs = split path "/"
-  let (dirs,file) = unsnoc parts
+  let (Right base) = baseDir (Lin <>< dirs) (Lin <>< modName)
-  let (name, ext) = splitFileName file
-
-  let parts = split1 fn "/"
-  let (dirs,file) = unsnoc parts
-  let (path, modName') = unsnoc $ split1 modName "."
-  unless (modName' == name) $ \ _ => error fc "module name \{modName'} doesn't match \{name}"
-  let (Right base) = baseDir (Lin <>< dirs) (Lin <>< path)
     | Left err => error fc err
   let base = if base == "" then "." else base
-  pure (base, QN path modName')
+  pure base
   where
     baseDir : SnocList String -> SnocList String -> Either String String
     baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
     baseDir (dirs :< d) (ns :< n) = if d == n
       then baseDir dirs ns
-      else Left "module path doesn't match directory"
+      else Left "module name \{joinBy "." modName} doesn't match path \{fn}"
-    baseDir Lin _ = Left "module path doesn't match directory"
+    baseDir Lin _ = Left "module name \{joinBy "." modName} doesn't match path \{fn}"
+

src/Main.newt

@@ -11,6 +11,7 @@ import Lib.Util
 import Lib.Parser.Impl
 import Lib.Prettier
 import Lib.ProcessDecl
+import Lib.ProcessModule
 import Lib.Tokenizer
 import Lib.TopContext
 import Lib.Types
@@ -20,6 +21,13 @@ import Node
 import Serialize
 import Revision
 
+dirFileSource : String → FileSource
+dirFileSource base = MkFileSource $ \fc fn => do
+        let fn = base ++ "/" ++ fn
+        (Right src) <- liftIO {M} $ readFile fn
+            | Left err => throwError $ E fc "error reading \{fn}: \{show err}"
+        pure (fn,src)
+
 -- For editors, dump some information about the context (fc, name, type)
 jsonTopContext : M Json
 jsonTopContext = do
@@ -35,16 +43,6 @@ jsonTopContext = do
       :: ("type", toJson (render 80 $ pprint Nil type) )
       :: Nil)
 
-dumpContext : TopContext -> M Unit
-dumpContext top = do
-    putStrLn "Context:"
-    go $ listValues top.defs
-    putStrLn "---"
-  where
-    go : List TopEntry -> M Unit
-    go Nil = pure MkUnit
-    go (x :: xs) = putStrLn "    \{show x}" >> go xs
-
 writeSource : String -> M Unit
 writeSource fn = do
   docs <- compile
@@ -57,139 +55,6 @@ writeSource fn = do
     | Left err => throwError $ E (MkFC fn $ MkBounds 0 0 0 0) err
   pure MkUnit
 
-
-parseDecls : String -> Operators -> TokenList -> SnocList Decl -> M (List Decl × Operators)
-parseDecls fn ops Nil acc = pure (acc <>> Nil, ops)
-parseDecls fn ops toks@(first :: _) acc =
-  case partialParse fn (sameLevel parseDecl) ops toks of
-    Left (err, toks) => do
-      putStrLn $ showError "" err
-      addError err
-      parseDecls fn ops (recover toks) acc
-    Right (decl,ops,toks) => parseDecls fn ops toks (acc :< decl)
-  where
-    recover : TokenList -> TokenList
-    recover Nil = Nil
-    -- skip to top token, but make sure there is progress
-    recover (tok :: toks) = if tok.bounds.startCol == 0 && tok.bounds /= first.bounds
-      then (tok :: toks)
-      else recover toks
-
-moduleHash : String → List (List String) → M String
-moduleHash src imports = do
-  srcHash <- liftIO $ checksum src
-  top <- getTop
-  let mods = mapMaybe (\x => lookupMap' x top.modules) imports
-  let modHashes = map (\x => x.csum) mods
-  liftIO $ checksum $ fastConcat $ srcHash :: modHashes
-
-importHints : List TopEntry → M Unit
-importHints Nil = pure MkUnit
-importHints (entry :: entries) = do
-  when (elem Hint entry.eflags) $ \ _ => addHint entry.name
-  importHints entries
-
-importToQN : Import → QName
-importToQN  (MkImport fc (_,name)) = uncurry QN $ unsnoc $ split1 name "."
-
--- New style loader, one def at a time
-processModule : FC -> String -> List String -> QName -> M String
-processModule importFC base stk qn@(QN ns nm) = do
-  top <- getTop
-  -- TODO make top.loaded a List QName
-  let modns = (snoc ns nm)
-  let name = joinBy "." modns
-  let (Nothing) = lookupMap modns top.modules | _ => pure ""
-  -- dummy entry for processing
-  modifyTop [modules := updateMap modns (emptyModCtx "") top.modules]
-  let fn = (joinBy "/" (base :: ns)) ++ "/" ++ nm ++ ".newt"
-  (Right src) <- liftIO {M} $ readFile fn
-    | Left err => throwError $ E importFC "error reading \{fn}: \{show err}"
-  let (Right toks) = tokenise fn src
-    | Left err => throwError err
-
-  let (Right ((nameFC, modName), ops, toks)) = partialParse fn parseModHeader top.ops toks
-    | 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'
-    | _ => 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) => throwError err
-
-  let importNames = map importToQN imports
-
-  imported <- for imports $ \case
-    MkImport fc (nameFC,name') => do
-      let (a,b) = unsnoc $ split1 name' "."
-      let qname = QN a b
-      when (elem name' stk) $ \ _ => error nameFC "import loop \{show name} -> \{show name'}"
-      processModule nameFC base (name :: stk) qname
-      pure $ split name' "."
-  let imported = snoc imported primNS
-  srcSum <- liftIO $ checksum src
-  csum <- moduleHash srcSum imported
-
-  putStrLn "module \{modName}"
-  top <- getTop
-  -- TODO we need a flag on this so `make newt3.js` properly tests self-compile
-  (Nothing) <- loadModule qn csum
-    | Just mod => do
-      let modules = updateMap modns mod top.modules
-
-      -- FIXME - we don't want stray operators in a module.
-      -- inject module ops into top
-      let ops = foldMap const top.ops $ toList mod.ctxOps
-      modifyTop [modules := modules; ops := ops ]
-      pure src  -- why am I returning this?
-
-  log 1 $ \ _ => "MODNS " ++ show modns
-  top <- getTop
-  (decls, ops) <- parseDecls fn top.ops toks Lin
-
-  top <- getTop
-  let freshMC = MC emptyMap Nil 0 CheckAll
-  -- set imported, mod, freshMC, ops  before processing
-  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)
-
-  log 1 $ \ _ => "process Decls"
-  traverse (tryProcessDecl src ns) (collectDecl decls)
-
-  -- update modules with result, leave the rest of context in case this is top file
-  top <- getTop
-
-  let mod = MkModCtx csum top.defs top.metaCtx top.ops importNames
-  if stk /= Nil && length' top.errors == 0
-    then dumpModule qn src mod
-    else pure MkUnit
-
-  let modules = updateMap modns mod top.modules
-  modifyTop [modules := modules]
-
-  logMetas $ reverse $ listValues top.metaCtx.metas
-  let (Nil) = top.errors
-    | errors => throwError $ E importFC "Failed to compile module \{show qn}"
-  pure src
-  where
-    tryProcessDecl : String -> List String → Decl -> M Unit
-    tryProcessDecl src ns decl = do
-      (Left err) <- tryError $ processDecl ns decl | _ => pure MkUnit
-      putStrLn $ showError src err
-      addError err
-
 -- unwind the module part of the path name
 baseDir : SnocList String -> SnocList String -> Either String String
 baseDir dirs Lin = Right $ joinBy "/" (dirs <>> Nil)
@@ -208,8 +73,8 @@ showErrors fn src = do
         throwError $ E (MkFC fn $ MkBounds 0 0 0 0) "Compile failed"
   pure MkUnit
 
-invalidateModule : QName -> M Unit
+invalidateModule : List String -> M Unit
-invalidateModule (QN ns nm) = modifyTop [modules $= deleteMap (snoc ns nm)]
+invalidateModule modname = modifyTop [modules $= deleteMap modname]
 
 -- processFile called on the top level file
 -- it sets up everything and then recurses into processModule
@@ -229,14 +94,9 @@ processFile fn = do
   let (Right ((nameFC, modName), _, _)) = partialParse fn parseModHeader emptyMap toks
     | Left (err,toks) => throwError err
 
-  (base,qn) <- getBaseDir fn nameFC modName
+  let modns = split modName "."
-
+  base <- getBaseDir fn nameFC modns
-  -- declare internal primitives
+  addPrimitives
-
-  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
   let modules = updateMap primNS (MkModCtx "" top.defs (MC emptyMap Nil 0 CheckAll) top.ops Nil) top.modules
@@ -247,9 +107,9 @@ processFile fn = do
             ; defs := emptyMap
             ]
 
-  invalidateModule qn
+  invalidateModule modns
-
+  let repo = dirFileSource base
-  src <- processModule emptyFC base Nil qn
+  src <- processModule emptyFC repo Nil modns
   top <- getTop
 
   showErrors fn src

src/Prelude.newt

@@ -953,3 +953,5 @@ pfunc fatalError : ∀ a. String → a := `(_, msg) => { throw new Error(msg) }`
 
 foldlM : ∀ m a e. {{Monad m}} → (a → e → m a) → a → List e → m a
 foldlM f a xs = foldl (\ ma b => ma >>= flip f b) (pure a) xs
+
+pfunc unsafePerformIO : ∀ a. IO a → a := `(a, f) => f().h1`

src/Serialize.newt

@@ -7,7 +7,7 @@ import Lib.Types
 import Data.SortedMap
 
 ModFile : U
-ModFile = (String × List TopEntry × List (String × OpDef) × List (QName × MetaEntry) × List QName)
+ModFile = (String × List TopEntry × List (String × OpDef) × List (QName × MetaEntry) × List (List String))
 
 pfunc checksum uses (MkIORes) : String → IO String := `(a) => (w) => {
   const arr = new TextEncoder().encode(a);
@@ -32,9 +32,9 @@ pfunc dumpModFile uses (MkIORes MkUnit): String → ModFile → IO Unit := `(fn,
 
 
 -- for now, include src and use that to see if something changed
-dumpModule : QName → String → ModContext → M Unit
+dumpModule : List String → String → ModContext → M Unit
 dumpModule qn src mod = do
-  let fn = "build/\{show qn}.newtmod"
+  let fn = "build/\{joinBy "." qn}.newtmod"
   let csum = mod.csum
   let defs = listValues mod.modDefs
   let ops = toList mod.ctxOps
@@ -54,9 +54,9 @@ pfunc readModFile uses (MkIORes Just Nothing): String → IO (Maybe ModFile) :=
   }
 }`
 
-loadModule : QName → String → M (Maybe ModContext)
+loadModule : List String → String → M (Maybe ModContext)
 loadModule qn src = do
-  let fn = "build/\{show qn}.newtmod"
+  let fn = "build/\{joinBy "." qn}.newtmod"
   (Just (csum, defs, ops, mctx, deps)) <- liftIO {M} $ readModFile fn
      | _ => pure Nothing