module UVMHS.Lib.Logging where

import UVMHS.Core
import UVMHS.Lib.Pretty

newtype LogLevel = LogLevel { LogLevel -> ℕ64
unLogLevel ∷ ℕ64 }
  deriving (LogLevel -> LogLevel -> Bool
(LogLevel -> LogLevel -> Bool)
-> (LogLevel -> LogLevel -> Bool) -> Eq LogLevel
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LogLevel -> LogLevel -> Bool
== :: LogLevel -> LogLevel -> Bool
$c/= :: LogLevel -> LogLevel -> Bool
/= :: LogLevel -> LogLevel -> Bool
Eq,Eq LogLevel
Eq LogLevel =>
(LogLevel -> LogLevel -> Ordering)
-> (LogLevel -> LogLevel -> Bool)
-> (LogLevel -> LogLevel -> Bool)
-> (LogLevel -> LogLevel -> Bool)
-> (LogLevel -> LogLevel -> Bool)
-> (LogLevel -> LogLevel -> LogLevel)
-> (LogLevel -> LogLevel -> LogLevel)
-> Ord LogLevel
LogLevel -> LogLevel -> Bool
LogLevel -> LogLevel -> Ordering
LogLevel -> LogLevel -> LogLevel
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LogLevel -> LogLevel -> Ordering
compare :: LogLevel -> LogLevel -> Ordering
$c< :: LogLevel -> LogLevel -> Bool
< :: LogLevel -> LogLevel -> Bool
$c<= :: LogLevel -> LogLevel -> Bool
<= :: LogLevel -> LogLevel -> Bool
$c> :: LogLevel -> LogLevel -> Bool
> :: LogLevel -> LogLevel -> Bool
$c>= :: LogLevel -> LogLevel -> Bool
>= :: LogLevel -> LogLevel -> Bool
$cmax :: LogLevel -> LogLevel -> LogLevel
max :: LogLevel -> LogLevel -> LogLevel
$cmin :: LogLevel -> LogLevel -> LogLevel
min :: LogLevel -> LogLevel -> LogLevel
Ord,Int -> LogLevel -> ShowS
[LogLevel] -> ShowS
LogLevel -> String
(Int -> LogLevel -> ShowS)
-> (LogLevel -> String) -> ([LogLevel] -> ShowS) -> Show LogLevel
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LogLevel -> ShowS
showsPrec :: Int -> LogLevel -> ShowS
$cshow :: LogLevel -> String
show :: LogLevel -> String
$cshowList :: [LogLevel] -> ShowS
showList :: [LogLevel] -> ShowS
Show,LogLevel -> Doc
(LogLevel -> Doc) -> Pretty LogLevel
forall a. (a -> Doc) -> Pretty a
$cpretty :: LogLevel -> Doc
pretty :: LogLevel -> Doc
Pretty)

