diff --git a/TODO.md b/TODO.md index e972ea3..cb22321 100644 --- a/TODO.md +++ b/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 diff --git a/newt-vscode/src/extension.ts b/newt-vscode/src/extension.ts index 29c02bc..37d7f24 100644 --- a/newt-vscode/src/extension.ts +++ b/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 end = new vscode.Position(0,1) - let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start,end) - const diag = new vscode.Diagnostic(range, "newt execution failed", vscode.DiagnosticSeverity.Error) - diagnostics.push(diag) + let start = new vscode.Position(0,0); + let end = new vscode.Position(0,1); + let range = document.getWordRangeAtPosition(start) ?? new vscode.Range(start,end); + const diag = new vscode.Diagnostic(range, "newt execution failed", vscode.DiagnosticSeverity.Error); + diagnostics.push(diag); } for (let i = 0; i < lines.length; i++) { diff --git a/newt-vscode/syntaxes/newt.tmLanguage.json b/newt-vscode/syntaxes/newt.tmLanguage.json index aa4c512..d0716e0 100644 --- a/newt-vscode/syntaxes/newt.tmLanguage.json +++ b/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" } ] } diff --git a/newt/equality.newt b/newt/Equality.newt similarity index 100% rename from newt/equality.newt rename to newt/Equality.newt diff --git a/newt/eq.newt b/newt/Equality1.newt similarity index 98% rename from newt/eq.newt rename to newt/Equality1.newt index 8ee0f11..c216a62 100644 --- a/newt/eq.newt +++ b/newt/Equality1.newt @@ -1,4 +1,4 @@ -module Equality +module Equality1 -- Leibniz equality Eq : {A : U} -> A -> A -> U diff --git a/newt/ex.newt b/newt/Foo.newt similarity index 100% rename from newt/ex.newt rename to newt/Foo.newt diff --git a/newt/order.newt b/newt/Order.newt similarity index 100% rename from newt/order.newt rename to newt/Order.newt diff --git a/newt/oper.newt b/newt/oper.newt deleted file mode 100644 index 90aef54..0000000 --- a/newt/oper.newt +++ /dev/null @@ -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 diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index a77708b..29372dc 100644 --- a/src/Lib/Parser.idr +++ 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 diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index 3455c77..13ac4f3 100644 --- a/src/Lib/ProcessDecl.idr +++ b/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 diff --git a/src/Main.idr b/src/Main.idr index af01499..22e7312 100644 --- a/src/Main.idr +++ b/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 () -processFile fn = do - putStrLn "*** Process \{fn}" +parseFile : String -> M (String,Module) +parseFile fn = do 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 - printLn "process Decls" + pure (src, res) + +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 diff --git a/tests/black/case3.newt b/tests/black/Case3.newt similarity index 100% rename from tests/black/case3.newt rename to tests/black/Case3.newt diff --git a/tests/black/caseeval.newt b/tests/black/CaseEval.newt similarity index 100% rename from tests/black/caseeval.newt rename to tests/black/CaseEval.newt diff --git a/tests/black/equality.newt b/tests/black/Equality.newt similarity index 100% rename from tests/black/equality.newt rename to tests/black/Equality.newt diff --git a/tests/black/let.newt b/tests/black/Let.newt similarity index 100% rename from tests/black/let.newt rename to tests/black/Let.newt diff --git a/tests/black/oper.newt b/tests/black/Oper.newt similarity index 100% rename from tests/black/oper.newt rename to tests/black/Oper.newt diff --git a/tests/black/Prelude.newt b/tests/black/Prelude.newt new file mode 100644 index 0000000..ba6b0e0 --- /dev/null +++ b/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 + diff --git a/tests/black/test1.newt b/tests/black/Test1.newt similarity index 93% rename from tests/black/test1.newt rename to tests/black/Test1.newt index 526b4e7..d17e526 100644 --- a/tests/black/test1.newt +++ b/tests/black/Test1.newt @@ -1,4 +1,4 @@ -module Scratch +module Test1 nat : U nat = {C : U} -> C -> (nat -> C) -> C diff --git a/tests/black/testcase.newt b/tests/black/TestCase.newt similarity index 98% rename from tests/black/testcase.newt rename to tests/black/TestCase.newt index ba3b754..ec04867 100644 --- a/tests/black/testcase.newt +++ b/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. diff --git a/tests/black/testcase2.newt b/tests/black/TestCase2.newt similarity index 98% rename from tests/black/testcase2.newt rename to tests/black/TestCase2.newt index 8bca1b6..f390366 100644 --- a/tests/black/testcase2.newt +++ b/tests/black/TestCase2.newt @@ -1,4 +1,4 @@ -module Scratch +module TestCase2 data Nat : U where Z : Nat diff --git a/tests/black/testcase3.newt b/tests/black/TestCase3.newt similarity index 97% rename from tests/black/testcase3.newt rename to tests/black/TestCase3.newt index 8c03694..89c2fdb 100644 --- a/tests/black/testcase3.newt +++ b/tests/black/TestCase3.newt @@ -1,4 +1,4 @@ -module Scratch2 +module TestCase3 data Nat : U where Z : Nat diff --git a/tests/black/TestImport.newt b/tests/black/TestImport.newt new file mode 100644 index 0000000..5d6dcd2 --- /dev/null +++ b/tests/black/TestImport.newt @@ -0,0 +1,7 @@ +module TestImport + +import Prelude + +one : Nat +one = S Z + diff --git a/tests/black/testprim.newt b/tests/black/TestPrim.newt similarity index 100% rename from tests/black/testprim.newt rename to tests/black/TestPrim.newt diff --git a/tests/black/typeclass.newt b/tests/black/TypeClass.newt similarity index 100% rename from tests/black/typeclass.newt rename to tests/black/TypeClass.newt diff --git a/tests/black/zoo2eg.newt b/tests/black/Zoo2eg.newt similarity index 97% rename from tests/black/zoo2eg.newt rename to tests/black/Zoo2eg.newt index 0855457..1364624 100644 --- a/tests/black/zoo2eg.newt +++ b/tests/black/Zoo2eg.newt @@ -1,4 +1,4 @@ -module Zoo2 +module Zoo2eg id : (A : U) -> A -> A id = \ A x => x diff --git a/tests/black/zoo3eg.newt b/tests/black/Zoo3eg.newt similarity index 98% rename from tests/black/zoo3eg.newt rename to tests/black/Zoo3eg.newt index 5b146cf..102b042 100644 --- a/tests/black/zoo3eg.newt +++ b/tests/black/Zoo3eg.newt @@ -1,4 +1,4 @@ -module Zoo3 +module Zoo3eg id : (A : _) -> A -> A id = \ A x => x diff --git a/tests/black/zoo4eg.newt b/tests/black/Zoo4eg.newt similarity index 99% rename from tests/black/zoo4eg.newt rename to tests/black/Zoo4eg.newt index 5da9952..b38e2bf 100644 --- a/tests/black/zoo4eg.newt +++ b/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