From 567176e0762bae16c64aed53398c4fb2c3ba00a2 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Fri, 5 Apr 2024 01:57:18 +0200 Subject: [PATCH] log refactors --- exe/CompileMonad.idr | 2 +- lib/Quox/EffExtra.idr | 14 +++- lib/Quox/Log.idr | 169 +++++++++++++++++++++++++++--------------- 3 files changed, 122 insertions(+), 63 deletions(-) diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr index 9bdc28a..f7b28d7 100644 --- a/exe/CompileMonad.idr +++ b/exe/CompileMonad.idr @@ -62,7 +62,7 @@ handleLog : IORef LevelStack -> OpenFile -> LogL x a -> IOErr Error a handleLog lvls f l = case f of OConsole ch => handleLogIO (const $ pure ()) lvls (consoleHandle ch) l OFile _ h => handleLogIO (const $ pure ()) lvls h l - ONone => handleLogDiscard l + ONone => handleLogDiscardIO !(newIORef (length !(readIORef lvls))) l private %inline withLogFile : Options -> diff --git a/lib/Quox/EffExtra.idr b/lib/Quox/EffExtra.idr index fc6da93..4090553 100644 --- a/lib/Quox/EffExtra.idr +++ b/lib/Quox/EffExtra.idr @@ -36,6 +36,15 @@ gets : Has (State s) fs => (s -> a) -> Eff fs a gets = getsAt () +export %inline +stateAt : (0 lbl : tag) -> Has (StateL lbl s) fs => (s -> (a, s)) -> Eff fs a +stateAt lbl f = do (res, x) <- getsAt lbl f; putAt lbl x $> res + +export %inline +state : Has (State s) fs => (s -> (a, s)) -> Eff fs a +state = stateAt () + + export handleStateIORef : HasIO m => IORef st -> StateL lbl st a -> m a handleStateIORef r Get = readIORef r @@ -47,7 +56,6 @@ handleStateSTRef r Get = liftST $ readSTRef r handleStateSTRef r (Put s) = liftST $ writeSTRef r s - public export data Length : List a -> Type where Z : Length [] @@ -98,8 +106,8 @@ handleReaderConst : Applicative m => r -> ReaderL lbl r a -> m a handleReaderConst x Ask = pure x export -handleWriterST : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a -handleWriterST ref (Tell w) = liftST $ modifySTRef ref (:< w) +handleWriterSTRef : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a +handleWriterSTRef ref (Tell w) = liftST $ modifySTRef ref (:< w) public export diff --git a/lib/Quox/Log.idr b/lib/Quox/Log.idr index 36a5ce7..b979205 100644 --- a/lib/Quox/Log.idr +++ b/lib/Quox/Log.idr @@ -17,11 +17,11 @@ import Derive.Prelude %language ElabReflection -public export +public export %inline maxLogLevel : Nat maxLogLevel = 100 -public export +public export %inline logCategories : List String logCategories = ["whnf", "equal", "check"] @@ -41,11 +41,20 @@ public export IsLogCategory : String -> Type IsLogCategory cat = So $ isLogCategory cat +-- Q: why are you using `So` instead of `LT` and `Elem` +-- A: ① proof search gives up before finding a proof of e.g. ``99 `LT` 100`` +-- (i.e. `LTESucc⁹⁹ LTEZero`) +-- ② the proofs aren't looked at in any way, i just wanted to make sure the +-- list of categories was consistent everywhere + +||| a verbosity level from 0–100. higher is noisier. each log entry has a +||| verbosity level above which it will be printed, chosen, uh, based on vibes. public export LogLevel : Type LogLevel = Subset Nat IsLogLevel +||| a logging category, like "check" (type checking), "whnf", or whatever. public export LogCategory : Type LogCategory = Subset String IsLogCategory @@ -66,10 +75,14 @@ toLogCategory c = Right _ => Nothing +||| verbosity levels for each category, if they differ from the default public export LevelMap : Type LevelMap = List (LogCategory, LogLevel) --- i tried SortedMap first, but it is too much overhead for LevelMaps + +-- Q: why `List` instead of `SortedMap` +-- A: oof ouch my constant factors (maybe this one was more obvious) + public export record LogLevels where @@ -81,25 +94,33 @@ record LogLevels where public export LevelStack : Type -LevelStack = List1 LogLevels +LevelStack = List LogLevels + +public export %inline +defaultLevel : LogLevel +defaultLevel = Element 0 Oh export %inline defaultLogLevels : LogLevels -defaultLogLevels = MkLogLevels (Element 0 Oh) [] +defaultLogLevels = MkLogLevels defaultLevel [] export %inline initStack : LevelStack -initStack = singleton defaultLogLevels - -||| right biased for the default and for overlapping elements -public export %inline -mergeLevels : LogLevels -> LogLevels -> LogLevels -mergeLevels (MkLogLevels _ map1) (MkLogLevels def map2) = - MkLogLevels def $ map1 ++ map2 +initStack = [] export %inline -getLevel : LogCategory -> LogLevels -> LogLevel -getLevel cat lvls = fromMaybe lvls.defLevel $ lookup cat lvls.levels +getLevel1 : LogCategory -> LogLevels -> LogLevel +getLevel1 cat (MkLogLevels def lvls) = fromMaybe def $ lookup cat lvls + +export %inline +getLevel : LogCategory -> LevelStack -> LogLevel +getLevel cat (lvls :: _) = getLevel1 cat lvls +getLevel cat [] = defaultLevel + +export %inline +getCurLevels : LevelStack -> LogLevels +getCurLevels (lvls :: _) = lvls +getCurLevels [] = defaultLogLevels public export @@ -107,14 +128,28 @@ LogDoc : Type LogDoc = Doc (Opts {lineLength = 80}) +private %inline +replace : Eq a => a -> b -> List (a, b) -> List (a, b) +replace k v kvs = (k, v) :: filter (\y => fst y /= k) kvs + +private %inline +mergeLeft : Eq a => List (a, b) -> List (a, b) -> List (a, b) +mergeLeft l r = foldl (\lst, (k, v) => replace k v lst) r l + + public export -data PushArg = SetDefault LogLevel | SetCats LevelMap +data PushArg = SetDefault LogLevel | SetCats LevelMap | SetAll LogLevel %name PushArg push export %inline -mergePush : PushArg -> LogLevels -> LogLevels -mergePush (SetDefault def) = {defLevel := def} -mergePush (SetCats map) = {levels $= (map ++)} +applyPush : PushArg -> LogLevels -> LogLevels +applyPush (SetDefault def) = {defLevel := def} +applyPush (SetCats map) = {levels $= mergeLeft map} +applyPush (SetAll lvl) = const $ MkLogLevels lvl [] + +export %inline +fromPush : PushArg -> LogLevels +fromPush p = applyPush p defaultLogLevels public export @@ -128,10 +163,15 @@ infix 0 :> public export data LogL : (lbl : tag) -> Type -> Type where - SayMany : (cat : LogCategory) -> (loc : Loc) -> - (msgs : List LogMsg) -> LogL lbl () - Push : (push : PushArg) -> LogL lbl () - Pop : LogL lbl () + ||| print some log messages + SayMany : (cat : LogCategory) -> (loc : Loc) -> + (msgs : List LogMsg) -> LogL lbl () + ||| set some verbosity levels + Push : (push : PushArg) -> LogL lbl () + ||| restore the previous verbosity levels. + ||| returns False if the stack was already empty + Pop : LogL lbl Bool + ||| returns the current verbosity levels CurLevels : LogL lbl LogLevels public export @@ -156,7 +196,7 @@ parameters (0 lbl : tag) {auto _ : Has (LogL lbl) fs} pushAt lvls = send $ Push {lbl} lvls public export %inline - popAt : Eff fs () + popAt : Eff fs Bool popAt = send $ Pop {lbl} public export %inline @@ -180,7 +220,7 @@ parameters {auto _ : Has Log fs} push = pushAt () public export %inline - pop : Eff fs () + pop : Eff fs Bool pop = popAt () public export %inline @@ -188,53 +228,64 @@ parameters {auto _ : Has Log fs} curLevels = curLevelsAt () +||| handles a `Log` effect with an existing `State` and `Writer` export %inline -doPush : PushArg -> LevelStack -> LevelStack -doPush push list = mergePush push (head list) `cons` list +handleLogSW : (0 s : ts) -> (0 w : tw) -> + Has (StateL s LevelStack) fs => Has (WriterL w LogDoc) fs => + LogL tag a -> Eff fs a +handleLogSW s w = \case + Push push => modifyAt s $ \lst => + applyPush push (fromMaybe defaultLogLevels (head' lst)) :: lst + Pop => stateAt s $ maybe (False, []) (True,) . tail' + SayMany cat loc msgs => do + catLvl <- getsAt s $ fst . getLevel cat + let loc = runPretty $ prettyLoc loc + for_ msgs $ \(lvl :> msg) => when (lvl <= catLvl) $ tellAt w $ + hcat [loc, text cat.fst, "@", pshow lvl, ":"] <++> msg + CurLevels => + getsAt s getCurLevels export %inline -doPop : List1 a -> List1 a -doPop (_ ::: x :: xs) = x ::: xs -doPop (x ::: []) = x ::: [] +handleLogSW_ : LogL tag a -> Eff [State LevelStack, Writer LogDoc] a +handleLogSW_ = handleLogSW () () export %inline -doSayMany : Applicative m => - LevelStack -> (LogDoc -> m ()) -> - LogCategory -> Loc -> List LogMsg -> m () -doSayMany (lvls ::: _) act cat loc msgs = do - let Element catLvl _ = getLevel cat lvls - loc = runPretty $ prettyLoc loc - for_ msgs $ \msg => when (msg.level <= catLvl) $ - act $ hcat [loc, text cat.fst, "@", pshow msg.level, ":"] <++> - msg.message - -export %inline -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 - SayMany cat loc msgs => doSayMany !(readIORef lvls) printMsg cat loc msgs - CurLevels => head <$> readIORef lvls +handleLogIO : HasIO m => MonadRec m => + (FileError -> m ()) -> IORef LevelStack -> File -> + LogL tag a -> m a +handleLogIO th lvls h act = + runEff (handleLogSW_ act) [handleStateIORef lvls, handleWriter {m} printMsg] where printMsg : LogDoc -> m () printMsg msg = fPutStr h (render _ msg) >>= either th pure export %inline -handleLogST : (HasST m, Monad (m s)) => +handleLogST : HasST m => MonadRec (m s) => STRef s (SnocList LogDoc) -> STRef s LevelStack -> LogL tag a -> m s a -handleLogST docs lvls = \case - Push push => modifySTRef' lvls $ doPush push - Pop => modifySTRef' lvls doPop - SayMany cat loc msgs => doSayMany !(readSTRef' lvls) printMsg cat loc msgs - CurLevels => head <$> readSTRef' lvls -where printMsg : LogDoc -> m s () - printMsg msg = modifySTRef' docs (:< msg) +handleLogST docs lvls act = + runEff (handleLogSW_ act) [handleStateSTRef lvls, handleWriterSTRef docs] export %inline -handleLogDiscard : Applicative m => LogL tag a -> m a -handleLogDiscard = \case +handleLogDiscard : (0 s : ts) -> Has (StateL s Nat) fs => + LogL tag a -> Eff fs a +handleLogDiscard s = \case + Push _ => modifyAt s S + Pop => stateAt s $ \k => (k > 0, pred k) SayMany {} => pure () - Push {} => pure () - Pop => pure () CurLevels => pure defaultLogLevels + +export %inline +handleLogDiscard_ : LogL tag a -> Eff [State Nat] a +handleLogDiscard_ = handleLogDiscard () + +export %inline +handleLogDiscardST : HasST m => MonadRec (m s) => STRef s Nat -> + LogL tag a -> m s a +handleLogDiscardST ref act = + runEff (handleLogDiscard_ act) [handleStateSTRef ref] + +export %inline +handleLogDiscardIO : HasIO m => MonadRec m => IORef Nat -> + LogL tag a -> m a +handleLogDiscardIO ref act = + runEff (handleLogDiscard_ act) [handleStateIORef ref]