imports

TODO.md

@@ -3,6 +3,8 @@
 
 I may be done with `U` - I keep typing `Type`.
 
+- [ ] Generate some programs that do stuff
+- [ ] import
 - [ ] consider making meta application implicit in term, so its more readable when printed
   - Currently we have explicit `App` surrounding `Meta` when inserting metas. Some people
     leave that implicit for efficiency. I think it would also make printing more readable.
@@ -23,7 +25,6 @@ I may be done with `U` - I keep typing `Type`.
   - [x] case statements
 - [x] SKIP list syntax
   - Agda doesn't have it, clashes with pair syntax
-- [ ] import
 - [ ] autos / typeclass resolution
   - We need special handling in unification to make this possible
   - options

newt-vscode/src/extension.ts

@@ -27,11 +27,11 @@ export function activate(context: vscode.ExtensionContext) {
       const diagnostics: vscode.Diagnostic[] = [];
 
       if (err) {
-        let start = new vscode.Position(0,0)
+        let start = new vscode.Position(0,0);
-        let end = new vscode.Position(0,1)
+        let end = new vscode.Position(0,1);
-        let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start,end)
+        let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start,end);
-        const diag = new vscode.Diagnostic(range, "newt execution failed", vscode.DiagnosticSeverity.Error)
+        const diag = new vscode.Diagnostic(range, "newt execution failed", vscode.DiagnosticSeverity.Error);
-        diagnostics.push(diag)
+        diagnostics.push(diag);
       }
 
       for (let i = 0; i < lines.length; i++) {

newt-vscode/syntaxes/newt.tmLanguage.json

@@ -16,7 +16,7 @@
     },
     {
       "name": "keyword.newt",
-      "match": "\\b(data|where|case|of|let|in|U|module|ptype|pfunc|infix|infixl|infixr)\\b"
+      "match": "\\b(data|where|case|of|let|in|U|module|import|ptype|pfunc|infix|infixl|infixr)\\b"
     }
   ]
 }

newt/Equality1.newt

@@ -1,4 +1,4 @@
-module Equality
+module Equality1
 
 -- Leibniz equality
 Eq : {A : U} -> A -> A -> U

newt/oper.newt

@@ -1,48 +0,0 @@
-module Oper
-
--- These are hard-coded at the moment
--- For now they must be of the form _op_, we'll circle back
--- with a different parser, but that works today.
-
--- this will be parsed as a top level decl, collected in TopContext, and
--- injected into the Parser. It'll need to be passed around or available
--- for read in the monad.
-
--- long term, I might want TopContext in the parser, and parse a top-level
--- declaration at a time (for incremental updates), but much longer term.
-
-infixl 4 _+_
-infixl 4 _-_
-infixl 5 _*_
-infixl 5 _/_
-
-ptype Int
-ptype String
-ptype JVoid
-
--- If we had a different quote here, we could tell vscode it's javascript.
--- or actually just switch modes inside pfunc
-pfunc log : String -> JVoid := "(x) => console.log(x)"
-pfunc plus : Int -> Int -> Int := "(x,y) => x + y"
-pfunc _*_ : Int -> Int -> Int := "(x,y) => x * y"
-
--- We now have to clean JS identifiers
-_+_ : Int -> Int -> Int
-_+_ x y = plus x y
-
-test : Int -> Int
-test x = 42 + x * 3 + 2
-
-infixr 2 _,_
-data Pair : U -> U -> U where
-  _,_ : {A B : U} -> A -> B -> Pair A B
-
-blah : Int -> Int -> Int -> Pair Int (Pair Int Int)
-blah x y z = (x, y, z)
-
-curryPlus : Pair Int Int -> Int
-curryPlus (a, b) = a + b
-
-caseCurry : Pair Int Int -> Int
-caseCurry x = case x of
-  (a,b) => a + b

src/Lib/Parser.idr

@@ -342,8 +342,6 @@ parseMod : Parser Module
 parseMod = do
   keyword "module"
   name <- uident
-  -- probably should be manySame, and we want to start with col -1
-  -- if we enforce blocks indent more than parent
   decls <- startBlock $ manySame $ parseDecl
   pure $ MkModule name decls
 

src/Lib/ProcessDecl.idr

@@ -107,7 +107,7 @@ processDecl (DCheck fc tm ty) = do
   putStrLn "norm \{pprint [] norm}"
   putStrLn "NF "
 
