0 | module Language.Reflection.Logging
  1 |
  2 | import Control.Monad.Writer
  3 | import public Data.So
  4 | import public Data.String -- public due to compiler's bug #2439
  5 |
  6 | import public Language.Reflection
  7 |
  8 | %default total
  9 |
 10 | public export
 11 | interface LogPosition a where
 12 |   logPosition : a -> String
 13 |
 14 | public export
 15 | data LogPositions : Type where
 16 |   Nil  : LogPositions
 17 |   (::) : LogPosition a => a -> LogPositions -> LogPositions
 18 |
 19 | export
 20 | Interpolation LogPositions where
 21 |   interpolate = joinBy " " . Prelude.toList . toList [<] where
 22 |     toList : SnocList String -> LogPositions -> SnocList String
 23 |     toList acc []      = acc
 24 |     toList acc (x::xs) = toList (acc :< logPosition x) xs
 25 |
 26 | export
 27 | length : LogPositions -> Nat
 28 | length []      = Z
 29 | length (_::xs) = S $ length xs
 30 |
 31 | public export
 32 | data LogLevel
 33 |   = Warning
 34 |   | Info
 35 |   | Details
 36 |   | FineDetails
 37 |   | Trace
 38 |   | DetailedTrace
 39 |   | Debug
 40 |   | DetailedDebug
 41 |
 42 | public export
 43 | interface ElabLogLevels where
 44 |   toNatLevel : LogLevel -> Nat
 45 |   defaultLogLevel : LogLevel
 46 |
 47 | public export %defaulthint
 48 | DefaultElabLogLevels : ElabLogLevels
 49 | DefaultElabLogLevels = I where
 50 |   [I] ElabLogLevels where
 51 |     toNatLevel Warning       = 0
 52 |     toNatLevel Info          = 2
 53 |     toNatLevel Details       = 5
 54 |     toNatLevel FineDetails   = 7
 55 |     toNatLevel Trace         = 10
 56 |     toNatLevel DetailedTrace = 12
 57 |     toNatLevel Debug         = 15
 58 |     toNatLevel DetailedDebug = 20
 59 |     defaultLogLevel = Trace
 60 |
 61 | public export
 62 | interface Monad m => MonadLog (0 m : Type -> Type) where
 63 |   constructor MkMonadLog
 64 |   logPoint : ElabLogLevels =>
 65 |              (level : LogLevel) ->
 66 |              (topic : String) -> So (topic /= "") =>
 67 |              (positions : LogPositions) ->
 68 |              (desc : String) ->
 69 |              m ()
 70 |
 71 | export
 72 | logPoint' : MonadLog m =>
 73 |             ElabLogLevels =>
 74 |             (topic : String) -> So (topic /= "") =>
 75 |             (positions : LogPositions) ->
 76 |             (desc : String) ->
 77 |             m ()
 78 | logPoint' = logPoint defaultLogLevel
 79 |
 80 | export %inline
 81 | withLogPoint : MonadLog m =>
 82 |                ElabLogLevels =>
 83 |                (level : LogLevel) ->
 84 |                (topic : String) -> So (topic /= "") =>
 85 |                (positions : LogPositions) ->
 86 |                (desc : String) ->
 87 |                m a -> m a
 88 | withLogPoint l t p d x = logPoint l t p d >> x
 89 |
 90 | export %inline
 91 | logValue : MonadLog m =>
 92 |            ElabLogLevels =>
 93 |            (level : LogLevel) ->
 94 |            (topic : String) -> So (topic /= "") =>
 95 |            (positions : LogPositions) ->
 96 |            (desc : String) ->
 97 |            a -> m a
 98 | logValue l t p d x = logPoint l t p d $> x
 99 |
100 | export
101 | logBounds : MonadLog m =>
102 |             ElabLogLevels =>
103 |             (level : LogLevel) ->
104 |             (topic : String) -> So (topic /= "") =>
105 |             (positions : LogPositions) ->
106 |             m a ->
107 |             m a
108 | logBounds level topic positions action = do
109 |   let ticksCnt = (4 `minus` length positions) `max` 1
110 |
111 |   let startFence = replicate ticksCnt '_'
112 |   let startMark = "\{startFence} start \{startFence}"
113 |
114 |   let endFence = replicate ticksCnt '^'
115 |   let endMark = "\{endFence}  end  \{endFence}"
116 |
117 |   let lg = logPoint level topic positions
118 |
119 |   -- vertical monadic style seems to use much less memory than `lg startMark *> action <* lg endMark`
120 |   lg startMark
121 |   r <- action
122 |   lg endMark
123 |   pure r
124 |
125 | export
126 | logBounds' : MonadLog m =>
127 |              ElabLogLevels =>
128 |              (topic : String) -> So (topic /= "") =>
129 |              (positions : LogPositions) ->
130 |              m a ->
131 |              m a
132 | logBounds' = logBounds defaultLogLevel
133 |
134 | export
135 | [ElabLog] Elaboration m => MonadLog m where
136 |   logPoint level topic positions desc = logMsg topic (toNatLevel level) "\{positions} \{desc}"
137 |
138 | export
139 | [WriterLog] MonadWriter String m => MonadLog m where
140 |   logPoint level topic positions desc = tell "\{topic} \{show $ toNatLevel level}: \{positions} \{desc}\n"
141 |
142 | export %defaulthint
143 | DefaultLog : Elaboration m => MonadLog m
144 | DefaultLog = ElabLog
145 |