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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
|
module Inky.Term.Pretty
import Data.Singleton
import Data.String
import Inky.Decidable.Maybe
import Inky.Term
import Inky.Type.Pretty
import Text.PrettyPrint.Prettyprinter
public export
data TermPrec = Atom | Prefix | Suffix | App | Annot | Open
%name TermPrec d
Eq TermPrec where
Atom == Atom = True
Prefix == Prefix = True
Suffix == Suffix = True
App == App = True
Annot == Annot = True
Open == Open = True
_ == _ = False
Ord TermPrec where
compare Atom Atom = EQ
compare Atom d2 = LT
compare Prefix Atom = GT
compare Prefix Prefix = EQ
compare Prefix d2 = LT
compare Suffix Atom = GT
compare Suffix Prefix = GT
compare Suffix Suffix = EQ
compare Suffix d2 = LT
compare App App = EQ
compare App Annot = LT
compare App Open = LT
compare App d2 = GT
compare Annot Annot = EQ
compare Annot Open = LT
compare Annot d2 = GT
compare Open Open = EQ
compare Open d2 = GT
export
prettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
prettyAllTerm : {tyCtx, tmCtx : SnocList String} -> List (Term tyCtx tmCtx) -> TermPrec -> List (Doc ann)
prettyTermCtx : {tyCtx, tmCtx : SnocList String} -> Context (Term tyCtx tmCtx) -> TermPrec -> SnocList (Doc ann)
prettyCases : {tyCtx, tmCtx : SnocList String} -> Context (x ** Term tyCtx (tmCtx :< x)) -> SnocList (Doc ann)
prettyLet : Doc ann -> Doc ann -> Doc ann
lessPrettyTerm : {tyCtx, tmCtx : SnocList String} -> Term tyCtx tmCtx -> TermPrec -> Doc ann
prettyTerm t d =
case isLit t <|> isCheckLit t of
Just k => pretty k
Nothing =>
if isSuc t
then pretty "suc"
else lessPrettyTerm t d
prettyAllTerm [] d = []
prettyAllTerm (t :: ts) d = prettyTerm t d :: prettyAllTerm ts d
prettyTermCtx [<] d = [<]
prettyTermCtx (ts :< (l :- t)) d = prettyTermCtx ts d :< (pretty l <+> ":" <++> prettyTerm t d)
prettyCases [<] = [<]
prettyCases (ts :< (l :- (x ** Abs (bound ** t)))) =
prettyCases ts :<
(group $ align $
pretty l <++> pretty x <++> "=>" <++>
"\\" <+> concatWith (surround $ "," <++> neutral) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open)
prettyCases (ts :< (l :- (x ** t))) =
prettyCases ts :<
(group $ align $
pretty l <++> pretty x <++> "=>" <+> line <+>
prettyTerm t Open)
prettyLet binding term =
(group $
pretty "let" <++>
(group $ hang (-2) $ binding) <+> line <+>
"in") <+> line <+>
term
lessPrettyTerm (Annot t a) d =
group $ align $ hang 2 $ parenthesise (d < Annot) $
prettyTerm t App <++> ":" <+> line <+> prettyType a Open
lessPrettyTerm (Var i) d = pretty (unVal $ nameOf i)
lessPrettyTerm (Let e (x ** t)) d =
-- TODO: pretty print annotated abstraction
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyTerm e Open)
(prettyTerm t Open)
lessPrettyTerm (LetTy a (x ** t)) d =
group $ align $ parenthesise (d < Open) $
prettyLet
(pretty x <++> "=" <+> line <+> prettyType a Open)
(prettyTerm t Open)
lessPrettyTerm (Abs (bound ** t)) d =
group $ hang 2 $ parenthesise (d < Open) $
"\\" <+> concatWith (surround $ "," <+> line) (map pretty bound) <++> "=>" <+> line <+>
prettyTerm t Open
lessPrettyTerm (App (Map (x ** a) b c) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "map"
:: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
:: prettyType b Atom
:: prettyType c Atom
:: prettyAllTerm ts Suffix)
lessPrettyTerm (App (GetChildren (x ** a) b) ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
( pretty "getChildren"
:: parens (group $ align $ hang 2 $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
:: prettyType b Atom
:: prettyAllTerm ts Suffix)
lessPrettyTerm (App f ts) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line) (prettyTerm f Suffix :: prettyAllTerm ts Suffix)
lessPrettyTerm (Tup (MkRow ts _)) d =
let parts = prettyTermCtx ts Open <>> [] in
group $ align $ enclose "<" ">" $
flatAlt
(neutral <++> concatWith (surround $ line' <+> "," <++> neutral) parts <+> line)
(concatWith (surround $ "," <++> neutral) parts)
lessPrettyTerm (Prj e l) d =
group $ align $ hang 2 $ parenthesise (d < Suffix) $
prettyTerm e Suffix <+> line' <+> "." <+> pretty l
lessPrettyTerm (Inj l t) d =
group $ align $ hang 2 $ parenthesise (d < App) $
pretty l <+> line <+> prettyTerm t Suffix
lessPrettyTerm (Case e (MkRow ts _)) d =
let parts = prettyCases ts <>> [] in
group $ align $ hang 2 $ parenthesise (d < Open) $
(group $ hang (-2) $ "case" <++> prettyTerm e Open <+> line <+> "of") <+> line <+>
(braces $
flatAlt
(neutral <++> concatWith (surround $ line' <+> ";" <++> neutral) parts <+> line)
(concatWith (surround $ ";" <++> neutral) parts))
lessPrettyTerm (Roll t) d =
pretty "~" <+>
parenthesise (d < Prefix) (group $ align $ hang 2 $ prettyTerm t Prefix)
lessPrettyTerm (Unroll e) d =
pretty "!" <+>
parenthesise (d > Prefix) (group $ align $ hang 2 $ prettyTerm e Prefix)
lessPrettyTerm (Fold e (x ** t)) d =
-- TODO: foldcase
group $ align $ hang 2 $ parenthesise (d < Open) $
"fold" <++> prettyTerm e Open <++> "by" <+> hardline <+>
(group $ align $ hang 2 $ parens $
"\\" <+> pretty x <++> "=>" <+> line <+> prettyTerm t Open)
lessPrettyTerm (Map (x ** a) b c) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "map"
, group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
, prettyType b Atom
, prettyType c Atom
]
lessPrettyTerm (GetChildren (x ** a) b) d =
group $ align $ hang 2 $ parenthesise (d < App) $
concatWith (surround line)
[ pretty "getChildren"
, group (align $ hang 2 $ parens $ "\\" <+> pretty x <++> "=>" <+> line <+> prettyType a Open)
, prettyType b Atom
]
|
