From acb37a2882a4a8c72fadb2380d0bef06ca6c1f8d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 23 Nov 2024 17:48:03 -0800 Subject: [PATCH] Only log metas for top file, remove metas from Context --- src/Lib/ProcessDecl.idr | 29 +++++++++++++++-------------- src/Lib/Types.idr | 18 ++++++------------ src/Main.idr | 6 ++++-- 3 files changed, 25 insertions(+), 28 deletions(-) diff --git a/src/Lib/ProcessDecl.idr b/src/Lib/ProcessDecl.idr index b8892fd..8617d70 100644 --- a/src/Lib/ProcessDecl.idr +++ b/src/Lib/ProcessDecl.idr @@ -31,7 +31,7 @@ findMatches ctx ty [] = pure [] findMatches ctx ty ((MkEntry name type def) :: xs) = do let True = isCandidate ty type | False => findMatches ctx ty xs top <- get - -- let ctx = mkCtx top.metas (getFC ty) + -- let ctx = mkCtx (getFC ty) -- FIXME we're restoring state, but the INFO logs have already been emitted -- Also redo this whole thing to run during elab, recheck constraints, etc. mc <- readIORef top.metas @@ -40,7 +40,7 @@ findMatches ctx ty ((MkEntry name type def) :: xs) = do let fc = getFC ty debug "TRY \{name} : \{pprint [] type} for \{show ty}" -- This check is solving metas, so we save mc below in case we want this solution - -- tm <- check (mkCtx top.metas fc) (RVar fc name) ty + -- tm <- check (mkCtx fc) (RVar fc name) ty tm <- check ctx (RVar fc name) ty debug "Found \{pprint [] tm} for \{show ty}" mc' <- readIORef top.metas @@ -127,6 +127,7 @@ dumpEnv ctx = then go names (S k) xs (" \{n} : \{pprint names !(quote ctx.lvl ty)}":: acc) else go names (S k) xs (" \{n} = \{pprint names !(quote ctx.lvl v)} : \{pprint names !(quote ctx.lvl ty)}":: acc) +export logMetas : Nat -> M () logMetas mstart = do -- FIXME, now this isn't logged for Sig / Data. @@ -168,7 +169,7 @@ processDecl (TypeSig fc names tm) = do let Nothing := lookup nm top | _ => error fc "\{show nm} is already defined" pure () - ty <- check (mkCtx top.metas fc) tm (VU fc) + ty <- check (mkCtx fc) tm (VU fc) putStrLn "TypeSig \{unwords names} : \{pprint [] ty}" debug "got \{pprint [] ty}" for_ names $ \nm => setDef nm fc ty Axiom @@ -177,12 +178,12 @@ processDecl (TypeSig fc names tm) = do processDecl (PType fc nm ty) = do top <- get - ty' <- check (mkCtx top.metas fc) (maybe (RU fc) id ty) (VU fc) + ty' <- check (mkCtx fc) (maybe (RU fc) id ty) (VU fc) setDef nm fc ty' PrimTCon processDecl (PFunc fc nm ty src) = do top <- get - ty <- check (mkCtx top.metas fc) ty (VU fc) + ty <- check (mkCtx fc) ty (VU fc) ty' <- nf [] ty putStrLn "pfunc \{nm} : \{pprint [] ty'} := \{show src}" setDef nm fc ty' (PrimFn src) @@ -206,7 +207,7 @@ processDecl (Def fc nm clauses) = do -- I can take LHS apart syntactically or elaborate it with an infer clauses' <- traverse (makeClause top) clauses - tm <- buildTree (mkCtx top.metas fc) (MkProb clauses' vty) + tm <- buildTree (mkCtx fc) (MkProb clauses' vty) -- putStrLn "Ok \{pprint [] tm}" mc <- readIORef top.metas @@ -219,17 +220,17 @@ processDecl (Def fc nm clauses) = do putStrLn "NF\n\{render 80 $ pprint[] tm'}" debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}" updateDef nm fc ty (Fn tm') - logMetas mstart + -- logMetas mstart processDecl (DCheck fc tm ty) = do putStrLn "----- DCheck" top <- get putStrLn "INFO at \{show fc}: check \{show tm} at \{show ty}" - ty' <- check (mkCtx top.metas fc) ty (VU fc) + ty' <- check (mkCtx fc) ty (VU fc) putStrLn " got type \{pprint [] ty'}" vty <- eval [] CBN ty' - res <- check (mkCtx top.metas fc) tm vty + res <- check (mkCtx fc) tm vty putStrLn " got \{pprint [] res}" norm <- nf [] res putStrLn " NF \{pprint [] norm}" @@ -286,7 +287,7 @@ processDecl (Instance instfc ty decls) = do top <- get let tyFC = getFC ty - vty <- check (mkCtx top.metas instfc) ty (VU instfc) + vty <- check (mkCtx instfc) ty (VU instfc) -- Here `tele` holds arguments to the instance let (codomain, tele) = splitTele vty -- env represents the environment of those arguments @@ -378,16 +379,16 @@ processDecl (Data fc nm ty cons) = do top <- get mc <- readIORef top.metas let mstart = length mc.metas - tyty <- check (mkCtx top.metas fc) ty (VU fc) + tyty <- check (mkCtx fc) ty (VU fc) case lookup nm top of Just (MkEntry name type Axiom) => do - unifyCatch fc (mkCtx top.metas fc) !(eval [] CBN tyty) !(eval [] CBN type) + unifyCatch fc (mkCtx fc) !(eval [] CBN tyty) !(eval [] CBN type) Just (MkEntry name type _) => error fc "\{show nm} already declared" Nothing => setDef nm fc tyty Axiom cnames <- for cons $ \x => case x of (TypeSig fc names tm) => do debug "check dcon \{show names} \{show tm}" - dty <- check (mkCtx top.metas fc) tm (VU fc) + dty <- check (mkCtx fc) tm (VU fc) debug "dty \{show names} is \{pprint [] dty}" -- We only check that codomain uses the right type constructor @@ -406,7 +407,7 @@ processDecl (Data fc nm ty cons) = do _ => throwError $ E (0,0) "expected constructor declaration" putStrLn "setDef \{nm} TCon \{show $ join cnames}" updateDef nm fc tyty (TCon (join cnames)) - logMetas mstart + -- logMetas mstart where checkDeclType : Tm -> M () checkDeclType (U _) = pure () diff --git a/src/Lib/Types.idr b/src/Lib/Types.idr index 4cbeed7..e70e893 100644 --- a/src/Lib/Types.idr +++ b/src/Lib/Types.idr @@ -415,9 +415,7 @@ record Context where -- so we'll try "bds" determines length of local context bds : Vect lvl BD -- bound or defined - -- We only need this here if we don't pass TopContext - -- top : TopContext - metas : IORef MetaContext + -- FC to use if we don't have a better option fc : FC %name Context ctx @@ -495,9 +493,10 @@ error' msg = throwError $ E (0,0) msg export freshMeta : Context -> FC -> Val -> MetaKind -> M Tm freshMeta ctx fc ty kind = do - mc <- readIORef ctx.metas + top <- get + mc <- readIORef top.metas debug "fresh meta \{show mc.next} : \{show ty}" - writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc + writeIORef top.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds where -- hope I got the right order here :) @@ -507,11 +506,6 @@ freshMeta ctx fc ty kind = do applyBDs k t (Bound :: xs) = App emptyFC (applyBDs (S k) t xs) (Bnd emptyFC k) applyBDs k t (Defined :: xs) = applyBDs (S k) t xs - -- makeType : Vect k (String, Val) -> Vect k BD -> Val - -- makeType [] [] = ?makeType_rhs_2 - -- makeType ((nm, ty) :: types) (Defined :: bds) = makeType types bds - -- makeType ((nm, ty) :: types) (Bound :: bds) = VPi emptyFC nm Explicit ty - export lookupMeta : Nat -> M MetaEntry lookupMeta ix = do @@ -527,5 +521,5 @@ lookupMeta ix = do -- we need more of topcontext later - Maybe switch it up so we're not passing -- around top export -mkCtx : IORef MetaContext -> FC -> Context -mkCtx metas fc = MkCtx 0 [] [] [] metas fc +mkCtx : FC -> Context +mkCtx fc = MkCtx 0 [] [] [] fc diff --git a/src/Main.idr b/src/Main.idr index eda85ce..28ff79e 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -82,6 +82,8 @@ processModule base stk name = do processModule base (name :: stk) name' top <- get + mc <- readIORef top.metas + let mstart = length mc.metas let Right (decls, ops, toks) := partialParse (manySame parseDecl) top.ops toks | Left err => fail (showError src err) let [] := toks @@ -92,7 +94,7 @@ processModule base stk name = do putStrLn "process Decls" Right _ <- tryError $ traverse_ processDecl (collectDecl decls) | Left y => fail (showError src y) - + if (stk == []) then logMetas mstart else pure () pure src processFile : String -> M () @@ -136,10 +138,10 @@ main' = do | _ => error emptyFC "error reading args" (out, files) <- cmdLine args traverse_ processFile files + case out of Nothing => pure () Just name => writeSource name - -- traverse_ processFile (filter (".newt" `isSuffixOf`) files) out %export "javascript:newtMain" main : IO ()