-processDecl (DImport fc str) = throwError $ E fc "import not implemented"
+processDecl (DImport fc str) = pure ()
 
 processDecl (Data fc nm ty cons) = do
   ctx <- get

src/Main.idr

@@ -23,8 +23,24 @@ import Lib.Syntax
 import System
 import System.Directory
 import System.File
+import System.Path
 
-fail : String -> M ()
+{-
+
+import
+
+need to find the file.
+- get base directory
+- . to /
+- add .newt
+
+
+
+loop back to processFile
+
+-}
+
+fail : String -> M a
 fail msg = putStrLn msg >> exitFailure
 
 dumpContext : TopContext -> M ()
@@ -42,19 +58,45 @@ dumpSource = do
   doc <- compile
   putStrLn $ render 90 doc
 
-processFile : String -> M ()
+parseFile : String -> M (String,Module)
-processFile fn = do
+parseFile fn = do
-  putStrLn "*** Process \{fn}"
   Right src <- readFile $ fn
-    | Left err => printLn err
+    | Left err => fail (show err)
   let toks = tokenise src
   let Right res = parse parseMod toks
     | Left y => fail (showError src y)
-  putStrLn $ render 80 $ pretty res
+  pure (src, res)
-  printLn "process Decls"
+
+loadModule : String -> String -> M ()
+loadModule base name = do
+  let fn = base ++ "/" ++ name ++ ".newt"
+  (src, res) <- parseFile fn
+  putStrLn "module \{res.name}"
+  let True = name == res.name
+    | _ => fail "module name \{show res.name} doesn't match file name \{show fn}"
+  -- TODO separate imports and detect loops / redundant 
+  for_ res.decls $ \ decl => case decl of
+    (DImport x str) => loadModule base str
+    _ => pure ()
+
+
+  putStrLn "process Decls"
   Right _ <- tryError $ traverse_ processDecl (collectDecl res.decls)
     | Left y => fail (showError src y)
 
+  pure ()
+
+processFile : String -> M ()
+processFile fn = do
+  putStrLn "*** Process \{fn}"
+  (src, res) <- parseFile fn
+  putStrLn "module \{res.name}"
+  let parts = splitPath fn
+  let file = fromMaybe "" $ last' parts
+  let dir = fromMaybe "./" $ parent fn
+  let (base,ext) = splitFileName (fromMaybe "" $ last' parts)
+  putStrLn "\{show dir} \{show base} \{show ext}"
+  loadModule dir base
   top <- get
   dumpContext top
   dumpSource

tests/black/Prelude.newt

@@ -0,0 +1,14 @@
+module Prelude
+
+data Nat : U where
+  Z : Nat
+  S : Nat -> Nat
+
+data Maybe : U -> U where
+  Just : {a : U} -> a -> Maybe a
+  Nothing : {a : U} -> Maybe a
+
+data Either : U -> U -> U where
+  Left : {a b : U} -> a -> Either a b
+  Right : {a b : U} -> b -> Either a b
+

tests/black/Test1.newt

@@ -1,4 +1,4 @@
-module Scratch
+module Test1
 
 nat : U
 nat = {C : U} -> C -> (nat -> C) -> C

tests/black/TestCase.newt

@@ -1,4 +1,4 @@
-module Scratch
+module TestCase
 
 -- I'm testing cases here, but using examples carefully design to be
 -- simple case trees. Patterns are a var or a constructor applied to vars.

tests/black/TestCase2.newt

@@ -1,4 +1,4 @@
-module Scratch
+module TestCase2
 
 data Nat : U where
   Z : Nat

tests/black/TestCase3.newt

@@ -1,4 +1,4 @@
-module Scratch2
+module TestCase3
 
 data Nat : U where
   Z : Nat

tests/black/TestImport.newt

@@ -0,0 +1,7 @@
+module TestImport
+
+import Prelude
+
+one : Nat
+one = S Z
+

tests/black/Zoo2eg.newt

@@ -1,4 +1,4 @@
-module Zoo2
+module Zoo2eg
 
 id : (A : U) -> A -> A
 id = \ A x => x

tests/black/Zoo3eg.newt

@@ -1,4 +1,4 @@
-module Zoo3
+module Zoo3eg
 
 id : (A : _) -> A -> A
 id = \ A x => x

tests/black/Zoo4eg.newt

@@ -1,4 +1,4 @@
-module Zoo4
+module Zoo4eg
 
 id : {A : U} -> A -> A
 id = \x => x   -- elaborated to \{A} x. x