From 0bb2d48d729d7d6a38222cd1e51c656d2efdd828 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sun, 21 Jul 2024 21:16:47 -0700 Subject: [PATCH] Additional work - Move processDecl to separate file - Add missing files - Move Syntax.idr to Lib --- newt/ptest1.newt | 12 ++++ newt/test1.newt | 8 +++ newt/zoo4.newt | 93 +++++++++++++++++++++++++ src/Lib/Check.idr | 147 +++++++++++++++++++++++++++------------ src/Lib/Parser.idr | 2 +- src/Lib/ProcessDecl.idr | 96 +++++++++++++++++++++++++ src/{ => Lib}/Syntax.idr | 2 +- src/Lib/TT.idr | 6 ++ src/Lib/TopContext.idr | 4 +- src/Lib/Types.idr | 39 ++++++++--- src/Main.idr | 94 ++----------------------- 11 files changed, 358 insertions(+), 145 deletions(-) create mode 100644 newt/ptest1.newt create mode 100644 newt/test1.newt create mode 100644 newt/zoo4.newt create mode 100644 src/Lib/ProcessDecl.idr rename src/{ => Lib}/Syntax.idr (99%) diff --git a/newt/ptest1.newt b/newt/ptest1.newt new file mode 100644 index 0000000..8d50d67 --- /dev/null +++ b/newt/ptest1.newt @@ -0,0 +1,12 @@ +module Bug + +Nat : U +Nat = (N : U) -> (N -> N) -> N -> N + +zero : Nat +zero = \ U s z => z + +-- This fails unification if we allow U on the LHS, because U is special on the RHS. +-- We need to not parse it on the LHS if we're not pattern matching. +succ : Nat -> Nat +succ = \ n U s z => s (n U s z) diff --git a/newt/test1.newt b/newt/test1.newt new file mode 100644 index 0000000..adbdba3 --- /dev/null +++ b/newt/test1.newt @@ -0,0 +1,8 @@ +module Scratch + +nat : U +nat = {C : U} -> C -> (nat -> C) -> C + +-- TESTCASE This was broken when I wasn't expanding Ref ty in check +succ : nat -> nat +succ = \n => \ z s => s n diff --git a/newt/zoo4.newt b/newt/zoo4.newt new file mode 100644 index 0000000..5da9952 --- /dev/null +++ b/newt/zoo4.newt @@ -0,0 +1,93 @@ +module Zoo4 + +id : {A : U} -> A -> A +id = \x => x -- elaborated to \{A} x. x + +-- implicit arg types can be omitted +const : {A B} -> A -> B -> A +const = \x y => x + +-- function arguments can be grouped: +group1 : {A B : U}(x y z : A) -> B -> B +group1 = \x y z b => b + +group2 : {A B}(x y z : A) -> B -> B +group2 = \x y z b=> b + +-- explicit id function used for annotation as in Idris +the : (A : _) -> A -> A +the = \_ x => x + +-- implicit args can be explicitly given +-- NB kovacs left off the type (different syntax), so I put a hole in there +argTest1 : _ +argTest1 = const {U} {U} U + +-- I've decided not to do = in the {} for now. +-- let argTest2 = const {B = U} U; -- only give B, the second implicit arg + +-- again no type, this hits a lambda in infer. +-- I think we need to create two metas and make a pi of them. +insert2 : _ +insert2 = (\{A} x => the A x) U -- (\{A} x => the A x) {U} U + +Bool : U +Bool = (B : _) -> B -> B -> B + +true : Bool +true = \B t f => t + +false : Bool +false = \B t f => f + +List : U -> U +List = \A => (L : _) -> (A -> L -> L) -> L -> L + +nil : {A} -> List A +nil = \L cons nil => nil + +cons : {A} -> A -> List A -> List A +cons = \ x xs L cons nil => cons x (xs L cons nil) + +map : {A B} -> (A -> B) -> List A -> List B +map = \{A} {B} f xs L c n => xs L (\a => c (f a)) n + +list1 : List Bool +list1 = cons true (cons false (cons true nil)) + +-- dependent function composition +comp : {A} {B : A -> U} {C : {a} -> B a -> U} + (f : {a} (b : B a) -> C b) + (g : (a : A) -> B a) + (a : A) + -> C (g a) +comp = \f g a => f (g a) + +compExample : _ +compExample = comp (cons true) (cons false) nil + +Nat : U +Nat = (N : U) -> (N -> N) -> N -> N + +-- TODO - first underscore there, why are there two metas? +mul : Nat -> Nat -> Nat +mul = \a b N s z => a _ (b _ s) z + +ten : Nat +ten = \N s z => (s (s (s (s (s (s (s (s (s (s z)))))))))) + +hundred : _ +hundred = mul ten ten + +-- Leibniz equality +Eq : {A} -> A -> A -> U +Eq = \{A} x y => (P : A -> U) -> P x -> P y + +refl : {A} {x : A} -> Eq x x +refl = \_ px => px + +sym : {A x y} -> Eq {A} x y -> Eq y x +sym = \p => p (\y => Eq y x) refl + +eqtest : Eq (mul ten ten) hundred +eqtest = refl diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 6bd3f50..56084b2 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -1,6 +1,8 @@ module Lib.Check +import Control.Monad.Error.Either import Control.Monad.Error.Interface +import Control.Monad.State import Control.Monad.Identity import Lib.Parser.Impl import Lib.Prettier @@ -10,11 +12,11 @@ import Data.String import Lib.Types import Lib.TT import Lib.TopContext -import Syntax +import Lib.Syntax -- renaming -- dom gamma ren -data PRen = PR Nat Nat (List Nat) +data Pden = PR Nat Nat (List Nat) -- IORef for metas needs IO @@ -24,6 +26,17 @@ forceMeta (VMeta ix sp) = case !(lookupMeta ix) of (Solved k t) => vappSpine t sp forceMeta x = pure x +-- Lennart needed more forcing +forceType : Val -> M Val +forceType (VRef nm sp) = + case lookup nm !(get) of + (Just (MkEntry name type (Fn t))) => eval [] CBN t + _ => pure (VRef nm sp) +forceType (VMeta ix sp) = case !(lookupMeta ix) of + (Unsolved x k xs) => pure (VMeta ix sp) + (Solved k t) => vappSpine t sp >>= forceType +forceType x = pure x + parameters (ctx: Context) -- return renaming, the position is the new VVar @@ -87,9 +100,9 @@ parameters (ctx: Context) unifySpine l True _ _ = error [DS "meta spine length mismatch"] unify l t u = do - putStrLn "Unify \{show ctx.lvl}" - putStrLn " \{show l} \{show t}" - putStrLn " =?= \{show u}" + debug "Unify \{show ctx.lvl}" + debug " \{show l} \{show t}" + debug " =?= \{show u}" t' <- forceMeta t u' <- forceMeta u case (t',u') of @@ -102,6 +115,7 @@ parameters (ctx: Context) else error [DS "vvar mismatch \{show k} \{show k'}"] (VRef k sp, VRef k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' + -- REVIEW - consider forcing? else error [DS "vref mismatch \{show k} \{show k'}"] (VMeta k sp, VMeta k' sp' ) => if k == k' then unifySpine l (k == k') sp sp' @@ -109,8 +123,23 @@ parameters (ctx: Context) (t, VMeta i' sp') => solve l i' sp' t (VMeta i sp, t' ) => solve l i sp t' (VU, VU) => pure () - -- REVIEW consider quoting back - _ => error [DS "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env}" ] + -- Lennart.newt cursed type references itself + -- We _could_ look up the ref, eval against [] and vappSpine... + (t, VRef k' sp') => do + debug "expand \{show t} =?= %ref \{k'}" + case lookup k' !(get) of + Just (MkEntry name ty (Fn tm)) => unify l t !(vappSpine !(eval [] CBN tm) sp') + _ => error [DS "unify failed \{show t'} =?= \{show u'} [no Fn]\n env is \{show ctx.env} \{show $ map fst ctx.types}" ] + -- REVIEW I'd like to quote this back, but we have l that aren't in the environment. + _ => error [DS "unify failed \{show t'} =?= \{show u'} \n env is \{show ctx.env} \{show $ map fst ctx.types}" ] + +unifyCatch : Context -> Val -> Val -> M () +unifyCatch ctx ty' ty = catchError (unify ctx ctx.lvl ty' ty) $ \(E x str) => do + let names = toList $ map fst ctx.types + a <- quote ctx.lvl ty' + b <- quote ctx.lvl ty + let msg = "\n failed to unify \{pprint names a}\n with \{pprint names b}\n " <+> str + throwError (E x msg) insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) insert ctx tm ty = do @@ -121,51 +150,81 @@ insert ctx tm ty = do insert ctx (App tm m) !(b $$ mv) va => pure (tm, va) +lookupName : Context -> Raw -> M (Maybe (Tm, Val)) +lookupName ctx (RVar nm) = go 0 ctx.types + where + go : Nat -> Vect n (String, Val) -> M (Maybe (Tm, Val)) + go i [] = case lookup nm !(get) of + Just (MkEntry name ty (Fn t)) => pure $ Just (Ref nm (Just t), !(eval [] CBN ty)) + Just (MkEntry name ty _) => pure $ Just (Ref nm Nothing, !(eval [] CBN ty)) + Nothing => pure Nothing + go i ((x, ty) :: xs) = if x == nm then pure $ Just (Bnd i, ty) + else go (i + 1) xs +lookupName ctx _ = pure Nothing + + export infer : Context -> Raw -> M (Tm, Val) export check : Context -> Raw -> Val -> M Tm -check ctx tm ty with (force ty) - check ctx (RSrcPos x tm) _ | ty = check ({pos := x} ctx) tm ty - check ctx t@(RLam nm icit tm) _ | ty = case ty of - (VPi nm' icit' a b) => do - putStrLn "icits \{nm} \{show icit} \{nm'} \{show icit'}" - if icit == icit' then do - let var = VVar (length ctx.env) [<] - let ctx' = extend ctx nm a - tm' <- check ctx' tm !(b $$ var) - pure $ Lam nm tm' - else if icit' == Implicit then do - let var = VVar (length ctx.env) [<] - ty' <- b $$ var - -- use nm' here if we want them automatically in scope - sc <- check (extend ctx nm' a) t ty' - pure $ Lam nm' sc - else - error [(DS "Icity issue checking \{show t} at \{show ty}")] - other => error [(DS "Expected pi type, got \{!(prval ty)}")] - check ctx tm _ | (VPi nm' Implicit a b) = do - putStrLn "XXX edge \{show tm} against VPi" +check ctx tm ty = case (tm, !(forceType ty)) of + (RSrcPos x tm, ty) => check ({pos := x} ctx) tm ty + -- Document a hole, pretend it's implemented + (RHole, ty) => do + ty' <- quote ctx.lvl ty + let names = (toList $ map fst ctx.types) + env <- for ctx.types $ \(n,ty) => pure " \{n} : \{pprint names !(quote ctx.lvl ty)}" + let msg = unlines (toList $ reverse env) ++ " -----------\n" ++ " goal \{pprint names ty'}" + debug "INFO at \{show ctx.pos}: " + debug msg + -- let context = unlines foo + -- need to print 'warning' with position + -- fixme - just put a name on it like idris and stuff it into top. + -- error [DS "hole:\n\{msg}"] + pure $ Ref "?" Nothing + (t@(RLam nm icit tm), ty@(VPi nm' icit' a b)) => do + debug "icits \{nm} \{show icit} \{nm'} \{show icit'}" + if icit == icit' then do + let var = VVar (length ctx.env) [<] + let ctx' = extend ctx nm a + tm' <- check ctx' tm !(b $$ var) + pure $ Lam nm tm' + else if icit' == Implicit then do + let var = VVar (length ctx.env) [<] + ty' <- b $$ var + -- use nm' here if we want them automatically in scope + sc <- check (extend ctx nm' a) t ty' + pure $ Lam nm' sc + else + error [(DS "Icity issue checking \{show t} at \{show ty}")] + (t@(RLam nm icit tm), ty) => + error [(DS "Expected pi type, got \{!(prvalCtx ty)}")] + + (tm, ty@(VPi nm' Implicit a b)) => do + let names = toList $ map fst ctx.types + debug "XXX edge add implicit lambda to \{show tm}" let var = VVar (length ctx.env) [<] ty' <- b $$ var + debug "XXX ty' is \{!(prvalCtx {ctx=(extend ctx nm' a)} ty')}" sc <- check (extend ctx nm' a) tm ty' pure $ Lam nm' sc - -- TODO Work in progress - -- I'd like to continue and also this is useless without some var names - check ctx RHole _ | ty = do - error [DS "hole has type \{show ty}"] - check ctx tm _ | ty = do - -- We need to insert if it's not a Lam - -- TODO figure out why the exception is here (cribbed from kovacs) - (tm', ty') <- case !(infer ctx tm) of - (tm'@(Lam{}),ty') => pure (tm', ty') - (tm', ty') => insert ctx tm' ty' - putStrLn "infer \{show tm} to \{pprint [] tm'} : \{show ty'} expect \{show ty}" - when( ctx.lvl /= length ctx.env) $ error [DS "level mismatch \{show ctx.lvl} \{show ctx.env}"] - unify ctx ctx.lvl ty' ty - pure tm' + (tm,ty) => do + -- We need to insert if tm is not an Implicit Lam + -- assuming all of the implicit ty have been handled above + let names = toList $ map fst ctx.types + (tm', ty') <- case !(infer ctx tm) of + -- Kovacs doesn't insert on tm = Implicit Lam, we don't have Plicity there + -- so I'll check the inferred type for an implicit pi + (tm'@(Lam{}), ty'@(VPi _ Implicit _ _)) => do debug "Lambda"; pure (tm', ty') + (tm', ty') => do + debug "RUN INSERT ON \{pprint names tm'} at \{show ty'}" + insert ctx tm' ty' + + debug "INFER \{show tm} to (\{pprint names tm'} : \{show ty'}) expect \{show ty}" + unifyCatch ctx ty' ty + pure tm' infer ctx (RVar nm) = go 0 ctx.types where @@ -194,7 +253,7 @@ infer ctx (RApp t u icit) = do -- If it's not a VPi, try to unify it with a VPi -- TODO test case to cover this. tty => do - putStrLn "unify PI for \{show tty}" + debug "unify PI for \{show tty}" a <- eval ctx.env CBN !(freshMeta ctx) b <- MkClosure ctx.env <$> freshMeta (extend ctx ":ins" a) unify ctx 0 tty (VPi ":ins" icit a b) @@ -222,7 +281,7 @@ infer ctx (RLam nm icit tm) = do a <- freshMeta ctx >>= eval ctx.env CBN let ctx' = extend ctx nm a (tm', b) <- infer ctx' tm - putStrLn "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}" + debug "make lam for \{show nm} scope \{pprint (names ctx) tm'} : \{show b}" pure $ (Lam nm tm', VPi nm icit a $ MkClosure ctx.env !(quote (S ctx.lvl) b)) -- error {ctx} [DS "can't infer lambda"] diff --git a/src/Lib/Parser.idr b/src/Lib/Parser.idr index 5496247..d931ba7 100644 --- a/src/Lib/Parser.idr +++ b/src/Lib/Parser.idr @@ -12,7 +12,7 @@ import Lib.Types import Lib.Token import Lib.Parser.Impl -import Syntax +import Lib.Syntax import Data.List import Data.Maybe diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr new file mode 100644 index 0000000..0eedf70 --- /dev/null +++ b/src/Lib/ProcessDecl.idr @@ -0,0 +1,96 @@ +module Lib.ProcessDecl + +import Data.IORef + +import Lib.Types +import Lib.Parser +import Lib.TT +import Lib.TopContext +import Lib.Check +import Lib.Syntax + +export +processDecl : Decl -> M () +processDecl (TypeSig nm tm) = do + top <- get + putStrLn "-----" + putStrLn "TypeSig \{nm} \{show tm}" + ty <- check (mkCtx top.metas) tm VU + ty' <- nf [] ty + putStrLn "got \{pprint [] ty'}" + modify $ claim nm ty' + +-- FIXME - this should be in another file +processDecl (Def nm raw) = do + putStrLn "-----" + putStrLn "def \{show nm}" + ctx <- get + let pos = case raw of + RSrcPos pos _ => pos + _ => (0,0) + + let Just entry = lookup nm ctx + | Nothing => throwError $ E pos "skip def \{nm} without Decl" + let (MkEntry name ty Axiom) := entry + | _ => throwError $ E pos "\{nm} already defined" + putStrLn "check \{nm} = \{show raw} at \{pprint [] ty}" + vty <- eval empty CBN ty + putStrLn "vty is \{show vty}" + tm <- check (mkCtx ctx.metas) raw vty + putStrLn "Ok \{pprint [] tm}" + + mc <- readIORef ctx.metas + for_ mc.metas $ \case + (Solved k x) => pure () + (Unsolved (l,c) k xs) => do + -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}" + throwError $ E (l,c) "Unsolved meta \{show k}" + + put (addDef ctx nm tm ty) + +processDecl (DCheck tm ty) = do + + top <- get + putStrLn "check \{show tm} at \{show ty}" + ty' <- check (mkCtx top.metas) tm VU + putStrLn "got type \{pprint [] ty'}" + vty <- eval [] CBN ty' + res <- check (mkCtx top.metas) ty vty + putStrLn "got \{pprint [] res}" + norm <- nf [] res + putStrLn "norm \{pprint [] norm}" + -- top <- get + -- ctx <- mkCtx top.metas + -- I need a type to check against + -- norm <- nf [] x + putStrLn "NF " + +processDecl (DImport str) = throwError $ E (0,0) "import not implemented" + +processDecl (Data nm ty cons) = do + -- It seems like the FC for the errors are not here? + ctx <- get + tyty <- check (mkCtx ctx.metas) ty VU + -- TODO check tm is VU or Pi ending in VU + -- Maybe a pi -> binders function + -- TODO we're putting in axioms, we need constructors + -- for each constructor, check and add + modify $ claim nm tyty + ctx <- get + for_ cons $ \x => case x of + -- expecting tm to be a Pi type + (TypeSig nm' tm) => do + ctx <- get + -- TODO check pi type ending in full tyty application + dty <- check (mkCtx ctx.metas) tm VU + modify $ claim nm' dty + _ => throwError $ E (0,0) "expected TypeSig" + + pure () + where + checkDeclType : Tm -> M () + checkDeclType U = pure () + checkDeclType (Pi str icit t u) = checkDeclType u + checkDeclType _ = throwError $ E (0,0) "data type doesn't return U" + + diff --git a/src/Syntax.idr b/src/Lib/Syntax.idr similarity index 99% rename from src/Syntax.idr rename to src/Lib/Syntax.idr index 817da4e..59fb0dd 100644 --- a/src/Syntax.idr +++ b/src/Lib/Syntax.idr @@ -1,4 +1,4 @@ -module Syntax +module Lib.Syntax import Data.String import Data.Maybe diff --git a/src/Lib/TT.idr b/src/Lib/TT.idr index 10eacdc..4a7f82a 100644 --- a/src/Lib/TT.idr +++ b/src/Lib/TT.idr @@ -174,6 +174,11 @@ export prval : Val -> M String prval v = pure $ pprint [] !(quote 0 v) +export +prvalCtx : {auto ctx : Context} -> Val -> M String +prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v) + + export solveMeta : TopContext -> Nat -> Val -> M () solveMeta ctx ix tm = do @@ -185,6 +190,7 @@ solveMeta ctx ix tm = do go [] _ = error' "Meta \{show ix} not found" go (meta@(Unsolved pos k _) :: xs) lhs = if k == ix then do + -- empty context should be ok, because this needs to be closed putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}" pure $ lhs <>> (Solved k tm :: xs) else go xs (lhs :< meta) diff --git a/src/Lib/TopContext.idr b/src/Lib/TopContext.idr index 108fdd2..55363b4 100644 --- a/src/Lib/TopContext.idr +++ b/src/Lib/TopContext.idr @@ -18,11 +18,11 @@ lookup nm top = go top.defs -- Maybe pretty print? export Show TopContext where - show (MkTop defs metas) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" + show (MkTop defs metas _) = "\nContext:\n [\{ joinBy "\n" $ map show defs}]" public export empty : HasIO m => m TopContext -empty = pure $ MkTop [] !(newIORef (MC [] 0)) +empty = pure $ MkTop [] !(newIORef (MC [] 0)) True public export claim : String -> Tm -> TopContext -> TopContext diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 7c84543..75a167b 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -4,20 +4,21 @@ module Lib.Types -- maybe watch https://www.youtube.com/watch?v=3gef0_NFz8Q -- or drop the indices for now. --- For SourcePos -import Lib.Parser.Impl +-- For SourcePos, Error +import public Lib.Parser.Impl import Lib.Prettier import public Control.Monad.Error.Either import public Control.Monad.Error.Interface import public Control.Monad.State -import Data.IORef import Data.Fin +import Data.IORef import Data.List import Data.SnocList -import Data.Vect import Data.SortedMap +import Data.String +import Data.Vect public export Name : Type @@ -87,6 +88,7 @@ Eq (Tm) where (Pi n icit t u) == (Pi n' icit' t' u') = icit == icit' && t == t' && u == u' _ == _ = False +-- FIXME prec export pprint : List String -> Tm -> String @@ -101,8 +103,10 @@ pprint names tm = render 80 $ go names tm go names (Lam nm t) = text "(\\ \{nm} =>" <+> go (nm :: names) t <+> ")" go names (App t u) = text "(" <+> go names t <+> go names u <+> ")" go names U = "U" - go names (Pi nm icit t u) = - text "(" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")" + go names (Pi nm Implicit t u) = + text "({" <+> text nm <+> ":" <+> go names t <+> "}" <+> "=>" <+> go (nm :: names) u <+> ")" + go names (Pi nm Explicit t u) = + text "((" <+> text nm <+> ":" <+> go names t <+> ")" <+> "=>" <+> go (nm :: names) u <+> ")" public export Pretty Tm where @@ -159,12 +163,13 @@ Show Val where show (VPi str Explicit x y) = "(%pi (\{str} : \{show x}). \{show y})" show VU = "U" - --- Not used yet +-- Not used - I was going to change context to have a List Binder +-- instead of env, types, bds +-- But when we get down into eval, we don't have types to put into the env data Binder : Type where Bind : (nm : String) -> (bd : BD) -> (val : Val) -> (ty : Val) -> Binder -export covering +covering Show Binder where show (Bind nm bd val ty) = "(\{show bd} \{show nm} \{show val} : \{show ty})" @@ -260,6 +265,7 @@ record TopContext where -- We'll add a map later? defs : List TopEntry metas : IORef MetaContext + verbose : Bool -- metas : TODO @@ -267,6 +273,7 @@ record TopContext where -- we'll use this for typechecking, but need to keep a TopContext around too. public export record Context where + [noHints] constructor MkCtx lvl : Nat -- shall we use lvl as an index? @@ -294,3 +301,17 @@ M = (StateT TopContext (EitherT Impl.Error IO)) export mkCtx : IORef MetaContext -> Context mkCtx metas = MkCtx 0 [] [] [] (0,0) metas + +||| Force argument and print if verbose is true +export +debug : Lazy String -> M () +debug x = do + top <- get + when top.verbose $ putStrLn x + +||| Version of debug that makes monadic computation lazy +export +debugM : M String -> M () +debugM x = do + top <- get + when top.verbose $ do putStrLn !(x) diff --git a/src/Main.idr b/src/Main.idr index f6718c2..09f811f 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -8,17 +8,18 @@ import Data.List import Data.String import Data.Vect import Data.IORef -import Lib.Check +-- import Lib.Check import Lib.Parser -import Lib.Parser.Impl +-- import Lib.Parser.Impl import Lib.Prettier +import Lib.ProcessDecl import Lib.Token import Lib.Tokenizer import Lib.TopContext import Lib.Types -import Lib.TT -import Syntax -import Syntax +-- import Lib.TT +import Lib.Syntax +import Lib.Syntax import System import System.Directory import System.File @@ -45,89 +46,6 @@ dumpContext top = do go [] = pure () go (x :: xs) = go xs >> putStrLn " \{show x}" -processDecl : Decl -> M () -processDecl (TypeSig nm tm) = do - top <- get - putStrLn "-----" - putStrLn "TypeSig \{nm} \{show tm}" - ty <- check (mkCtx top.metas) tm VU - ty' <- nf [] ty - putStrLn "got \{pprint [] ty'}" - modify $ claim nm ty' - --- FIXME - this should be in another file -processDecl (Def nm raw) = do - putStrLn "-----" - putStrLn "def \{show nm}" - ctx <- get - let pos = case raw of - RSrcPos pos _ => pos - _ => (0,0) - - let Just entry = lookup nm ctx - | Nothing => throwError $ E pos "skip def \{nm} without Decl" - let (MkEntry name ty Axiom) := entry - | _ => throwError $ E pos "\{nm} already defined" - putStrLn "check \{nm} = \{show raw} at \{pprint [] ty}" - vty <- eval empty CBN ty - putStrLn "vty is \{show vty}" - tm <- check (mkCtx ctx.metas) raw vty - putStrLn "Ok \{pprint [] tm}" - - mc <- readIORef ctx.metas - for_ mc.metas $ \case - (Solved k x) => pure () - (Unsolved (l,c) k xs) => do - -- putStrLn "ERROR at (\{show l}, \{show c}): Unsolved meta \{show k}" - throwError $ E (l,c) "Unsolved meta \{show k}" - - put (addDef ctx nm tm ty) - -processDecl (DCheck tm ty) = do - - top <- get - putStrLn "check \{show tm} at \{show ty}" - ty' <- check (mkCtx top.metas) tm VU - putStrLn "got type \{pprint [] ty'}" - vty <- eval [] CBN ty' - res <- check (mkCtx top.metas) ty vty - putStrLn "got \{pprint [] res}" - norm <- nf [] res - putStrLn "norm \{pprint [] norm}" - -- top <- get - -- ctx <- mkCtx top.metas - -- I need a type to check against - -- norm <- nf [] x - putStrLn "NF " - -processDecl (DImport str) = throwError $ E (0,0) "import not implemented" - -processDecl (Data nm ty cons) = do - -- It seems like the FC for the errors are not here? - ctx <- get - tyty <- check (mkCtx ctx.metas) ty VU - -- TODO check tm is VU or Pi ending in VU - -- Maybe a pi -> binders function - -- TODO we're putting in axioms, we need constructors - -- for each constructor, check and add - modify $ claim nm tyty - ctx <- get - for_ cons $ \x => case x of - -- expecting tm to be a Pi type - (TypeSig nm' tm) => do - ctx <- get - -- TODO check pi type ending in full tyty application - dty <- check (mkCtx ctx.metas) tm VU - modify $ claim nm' dty - _ => throwError $ E (0,0) "expected TypeSig" - - pure () - where - checkDeclType : Tm -> M () - checkDeclType U = pure () - checkDeclType (Pi str icit t u) = checkDeclType u - checkDeclType _ = throwError $ E (0,0) "data type doesn't return U" - processFile : String -> M () processFile fn = do putStrLn "*** Process \{fn}"