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