diff --git a/TODO.md b/TODO.md index 250ed82..8651300 100644 --- a/TODO.md +++ b/TODO.md @@ -1,6 +1,11 @@ ## TODO +- [x] get port to run + - [ ] 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 + 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 diff --git a/done/Data/IORef.newt b/done/Data/IORef.newt index c9f2232..08014ed 100644 --- a/done/Data/IORef.newt +++ b/done/Data/IORef.newt @@ -7,7 +7,7 @@ import Prelude ptype IORef : U → U pfunc primNewIORef uses (MkIORes MkUnit) : ∀ a. a → IO (IORef a) := `(_, a) => (w) => MkIORes(undefined, [a], w)` pfunc primReadIORef uses (MkIORes MkUnit) : ∀ a. IORef a → IO a := `(_, ref) => (w) => MkIORes(undefined, ref[0], w)` -pfunc primWriteIORef uses (MkIORes MkUnit) : ∀ a. IORef a → a → IO a := `(_, ref, a) => (w) => { +pfunc primWriteIORef uses (MkIORes MkUnit) : ∀ a. IORef a → a → IO Unit := `(_, ref, a) => (w) => { ref[0] = a return MkIORes(undefined,MkUnit,w) }` @@ -19,7 +19,7 @@ readIORef : ∀ io a. {{HasIO io}} → IORef a → io a readIORef ref = liftIO $ primReadIORef ref writeIORef : ∀ io a. {{HasIO io}} → IORef a -> a -> io Unit -writeIORef ref a = liftIO $ writeIORef ref a +writeIORef ref a = liftIO $ primWriteIORef ref a -- Idris HasIO constraints to monad, we don't have those constraints yet modifyIORef : ∀ io a. {{Monad io}} {{HasIO io}} → IORef a -> (a -> a) -> io Unit diff --git a/done/Hello.newt b/done/Hello.newt new file mode 100644 index 0000000..7648652 --- /dev/null +++ b/done/Hello.newt @@ -0,0 +1,7 @@ +module Hello + +import Prelude + +main : IO Unit +main = do + putStrLn "hello, world" diff --git a/done/Lib/ProcessDecl.newt b/done/Lib/ProcessDecl.newt index 0885c2c..2e8660c 100644 --- a/done/Lib/ProcessDecl.newt +++ b/done/Lib/ProcessDecl.newt @@ -122,7 +122,7 @@ processDecl ns (TypeSig fc names tm) = do ty <- check (mkCtx fc) tm (VU fc) ty <- zonk top 0 Nil ty putStrLn "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}" - for_ names $ \nm => setDef (QN ns nm) fc ty Axiom + ignore $ for names $ \nm => setDef (QN ns nm) fc ty Axiom -- Zoo4eg has metas in TypeSig, need to decide if I want to support leaving them unsolved here -- logMetas mstart @@ -444,7 +444,7 @@ processDecl ns (Record recordFC nm tele cname decls) = do putStrLn "Decl:" putStrLn $ render 90 $ pretty decl processDecl ns decl - for_ fields $ \case + ignore $ for fields $ \case (fc,name,ty) => do -- TODO dependency isn't handled yet -- we'll need to replace stuff like `len` with `len self`. diff --git a/done/Main.newt b/done/Main.newt index 0d1ba52..3692c70 100644 --- a/done/Main.newt +++ b/done/Main.newt @@ -106,7 +106,7 @@ processModule importFC base stk qn@(QN ns nm) = do let (Right (imports, ops, toks)) = partialParse fn parseImports ops toks | Left (err, toks) => exitFailure (showError src err) - for_ imports $ \case + for imports $ \case MkImport fc name' => do let (a,b) = unsnoc $ split1 name' "." let qname = QN a b @@ -214,7 +214,7 @@ main' = do let (arg0 :: args) = getArgs | _ => error emptyFC "error reading args" (out, files) <- cmdLine args - traverse_ processFile files + traverse processFile files when (elem "--top" args) $ \ _ => do json <- jsonTopContext diff --git a/done/Node.newt b/done/Node.newt index 1577e9c..bb04eb6 100644 --- a/done/Node.newt +++ b/done/Node.newt @@ -17,7 +17,7 @@ pfunc readFile uses (fs MkIORes Left Right) : (fn : String) -> IO (Either String }` -- I wonder if I should automatically `uses` the constructors in the types -pfunc writeFile uses (fs MkIORes MkUnit) : String → String → IO (Either String Unit) := `(fn, content) => { +pfunc writeFile uses (fs MkIORes MkUnit) : String → String → IO (Either String Unit) := `(fn, content) => (w) => { let result try { fs.writeFileSync(fn, content, 'utf8') diff --git a/newt/Prelude.newt b/newt/Prelude.newt index 6c7c715..76b58ea 100644 --- a/newt/Prelude.newt +++ b/newt/Prelude.newt @@ -185,15 +185,15 @@ instance Traversable List where traverse f Nil = return Nil traverse f (x :: xs) = return _::_ <*> f x <*> 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 +-- 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 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 @@ -330,8 +330,8 @@ pfunc intToNat uses (Z S) : Int -> Nat := `(n) => { -pfunc fastConcat : List String → String := `(xs) => listToArray(undefined, xs).join('')` -pfunc replicate : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` +pfunc fastConcat uses (listToArray) : List String → String := `(xs) => listToArray(undefined, xs).join('')` +pfunc replicate uses (natToInt) : Nat -> Char → String := `(n,c) => c.repeat(natToInt(n))` -- I don't want to use an empty type because it would be a proof of void ptype World