0 | ||| Pretty Printing of Elab Data-Types
  1 | |||
  2 | ||| This module can be used in the repl to evaluate, how
  3 | ||| syntax is translated to TTImp and Decl representations.
  4 | ||| Use `putPretty` together with a quoted expression and
  5 | ||| inspect the underlying implementation.
  6 | |||
  7 | ||| Note, to improve readability, some constructs are pretty printed
  8 | ||| as infix operator chains. The operators in question can be found in
  9 | ||| module `Language.Reflection.Syntax.Ops`.
 10 | |||
 11 | ||| REPL Examples:
 12 | |||
 13 | |||   :exec putPretty `{{ Name.In.A.Namespace }}
 14 | |||   :exec putPretty `(Just (7 * x))
 15 | |||   :exec putPretty `((1 index : Fin n) -> Vect n t -> t)
 16 | module Language.Reflection.Pretty
 17 |
 18 | import Derive.Pretty
 19 | import Data.String
 20 | import Data.Vect.Quantifiers
 21 | import Language.Reflection.Util
 22 | import Language.Reflection.TTImp
 23 |
 24 | %language ElabReflection
 25 | %default total
 26 |
 27 | --------------------------------------------------------------------------------
 28 | --          Utils
 29 | --------------------------------------------------------------------------------
 30 |
 31 | public export
 32 | Opts80 : LayoutOpts
 33 | Opts80 = Opts 80
 34 |
 35 | ||| Pretty but uncolored output to the terminal
 36 | export %inline
 37 | putDoc : HasIO io => Doc Opts80 -> io ()
 38 | putDoc = putStr . render Opts80
 39 |
 40 | ||| Pretty but uncolored output to the terminal
 41 | export %inline
 42 | putPretty : HasIO io => Pretty t => t -> io ()
 43 | putPretty = putDoc . pretty
 44 |
 45 | public export
 46 | 0 WithName : Type -> Type
 47 | WithName = Pair String
 48 |
 49 | export
 50 | conH :
 51 |      {opts : _}
 52 |   -> {auto _ : All Pretty ts}
 53 |   -> Prec
 54 |   -> String
 55 |   -> All Prelude.id ts
 56 |   -> Doc opts
 57 | conH p str ps = prettyCon p str $ go ps
 58 |
 59 |   where
 60 |     go : All Pretty ss => All Prelude.id ss -> List (Doc opts)
 61 |     go @{[]}     []             = []
 62 |     go @{_ :: _} (v :: ps) = prettyArg v :: go ps
 63 |
 64 | export
 65 | recordH :
 66 |      {opts : _}
 67 |   -> {auto _ : All Pretty ts}
 68 |   -> Prec
 69 |   -> String
 70 |   -> All WithName ts
 71 |   -> Doc opts
 72 | recordH p str ps = prettyRecord p str $ go ps
 73 |
 74 |   where
 75 |     go : All Pretty ss => All WithName ss -> List (Doc opts)
 76 |     go @{[]}     []             = []
 77 |     go @{_ :: _} ((fn,v) :: ps) = prettyField fn v :: go ps
 78 |
 79 | export
 80 | op :
 81 |      {opts : _}
 82 |   -> Prec
 83 |   -> (fixity : Nat)
 84 |   -> (fst  : Doc opts)
 85 |   -> (args : List (String,Doc opts))
 86 |   -> Doc opts
 87 | op p fixity fst args@((o,_) :: _) =
 88 |   let len    := length o
 89 |       opArgs := map (\(x,y) => line {opts} x <++> y) args
 90 |       sngl   := hsep (fst :: opArgs)
 91 |       mult   := vsep (indent (S len) fst :: opArgs)
 92 |    in parenthesise (p >= User fixity) $ ifMultiline sngl mult
 93 | op _ _ fst [] = fst
 94 |
 95 | --------------------------------------------------------------------------------
 96 | --          Pretty instances for TT Types
 97 | --------------------------------------------------------------------------------
 98 |
 99 | public export
100 | Pretty Namespace where
101 |   prettyPrec _ (MkNS xs) = line . concat . intersperse "." $ reverse xs
102 |
103 | export
104 | Pretty Name where
105 |   prettyPrec _ = dquotes . line . show
106 |
107 | export
108 | Pretty FC where
109 |   prettyPrec _ _ = line "emptyFC"
110 |
111 | export
112 | Pretty a => Pretty (WithFC a) where
113 |   prettyPrec n x = prettyPrec n x.value
114 |
115 | export
116 | Pretty a => Pretty (WithDefault a def') where
117 |   prettyPrec p withDef =
118 |     onWithDefault (line "defaulted")
119 |                   (\v => prettyCon p "specified" [prettyArg v])
120 |                   withDef
121 |
122 | %runElab derive "Count" [Pretty]
123 | %runElab derive "PiInfo" [Pretty]
124 | %runElab derive "LazyReason" [Pretty]
125 | %runElab derive "TotalReq" [Pretty]
126 | %runElab derive "Visibility" [Pretty]
127 | %runElab derive "PrimType" [Pretty]
128 | %runElab derive "Constant" [Pretty]
129 |
130 | --------------------------------------------------------------------------------
131 | --          Pretty instance for TTImp
132 | --------------------------------------------------------------------------------
133 |
134 | %runElab derive "BindMode" [Pretty]
135 | %runElab derive "UseSide" [Pretty]
136 | %runElab derive "DotReason" [Pretty]
137 | %runElab derive "BuiltinType" [Pretty]
138 | %runElab derive "WithFlag" [Pretty]
139 | %runElab derive "DataOpt" [Pretty]
140 |
141 | export %hint
142 | prettyImplTTImp : Pretty TTImp
143 |
144 | export %hint
145 | prettyImplArg : Pretty Arg
146 |
147 | export %hint
148 | prettyImplClause : Pretty Clause
149 |
150 | export %hint
151 | prettyImplITy : Pretty ITy
152 |
153 | %runElab deriveMutual
154 |   [ "IFieldUpdate"
155 |   , "AltType"
156 |   , "FnOpt"
157 |   , "Data"
158 |   , "IField"
159 |   , "Record"
160 |   , "Decl"
161 |   , "IClaimData"
162 |   ] [Pretty]
163 |
164 | prettyImplITy = MkPretty $ \p,v => case v of
165 |   (MkTy _ n ty) => recordH p "mkTy" [("name", n.value), ("type", ty)]
166 |
167 | prettyImplArg = MkPretty $ \p,v =>
168 |   conH p "MkArg" [v.count, v.piInfo, v.name, v.type]
169 |
170 | prettyImplClause = assert_total $ MkPretty $ \p,v => case v of
171 |   PatClause fc lhs rhs =>
172 |     op p 3 (prettyPrec (User 3) lhs) [(".=", prettyPrec (User 3) rhs)]
173 |   WithClause fc lhs rig wval prf flags cls =>
174 |     recordH p "withClause"
175 |       [ ("lhs", lhs)
176 |       , ("rig", rig)
177 |       , ("wval", wval)
178 |       , ("prf", prf)
179 |       , ("flags", flags)
180 |       , ("clauses", cls)
181 |       ]
182 |   ImpossibleClause fc lhs => conH p "impossibleClause" [lhs]
183 |
184 | appOp : {opts : _} -> Either String Name -> TTImp -> (String, Doc opts)
185 | appOp (Left x)  s = (x, prettyPrec (User 6) s)
186 | appOp (Right x) s = (".!", prettyPrec (User 6) (x,s))
187 |
188 | appPairs :
189 |      {opts : _}
190 |   -> List (String,Doc opts)
191 |   -> TTImp
192 |   -> (Doc opts, List (String,Doc opts))
193 | appPairs ps (IApp fc s t)     = appPairs (appOp (Left ".$") t :: ps) s
194 | appPairs ps (IAutoApp fc s t) = appPairs (appOp (Left ".@") t :: ps) s
195 | appPairs ps (INamedApp fc s nm t) = appPairs (appOp (Right nm) t :: ps) s
196 | appPairs ps t = (prettyPrec (User 6) t, ps)
197 |
198 | prettyImplTTImp = assert_total $ MkPretty $ \p,v => case v of
199 |   IVar _ nm => conH p "var" [nm]
200 |
201 |   IPi _ rig pinfo mnm argTy retTy =>
202 |     let (args,res) := unPi retTy
203 |         pargs      := prettyPrec (User 5) <$> args
204 |         pres       := prettyPrec (User 5) res
205 |         fst        := prettyPrec (User 5) $ MkArg rig pinfo mnm argTy
206 |      in op p 5 fst $ (".->",) <$> (pargs ++ [pres])
207 |
208 |   ILam _ rig pinfo mnm argTy lamTy =>
209 |     let (args,res) := unLambda lamTy
210 |         pargs      := prettyPrec (User 3) <$> args
211 |         pres       := prettyPrec (User 3) res
212 |         fst        := prettyPrec (User 3) $ MkArg rig pinfo mnm argTy
213 |      in op p 3 fst $ (".=>",) <$> (pargs ++ [pres])
214 |
215 |   ILet _ _ rig nm nTy nVal scope =>
216 |     recordH p "ilet"
217 |       [ ("count", rig)
218 |       , ("name", nm)
219 |       , ("type", nTy)
220 |       , ("val", nVal)
221 |       , ("scope", scope)
222 |       ]
223 |
224 |   ICase _ _ s ty cls =>
225 |     recordH p "iCase" [("sc", s), ("ty", ty), ("clauses", cls)]
226 |
227 |   ILocal _ decls s => recordH p "local" [("decls", decls), ("scope", s)]
228 |
229 |   IUpdate _ upds s => recordH p "update" [("updates", upds), ("arg", s)]
230 |
231 |   IApp _ s t =>
232 |     let (fst,ps) := appPairs [appOp (Left ".$") t] s
233 |      in op p 6 fst ps
234 |
235 |   INamedApp _ s nm t =>
236 |     let (fst,ps) := appPairs [appOp (Right nm) t] s
237 |      in op p 6 fst ps
238 |
239 |   IAutoApp _ s t =>
240 |     let (fst,ps) := appPairs [appOp (Left ".@") t] s
241 |      in op p 6 fst ps
242 |
243 |   IWithApp _ s t => recordH p "withApp" [("fun", s), ("arg", t)]
244 |   ISearch _ depth => conH p "iSearch" [depth]
245 |   IAlternative _ x ss => recordH p "alternative" [("tpe", x), ("alts", ss)]
246 |   IRewrite _ s t => recordH p "iRewrite" [("eq", s), ("scope", t)]
247 |   IBindHere _ bm s => recordH p "bindHere" [("mode", bm), ("arg", s)]
248 |   IBindVar _ str => conH p "bindVar" [str]
249 |   IAs _ _ side nm s =>
250 |     recordH p "iAs" [("side", side), ("name", nm), ("val", s)]
251 |   IMustUnify _ dr s => recordH p "mustUnify" [("reason", dr), ("val", s)]
252 |   IDelayed _ lr s => recordH p "iDelayed" [("reason", lr), ("arg", s)]
253 |   IDelay _ s => conH p "iDelay" [s]
254 |   IForce _ s => conH p "iForce" [s]
255 |   IQuote _ s => conH p "quote" [s]
256 |   IQuoteName _ nm => conH p "quoteName" [nm]
257 |   IQuoteDecl _ decls => conH p "quoteName" [decls]
258 |   IUnquote _ s => conH p "unquote" [s]
259 |   IPrimVal _ c => conH p "primVal" [c]
260 |   IType _ => line "type"
261 |   IHole _ str => conH p "hole" [str]
262 |   Implicit _ False => line "implicitFalse"
263 |   Implicit _ True  => line "implicitTrue"
264 |   IWithUnambigNames fc xs s => conH p "IWithUnambigNames" [fc, xs, s]
265 |
266 | --------------------------------------------------------------------------------
267 | --          Pretty instances for library types
268 | --------------------------------------------------------------------------------
269 |
270 | export %inline
271 | Pretty (Fin n) where
272 |   prettyPrec _ = line . show
273 |
274 | %runElab deriveIndexed "MissingInfo" [Pretty]
275 | %runElab deriveIndexed "AppArg" [Pretty]
276 |
277 | export
278 | Pretty (All AppArg vs) where
279 |   prettyPrec _ vs = list $ go vs
280 |
281 |     where
282 |       go : All AppArg bs -> List (Doc opts)
283 |       go []       = []
284 |       go (x :: y) = pretty x :: go y
285 |
286 | %runElab deriveIndexed "Con" [Pretty]
287 | %runElab deriveIndexed "TypeInfo" [Pretty]
288 | %runElab deriveIndexed "ParamTag" [Pretty]
289 |
290 | export
291 | Pretty (ParamPattern m n) where
292 |   prettyPrec _ vs = list $ go vs
293 |
294 |     where
295 |       go : ParamPattern x y -> List (Doc opts)
296 |       go []       = []
297 |       go (x :: y) = pretty x :: go y
298 |
299 | %runElab deriveIndexed "PArg" [Pretty]
300 | %runElab deriveIndexed "ConArg" [Pretty]
301 | %runElab deriveIndexed "ParamCon" [Pretty]
302 | %runElab deriveIndexed "ParamTypeInfo" [Pretty]
303 |