From 8b8bec250a0cf4bac1cf32a3859ea5dba0034c42 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 29 Jan 2024 18:17:17 +0100 Subject: [PATCH] wip --- exe/CompileMonad.idr | 3 +- exe/Options.idr | 2 +- lib/Control/Monad/ST/Extra.idr | 14 ++++ lib/Quox/Equal.idr | 93 ++++++++++++----------- lib/Quox/Log.idr | 121 ++++++++++++++---------------- lib/Quox/Typechecker.idr | 19 +++-- lib/Quox/Typing.idr | 4 +- lib/Quox/Whnf/ComputeElimType.idr | 10 ++- lib/Quox/Whnf/Main.idr | 26 ++++--- 9 files changed, 155 insertions(+), 137 deletions(-) diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr index ba3222d..3839d91 100644 --- a/exe/CompileMonad.idr +++ b/exe/CompileMonad.idr @@ -69,7 +69,8 @@ withLogFile : Options -> (IORef LevelStack -> OpenFile -> IO (Either Error a)) -> IO (Either Error a) withLogFile opts act = do - withOutFile CErr opts.logFile fromError $ act !(newIORef initStack) + lvlStack <- newIORef $ singleton opts.logLevels + withOutFile CErr opts.logFile fromError $ act lvlStack where fromError : String -> FileError -> IO (Either Error a) fromError file err = pure $ Left $ WriteError file err diff --git a/exe/Options.idr b/exe/Options.idr index 68032f2..f1788df 100644 --- a/exe/Options.idr +++ b/exe/Options.idr @@ -156,7 +156,7 @@ splitLogFlag = traverse flag1 . toList . split (== ':') where case strM second of StrCons '=' lvl => do cat <- parseLogCategory first - lvl <- parseLogLevel second + lvl <- parseLogLevel lvl pure (Just cat, lvl) StrNil => (Nothing,) <$> parseLogLevel first _ => Left "invalid log flag \{str}" diff --git a/lib/Control/Monad/ST/Extra.idr b/lib/Control/Monad/ST/Extra.idr index 52e16ee..f3885e0 100644 --- a/lib/Control/Monad/ST/Extra.idr +++ b/lib/Control/Monad/ST/Extra.idr @@ -62,3 +62,17 @@ export %inline HasST (STErr e) where liftST = STE . map Right export stLeft : e -> STErr e s a stLeft e = STE $ pure $ Left e + + +parameters {auto _ : HasST m} + export %inline + readSTRef' : STRef s a -> m s a + readSTRef' r = liftST $ ST.readSTRef r + + export %inline + writeSTRef' : STRef s a -> a -> m s () + writeSTRef' r x = liftST $ ST.writeSTRef r x + + export %inline + modifySTRef' : STRef s a -> (a -> a) -> m s () + modifySTRef' r f = liftST $ ST.modifySTRef r f diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 3741cbc..4541373 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -86,12 +86,13 @@ isEmptyNoLog : Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool isEmpty defs ctx sg ty = do - say "equal" logLevel "isEmpty" - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] + say "equal" logLevel ty.loc "isEmpty" + say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "equal" logLevel ty.loc $ + hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] res <- isEmptyNoLog defs ctx sg ty - say "equal" logLevel $ hsep ["isEmpty ⇝", pshow res] + say "equal" logLevel ty.loc $ hsep ["isEmpty ⇝", pshow res] pure res isEmptyNoLog defs ctx sg ty0 = do @@ -134,12 +135,13 @@ isSubSingNoLog : Definitions -> EqContext n -> SQty -> Term 0 n -> Eff EqualInner Bool isSubSing defs ctx sg ty = do - say "equal" logLevel "isSubSing" - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "equal" logLevel $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] + say "equal" logLevel ty.loc "isSubSing" + say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 95 ty.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "equal" logLevel ty.loc $ + hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] res <- isSubSingNoLog defs ctx sg ty - say "equal" logLevel $ hsep ["isSubsing ⇝", pshow res] + say "equal" logLevel ty.loc $ hsep ["isSubsing ⇝", pshow res] pure res isSubSingNoLog defs ctx sg ty0 = do @@ -180,9 +182,10 @@ ensureTyConNoLog loc ctx ty = do Right n => throw $ NotType loc (toTyContext ctx) (ty // shift0 ctx.dimLen) ensureTyCon loc ctx ty = do - say "equal" 60 "ensureTyCon" - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 60 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] + say "equal" 60 ty.loc "ensureTyCon" + say "equal" 95 ty.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 60 ty.loc $ + hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] ensureTyConNoLog loc ctx ty @@ -805,13 +808,14 @@ namespace Term compare0' defs ctx sg ty' s' t' compare0 defs ctx sg ty s t = do - say "equal" 30 "Term.compare0" - say "equal" 30 $ hsep ["mode =", pshow !mode] - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "equal" 31 $ hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] - say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] - say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] + say "equal" 30 s.loc "Term.compare0" + say "equal" 30 s.loc $ hsep ["mode =", pshow !mode] + say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "equal" 31 s.loc $ + hsep ["ty =", runPretty $ prettyTerm [<] ctx.tnames ty] + say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] + say "equal" 30 s.loc $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] compare0NoLog defs ctx sg ty s t namespace Elim @@ -824,14 +828,15 @@ namespace Elim maybe (pure ty) throw err compare0 defs ctx sg e f = do - say "equal" 30 "Elim.compare0" - say "equal" 30 $ hsep ["mode =", pshow !mode] - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "equal" 30 $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e] - say "equal" 30 $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f] + say "equal" 30 e.loc "Elim.compare0" + say "equal" 30 e.loc $ hsep ["mode =", pshow !mode] + say "equal" 95 e.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 95 e.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "equal" 30 e.loc $ hsep ["e =", runPretty $ prettyElim [<] ctx.tnames e] + say "equal" 30 e.loc $ hsep ["f =", runPretty $ prettyElim [<] ctx.tnames f] ty <- compare0NoLog defs ctx sg e f - say "equal" 31 $ hsep ["ty ⇝", runPretty $ prettyTerm [<] ctx.tnames ty] + say "equal" 31 e.loc $ + hsep ["ty ⇝", runPretty $ prettyTerm [<] ctx.tnames ty] pure ty export covering %inline @@ -846,11 +851,11 @@ compareTypeNoLog defs ctx s t = do compareType' defs ctx s' t' compareType defs ctx s t = do - say "equal" 30 "compareType" - say "equal" 30 $ hsep ["mode =", pshow !mode] - say "equal" 95 $ hsep ["ctx =", runPretty $ prettyEqContext ctx] - say "equal" 30 $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] - say "equal" 30 $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] + say "equal" 30 s.loc "compareType" + say "equal" 30 s.loc $ hsep ["mode =", pshow !mode] + say "equal" 95 s.loc $ hsep ["ctx =", runPretty $ prettyEqContext ctx] + say "equal" 30 s.loc $ hsep ["s =", runPretty $ prettyTerm [<] ctx.tnames s] + say "equal" 30 s.loc $ hsep ["t =", runPretty $ prettyTerm [<] ctx.tnames t] compareTypeNoLog defs ctx s t @@ -874,10 +879,10 @@ parameters (loc : Loc) (ctx : TyContext d n) fromInner = lift . map fst . runState mode private - eachCorner : Has Log fs => FreeVars d -> - (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs () - eachCorner fvs act = do - say "equal" 50 $ + eachCorner : Has Log fs => Loc -> FreeVars d -> + (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs () + eachCorner loc fvs act = do + say "equal" 50 loc $ hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs) for_ (splits loc ctx.dctx fvs) $ \th => act (makeEqContext ctx th) th @@ -888,8 +893,8 @@ parameters (loc : Loc) (ctx : TyContext d n) Definitions -> EqContext n -> DSubst d 0 -> Eff EqualInner () private - runCompare : FreeVars d -> CompareAction d n -> Eff Equal () - runCompare fvs act = fromInner $ eachCorner fvs $ act !(askAt DEFS) + runCompare : Loc -> FreeVars d -> CompareAction d n -> Eff Equal () + runCompare loc fvs act = fromInner $ eachCorner loc fvs $ act !(askAt DEFS) private foldMap1 : Semigroup b => (a -> b) -> List1 a -> b @@ -903,21 +908,21 @@ parameters (loc : Loc) (ctx : TyContext d n) namespace Term export covering compare : SQty -> (ty, s, t : Term d n) -> Eff Equal () - compare sg ty s t = runCompare (fdvAll [ty, s, t]) $ \defs, ectx, th => - compare0 defs ectx sg (ty // th) (s // th) (t // th) + compare sg ty s t = runCompare s.loc (fdvAll [ty, s, t]) $ + \defs, ectx, th => compare0 defs ectx sg (ty // th) (s // th) (t // th) export covering compareType : (s, t : Term d n) -> Eff Equal () - compareType s t = runCompare (fdvAll [s, t]) $ \defs, ectx, th => - compareType defs ectx (s // th) (t // th) + compareType s t = runCompare s.loc (fdvAll [s, t]) $ + \defs, ectx, th => compareType defs ectx (s // th) (t // th) namespace Elim ||| you don't have to pass the type in but the arguments must still be ||| of the same type!! export covering compare : SQty -> (e, f : Elim d n) -> Eff Equal () - compare sg e f = runCompare (fdvAll [e, f]) $ \defs, ectx, th => - ignore $ compare0 defs ectx sg (e // th) (f // th) + compare sg e f = runCompare e.loc (fdvAll [e, f]) $ + \defs, ectx, th => ignore $ compare0 defs ectx sg (e // th) (f // th) namespace Term export covering %inline diff --git a/lib/Quox/Log.idr b/lib/Quox/Log.idr index 18295ae..247a479 100644 --- a/lib/Quox/Log.idr +++ b/lib/Quox/Log.idr @@ -1,11 +1,12 @@ module Quox.Log +import Quox.Loc +import Quox.Pretty + import Data.So import Data.DPair import Data.Maybe import Data.List1 - -import Quox.Pretty import Control.Eff import Control.Monad.ST.Extra import Data.IORef @@ -28,18 +29,26 @@ public export %inline isLogLevel : Nat -> Bool isLogLevel l = l <= maxLogLevel +public export +IsLogLevel : Nat -> Type +IsLogLevel l = So $ isLogLevel l + public export %inline isLogCategory : String -> Bool isLogCategory cat = cat `elem` logCategories +public export +IsLogCategory : String -> Type +IsLogCategory cat = So $ isLogCategory cat + public export LogLevel : Type -LogLevel = Subset Nat (So . isLogLevel) +LogLevel = Subset Nat IsLogLevel public export LogCategory : Type -LogCategory = Subset String (So . isLogCategory) +LogCategory = Subset String IsLogCategory public export %inline @@ -82,25 +91,6 @@ export %inline initStack : LevelStack initStack = singleton defaultLogLevels -export -makeLogLevels : Nat -> List (String, Nat) -> Either String LogLevels -makeLogLevels d ls = do - d <- toLevel d - ls <- traverse (bitraverse toCat toLevel) ls - pure $ MkLogLevels d ls -where - toCat : String -> Either String LogCategory - toCat str = do - let Left p = choose $ isLogCategory str - | _ => Left "not a log category: \{str}" - Right $ Element str p - - toLevel : Nat -> Either String LogLevel - toLevel l = do - let Left p = choose $ isLogLevel l - | _ => Left "log level not in range: \{show l}" - Right $ Element l p - ||| right biased for the default and for overlapping elements public export %inline mergeLevels : LogLevels -> LogLevels -> LogLevels @@ -122,48 +112,48 @@ data PushArg = SetDefault LogLevel | SetCats LevelMap %name PushArg push export %inline -mergePush : LogLevels -> PushArg -> LogLevels -mergePush lvls (SetDefault def) = {defLevel := def} lvls -mergePush lvls (SetCats map) = {levels $= (map ++)} lvls +mergePush : PushArg -> LogLevels -> LogLevels +mergePush (SetDefault def) = {defLevel := def} +mergePush (SetCats map) = {levels $= (map ++)} public export -data LogL : tag -> Type -> Type where - Say : (cat : LogCategory) -> (lvl : LogLevel) -> (msg : Lazy LogDoc) -> - LogL tag () - Push : (push : PushArg) -> LogL tag () - Pop : LogL tag () - CurLevels : LogL tag LogLevels +data LogL : (lbl : tag) -> Type -> Type where + Say : (cat : LogCategory) -> (lvl : LogLevel) -> + (loc : Loc) -> (msg : Lazy LogDoc) -> LogL lbl () + Push : (push : PushArg) -> LogL lbl () + Pop : LogL lbl () + CurLevels : LogL lbl LogLevels public export Log : Type -> Type Log = LogL () -parameters (0 tag : a) {auto _ : Has (LogL tag) fs} +parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs} public export %inline - sayAt : (cat : String) -> (0 _ : So $ isLogCategory cat) => - (lvl : Nat) -> (0 _ : So $ isLogLevel lvl) => - Lazy LogDoc -> Eff fs () - sayAt cat lvl msg = - send $ Say {tag} (Element cat %search) (Element lvl %search) msg + sayAt : (cat : String) -> (0 catOk : IsLogCategory cat) => + (lvl : Nat) -> (0 lvlOk : IsLogLevel lvl) => + Loc -> Lazy LogDoc -> Eff fs () + sayAt cat lvl loc msg {catOk, lvlOk} = + send $ Say {lbl} (Element cat catOk) (Element lvl lvlOk) loc msg public export %inline pushAt : PushArg -> Eff fs () - pushAt lvls = send $ Push {tag} lvls + pushAt lvls = send $ Push {lbl} lvls public export %inline popAt : Eff fs () - popAt = send $ Pop {tag} + popAt = send $ Pop {lbl} public export %inline curLevelsAt : Eff fs LogLevels - curLevelsAt = send $ CurLevels {tag} + curLevelsAt = send $ CurLevels {lbl} parameters {auto _ : Has Log fs} public export %inline - say : (cat : String) -> (0 _ : So $ isLogCategory cat) => - (lvl : Nat) -> (0 _ : So $ isLogLevel lvl) => - Lazy LogDoc -> Eff fs () + say : (cat : String) -> (0 _ : IsLogCategory cat) => + (lvl : Nat) -> (0 _ : IsLogLevel lvl) => + Loc -> Lazy LogDoc -> Eff fs () say = sayAt () public export %inline @@ -179,47 +169,48 @@ parameters {auto _ : Has Log fs} curLevels = curLevelsAt () -export %inline +export doPush : PushArg -> LevelStack -> LevelStack -doPush push list = mergePush (head list) push `cons` list +doPush push list = mergePush push (head list) `cons` list -export %inline +export doPop : List1 a -> List1 a doPop list = fromMaybe list $ fromList list.tail -export %inline +export doSay : Applicative m => LevelStack -> (LogDoc -> m ()) -> - LogCategory -> LogLevel -> LogDoc -> m () -doSay list act cat lvl msg = - when (lvl <= getLevel cat (head list)) $ - act $ hcat [text cat.fst, ":", pshow lvl.fst, ":"] <++> msg + LogCategory -> LogLevel -> Loc -> Lazy LogDoc -> m () +doSay (map ::: _) act cat lvl loc msg = + when (lvl <= getLevel cat map) $ do + let loc = runPretty $ prettyLoc loc + act $ hcat [loc, text cat.fst, "@", pshow lvl.fst, ":"] <++> msg -export %inline +export handleLogIO : HasIO m => (FileError -> m ()) -> IORef LevelStack -> File -> LogL tag a -> m a handleLogIO th lvls h = \case - Push push => modifyIORef lvls $ doPush push - Pop => modifyIORef lvls doPop - Say cat lvl msg => doSay !(readIORef lvls) printMsg cat lvl msg - CurLevels => head <$> readIORef lvls + Push push => modifyIORef lvls $ doPush push + Pop => modifyIORef lvls doPop + Say cat lvl loc msg => doSay !(readIORef lvls) printMsg cat lvl loc msg + CurLevels => head <$> readIORef lvls where printMsg : LogDoc -> m () - printMsg msg = fPutStrLn h (render _ msg) >>= either th pure + printMsg msg = fPutStr h (render _ msg) >>= either th pure -export %inline +export handleLogST : (HasST m, Monad (m s)) => STRef s (SnocList LogDoc) -> STRef s LevelStack -> LogL tag a -> m s a handleLogST docs lvls = \case - Push push => liftST $ modifySTRef lvls $ doPush push - Pop => liftST $ modifySTRef lvls doPop - Say cat lvl msg => doSay !(liftST $ readSTRef lvls) printMsg cat lvl msg - CurLevels => head <$> liftST (readSTRef lvls) + Push push => modifySTRef' lvls $ doPush push + Pop => modifySTRef' lvls doPop + Say cat lvl loc msg => doSay !(readSTRef' lvls) printMsg cat lvl loc msg + CurLevels => head <$> readSTRef' lvls where printMsg : LogDoc -> m s () - printMsg msg = liftST $ modifySTRef docs (:< msg) + printMsg msg = modifySTRef' docs (:< msg) -export %inline +export handleLogDiscard : Applicative m => LogL tag a -> m a handleLogDiscard = \case Say {} => pure () diff --git a/lib/Quox/Typechecker.idr b/lib/Quox/Typechecker.idr index 804f4ce..04a5ebd 100644 --- a/lib/Quox/Typechecker.idr +++ b/lib/Quox/Typechecker.idr @@ -52,13 +52,12 @@ private checkLogs : String -> TyContext d n -> SQty -> Term d n -> Maybe (Term d n) -> Eff TC () checkLogs fun ctx sg subj ty = do - say "check" 10 $ text fun - say "check" 95 $ hsep ["ctx =", runPretty $ prettyTyContext ctx] - say "check" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "check" 10 $ hsep ["subj =", runPretty $ prettyTermTC ctx subj] - case ty of - Just ty => say "check" 10 $ hsep ["ty =", runPretty $ prettyTermTC ctx ty] - _ => pure () + say "check" 10 subj.loc $ text fun + say "check" 95 subj.loc $ hsep ["ctx =", runPretty $ prettyTyContext ctx] + say "check" 95 subj.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "check" 10 subj.loc $ hsep ["subj =", runPretty $ prettyTermTC ctx subj] + let Just ty = ty | Nothing => pure () + say "check" 10 subj.loc $ hsep ["ty =", runPretty $ prettyTermTC ctx ty] mutual ||| "Ψ | Γ ⊢ σ · s ⇐ A ⊳ Σ" @@ -76,7 +75,7 @@ mutual checkLogs "check" ctx sg subj (Just ty) ifConsistentElse ctx.dctx (checkC ctx sg subj ty) - (say "check" 20 "check: 0=1") + (say "check" 20 subj.loc "check: 0=1") ||| "Ψ | Γ ⊢₀ s ⇐ A" ||| @@ -112,7 +111,7 @@ mutual checkLogs "checkType" ctx SZero subj univ ignore $ ifConsistentElse ctx.dctx (checkTypeC ctx subj l) - (say "check" 20 "checkType: 0=1") + (say "check" 20 subj.loc "checkType: 0=1") export covering %inline checkTypeC : TyContext d n -> Term d n -> Maybe Universe -> Eff TC () @@ -139,7 +138,7 @@ mutual checkLogs "infer" ctx sg (E subj) Nothing ifConsistentElse ctx.dctx (inferC ctx sg subj) - (say "check" 20 "infer: 0=1") + (say "check" 20 subj.loc "infer: 0=1") ||| `infer`, assuming the dimension context is consistent export covering %inline diff --git a/lib/Quox/Typing.idr b/lib/Quox/Typing.idr index a19222f..1082a51 100644 --- a/lib/Quox/Typing.idr +++ b/lib/Quox/Typing.idr @@ -88,7 +88,7 @@ parameters (defs : Definitions) expect what err pat rhs = Prelude.do match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) pure $ \term => do - say "check" 30 $ hsep ["expecting:", text what] + say "check" 30 term.loc $ hsep ["expecting:", text what] res <- whnf term maybe (throw $ err loc ctx.names term) pure $ match $ fst res @@ -144,7 +144,7 @@ parameters (defs : Definitions) expect what err pat rhs = do match <- check `(\case ~(pat) => Just ~(rhs); _ => Nothing) pure $ \term => do - say "equal" 30 $ hsep ["expecting:", text what] + say "equal" 30 term.loc $ hsep ["expecting:", text what] res <- whnf term let t0 = delay $ term // shift0 ctx.dimLen maybe (throw $ err loc ctx.names t0) pure $ match $ fst res diff --git a/lib/Quox/Whnf/ComputeElimType.idr b/lib/Quox/Whnf/ComputeElimType.idr index ce969e8..3237f0e 100644 --- a/lib/Quox/Whnf/ComputeElimType.idr +++ b/lib/Quox/Whnf/ComputeElimType.idr @@ -93,11 +93,13 @@ computeElimTypeNoLog defs ctx sg e = computeElimType defs ctx sg e {ne} = do let Val n = ctx.termLen - say "whnf" 90 "computeElimType" - say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] - say "whnf" 90 $ hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e] + say "whnf" 90 e.loc "computeElimType" + say "whnf" 95 e.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] + say "whnf" 90 e.loc $ + hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e] res <- computeElimTypeNoLog defs ctx sg e {ne} - say "whnf" 91 $ hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res] + say "whnf" 91 e.loc $ + hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res] pure res computeWhnfElimType0 defs ctx sg e = diff --git a/lib/Quox/Whnf/Main.idr b/lib/Quox/Whnf/Main.idr index 5aeea2a..2caaa27 100644 --- a/lib/Quox/Whnf/Main.idr +++ b/lib/Quox/Whnf/Main.idr @@ -15,24 +15,30 @@ export covering CanWhnf Term Interface.isRedexT export covering CanWhnf Elim Interface.isRedexE +-- the String is what to call the "s" argument in logs (maybe "s", or "e") private %inline whnfDefault : - {0 isRedex : RedexTest tm} -> CanWhnf tm isRedex => - String -> (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) -> - (defs : Definitions) -> (ctx : WhnfContext d n) -> (q : SQty) -> - tm d n -> Eff Whnf (Subset (tm d n) (No . isRedex defs ctx q)) + {0 isRedex : RedexTest tm} -> + (CanWhnf tm isRedex, Located2 tm) => + String -> + (forall d, n. WhnfContext d n -> tm d n -> Eff Pretty LogDoc) -> + (defs : Definitions) -> + (ctx : WhnfContext d n) -> + (sg : SQty) -> + (s : tm d n) -> + Eff Whnf (Subset (tm d n) (No . isRedex defs ctx sg)) whnfDefault name ppr defs ctx sg s = do - say "whnf" 10 "whnf" - say "whnf" 95 $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] - say "whnf" 95 $ hsep ["sg =", runPretty $ prettyQty sg.qty] - say "whnf" 10 $ hsep [text name, "=", runPretty $ ppr ctx s] + say "whnf" 10 s.loc "whnf" + say "whnf" 95 s.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx] + say "whnf" 95 s.loc $ hsep ["sg =", runPretty $ prettyQty sg.qty] + say "whnf" 10 s.loc $ hsep [text name, "=", runPretty $ ppr ctx s] res <- whnfNoLog defs ctx sg s - say "whnf" 11 $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst] + say "whnf" 11 s.loc $ hsep ["whnf ⇝", runPretty $ ppr ctx res.fst] pure res covering CanWhnf Elim Interface.isRedexE where - whnf = whnfDefault "s" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e + whnf = whnfDefault "e" $ \ctx, e => prettyElim ctx.dnames ctx.tnames e whnfNoLog defs ctx sg (F x u loc) with (lookupElim0 x u defs) proof eq _ | Just y = whnf defs ctx sg $ setLoc loc $ injElim ctx y