blob: 04e3109ff4b3310a61a2898fd3aa43e98699a0dd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
module CC.Term.Pretty
import CC.Name
import CC.Term
import Text.PrettyPrint.Prettyprinter
--------------------------------------------------------------------------------
startPrec, leftAppPrec, appPrec : Prec
startPrec = Open
leftAppPrec = Backtick
appPrec = App
prettyVar : (ctx : Context) -> (k : Nat) -> (0 _ : IsVar k n ctx) -> Doc ann
prettyVar (_ :< n) 0 (Here eq) = pretty n
prettyVar (ctx :< _) (S k) (There prf) = prettyVar ctx k prf
prettyTerm : {ctx : Context} -> Prec -> Term ctx -> Doc ann
prettyTerm d (Var k _ prf) = prettyVar ctx k prf
prettyTerm d (Abs n t) =
let (names, body) = mapFst (pretty n ::) $ getNames t in
parenthesise (d > startPrec) $ group $
backslash <+> concatWith (\x, y => x <+> comma <+> line <+> y) names <++>
pretty "=>" <+> softline <+> body
where
getNames : {ctx : Context} -> Term ctx -> (List (Doc ann), Doc ann)
getNames (Abs n t) = mapFst (pretty n ::) (getNames t)
getNames t = ([], prettyTerm startPrec t)
prettyTerm d (App t u) =
parenthesise (d >= appPrec) $ group $
prettyTerm leftAppPrec t <++> prettyTerm appPrec u
prettyTerm d (Let n t u) =
parenthesise (d > startPrec) $ group $ align $
pretty "let" <++>
(group $ align $ hang 2 $ pretty n <++> pretty "=" <+> line <+> prettyTerm startPrec t) <+>
pretty ";" <+> line <+>
prettyTerm startPrec u
export
{ctx : Context} -> Pretty (Term ctx) where
prettyPrec = prettyTerm
|