newtype LogDepth = LogDepth { LogDepth -> ℕ64
unLogDepth ∷ ℕ64 }
  deriving (LogDepth -> LogDepth -> Bool
(LogDepth -> LogDepth -> Bool)
-> (LogDepth -> LogDepth -> Bool) -> Eq LogDepth
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LogDepth -> LogDepth -> Bool
== :: LogDepth -> LogDepth -> Bool
$c/= :: LogDepth -> LogDepth -> Bool
/= :: LogDepth -> LogDepth -> Bool
Eq,Eq LogDepth
Eq LogDepth =>
(LogDepth -> LogDepth -> Ordering)
-> (LogDepth -> LogDepth -> Bool)
-> (LogDepth -> LogDepth -> Bool)
-> (LogDepth -> LogDepth -> Bool)
-> (LogDepth -> LogDepth -> Bool)
-> (LogDepth -> LogDepth -> LogDepth)
-> (LogDepth -> LogDepth -> LogDepth)
-> Ord LogDepth
LogDepth -> LogDepth -> Bool
LogDepth -> LogDepth -> Ordering
LogDepth -> LogDepth -> LogDepth
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LogDepth -> LogDepth -> Ordering
compare :: LogDepth -> LogDepth -> Ordering
$c< :: LogDepth -> LogDepth -> Bool
< :: LogDepth -> LogDepth -> Bool
$c<= :: LogDepth -> LogDepth -> Bool
<= :: LogDepth -> LogDepth -> Bool
$c> :: LogDepth -> LogDepth -> Bool
> :: LogDepth -> LogDepth -> Bool
$c>= :: LogDepth -> LogDepth -> Bool
>= :: LogDepth -> LogDepth -> Bool
$cmax :: LogDepth -> LogDepth -> LogDepth
max :: LogDepth -> LogDepth -> LogDepth
$cmin :: LogDepth -> LogDepth -> LogDepth
min :: LogDepth -> LogDepth -> LogDepth
Ord,Int -> LogDepth -> ShowS
[LogDepth] -> ShowS
LogDepth -> String
(Int -> LogDepth -> ShowS)
-> (LogDepth -> String) -> ([LogDepth] -> ShowS) -> Show LogDepth
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LogDepth -> ShowS
showsPrec :: Int -> LogDepth -> ShowS
$cshow :: LogDepth -> String
show :: LogDepth -> String
$cshowList :: [LogDepth] -> ShowS
showList :: [LogDepth] -> ShowS
Show,LogDepth -> Doc
(LogDepth -> Doc) -> Pretty LogDepth
forall a. (a -> Doc) -> Pretty a
$cpretty :: LogDepth -> Doc
pretty :: LogDepth -> Doc
Pretty)

data LogOptions = LogOptions
  { LogOptions -> ℕ64
logOptionsLevel ∷ ℕ64
  , LogOptions -> ℕ64
logOptionsDepth ∷ ℕ64
  , LogOptions -> Bool
logOptionsShowLevel ∷ 𝔹
  } deriving (LogOptions -> LogOptions -> Bool
(LogOptions -> LogOptions -> Bool)
-> (LogOptions -> LogOptions -> Bool) -> Eq LogOptions
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: LogOptions -> LogOptions -> Bool
== :: LogOptions -> LogOptions -> Bool
$c/= :: LogOptions -> LogOptions -> Bool
/= :: LogOptions -> LogOptions -> Bool
Eq,Eq LogOptions
Eq LogOptions =>
(LogOptions -> LogOptions -> Ordering)
-> (LogOptions -> LogOptions -> Bool)
-> (LogOptions -> LogOptions -> Bool)
-> (LogOptions -> LogOptions -> Bool)
-> (LogOptions -> LogOptions -> Bool)
-> (LogOptions -> LogOptions -> LogOptions)
-> (LogOptions -> LogOptions -> LogOptions)
-> Ord LogOptions
LogOptions -> LogOptions -> Bool
LogOptions -> LogOptions -> Ordering
LogOptions -> LogOptions -> LogOptions
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: LogOptions -> LogOptions -> Ordering
compare :: LogOptions -> LogOptions -> Ordering
$c< :: LogOptions -> LogOptions -> Bool
< :: LogOptions -> LogOptions -> Bool
$c<= :: LogOptions -> LogOptions -> Bool
<= :: LogOptions -> LogOptions -> Bool
$c> :: LogOptions -> LogOptions -> Bool
> :: LogOptions -> LogOptions -> Bool
$c>= :: LogOptions -> LogOptions -> Bool
>= :: LogOptions -> LogOptions -> Bool
$cmax :: LogOptions -> LogOptions -> LogOptions
max :: LogOptions -> LogOptions -> LogOptions
$cmin :: LogOptions -> LogOptions -> LogOptions
min :: LogOptions -> LogOptions -> LogOptions
Ord,Int -> LogOptions -> ShowS
[LogOptions] -> ShowS
LogOptions -> String
(Int -> LogOptions -> ShowS)
-> (LogOptions -> String)
-> ([LogOptions] -> ShowS)
-> Show LogOptions
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> LogOptions -> ShowS
showsPrec :: Int -> LogOptions -> ShowS
$cshow :: LogOptions -> String
show :: LogOptions -> String
$cshowList :: [LogOptions] -> ShowS
showList :: [LogOptions] -> ShowS
Show)
makeLenses ''LogOptions

