log refactors

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 ->

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
+handleWriterSTRef : HasST m => STRef s (SnocList w) -> WriterL lbl w a -> m s a
-handleWriterST ref (Tell w) = liftST $ modifySTRef ref (:< w)
+handleWriterSTRef ref (Tell w) = liftST $ modifySTRef ref (:< w)
 
 
 public export

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
+initStack = []
-
-||| 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
 
 export %inline
-getLevel : LogCategory -> LogLevels -> LogLevel
+getLevel1 : LogCategory -> LogLevels -> LogLevel
-getLevel cat lvls = fromMaybe lvls.defLevel $ lookup cat lvls.levels
+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
+applyPush : PushArg -> LogLevels -> LogLevels
-mergePush (SetDefault def) = {defLevel := def}
+applyPush (SetDefault def) = {defLevel := def}
-mergePush (SetCats    map) = {levels   $= (map ++)}
+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) ->
+  ||| print some log messages
-              (msgs : List LogMsg) -> LogL lbl ()
+  SayMany : (cat : LogCategory) -> (loc : Loc) ->
-  Push      : (push : PushArg) -> LogL lbl ()
+            (msgs : List LogMsg) -> LogL lbl ()
-  Pop       : 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
+handleLogSW : (0 s : ts) -> (0 w : tw) ->
-doPush push list = mergePush push (head list) `cons` list
+              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
+handleLogSW_ : LogL tag a -> Eff [State LevelStack, Writer LogDoc] a
-doPop (_ ::: x :: xs) = x ::: xs
+handleLogSW_ = handleLogSW () ()
-doPop (x ::: [])      = x ::: []
 
 export %inline
-doSayMany : Applicative m =>
+handleLogIO : HasIO m => MonadRec m =>
-            LevelStack -> (LogDoc -> m ()) ->
+              (FileError -> m ()) -> IORef LevelStack -> File ->
-            LogCategory -> Loc -> List LogMsg -> m ()
+              LogL tag a -> m a
-doSayMany (lvls ::: _) act cat loc msgs = do
+handleLogIO th lvls h act =
-  let Element catLvl _ = getLevel cat lvls
+  runEff (handleLogSW_ act) [handleStateIORef lvls, handleWriter {m} printMsg]
-      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
 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
+handleLogST docs lvls act =
-  Push push            => modifySTRef' lvls $ doPush push
+  runEff (handleLogSW_ act) [handleStateSTRef lvls, handleWriterSTRef docs]
-  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)
 
 export %inline
-handleLogDiscard : Applicative m => LogL tag a -> m a
+handleLogDiscard : (0 s : ts) -> Has (StateL s Nat) fs =>
-handleLogDiscard = \case
+                   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]