diff --git a/playground/samples/Prelude.newt b/playground/samples/Prelude.newt index da29d0a..9ac4446 100644 --- a/playground/samples/Prelude.newt +++ b/playground/samples/Prelude.newt @@ -37,23 +37,23 @@ fromMaybe a Nothing = a fromMaybe _ (Just a) = a data Either : U -> U -> U where - Left : {a b : U} -> a -> Either a b - Right : {a b : U} -> b -> Either a b + Left : {0 a b : U} -> a -> Either a b + Right : {0 a b : U} -> b -> Either a b infixr 7 _::_ data List : U -> U where - Nil : {A} → List A - _::_ : {A} → A → List A → List A + Nil : ∀ A. List A + _::_ : ∀ A. A → List A → List A infixl 7 _:<_ data SnocList : U → U where - Lin : {A} → SnocList A - _:<_ : {A} → SnocList A → A → SnocList A + Lin : ∀ A. SnocList A + _:<_ : ∀ A. SnocList A → A → SnocList A -- 'chips' infixr 6 _<>>_ -_<>>_ : {a} → SnocList a → List a → List a +_<>>_ : ∀ a. SnocList a → List a → List a Lin <>> ys = ys (xs :< x) <>> ys = xs <>> x :: ys @@ -67,7 +67,7 @@ f $ a = f a infixr 8 _×_ infixr 2 _,_ data _×_ : U → U → U where - _,_ : {A B} → A → B → A × B + _,_ : ∀ A B. A → B → A × B infixl 6 _<_ class Ord a where @@ -81,14 +81,14 @@ instance Ord Nat where -- Monad class Monad (m : U → U) where - bind : {a b} → m a → (a → m b) → m b - pure : {a} → a → m a + bind : {0 a b} → m a → (a → m b) → m b + pure : {0 a} → a → m a infixl 1 _>>=_ _>>_ -_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b +_>>=_ : {0 m} {{Monad m}} {0 a b} -> (m a) -> (a -> m b) -> m b ma >>= amb = bind ma amb -_>>_ : {m} {{Monad m}} {a b} -> m a -> m b -> m b +_>>_ : {0 m} {{Monad m}} {0 a b} -> m a -> m b -> m b ma >> mb = mb -- Equality @@ -108,10 +108,10 @@ sym Refl = Refl -- Functor class Functor (m : U → U) where - map : {a b} → (a → b) → m a → m b + map : {0 a b} → (a → b) → m a → m b infixr 4 _<$>_ -_<$>_ : {f} {{Functor f}} {a b} → (a → b) → f a → f b +_<$>_ : {0 f} {{Functor f}} {0 a b} → (a → b) → f a → f b f <$> ma = map f ma instance Functor Maybe where @@ -130,12 +130,12 @@ instance Functor SnocList where infixl 3 _<*>_ class Applicative (f : U → U) where -- appIsFunctor : Functor f - return : {a} → a → f a - _<*>_ : {a b} -> f (a → b) → f a → f b + return : {0 a} → a → f a + _<*>_ : {0 a b} -> f (a → b) → f a → f b infixr 2 _<|>_ class Alternative (m : U → U) where - _<|>_ : {a} → m a → m a → m a + _<|>_ : {0 a} → m a → m a → m a instance Alternative Maybe where Nothing <|> x = x @@ -266,9 +266,9 @@ instance Monad IO where MkIORes a w => mab a w pure a = \ w => MkIORes a w -pfunc putStrLn : String -> IO Unit := `(s) => (w) => { +pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => { console.log(s) - return MkIORes(Unit,MkUnit,w) + return MkIORes(undefined,MkUnit,w) }` pfunc showInt : Int -> String := `(i) => String(i)` @@ -285,8 +285,7 @@ instance Show Int where pfunc ord : Char -> Int := `(c) => c.charCodeAt(0)` infix 6 _<=_ -pfunc _<=_ : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False` - +pfunc _<=_ uses (True False) : Int -> Int -> Bool := `(x,y) => (x <= y) ? True : False` pfunc unpack : String -> List Char := `(s) => { @@ -309,7 +308,7 @@ _∘_ : {A B C : U} -> (B -> C) -> (A -> B) -> A -> C pfunc addInt : Int → Int → Int := `(x,y) => x + y` pfunc mulInt : Int → Int → Int := `(x,y) => x * y` pfunc subInt : Int → Int → Int := `(x,y) => x - y` -pfunc ltInt : Int → Int → Bool := `(x,y) => x < y ? True : False` +pfunc ltInt uses (True False) : Int → Int → Bool := `(x,y) => x < y ? True : False` instance Mul Int where x * y = mulInt x y diff --git a/playground/samples/Tour.newt b/playground/samples/Tour.newt index 3c5977a..b0195e3 100644 --- a/playground/samples/Tour.newt +++ b/playground/samples/Tour.newt @@ -209,3 +209,33 @@ prod xs ys = do x <- xs y <- ys pure (x, y) + +-- The playground is compiling to javascript and will give an error if +-- main isn't implemented, so I'll crib the definition of IO from +-- Prelude: + +data Unit : U where + MkUnit : Unit + +ptype World + +data IORes : U -> U where + MkIORes : ∀ a. a -> World -> IORes a + +IO : U -> U +IO a = World -> IORes a + +instance Monad IO where + bind ma mab = \ w => case ma w of + MkIORes a w => mab a w + pure a = \ w => MkIORes a w + +-- Here we declare `uses` to let the dead code elimination know we're poking +-- at MKIORes and MkUnit behind the compiler's back. +pfunc putStrLn uses (MkIORes MkUnit) : String -> IO Unit := `(s) => (w) => { + console.log(s) + return MkIORes(undefined,MkUnit,w) +}` + +main : IO Unit +main = putStrLn "hello, world" diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 621c6f9..2a9dc46 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -308,7 +308,12 @@ process (done,docs) nm = do export compile : M (List Doc) --- compile = do --- top <- get --- traverse entryToDoc top.defs -compile = reverse . snd <$> process ([],[]) "main" +compile = do + top <- get + case lookup "main" top of + Just _ => reverse . snd <$> process ([],[]) "main" + -- If there is no main, compile everything for the benefit of the playground + Nothing => do + top <- get + traverse entryToDoc top.defs + diff --git a/src/Lib/CompileExp.idr b/src/Lib/CompileExp.idr index 833dfa6..0626482 100644 --- a/src/Lib/CompileExp.idr +++ b/src/Lib/CompileExp.idr @@ -110,20 +110,8 @@ compileTerm (Meta _ k) = pure $ CRef "meta$\{show k}" -- FIXME compileTerm (Lam _ nm t) = pure $ CLam nm !(compileTerm t) compileTerm tm@(App _ _ _) with (funArgs tm) _ | (Meta _ k, args) = do - -- FIXME get arity or zonk? - -- let's see if this happens after zonking - error (getFC tm) "Lambda in CompileExp" - -- Maybe we should be storing the Term without the lambdas... - -- we don't have a lot here, but JS has an "environment" with names and - -- we can assume fully applied. - -- meta <- lookupMeta k - -- args' <- traverse compileTerm args - -- -- apply (CRef "Meta\{show k}") args' [<] 0 - -- arity <- case meta of - -- -- maybe throw - -- (Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds - -- (Solved _ j tm) => pure $ lamArity !(quote 0 tm) - -- apply (CRef "Meta\{show k}") args' [<] arity + -- this will be undefined, should only happen for use metas + pure $ CApp (CRef "Meta\{show k}") [] _ | (t@(Ref fc nm _), args) = do args' <- traverse compileTerm args arity <- arityForName fc nm @@ -160,4 +148,3 @@ compileFun tm = go tm [<] go tm args = pure $ CFun (args <>> []) !(compileTerm tm) -