diff --git a/eg/ex.newt b/eg/ex.newt index de13ec0..94431b5 100644 --- a/eg/ex.newt +++ b/eg/ex.newt @@ -8,4 +8,12 @@ id = \ a => \ x => x -- errors aren't cutting to the top -- I think we need the errors to be fatal if anything is consumed (since the nearest alt) -foo +List : U -> U +List = \ A => (L : U) -> L -> (A -> L -> L) -> L + +-- need more sugar for lambdas +nil : (A : U) -> (L : U) -> L -> (A -> L -> L) -> L +nil = \ A => \ L => \ n => \ f => n + +Bool : U + diff --git a/newt.ipkg b/newt.ipkg index 7fc9326..3acd574 100644 --- a/newt.ipkg +++ b/newt.ipkg @@ -13,7 +13,7 @@ authors = "Steve Dunham" -- langversion -- packages to add to search path -depends = contrib, base +depends = contrib, base, elab-util -- modules to install -- modules = diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 24c7e78..e7fb559 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -6,10 +6,11 @@ import Lib.Parser.Impl import Data.Vect import Data.String import Lib.TT +import Lib.TopContext import Syntax -- cribbed this, it avoids MonadError String m => everywhere -parameters {0 m : Type -> Type} {auto _ : MonadError String m} +parameters {0 m : Type -> Type} {auto _ : MonadError String m} (top : TopContext) export infer : Context -> Raw -> m (Tm, Val) @@ -33,7 +34,7 @@ parameters {0 m : Type -> Type} {auto _ : MonadError String m} infer ctx (RVar nm) = go 0 ctx.types where - go : Nat -> List (String, Val) -> m (Tm, Val) + go : Nat -> Vect n (String, Val) -> m (Tm, Val) go i [] = throwError "\{show nm} not in scope \{show $ map fst ctx.types}" go i ((x, ty) :: xs) = if x == nm then pure $ (Bnd i, ty) else go (i + 1) xs diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index eba762d..d0fc676 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -26,6 +26,11 @@ import Data.List -- exercises. There is some fill in the parser stuff that may show -- the future. +-- kovacs desugars the (a b c : Foo) during parsing (foldr) + +-- We need to allow A -> B -> C in functions +-- We need to handle A -> (A -> B) -> C + ident = token Ident parens : Parser a -> Parser a @@ -51,7 +56,7 @@ lit = do t <- token Number pure $ RLit (LInt (cast t)) --- I can haz arrows +-- typeExpr is term with arrows. export typeExpr : Parser Raw export term : (Parser Raw) @@ -64,7 +69,7 @@ atom = withPos (RU <$ keyword "U" <|> RVar <$> ident <|> lit <|> RHole <$ keyword "_") - <|> parens term + <|> parens typeExpr -- Argument to a Spine pArg : Parser (Icit,Raw) @@ -112,7 +117,7 @@ letExpr = do commit alts <- startBlock $ someSame $ letAssign keyword' "in" - scope <- term + scope <- typeExpr pure $ foldl (\ acc, (n,v) => RLet n RHole v acc) scope alts where @@ -121,7 +126,7 @@ letExpr = do name <- ident -- TODO type assertion keyword "=" - t <- term + t <- typeExpr pure (name,t) pLetArg : Parser (Icit, String, Maybe Raw) @@ -138,7 +143,7 @@ lamExpr = do commit (icit, name, ty) <- pLetArg keyword "=>" - scope <- term + scope <- typeExpr -- TODO optional type pure $ RLam name icit scope diff --git a/src/Lib/Prettier.idr b/src/Lib/Prettier.idr index 8f8ca1e..42ac269 100644 --- a/src/Lib/Prettier.idr +++ b/src/Lib/Prettier.idr @@ -66,6 +66,7 @@ public export Semigroup Doc where x <+> y = Seq x (Seq (Text " ") y) -- Match System.File so we don't get warnings +public export infixl 5 export diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index f93f4a8..e1ffc95 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -1,4 +1,5 @@ -- I'm not sure this is related, or just a note to self (Presheaves on Porpoise) + -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q -- or drop the indices for now. @@ -7,9 +8,12 @@ module Lib.TT -- For SourcePos import Lib.Parser.Impl + import Control.Monad.Error.Interface import Data.Fin import Data.List +import Data.Vect +import Data.SortedMap public export Name : Type @@ -107,7 +111,8 @@ public export ($$) : Closure -> Val -> Val ($$) (MkClosure env tm) u = eval (u :: env) tm -infixl 8 $$ +public export +infixl 8 $$ export vapp : Val -> Val -> Val @@ -152,30 +157,69 @@ conv : (lvl : Nat) -> Val -> Val -> Bool -- Types = List (Name, Lazy Val) +{- +smalltt + +smalltt gets into weird haskell weeds in eval - shifting top level to the left +and tagging meta vs top with a bit. + +I think something subtle is going on with laziness on Elaboration.hs:300 +yeah, and define is even inlined. + +So it has a top context, and clears out almost everything for processing a def in +a different kind of context. + +we very much need an idea of local context for metas. I don't want to abstract over +the entire program. + +So I guess we have top and local then? + +With haskell syntax. I think we can have Axiom for claims and rewrite to def later. + +Hmm, so given ezoo, if I'm going simple, I could keep BDs short, and use the normal +context. (Zoo4.lean:222) I'd probably still need an undefined/axiom marker as a value? + +ok, so with just one context, Env is List Val and we're getting Tm back from type checking. + +Can I get val back? Do we need to quote? What happens if we don't? + +-} + +data BD = Bound | Defined + +-- we'll use this for typechecking, but need to keep a TopContext around too. public export record Context where constructor MkCtx + lvl : Nat + -- shall we use lvl as an index? env : Env -- Values in scope - types : List (String, Val) -- types and names in scope - -- bds : List BD -- bind or define - -- lvl = length types + types : Vect lvl (String, Val) -- types and names in scope + -- so we'll try "bds" determines length of local context + bds : List BD -- bound or defined + pos : SourcePos -- the last SourcePos that we saw export empty : Context -empty = MkCtx [] [] (0,0) +empty = MkCtx 0 [] [] [] (0,0) export partial Show Context where show ctx = "Context \{show $ map fst $ ctx.types}" --- Kovacs Small-TT has locals and globals, lets do that. - ||| add a binding to environment export extend : Context -> String -> Val -> Context -extend (MkCtx env types pos) name ty = - MkCtx (VVar (length env) :: env) ((name, ty) :: types) pos +extend (MkCtx lvl env types bds pos) name ty = + MkCtx (S lvl) (VVar lvl :: env) ((name, ty) :: types) (Bound :: bds) pos + +-- I guess we define things as values? +export +define : Context -> String -> Val -> Val -> Context +define (MkCtx lvl env types bds pos) name val ty = + MkCtx (S lvl) (val :: env) ((name, ty) :: types) (Defined :: bds) pos + update : Context -> String -> Tm -> Context -- oof @@ -184,7 +228,7 @@ lookup : {0 m : Type -> Type} -> {auto _ : MonadError String m} -> Context -> String -> m Val lookup ctx nm = go ctx.types where - go : List (String,Val) -> m Val + go : Vect n (String,Val) -> m Val go [] = throwError "Name \{nm} not in scope" go ((n, ty) :: xs) = if n == nm then pure ty else go xs diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr new file mode 100644 index 0000000..babbe37 --- /dev/null +++ b/src/Lib/TopContext.idr @@ -0,0 +1,69 @@ +module Lib.TopContext + +import Data.String +import Lib.TT + + +public export +data Def = Axiom | TCon (List String) | DCon Nat | Fn Tm + +Show Def where + show Axiom = "axiom" + show (TCon strs) = "TCon \{show strs}" + show (DCon k) = "DCon \{show k}" + show (Fn t) = "Fn \{show t}" + +||| entry in the top level context +public export +record TopEntry where + constructor MkEntry + name : String + type : Tm + def : Def + +-- FIXME snoc + +export +Show TopEntry where + show (MkEntry name type def) = "\{show name} : \{show type} := \{show def}" + +||| Top level context. +||| Most of the reason this is separate is to have a different type +||| `Def` for the entries. +||| +||| The price is that we have names in addition to levels. Do we want to +||| expand these during conversion? +public export +record TopContext where + constructor MkTop + -- We'll add a map later? + defs : List TopEntry + + +export +lookup : String -> TopContext -> Maybe TopEntry +lookup nm top = go top.defs + where + go : List TopEntry -> Maybe TopEntry + go [] = Nothing + go (entry :: xs) = if entry.name == nm then Just entry else go xs + +-- Maybe pretty print? +export +Show TopContext where + show (MkTop defs) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" + +public export +empty : TopContext +empty = MkTop [] + +public export +claim : TopContext -> String -> Tm -> TopContext +claim tc name ty = { defs $= (MkEntry name ty Axiom ::) } tc + +-- TODO update existing, throw, etc. + +public export +addDef : TopContext -> String -> Tm -> Tm -> TopContext +addDef tc name tm ty = { defs $= (MkEntry name ty (Fn tm) ::) } tc + diff --git a/src/Main.idr b/src/Main.idr index 8c0e5cc..7e2f2a4 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -2,6 +2,8 @@ module Main import Control.App import Data.String +import Data.Vect +import Data.List import Control.Monad.Error.Interface import Control.Monad.Error.Either import Control.Monad.State @@ -12,6 +14,7 @@ import Lib.Prettier import Lib.Token import Lib.Tokenizer import Lib.TT +import Lib.TopContext import Syntax import Syntax import System @@ -20,38 +23,46 @@ import System.File {- +- [ ] Replace on define +- [ ] more sugar on lambdas + + Currently working through checking of decl / def Running check is awkward. I need a monad stack. Main2.idr has an older App attempt without the code below. Retrofit. + +App isn't compatible with javascript (without a way to short circuit +the fork foreign function.) + -} M : Type -> Type -M = (StateT Context (EitherT String IO)) +M = (StateT TopContext (EitherT String IO)) processDecl : Decl -> M () processDecl (TypeSig nm tm) = do ctx <- get putStrLn "TypeSig \{nm} \{show tm}" - ty <- check ctx tm VU + ty <- check ctx empty tm VU putStrLn "got \{show ty}" - let vty = eval ctx.env ty - putStrLn "--- \{show $ quote 0 vty}" - put $ extend ctx nm vty + + put $ claim ctx nm ty processDecl (Def nm raw) = do putStrLn "def \{show nm}" ctx <- get - let Just ty = lookup nm ctx.types + let Just entry = lookup nm ctx | Nothing => printLn "skip def \{nm} without Decl" - putStrLn "check \{nm} = \{show raw} at \{show $ quote 0 ty}" - Right tm <- pure $ the (Either String Tm) (check ctx raw ty) + let (MkEntry name ty Axiom) := entry + -- FIXME error + | _ => printLn "\{nm} already defined" + putStrLn "check \{nm} = \{show raw} at \{show $ ty}" + let vty = eval empty ty + Right tm <- pure $ the (Either String Tm) (check ctx empty raw vty) | Left err => printLn err putStrLn "got \{show tm}" - -- XXXXX here I need to update the environment - -- I may want to rework things to have a top environment with names, - -- then levels / indices for local stuff. - + put (addDef ctx nm tm ty) processDecl decl = putStrLn "skip \{show decl}" @@ -81,6 +92,6 @@ main' = do main : IO () main = do - foo <- runEitherT $ runStateT TT.empty $ main' + foo <- runEitherT $ runStateT empty $ main' putStrLn "done"