approximate log stack in handleLogDiscard

exe/CompileMonad.idr

@@ -14,6 +14,7 @@ import Error
 
 import System.File
 import Data.IORef
+import Data.Maybe
 import Control.Eff
 
 %default total
@@ -57,12 +58,18 @@ Compile =
    ReaderL STATE State, ReaderL OPTS Options, Log,
    LoadFile, IO]
 
+
 export %inline
 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       => handleLogDiscardIO !(newIORef (length !(readIORef lvls))) l
+handleLog ref f l = case f of
+  OConsole ch => handleLogIO (const $ pure ()) ref (consoleHandle ch) l
+  OFile _ h   => handleLogIO (const $ pure ()) ref h l
+  ONone       => do
+    lvls   <- readIORef ref
+    lenRef <- newIORef (length lvls)
+    res    <- handleLogDiscardIO lenRef l
+    writeIORef ref $ fixupDiscardedLog !(readIORef lenRef) lvls
+    pure res
 
 private %inline
 withLogFile : Options ->

lib/Quox/Log.idr

@@ -289,3 +289,16 @@ handleLogDiscardIO : HasIO m => MonadRec m => IORef Nat ->
                      LogL tag a -> m a
 handleLogDiscardIO ref act =
   runEff (handleLogDiscard_ act) [handleStateIORef ref]
+
+
+||| approximate the push/pop effects in a discarded log by trimming a stack or
+||| repeating its most recent element
+export %inline
+fixupDiscardedLog : Nat -> LevelStack -> LevelStack
+fixupDiscardedLog want lvls =
+  let len = length lvls in
+  case compare len want of
+    EQ => lvls
+    GT => drop (len `minus` want) lvls
+    LT => let new = fromMaybe defaultLogLevels $ head' lvls in
+          replicate (want `minus` len) new ++ lvls

tests/Tests/Equal.idr

@@ -27,7 +27,7 @@ parameters (label : String) (act : Eff Equal ())
   testEq = test label $ runEqual globals act
 
   testNeq : Test
-  testNeq = testThrows label (const True) $ runTC globals act $> "()"
+  testNeq = testThrows label (const True) $ runTC globals act $> "ok"
 
 
 parameters (ctx : TyContext d n)

tests/Tests/Reduce.idr

@@ -14,9 +14,10 @@ import Control.Eff
 
 runWhnf : Eff Whnf a -> Either Error a
 runWhnf act = runSTErr $ do
-  runEff act [handleExcept (\e => stLeft e),
-              handleStateSTRef !(liftST $ newSTRef 0),
-              handleLogDiscard]
+  runEff act $ with Union.(::)
+    [handleExcept (\e => stLeft e),
+     handleStateSTRef !(newSTRef' 0),
+     handleLogDiscardST !(newSTRef' 0)]
 
 parameters {0 isRedex : RedexTest tm} {auto _ : CanWhnf tm isRedex} {d, n : Nat}
            {auto _ : (Eq (tm d n), Show (tm d n))}

tests/Tests/Typechecker.idr

@@ -114,11 +114,11 @@ parameters (label : String) (act : Lazy (Eff Test ()))
            {default defGlobals globals : Definitions}
   testTC : Test
   testTC = test label {e = Error', a = ()} $
-    extract $ runExcept $ runReaderAt DEFS globals act
+    runEff act [handleExcept (\e => Left e), handleReaderConst globals]
 
   testTCFail : Test
   testTCFail = testThrows label (const True) $
-    (extract $ runExcept $ runReaderAt DEFS globals act) $> "()"
+    runEff act [handleExcept (\e => Left e), handleReaderConst globals] $> "ok"
 
 
 inferredTypeEq : TyContext d n -> (exp, got : Term d n) -> Eff Test ()

tests/TypingImpls.idr

@@ -25,8 +25,8 @@ runEqual defs act = runSTErr $ do
   runEff act $ with Union.(::)
     [handleExcept (\e => stLeft e),
      handleReaderConst defs,
-     handleStateSTRef !(liftST $ newSTRef 0),
-     handleLogDiscard]
+     handleStateSTRef !(newSTRef' 0),
+     handleLogDiscardST !(newSTRef' 0)]
 
 export
 runTC : Definitions -> Eff TC a -> Either Error a