logOptions₀ ∷ LogOptions
logOptions₀ :: LogOptions
logOptions₀ = ℕ64 -> ℕ64 -> Bool -> LogOptions
LogOptions ℕ64
0 ℕ64
0 Bool
False

pplog ∷ (Monad m,MonadIO m,MonadReader r m,HasLens r LogOptions) ⇒ ℕ64 → (() → Doc) → m ()
pplog :: forall (m :: * -> *) r.
(Monad m, MonadIO m, MonadReader r m, HasLens r LogOptions) =>
ℕ64 -> (() -> Doc) -> m ()
pplog ℕ64
l () -> Doc
msg = do
  ℕ64
ll ← (r ⟢ ℕ64) -> m ℕ64
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL ((r ⟢ ℕ64) -> m ℕ64) -> (r ⟢ ℕ64) -> m ℕ64
forall a b. (a -> b) -> a -> b
$ LogOptions ⟢ ℕ64
logOptionsLevelL (LogOptions ⟢ ℕ64) -> (r ⟢ LogOptions) -> r ⟢ ℕ64
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens
  Bool
b ← (r ⟢ Bool) -> m Bool
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL ((r ⟢ Bool) -> m Bool) -> (r ⟢ Bool) -> m Bool
forall a b. (a -> b) -> a -> b
$ LogOptions ⟢ Bool
logOptionsShowLevelL (LogOptions ⟢ Bool) -> (r ⟢ LogOptions) -> r ⟢ Bool
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens
  Bool -> (() -> m ()) -> m ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (ℕ64
l ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
≤ ℕ64
ll) ((() -> m ()) -> m ()) -> (() -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ () → IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    Doc -> IO ()
forall a. Pretty a => a -> IO ()
pprint (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ if Bool -> Bool
not Bool
b then Doc
forall a. Null a => a
null else [Doc] -> Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
          [ Color -> Doc -> Doc
ppBG Color
grayDark (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Color -> Doc -> Doc
ppFG Color
white (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString (𝕊 -> Doc) -> 𝕊 -> Doc
forall a b. (a -> b) -> a -> b
$ [𝕊] -> 𝕊
forall a t. (Monoid a, ToIter a t) => t -> a
concat [𝕊
"▷",ℕ64 -> 𝕊
forall a. Show a => a -> 𝕊
show𝕊 ℕ64
l,𝕊
"◁"]
          , ℕ64 -> Doc
ppSpace ℕ64
1
          ]
      , Doc -> Doc
ppGA (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ () -> Doc
msg ()
      ]
    IO ()
oflush

pplogd ∷ (Monad m,MonadIO m,MonadReader r m,HasLens r LogOptions) ⇒ ℕ64 → (() → Doc) → m ()
pplogd :: forall (m :: * -> *) r.
(Monad m, MonadIO m, MonadReader r m, HasLens r LogOptions) =>
ℕ64 -> (() -> Doc) -> m ()
pplogd ℕ64
l () -> Doc
msg = do
  ℕ64
ld ← (r ⟢ ℕ64) -> m ℕ64
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL ((r ⟢ ℕ64) -> m ℕ64) -> (r ⟢ ℕ64) -> m ℕ64
forall a b. (a -> b) -> a -> b
$ LogOptions ⟢ ℕ64
logOptionsDepthL (LogOptions ⟢ ℕ64) -> (r ⟢ LogOptions) -> r ⟢ ℕ64
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens
  ℕ64 -> (() -> Doc) -> m ()
forall (m :: * -> *) r.
(Monad m, MonadIO m, MonadReader r m, HasLens r LogOptions) =>
ℕ64 -> (() -> Doc) -> m ()
pplog ℕ64
l ((() -> Doc) -> m ()) -> (() -> Doc) -> m ()
forall a b. (a -> b) -> a -> b
$ \ () → ℕ64 -> Doc
ppSpace (ℕ64
ld ℕ64 -> ℕ64 -> ℕ64
forall a. Times a => a -> a -> a
× ℕ -> ℕ64
𝕟64 ℕ
2) Doc -> Doc -> Doc
forall a. Append a => a -> a -> a
⧺ Doc -> Doc
ppGA (() -> Doc
msg ())

pplogdIndent ∷ (Monad m,MonadIO m,MonadReader r m,HasLens r LogOptions) ⇒ m a → m a
pplogdIndent :: forall (m :: * -> *) r a.
(Monad m, MonadIO m, MonadReader r m, HasLens r LogOptions) =>
m a -> m a
pplogdIndent = (r ⟢ ℕ64) -> (ℕ64 -> ℕ64) -> m a -> m a
forall (m :: * -> *) r₁ r₂ a.
(Monad m, MonadReader r₁ m) =>
(r₁ ⟢ r₂) -> (r₂ -> r₂) -> m a -> m a
mapEnvL (LogOptions ⟢ ℕ64
logOptionsDepthL (LogOptions ⟢ ℕ64) -> (r ⟢ LogOptions) -> r ⟢ ℕ64
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens) ℕ64 -> ℕ64
forall a. (One a, Plus a) => a -> a
succ

pplogdIndentReset ∷ (Monad m,MonadIO m,MonadReader r m,HasLens r LogOptions) ⇒ m a → m a
pplogdIndentReset :: forall (m :: * -> *) r a.
(Monad m, MonadIO m, MonadReader r m, HasLens r LogOptions) =>
m a -> m a
pplogdIndentReset = (r ⟢ ℕ64) -> ℕ64 -> m a -> m a
forall a r'. (r ⟢ r') -> r' -> m a -> m a
forall r (m :: * -> *) a r'.
MonadReader r m =>
(r ⟢ r') -> r' -> m a -> m a
localL (LogOptions ⟢ ℕ64
logOptionsDepthL (LogOptions ⟢ ℕ64) -> (r ⟢ LogOptions) -> r ⟢ ℕ64
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens) ℕ64
forall a. Zero a => a
zero

whenLogLevel ∷ (Monad m,MonadReader r m,HasLens r LogOptions) ⇒ ℕ64 → (() → m ()) → m ()
whenLogLevel :: forall (m :: * -> *) r.
(Monad m, MonadReader r m, HasLens r LogOptions) =>
ℕ64 -> (() -> m ()) -> m ()
whenLogLevel ℕ64
l () -> m ()
f = do
  ℕ64
ll ← (r ⟢ ℕ64) -> m ℕ64
forall r'. (r ⟢ r') -> m r'
forall r (m :: * -> *) r'. MonadReader r m => (r ⟢ r') -> m r'
askL ((r ⟢ ℕ64) -> m ℕ64) -> (r ⟢ ℕ64) -> m ℕ64
forall a b. (a -> b) -> a -> b
$ LogOptions ⟢ ℕ64
logOptionsLevelL (LogOptions ⟢ ℕ64) -> (r ⟢ LogOptions) -> r ⟢ ℕ64
forall b c a. (b ⟢ c) -> (a ⟢ b) -> a ⟢ c
forall {k} (t :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Transitive t =>
t b c -> t a b -> t a c
⊚ r ⟢ LogOptions
forall a b. HasLens a b => a ⟢ b
hasLens
  Bool -> (() -> m ()) -> m ()
forall (m :: * -> *). Return m => Bool -> (() -> m ()) -> m ()
when (ℕ64
l ℕ64 -> ℕ64 -> Bool
forall a. Ord a => a -> a -> Bool
≤ ℕ64
ll) () -> m ()
f