blob: 52a358cf9b64f7b5be66e83e54ff928de91471bb (
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 Obs.Pretty
import public Text.PrettyPrint.Prettyprinter
-- ty is rendered Open
export
prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
-- ty and tail are rendered Open
export
prettyDeclForm : (prec : Prec) ->
(name : String) ->
(ty : Doc ann) ->
(sep : String) ->
(tail : Doc ann) ->
Doc ann
prettyDeclForm d name ty sep tail =
parenthesise (d > Open) $ group $ vsep $ [prettyDecl name ty <++> pretty sep, align tail]
-- body is rendered Open
export
prettyLambda : (prec : Prec) -> (name : String) -> (body : Doc ann) -> Doc ann
prettyLambda d name body =
parenthesise (d >= App) $ 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) $ group $ vsep (align head :: map (hang 2) tail)
-- first and second are rendered Open
export
prettyPair : (first, second : Doc ann) -> Doc ann
prettyPair first second =
angles $ 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) $ group $ vsep [align left <++> pretty "~", align right]
|
