blob: f32542e43ab9d205de7994601c5d9f5f2d47fdb3 (
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
|
module Obs.Pretty
import public Text.PrettyPrint.Prettyprinter
-- ty is rendered Open
export
prettyDecl : (name : Maybe String) -> (ty : Doc ann) -> Doc ann
prettyDecl Nothing ty = parens $ group $ align ty
prettyDecl (Just name) ty = parens $ align $ group (pretty name <++> colon <+> line <+> align ty)
-- names are rendered Open
export
prettyDeclForm : (prec : Prec) ->
(decls : List (Doc ann)) ->
(sep : String) ->
(tail : Doc ann) ->
Doc ann
prettyDeclForm d decls sep tail =
parenthesise (d > Open) $
align $
group $
concatWith (\x, y => x <++> pretty sep <+> line <+> y) $
decls ++ [align tail]
-- body is rendered Open
export
prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
prettyLambda d name body =
parenthesise (d >= App) $ align $ group $
vsep [backslash <+> pretty name <++> pretty "=>", align body]
-- head is rendered Open, tail are rendered App
export
prettyApp : (prec : Prec) -> (head : Doc ann) -> (tail : List (Doc ann)) -> Doc ann
prettyApp d head tail =
parenthesise (d >= App) $ hang 2 $ group $ vsep (align head :: tail)
-- first and second are rendered Open
export
prettyPair : (first, second : Doc ann) -> Doc ann
prettyPair first second =
angles $ align $ group $
neutral <++> align first <+> comma <+> line <+> align second <++> neutral
-- left and right are rendered Equal
export
prettyEqual : (prec : Prec) -> (left, right : Doc ann) -> Doc ann
prettyEqual d left right =
parenthesise (d >= Equal) $ align $ group $ vsep [align left <++> pretty "~", align right]
|
