blob: 2b56e16e1866d1b1f764c754cbe368709c605ab0 (
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
43
44
45
46
47
48
49
50
51
52
|
module CC.Term.Pretty
import CC.Name
import CC.Term
import Text.PrettyPrint.Prettyprinter
--------------------------------------------------------------------------------
startPrec, leftArrowPrec, leftAppPrec, appPrec : Prec
startPrec = Open
leftArrowPrec = Backtick
leftAppPrec = Open
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
export
{ctx : Context} -> Pretty (Term ctx) where
prettyPrec d (Var k n prf) = prettyVar ctx k prf
prettyPrec d (Let n Nothing val t) =
parenthesise (d > startPrec) $ group $ align $
pretty "let" <++>
(group $ align $ hang 2 $ pretty n <++> equals <+> line <+> pretty val) <+>
pretty ";" <+> line <+> pretty t
prettyPrec d (Let n (Just ty) val t) =
parenthesise (d > startPrec) $ group $ align $
pretty "let" <++>
(group $ align $ hang 2 $
pretty n <++> colon <++> pretty ty <++> equals <+> line <+> pretty val) <+>
pretty ";" <+> line <+> pretty t
prettyPrec d Set = pretty "Set"
prettyPrec d (Pi Nothing dom cod) =
parenthesise (d > startPrec) $ group $
prettyPrec leftArrowPrec dom <++> pretty "->" <++> pretty cod
prettyPrec d (Pi (Just n) dom cod) =
parenthesise (d > startPrec) $ group $
parens (pretty n <++> colon <++> pretty dom) <++> pretty "->" <+> softline <+> pretty cod
prettyPrec 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 = ([], pretty t)
prettyPrec d (App t u) =
parenthesise (d >= appPrec) $ group $
prettyPrec leftAppPrec t <++> prettyPrec appPrec u
|
