From 861bd55f9463e5e583802438ad40c6f2e33657b1 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 4 Apr 2024 18:23:50 +0200
Subject: [PATCH] add log effects to FromParser

---
 exe/CompileMonad.idr           |  1 +
 lib/Quox/Parser/FromParser.idr | 58 ++++++++++++++++++----------------
 tests/Tests/FromPTerm.idr      |  2 +-
 3 files changed, 33 insertions(+), 28 deletions(-)

diff --git a/exe/CompileMonad.idr b/exe/CompileMonad.idr
index 4ec2a76..3f20fc7 100644
--- a/exe/CompileMonad.idr
+++ b/exe/CompileMonad.idr
@@ -138,6 +138,7 @@ liftFromParser act =
      handleStateIORef !(asksAt STATE defs),
      handleStateIORef !(asksAt STATE ns),
      handleStateIORef !(asksAt STATE suf),
+     \g => send g,
      \g => send g]
 
 export %inline
diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr
index ce22ae2..b49976d 100644
--- a/lib/Quox/Parser/FromParser.idr
+++ b/lib/Quox/Parser/FromParser.idr
@@ -32,41 +32,44 @@ data StateTag = NS | SEEN
 
 public export
 FromParserPure : List (Type -> Type)
-FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen]
+FromParserPure = [Except Error, DefsState, StateL NS Mods, NameGen, Log]
 
 public export
 FromParserIO : List (Type -> Type)
 FromParserIO = FromParserPure ++ [LoadFile]
 
 
+public export
+record PureParserResult a where
+  constructor MkPureParserResult
+  val       : a
+  suf       : NameSuf
+  defs      : Definitions
+  log       : SnocList LogDoc
+  logLevels : LevelStack
+
 export
 fromParserPure : {default [<] ns : Mods} ->
-                 NameSuf -> Definitions ->
-                 Eff FromParserPure a ->
-                 Either Error (a, NameSuf, Definitions)
-fromParserPure suf defs act = runSTErr $ do
-  suf  <- liftST $ newSTRef suf
-  defs <- liftST $ newSTRef defs
+                 NameSuf -> Definitions -> LevelStack ->
+                 Eff FromParserPure a -> Either Error (PureParserResult a)
+fromParserPure suf defs lvls act = runSTErr $ do
+  suf  <- newSTRef' suf
+  defs <- newSTRef' defs
+  log  <- newSTRef' [<]
+  lvls <- newSTRef' lvls
   res  <- runEff act $ with Union.(::)
-    [handleExcept (\e => stLeft e),
+    [handleExcept $ \e => stLeft e,
      handleStateSTRef defs,
-     handleStateSTRef !(liftST $ newSTRef ns),
-     handleStateSTRef suf]
-  pure (res, !(liftST $ readSTRef suf), !(liftST $ readSTRef defs))
-
-
-export covering
-fromParserIO : (MonadRec io, HasIO io) =>
-               IncludePath -> IORef SeenSet ->
-               IORef NameSuf -> IORef Definitions ->
-               Eff FromParserIO a -> io (Either Error a)
-fromParserIO inc seen suf defs act =
-  liftIO $ fromIOErr $ runEff act $ with Union.(::)
-    [handleExcept (\e => ioLeft e),
-     handleStateIORef defs,
-     handleStateIORef !(newIORef [<]),
-     handleStateIORef suf,
-     handleLoadFileIOE LoadError WrapParseError seen inc]
+     handleStateSTRef !(newSTRef' ns),
+     handleStateSTRef suf,
+     handleLogST log lvls]
+  pure $ MkPureParserResult {
+    val       = res,
+    suf       = !(readSTRef' suf),
+    defs      = !(readSTRef' defs),
+    log       = !(readSTRef' log),
+    logLevels = !(readSTRef' lvls)
+  }
 
 
 parameters {auto _ : Functor m} (b : Var n -> m a) (f : PName -> m a)
@@ -370,8 +373,9 @@ data HasFail = NoFail | AnyFail | FailWith String
 
 export covering
 expectFail : Loc -> Eff FromParserPure a -> Eff FromParserPure Error
-expectFail loc act =
-  case fromParserPure !(getAt GEN) !(getAt DEFS) {ns = !(getAt NS)} act of
+expectFail loc act = do
+  gen <- getAt GEN; defs <- getAt DEFS; ns <- getAt NS; lvl <- curLevels
+  case fromParserPure {ns} gen defs (singleton lvl) act of
     Left  err => pure err
     Right _   => throw $ ExpectedFail loc
 
diff --git a/tests/Tests/FromPTerm.idr b/tests/Tests/FromPTerm.idr
index b7bbf6e..319d407 100644
--- a/tests/Tests/FromPTerm.idr
+++ b/tests/Tests/FromPTerm.idr
@@ -68,7 +68,7 @@ parameters {c : Bool} {auto _ : Show b}
 
 runFromParser : {default empty defs : Definitions} ->
                 Eff FromParserPure a -> Either FromParser.Error a
-runFromParser = map fst . fromParserPure 0 defs
+runFromParser = map val . fromParserPure 0 defs initStack
 
 export
 tests : Test