From 793c3a99991cff38b9d5cc63fd38384743b53f6b Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 11 Jan 2025 20:07:50 -0800 Subject: [PATCH] qn for metas --- port/Lib/Common.newt | 17 ++++++++++++--- port/Lib/Elab.newt | 45 ++++++++++++++++++++------------------- port/Lib/Eval.newt | 9 ++++---- port/Lib/ProcessDecl.newt | 32 ++++++++-------------------- port/Lib/TopContext.newt | 2 +- port/Lib/Types.newt | 40 +++++++++++----------------------- port/Main.newt | 19 ++++++----------- src/Lib/Elab.idr | 2 +- src/Main.idr | 7 +++++- 9 files changed, 79 insertions(+), 94 deletions(-) diff --git a/port/Lib/Common.newt b/port/Lib/Common.newt index 9a5cfa7..a0ffc5b 100644 --- a/port/Lib/Common.newt +++ b/port/Lib/Common.newt @@ -96,11 +96,22 @@ emptyFC = MkFC "" (0,0) -- Error of a parse +data QName : U where + QN : List String -> String -> QName + +instance Eq QName where + QN ns n == QN ns' n' = n == n' && ns == ns' + +instance Show QName where + show (QN Nil n) = n + show (QN ns n) = joinBy "." ns ++ "." ++ n + +instance Ord QName where + compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' + data Error = E FC String - | Postpone FC Int String - - + | Postpone FC QName String instance Show FC where show fc = "\{fc.file}:\{show fc.start}" diff --git a/port/Lib/Elab.newt b/port/Lib/Elab.newt index f8f3d5d..360477a 100644 --- a/port/Lib/Elab.newt +++ b/port/Lib/Elab.newt @@ -92,8 +92,8 @@ forceMeta : Val -> M Val forceMeta (VMeta fc ix sp) = do meta <- lookupMeta ix case meta of - (Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp) (Solved _ k t) => vappSpine t sp >>= forceMeta + _ => pure (VMeta fc ix sp) forceMeta x = pure x @@ -199,7 +199,7 @@ makeSpine k (Defined :: xs) = makeSpine (k - 1) xs makeSpine k (Bound :: xs) = makeSpine (k - 1) xs :< VVar emptyFC (k - 1) Lin -solve : Env -> (k : Int) -> SnocList Val -> Val -> M Unit +solve : Env -> QName -> SnocList Val -> Val -> M Unit @@ -259,8 +259,8 @@ solveAutos : Int -> M Unit solveAutos mstart = do top <- get mc <- readIORef top.metaCtx - let mlen = length' mc.metas - mstart - res <- run $ filter isAuto (ite (mstart == 0) mc.metas $ take (cast mlen) mc.metas) + + res <- run $ filter isAuto (listValues mc.metas) if res then solveAutos mstart else pure MkUnit where isAuto : MetaEntry -> Bool @@ -275,20 +275,16 @@ solveAutos mstart = do -- We need to switch to SortedMap here -updateMeta : Int -> (MetaEntry -> M MetaEntry) -> M Unit +updateMeta : QName -> (MetaEntry -> M MetaEntry) -> M Unit updateMeta ix f = do top <- get - mc <- readIORef top.metaCtx - metas <- go mc.metas - writeIORef top.metaCtx $ MC metas mc.next mc.mcmode - where - go : List MetaEntry -> M (List MetaEntry) - go Nil = error' "Meta \{show ix} not found" - go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs - go (x@((Solved _ k y)) :: xs) = if k == ix then (flip _::_ xs) <$> f x else (_::_ x) <$> go xs + mc <- readIORef {M} top.metaCtx + let (Just me) = lookupMap' ix mc.metas | Nothing => pure MkUnit + me <- f me + writeIORef top.metaCtx $ MC (updateMap ix me mc.metas) mc.next mc.mcmode -checkAutos : Int -> List MetaEntry -> M Unit +checkAutos : QName -> List MetaEntry -> M Unit checkAutos ix Nil = pure MkUnit checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do ty' <- quote ctx.lvl ty @@ -302,8 +298,7 @@ checkAutos ix (entry@(Unsolved fc k ctx ty AutoSolve _) :: rest) = do checkAutos ix (_ :: rest) = checkAutos ix rest - -addConstraint : Env -> Int -> SnocList Val -> Val -> M Unit +addConstraint : Env -> QName -> SnocList Val -> Val -> M Unit addConstraint env ix sp tm = do top <- get mc <- readIORef top.metaCtx @@ -313,8 +308,9 @@ addConstraint env ix sp tm = do debug $ \ _ => "Add constraint m\{show ix} \{show sp} =?= \{show tm}" pure (Unsolved pos k a b c (MkMc (getFC tm) env sp tm :: cons)) (Solved _ k tm) => error' "Meta \{show k} already solved (addConstraint :: Nil)" + (OutOfScope) => error' "Meta \{show ix} out of scope" mc <- readIORef top.metaCtx - checkAutos ix mc.metas + checkAutos ix (listValues mc.metas) -- this loops too -- solveAutos 0 mc.metas pure MkUnit @@ -341,9 +337,9 @@ invert lvl sp = go sp Nil -- I think that essentially means our domain ix are one bigger, since we're looking at lvl -- in the codomain, so maybe we can just keep that value -rename : Int -> List Int -> Int -> Val -> M Tm +rename : QName -> List Int -> Int -> Val -> M Tm -renameSpine : Int -> List Int -> Int -> Tm -> SnocList Val -> M Tm +renameSpine : QName -> List Int -> Int -> Tm -> SnocList Val -> M Tm renameSpine meta ren lvl tm Lin = pure tm renameSpine meta ren lvl tm (xs :< x) = do xtm <- rename meta ren lvl x @@ -447,6 +443,7 @@ solve env m sp t = do updateMeta m $ \case (Unsolved pos k _ _ _ cons) => pure $ Solved pos k soln (Solved _ k x) => error' "Meta \{show ix} already solved! (solve2 :: Nil)" + OutOfScope => error' "Meta \{show ix} out of scope" maybeCheck $ for_ cons $ \case MkMc fc env sp rhs => do val <- vappSpine soln sp @@ -646,11 +643,14 @@ freshMeta ctx fc ty kind = do top <- get mc <- readIORef top.metaCtx debug $ \ _ => "fresh meta \{show mc.next} : \{show ty} (\{show kind})" - let newmeta = Unsolved fc mc.next ctx ty kind Nil - writeIORef top.metaCtx $ MC (newmeta :: mc.metas) (1 + mc.next) mc.mcmode + -- need the ns here + -- we were fudging this for v1 + let qn = QN ("$meta" :: Nil) (show mc.next) + let newmeta = Unsolved fc qn ctx ty kind Nil + writeIORef top.metaCtx $ MC (updateMap qn newmeta mc.metas) (1 + mc.next) mc.mcmode -- infinite loop - keeps trying Ord a => Ord (a \x a) -- when (kind == AutoSolve) $ \ _ => ignore $ trySolveAuto newmeta - pure $ applyBDs 0 (Meta fc mc.next) ctx.bds + pure $ applyBDs 0 (Meta fc qn) ctx.bds where -- hope I got the right order here :) applyBDs : Int -> Tm -> List BD -> Tm @@ -1269,6 +1269,7 @@ buildTree ctx prob@(MkProb ((MkClause fc constraints Nil expr) :: cs) ty) = do -- TODO - only hit the relevant ones ignore $ solveAutos 0 forceType ctx.env scty' + OutOfScope => pure scty' _ => pure scty' diff --git a/port/Lib/Eval.newt b/port/Lib/Eval.newt index 624f198..e4ccdf3 100644 --- a/port/Lib/Eval.newt +++ b/port/Lib/Eval.newt @@ -93,8 +93,9 @@ forceType : Env -> Val -> M Val forceType env (VMeta fc ix sp) = do meta <- lookupMeta ix case meta of - (Unsolved x k xs _ _ _) => pure (VMeta fc ix sp) (Solved _ k t) => vappSpine t sp >>= forceType env + _ => pure (VMeta fc ix sp) + forceType env x = do Just x' <- tryEval env x | _ => pure x @@ -158,8 +159,8 @@ eval env mode (Erased fc) = pure (VErased fc) eval env mode (Meta fc i) = do meta <- lookupMeta i case meta of - (Unsolved _ k xs _ _ _) => pure $ VMeta fc i Lin (Solved _ k t) => pure $ t + _ => pure $ VMeta fc i Lin eval env mode (Lam fc x icit rig t) = pure $ VLam fc x icit rig (MkClosure env t) eval env mode (Pi fc x icit rig a b) = do a' <- eval env mode a @@ -207,8 +208,8 @@ quote l (VVar fc k sp) = if k < l quote l (VMeta fc i sp) = do meta <- lookupMeta i case meta of - (Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp (Solved _ k t) => vappSpine t sp >>= quote l + _ => quoteSp l (Meta fc i) sp quote l (VLam fc x icit rig t) = do val <- t $$ VVar emptyFC l Lin tm <- quote (1 + l) val @@ -308,7 +309,7 @@ zonkApp top l env t@(Meta fc k) sp = do foo <- vappSpine v (Lin <>< sp') debug $ \ _ => "-> result is \{show foo}" tweakFC fc <$> quote l foo - (Unsolved x j xs _ _ _) => pure $ appSpine t sp + _ => pure $ appSpine t sp zonkApp top l env t sp = do t' <- zonk top l env t pure $ appSpine t' sp diff --git a/port/Lib/ProcessDecl.newt b/port/Lib/ProcessDecl.newt index e6515c6..e0a3b17 100644 --- a/port/Lib/ProcessDecl.newt +++ b/port/Lib/ProcessDecl.newt @@ -33,26 +33,18 @@ dumpEnv ctx = go names (1 + k) xs (" \{n} = \{render 90 $ pprint names v'} : \{render 90 $ pprint names ty'}":: acc) -logMetas : Int -> M Unit -logMetas mstart = do - -- FIXME, now this isn't logged for Sig / Data. - top <- get - mc <- readIORef {M} top.metaCtx - let mlen = cast {Int} {Nat} $ length' mc.metas - mstart - ignore $ for (reverse $ take mlen mc.metas) $ \case - (Solved fc k soln) => do - -- TODO put a flag on this, vscode is getting overwhelmed and - -- dropping errors - --info fc "solve \{show k} as \{render 90 $ pprint Nil !(quote 0 soln)}" - pure MkUnit - (Unsolved fc k ctx ty User cons) => do +logMetas : List MetaEntry -> M Unit +logMetas Nil = pure MkUnit +logMetas (OutOfScope :: rest) = logMetas rest +logMetas (Solved fc k soln :: rest) = logMetas rest +logMetas (Unsolved fc k ctx ty User cons :: rest) = do ty' <- quote ctx.lvl ty let names = map fst ctx.types env <- dumpEnv ctx let msg = "\{env} -----------\n \{render 90 $ pprint names ty'}" info fc "User Hole\n\{msg}" - - (Unsolved fc k ctx ty kind cons) => do + logMetas rest +logMetas (Unsolved fc k ctx ty kind cons :: rest) = do ty' <- forceMeta ty tm <- quote ctx.lvl ty' -- Now that we're collecting errors, maybe we simply check at the end @@ -79,7 +71,7 @@ logMetas mstart = do _ => pure Nil info fc $ unlines ((msg :: Nil) ++ msgs ++ sols) - -- addError $ E fc $ unlines ((msg :: Nil) ++ msgs ++ sols) + logMetas rest -- Used for Class and Record @@ -120,8 +112,6 @@ processDecl ns (TypeSig fc names tm) = do ty <- zonk top 0 Nil ty putStrLn "TypeSig \{unwords names} : \{render 90 $ pprint Nil ty}" 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 processDecl ns (PType fc nm ty) = do top <- get @@ -144,7 +134,6 @@ processDecl ns (Def fc nm clauses) = do putStrLn "Def \{show nm}" top <- get mc <- readIORef top.metaCtx - let mstart = length' mc.metas let (Just entry) = lookupRaw nm top | Nothing => throwError $ E fc "No declaration for \{nm}" let (MkEntry fc name ty Axiom) = entry @@ -161,8 +150,7 @@ processDecl ns (Def fc nm clauses) = do -- putStrLn "Ok \{render 90 $ pprint Nil tm}" mc <- readIORef top.metaCtx - let mlen = length' mc.metas - mstart - solveAutos mstart + solveAutos 0 -- TODO - make nf that expands all metas and drop zonk -- Idris2 doesn't expand metas for performance - a lot of these are dropped during erasure. -- Day1.newt is a test case @@ -177,7 +165,6 @@ processDecl ns (Def fc nm clauses) = do when top.verbose $ \ _ => putStrLn "ERASED\n\{render 80 $ pprint Nil tm'}" debug $ \ _ => "Add def \{nm} \{render 90 $ pprint Nil tm'} : \{render 90 $ pprint Nil ty}" updateDef (QN ns nm) fc ty (Fn tm') - -- logMetas mstart processDecl ns (DCheck fc tm ty) = do putStrLn "----- DCheck" @@ -414,7 +401,6 @@ processDecl ns (Data fc nm ty cons) = do decl => throwError $ E (getFC decl) "expected constructor declaration" putStrLn "setDef \{nm} TCon \{show $ join cnames}" updateDef (QN ns nm) fc tyty (TCon (join cnames)) - -- logMetas mstart where binderName : Binder → Name binderName (MkBinder _ nm _ _ _) = nm diff --git a/port/Lib/TopContext.newt b/port/Lib/TopContext.newt index 8834135..e738438 100644 --- a/port/Lib/TopContext.newt +++ b/port/Lib/TopContext.newt @@ -30,7 +30,7 @@ instance Show TopContext where -- TODO need to get class dependencies working emptyTop : ∀ io. {{Monad io}} {{HasIO io}} -> io TopContext emptyTop = do - mcctx <- newIORef (MC Nil 0 CheckAll) + mcctx <- newIORef (MC EmptyMap 0 CheckAll) errs <- newIORef $ the (List Error) Nil pure $ MkTop EmptyMap mcctx False errs Nil EmptyMap diff --git a/port/Lib/Types.newt b/port/Lib/Types.newt index df7bb3a..ca40590 100644 --- a/port/Lib/Types.newt +++ b/port/Lib/Types.newt @@ -9,19 +9,6 @@ import Data.SnocList import Data.SortedMap import Data.String -data QName : U where - QN : List String -> String -> QName - -instance Eq QName where - QN ns n == QN ns' n' = n == n' && ns == ns' - -instance Show QName where - show (QN Nil n) = n - show (QN ns n) = joinBy "." ns ++ "." ++ n - -instance Ord QName where - compare (QN ns nm) (QN ns' nm') = if ns == ns' then compare nm nm' else compare ns ns' - Name : U Name = String @@ -88,9 +75,7 @@ data Tm : U where Bnd : FC -> Int -> Tm -- Maybe Def here instead of Maybe Tm, we'll have DCon, TCon, etc. Ref : FC -> QName -> Def -> Tm - Meta : FC -> Int -> Tm - -- kovacs optimization, I think we can App out meta instead - -- InsMeta : Int -> List BD -> Tm + Meta : FC -> QName -> Tm Lam : FC -> Name -> Icit -> Quant -> Tm -> Tm App : FC -> Tm -> Tm -> Tm UU : FC -> Tm @@ -236,7 +221,7 @@ data Val : U where -- neutral case VCase : FC -> (sc : Val) -> List CaseAlt -> Val -- we'll need to look this up in ctx with IO - VMeta : FC -> (ix : Int) -> (sp : SnocList Val) -> Val + VMeta : FC -> QName -> (sp : SnocList Val) -> Val VLam : FC -> Name -> Icit -> Quant -> Closure -> Val VPi : FC -> Name -> Icit -> Quant -> (a : Val) -> (b : Closure) -> Val VLet : FC -> Name -> Val -> Val -> Val @@ -305,7 +290,10 @@ instance Show MetaKind where data MConstraint = MkMc FC Env (SnocList Val) Val -data MetaEntry = Unsolved FC Int Context Val MetaKind (List MConstraint) | Solved FC Int Val +data MetaEntry + = Unsolved FC QName Context Val MetaKind (List MConstraint) + | Solved FC QName Val + | OutOfScope -- The purpose of this is to only check one level of constraints when trying an Auto solution -- The idea being we narrow it down to the likely solution, and let any consequent type error @@ -315,7 +303,7 @@ data MetaMode = CheckAll | CheckFirst | NoCheck record MetaContext where constructor MC - metas : List MetaEntry + metas : SortedMap QName MetaEntry next : Int mcmode : MetaMode @@ -391,6 +379,7 @@ define (MkCtx lvl env types bds ctxFC) name val ty = instance Show MetaEntry where show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}" show (Solved _ k x) = "Solved \{show k} \{show x}" + show OutOfScope = "OutOfScope" withPos : Context -> FC -> Context withPos (MkCtx lvl env types bds ctxFC) fc = (MkCtx lvl env types bds fc) @@ -492,16 +481,13 @@ error fc msg = throwError $ E fc msg error' : ∀ a. String -> M a error' msg = throwError $ E emptyFC msg -lookupMeta : Int -> M MetaEntry +lookupMeta : QName -> M MetaEntry lookupMeta ix = do top <- get - mc <- readIORef top.metaCtx - go mc.metas - where - go : List MetaEntry -> M MetaEntry - go Nil = error' "Meta \{show ix} not found" - go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs - go (meta@(Solved _ k x) :: xs) = if k == ix then pure meta else go xs + mc <- readIORef {M} top.metaCtx + case lookupMap' ix mc.metas of + Just meta => pure meta + Nothing => pure OutOfScope mkCtx : FC -> Context mkCtx fc = MkCtx 0 Nil Nil Nil fc diff --git a/port/Main.newt b/port/Main.newt index 870add7..393e3c7 100644 --- a/port/Main.newt +++ b/port/Main.newt @@ -110,26 +110,21 @@ processModule importFC base stk qn@(QN ns nm) = do top <- get mc <- readIORef top.metaCtx - -- REVIEW suppressing unsolved and solved metas from previous files - -- I may want to know about (or exitFailure early on) unsolved - let mstart = length mc.metas - -- let Right (decls, ops, toks) = partialParse fn (manySame parseDecl) top.ops toks - -- | Left (err, toks) => exitFailure (showError src err) + (decls, ops) <- parseDecls fn top.ops toks Lin modify (\ top => MkTop top.defs top.metaCtx top.verbose top.errors top.loaded ops) putStrLn "process Decls" traverse (tryProcessDecl ns) (collectDecl decls) - -- we don't want implict errors from half-processed functions - -- but suppress them all on error for simplicity. - errors <- readIORef top.errors - if stk == Nil then logMetas (cast mstart) else pure MkUnit + (Nil) <- liftIO {M} $ readIORef top.errors + | errors => do + for_ errors $ \err => + putStrLn (showError src err) + exitFailure "Compile failed" + if stk == Nil then logMetas $ reverse $ listValues mc.metas else pure MkUnit pure src where - - -- parseDecls : - -- tryParseDecl : tryProcessDecl : List String -> Decl -> M Unit tryProcessDecl ns decl = do Left err <- tryError $ processDecl ns decl | _ => pure MkUnit diff --git a/src/Lib/Elab.idr b/src/Lib/Elab.idr index 611f3be..b065d86 100644 --- a/src/Lib/Elab.idr +++ b/src/Lib/Elab.idr @@ -1251,7 +1251,7 @@ check ctx tm ty = case (tm, !(forceType ctx.env ty)) of clauses <- traverse (\(MkAlt pat rawRHS) => pure $ MkClause (getFC pat) [(scnm, !(mkPat top (pat, Explicit)))] [] rawRHS ) alts -- buildCase expects scrutinee to be a name in the context, so we need to let it. -- if it's a Bnd and not shadowed we could skip the let, but that's messy. - let ctx' = extend ctx scnm scty + let ctx' = withPos (extend ctx scnm scty) (getFC tm) pure $ Let fc scnm sc !(buildTree ctx' $ MkProb clauses ty) -- rendered in ProcessDecl diff --git a/src/Main.idr b/src/Main.idr index aa8d590..65a78eb 100644 --- a/src/Main.idr +++ b/src/Main.idr @@ -139,7 +139,12 @@ processModule importFC base stk qn@(QN ns nm) = do -- we don't want implict errors from half-processed functions -- but suppress them all on error for simplicity. - errors <- readIORef top.errors + [] <- readIORef top.errors + | errors => do + for_ errors $ \err => + putStrLn (showError src err) + exitFailure + if stk == [] then logMetas mstart else pure () pure src where