diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr index f7b28d7..bc0b3e5 100644 --- a/exe/CompileMonad.idr +++ b/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 -> diff --git a/lib/Quox/Log.idr b/lib/Quox/Log.idr index b979205..faf8385 100644 --- a/lib/Quox/Log.idr +++ b/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 diff --git a/tests/Tests/Equal.idr b/tests/Tests/Equal.idr index 60f71ad..efd1b33 100644 --- a/tests/Tests/Equal.idr +++ b/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) diff --git a/tests/Tests/Reduce.idr b/tests/Tests/Reduce.idr index f566f07..0635199 100644 --- a/tests/Tests/Reduce.idr +++ b/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))} diff --git a/tests/Tests/Typechecker.idr b/tests/Tests/Typechecker.idr index f99886a..42af71e 100644 --- a/tests/Tests/Typechecker.idr +++ b/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 () diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr index 80b2bbd..c86ad66 100644 --- a/tests/TypingImpls.idr +++ b/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