diff --git a/TODO.md b/TODO.md index 8651300..fcaed6a 100644 --- a/TODO.md +++ b/TODO.md @@ -1,17 +1,27 @@ ## TODO +- [ ] redo code to determine base path +- [ ] save/load results of processing a module + - [ ] keep each module separate in context + - search would include imported modules, collect ops into and from modules + - should I allow the idris assignment hack? + - >>> sort out metas (maybe push them up to the main list) + - eventually we may want to support resuming halfway through a file + - [x] get port to run - - [ ] something goes terribly wrong with traverse_ and for_ (related to erasure, I think) + - [x] something goes terribly wrong with traverse_ and for_ (related to erasure, I think) - [ ] sort through issues that came up during port -- [ ] don't use `take` - it's not stack safe +- [x] ~~don't use `take` - it's not stack safe~~ The newt version is stack safe +- [ ] move idris version into a bootstrap directory + - (Need Idris/chez or newt-in-newt to bootstrap!) More comments in code! This is getting big enough that I need to re-find my bearings when fixing stuff. - [ ] report info in case of error - [x] tokenizer that can be ported to newt - [ ] Add default path for library, so we don't need symlinks everywhere and can write tests for the library -- [ ] string interpolation? +- [x] string interpolation? - The tricky part here is the `}` - I need to run the normal tokenizer in a way that treats `}` specially. - Idris handles `putStrLn "done \{ show $ add {x=1} 2}"` - it recurses for `{` `}` pairs. Do we want that complexity? - The mini version would be recurse on `{`, pop on `}` (and expect caller to handle), fail if we get to the top with a tokens remaining. @@ -41,7 +51,7 @@ More comments in code! This is getting big enough that I need to re-find my bear - [x] syntax for negative integers - [ ] White box tests in `test` directory (I can't get this to work right with pack et al) - [x] Put worker in iframe on safari -- [ ] Warnings or errors for missing definitions +- [ ] Warnings or errors for missing definitions (e.g. on `Axiom` in codegen) - [ ] Add the type name to dcon so confusion detection in case split is simpler - [ ] Warnings or errors for unused cases - This is important when misspelled constructors become pattern vars diff --git a/newt/Prelude.newt b/newt/Prelude.newt index a920f47..d04ff82 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -185,15 +185,14 @@ instance Traversable List where traverse f Nil = return Nil traverse f (x :: xs) = return _::_ <*> f x <*> traverse f xs --- something goes madly wrong with erasure in here. --- traverse_ : ∀ t f a b. {{Traversable t}} {{Applicative f}} → (a → f b) → t a → f Unit --- traverse_ f xs = return (const MkUnit) <*> traverse f xs +traverse_ : ∀ t f a b. {{Traversable t}} {{Applicative f}} → (a → f b) → t a → f Unit +traverse_ f xs = return (const MkUnit) <*> traverse f xs for : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f (t b) for stuff fun = traverse fun stuff --- for_ : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f Unit --- for_ stuff fun = return (const MkUnit) <*> traverse fun stuff +for_ : {t : U → U} {f : U → U} → {{Traversable t}} {{appf : Applicative f}} → {a : U} → {b : U} → t a → (a → f b) → f Unit +for_ stuff fun = return (const MkUnit) <*> traverse fun stuff instance Applicative Maybe where return a = Just a diff --git a/port/Data/Fin.newt b/port/Data/Fin.newt deleted file mode 100644 index 88094ba..0000000 --- a/port/Data/Fin.newt +++ /dev/null @@ -1 +0,0 @@ -module Data.Fin diff --git a/port/Data/List.newt b/port/Data/List.newt deleted file mode 100644 index ffa4b72..0000000 --- a/port/Data/List.newt +++ /dev/null @@ -1 +0,0 @@ -module Data.List diff --git a/port/Data/Maybe.newt b/port/Data/Maybe.newt deleted file mode 100644 index 7f138d4..0000000 --- a/port/Data/Maybe.newt +++ /dev/null @@ -1 +0,0 @@ -module Data.Maybe diff --git a/port/Data/Nat.newt b/port/Data/Nat.newt deleted file mode 100644 index 30b96f8..0000000 --- a/port/Data/Nat.newt +++ /dev/null @@ -1 +0,0 @@ -module Data.Nat diff --git a/port/Data/String.newt b/port/Data/String.newt index ccc39f7..5a75cce 100644 --- a/port/Data/String.newt +++ b/port/Data/String.newt @@ -1,11 +1,7 @@ module Data.String - import Prelude -class Interpolation a where - interpolate : a → String - unwords : List String → String unwords stuff = joinBy " " stuff diff --git a/port/Data/Vect.newt b/port/Data/Vect.newt deleted file mode 100644 index 160a6fe..0000000 --- a/port/Data/Vect.newt +++ /dev/null @@ -1 +0,0 @@ -module Data.Vect diff --git a/port/Hello.newt b/port/Hello.newt deleted file mode 100644 index 7648652..0000000 --- a/port/Hello.newt +++ /dev/null @@ -1,7 +0,0 @@ -module Hello - -import Prelude - -main : IO Unit -main = do - putStrLn "hello, world" diff --git a/port/Lib/Common.newt b/port/Lib/Common.newt index 2beba96..9a5cfa7 100644 --- a/port/Lib/Common.newt +++ b/port/Lib/Common.newt @@ -2,7 +2,6 @@ module Lib.Common import Data.String import Data.Int -import Data.Maybe import Data.SortedMap -- l is environment size, this works for both lvl2ix and ix2lvl diff --git a/port/Lib/Compile.newt b/port/Lib/Compile.newt index a046ba1..fa90232 100644 --- a/port/Lib/Compile.newt +++ b/port/Lib/Compile.newt @@ -6,7 +6,6 @@ import Lib.Prettier import Lib.CompileExp import Lib.TopContext import Data.String -import Data.Maybe import Data.Int data StKind = Plain | Return | Assign String diff --git a/port/Lib/CompileExp.newt b/port/Lib/CompileExp.newt index acdc900..b3ed461 100644 --- a/port/Lib/CompileExp.newt +++ b/port/Lib/CompileExp.newt @@ -7,17 +7,13 @@ -- I could make names unique (e.q. on lambdas), but I might want that to vary per backend? module Lib.CompileExp -import Data.List - import Lib.Types -- Name / Tm import Lib.TopContext import Lib.Prettier import Lib.Util - CExp : U - data CAlt : U where CConAlt : String -> List String -> CExp -> CAlt -- REVIEW keep var name? diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt index b4b0513..e6461e6 100644 --- a/port/Lib/Elab.newt +++ b/port/Lib/Elab.newt @@ -2,7 +2,6 @@ module Lib.Elab import Lib.Parser.Impl import Lib.Prettier -import Data.List import Data.String import Data.IORef import Lib.Types diff --git a/port/Lib/Erasure.newt b/port/Lib/Erasure.newt index 3999802..be5fd06 100644 --- a/port/Lib/Erasure.newt +++ b/port/Lib/Erasure.newt @@ -1,7 +1,6 @@ module Lib.Erasure import Lib.Types -import Data.Maybe import Data.SnocList import Lib.TopContext diff --git a/port/Lib/Eval.newt b/port/Lib/Eval.newt index 30395fb..624f198 100644 --- a/port/Lib/Eval.newt +++ b/port/Lib/Eval.newt @@ -4,10 +4,7 @@ import Lib.Types import Lib.TopContext import Data.IORef -import Data.Fin -import Data.List import Data.SnocList -import Data.Vect import Data.SortedMap @@ -252,7 +249,7 @@ nfv env t = eval env CBV t >>= quote (length' env) prvalCtx : {{ctx : Context}} -> Val -> M String prvalCtx {{ctx}} v = do tm <- quote ctx.lvl v - pure $ interpolate $ pprint (map fst ctx.types) tm + pure $ render 90 $ pprint (map fst ctx.types) tm -- REVIEW - might be easier if we inserted the meta without a bunch of explicit App -- I believe Kovacs is doing that. diff --git a/port/Lib/Parser.newt b/port/Lib/Parser.newt index 3542d83..c69de78 100644 --- a/port/Lib/Parser.newt +++ b/port/Lib/Parser.newt @@ -2,7 +2,6 @@ module Lib.Parser -- NOW Still working on this. -import Data.Maybe import Data.String import Lib.Parser.Impl import Lib.Syntax diff --git a/port/Lib/Prettier.newt b/port/Lib/Prettier.newt index 700c893..6da0bb9 100644 --- a/port/Lib/Prettier.newt +++ b/port/Lib/Prettier.newt @@ -2,9 +2,7 @@ -- https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf module Lib.Prettier -import Data.String import Data.Int -import Data.Maybe -- `Doc` is a pretty printing document. Constructors are private, use -- methods below. `Alt` in particular has some invariants on it, see paper @@ -150,7 +148,3 @@ fill (x :: y :: xs) = Alt (flatten x <+> fill (flatten y :: xs)) (x fill (y commaSep : List Doc -> Doc commaSep = folddoc (\a b => a ++ text "," <+/> b) --- If we stick Doc into a String, try to avoid line-breaks via `flatten` - -instance Interpolation Doc where - interpolate = render 80 ∘ flatten diff --git a/port/Lib/ProcessDecl.newt b/port/Lib/ProcessDecl.newt index 2e8660c..a079a66 100644 --- a/port/Lib/ProcessDecl.newt +++ b/port/Lib/ProcessDecl.newt @@ -2,9 +2,6 @@ module Lib.ProcessDecl import Data.IORef import Data.String -import Data.Vect -import Data.List -import Data.Maybe import Lib.Elab import Lib.Parser @@ -78,7 +75,7 @@ logMetas mstart = do matches <- findMatches ctx ty $ map snd $ toList top.defs -- TODO try putting mc into TopContext for to see if it gives better terms pure $ (" \{show $ length' matches} Solutions: \{show matches}" :: Nil) - -- pure $ " \{show $ length' matches} Solutions:" :: map ((" " ++) ∘ interpolate ∘ pprint (names ctx) ∘ fst) matches + -- pure $ " \{show $ length' matches} Solutions:" :: map ((" " ++) ∘ render 90 ∘ pprint (names ctx) ∘ fst) matches _ => pure Nil info fc $ unlines ((msg :: Nil) ++ msgs ++ sols) @@ -262,7 +259,7 @@ processDecl ns (Instance instfc ty decls) = do -- ok so we need a name, a hack for now. -- Maybe we need to ask the user (e.g. `instance someName : Monad Foo where`) -- or use "Monad\{show $ length' defs}" - let instname = interpolate $ pprint Nil codomain + let instname = render 90 $ pprint Nil codomain let sigDecl = TypeSig instfc (instname :: Nil) ty -- This needs to be declared before processing the defs, but the defs need to be -- declared before this - side effect is that a duplicate def is noted at the first diff --git a/port/Lib/Syntax.newt b/port/Lib/Syntax.newt index 7691be1..d8f2b8d 100644 --- a/port/Lib/Syntax.newt +++ b/port/Lib/Syntax.newt @@ -1,7 +1,6 @@ module Lib.Syntax import Data.String -import Data.Maybe import Lib.Parser.Impl import Lib.Prettier import Lib.Types diff --git a/port/Lib/Types.newt b/port/Lib/Types.newt index 54a1581..77f87b6 100644 --- a/port/Lib/Types.newt +++ b/port/Lib/Types.newt @@ -4,13 +4,10 @@ module Lib.Types import Lib.Common import Lib.Prettier -import Data.Fin import Data.IORef -import Data.List import Data.SnocList import Data.SortedMap import Data.String -import Data.Vect data QName : U where QN : List String -> String -> QName @@ -22,9 +19,6 @@ instance Show QName where show (QN Nil n) = n show (QN ns n) = joinBy "." ns ++ "." ++ n -instance Interpolation QName where - interpolate = show - instance Ord QName where compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' diff --git a/port/Main.newt b/port/Main.newt index a5cb62d..c8f4e4a 100644 --- a/port/Main.newt +++ b/port/Main.newt @@ -1,9 +1,7 @@ module Main -import Data.List import Data.List1 import Data.String -import Data.Vect import Data.IORef import Lib.Common import Lib.Compile @@ -19,11 +17,6 @@ import Lib.Types import Lib.Syntax import Lib.Syntax import Node --- import System --- import System.Directory --- import System.File --- import System.Path --- import Data.Buffer jsonTopContext : M Json jsonTopContext = do @@ -155,7 +148,7 @@ showErrors fn src = do top <- get (Nil) <- liftIO {M} $ readIORef top.errors | errors => do - ignore $ for errors $ \err => + for_ errors $ \err => putStrLn (showError src err) -- if err.file == fn -- then putStrLn (showError src err)