null
PrintAs.hs revision 078dd2f6a402c8d9804616dc9616b27ce380a2ea
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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder{- HetCATS/HasCASL/PrintAs.hs
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder $Id$
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Authors: Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Year: 2002
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printing As data types
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-}
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maedermodule PrintAs where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport As
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Keywords
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport HToken
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Pretty
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport PrettyPrint
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederimport GlobalAnnotations(GlobalAnnos)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederimport Print_AS_Annotation()
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maedercommas, semis :: PrettyPrint a => GlobalAnnos -> [a] -> Doc
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maedercommas ga l = fcat $ punctuate comma (map (printText0 ga) l)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maedersemis ga l = sep $ punctuate semi (map (printText0 ga) l)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint TypePattern where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (TypePattern name args _) = printText0 ga name
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <> fcat (map (parens . printText0 ga) args)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypePatternToken t) = printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (MixfixTypePattern ts) = fsep (map (printText0 ga) ts)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (BracketTypePattern k l _) = bracket k $ commas ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypePatternArgs l) = semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederbracket :: BracketKind -> Doc -> Doc
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederbracket Parens t = parens t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederbracket Squares t = Pretty.brackets t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederbracket Braces t = braces t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian MaederprintKind :: GlobalAnnos -> Kind -> Doc
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederprintKind ga kind = case kind of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Kind [] (Intersection [] _) _ -> empty
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ -> space <> colon <> printText0 ga kind
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maederinstance PrettyPrint Type where
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (TypeConstrAppl name i kind args _) = printText0 ga name
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <> if i == 0 then empty
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder else parens (int i)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <> printKind ga kind
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> if null args then empty
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder else parens (commas ga args)
a2149e576afc5770597d033a1884da0627df0a4eChristian Maeder printText0 ga (TypeToken t) = printText0 ga t
a2149e576afc5770597d033a1884da0627df0a4eChristian Maeder printText0 ga (BracketType k l _) = bracket k $ commas ga l
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (KindedType t kind _) = printText0 ga t
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <> printKind ga kind
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (MixfixType ts) = fsep (map (printText0 ga) ts)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (LazyType t _) = text quMark <+> printText0 ga (t)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ProductType ts _) = fsep (punctuate (space <> text timesS)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder (map (printText0 ga) ts))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (FunType t1 arr t2 _) = printText0 ga t1
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga arr
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t2
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Pred where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (IsIn c ts) = if null ts then printText0 ga c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder else if null $ tail ts then
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (head ts) <+>
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder colon <+> printText0 ga c
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder else printText0 ga c <+>
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder fsep (punctuate space
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder (map (printText0 ga) ts))
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint t => PrettyPrint (Qual t) where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (ps :=> t) = (if null ps then empty
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder else parens $ commas ga ps <+>
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder ptext implS <+> space) <>
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga t
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder-- no curried notation for bound variables
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint TypeScheme where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (SimpleTypeScheme t) = printText0 ga t
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (TypeScheme vs t _) = text forallS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> semis ga vs
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> text dotS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Partiality where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ Partial = text quMark
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ Total = text exMark
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
fe883661c9d1a5a8b42ac4e8673ec133d9dad354Christian Maederinstance PrettyPrint Arrow where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ FunArr = text funS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ PFunArr = text pFun
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ ContFunArr = text contFun
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ PContFunArr = text pContFun
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint Quantifier where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ Universal = text forallS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ Existential = text existsS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ Unique = text $ existsS ++ exMark
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint TypeQual where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ OfType = colon
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ AsType = text asS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ InType = text inS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint LogOp where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ NotOp = text notS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ AndOp = text lAnd
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ OrOp = text lOr
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 _ ImplOp = text implS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 _ EquivOp = text equivS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederinstance PrettyPrint EqOp where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 _ EqualOp = text equalS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 _ ExEqualOp = text exEqual
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederinstance PrettyPrint Formula where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (TermFormula t) = printText0 ga t
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (ConnectFormula o fs _) = parens $
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder fsep (punctuate (space <> printText0 ga o) (map (printText0 ga) fs))
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (EqFormula o t1 t2 _) = printText0 ga t1
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga o
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga t2
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (DefFormula t _) = text defS <+> printText0 ga t
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (QuantifiedFormula q vs f _) =
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga q <+> semis ga vs <+> text dotS <+> printText0 ga f
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (PolyFormula ts f _) =
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder text forallS <+> semis ga ts <+> text dotS <+> printText0 ga f
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederinstance PrettyPrint Term where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (CondTerm t1 f t2 _) = printText0 ga t1
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> text whenS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga f
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> text elseS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t2
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (QualVar v t _) = parens $ text varS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga v
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (QualOp n t _) = parens $
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder text opS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ApplTerm t1 t2 _) = printText0 ga t1
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> parens (printText0 ga t2)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TupleTerm ts _) = parens $ commas ga ts
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypedTerm term q typ _) = printText0 ga term
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga q
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga typ
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (QuantifiedTerm q vs t _) = printText0 ga q
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> semis ga vs
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text dotS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (LambdaTerm ps q t _) = text lamS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> (if length ps == 1 then
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga $ head ps
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder else fcat $ map
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (parens.printText0 ga) ps)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> (case q of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Partial -> text dotS
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder Total -> text $ dotS ++ exMark)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (CaseTerm t es _ ) = text caseS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> text ofS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> vcat (punctuate (text " | ")
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (map (printEq0 ga funS) es))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (LetTerm es t _) = text letS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> vcat (punctuate semi
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder (map (printEq0 ga equalS) es))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text inS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TermToken t) = printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (MixfixTerm ts) = fsep $ map (printText0 ga) ts
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder printText0 ga (BracketTerm k l _) = bracket k $ commas ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Pattern where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PatternVars vs _) = semis ga vs
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PatternConstr n t args _) = printText0 ga n
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> colon
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> fcat (map (parens.printText0 ga) args)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PatternToken t) = printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (BracketPattern k l _) = bracket k $ commas ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TuplePattern ps _) = parens $ commas ga ps
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (MixfixPattern ps) = fsep (map (printText0 ga) ps)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypedPattern p t _) = printText0 ga p
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder <+> colon
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder <+> printText0 ga t
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder printText0 ga (AsPattern v p _) = printText0 ga v
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder <+> text asP
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga p
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian MaederprintEq0 :: GlobalAnnos -> String -> ProgEq -> Doc
86c119e3e74ba4b1b4ca728531282e9100789939Christian MaederprintEq0 ga s (ProgEq p t _) = fsep [printText0 ga p
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder , text s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder , printText0 ga t]
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint VarDecl where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (VarDecl v t _ _) = printText0 ga v <+> colon
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maederinstance PrettyPrint TypeVarDecl where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypeVarDecl v c _ _) =
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga v <+>
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder case c of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Kind [] (Downset t) _ ->
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder text lessS <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ -> colon <+> printText0 ga c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint GenVarDecl where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (GenVarDecl v) = printText0 ga v
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (GenTypeVarDecl tv) = printText0 ga tv
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint TypeArg where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 ga (TypeArg v c _ _) = printText0 ga v <> colon
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> printText0 ga c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Variance where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ CoVar = text plusS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ ContraVar = text minusS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 _ InVar = empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint ExtClass where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ExtClass c v _) = printText0 ga c <> printText0 ga v
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> space
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (KindArg k) = parens (printText0 ga k)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint ProdClass where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ProdClass l _) = fcat $ punctuate (text timesS)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder (map (printText0 ga) l)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint Kind where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (Kind l c _) = (if null l then empty else
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder (fcat $ punctuate (text funS)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder (map (printText0 ga) l))
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <> text funS)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <> printText0 ga c
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint Class where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (Downset t) = braces $
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder text "_" <+> text lessS <+> printText0 ga t
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (Intersection c _) = if null c then ptext "Type"
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder else if null $ tail c then printText0 ga $ head c
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder else parens $ commas ga c
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
e289294500ad68fa0706b09521af340bbb356a69Christian Maederinstance PrettyPrint Types where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (Types l _) = Pretty.brackets $ commas ga l
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint InstOpName where
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga (InstOpName n l) = printText0 ga n
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder <> fcat(map (printText0 ga) l)
880ba2a650103f63739485d0ed2b7d39052aeb15Christian Maeder
5dcec414fdc0d68ebcd5188e418c1fae9b32e738Christian Maeder------------------------------------------------------------------------
5dcec414fdc0d68ebcd5188e418c1fae9b32e738Christian Maeder-- item stuff
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder------------------------------------------------------------------------
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint PseudoType where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (SimplePseudoType t) = printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (PseudoType l t _) = text lamS
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder <+> fcat(map (printText0 ga) l)
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder <+> text dotS <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint TypeArgs where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (TypeArgs l _) = semis ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint TypeVarDecls where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (TypeVarDecls l _) = Pretty.brackets $ semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint BasicSpec where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (BasicSpec l) = vcat (map (printText0 ga) l)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint ProgEq where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga = printEq0 ga equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint BasicItem where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (SigItems s) = printText0 ga s
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ProgItems l _) = text programS <+> semis ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (ClassItems i l _) = text classS <+> printText0 ga i
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (GenVarItems l _) = text varS <+> semis ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (FreeDatatype l _) = text freeS <+> text typeS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (GenItems l _) = text generatedS <+> braces (semis ga l)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (AxiomItems vs fs _) = (if null vs then empty
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder else text forallS <+> semis ga vs)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder $$ vcat (map
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (\x -> text dotS <+> printText0 ga x)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder fs)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint SigItems where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypeItems i l _) = text typeS <+> printText0 ga i
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (OpItems l _) = text opS <+> semis ga l
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maeder printText0 ga (PredItems l _) = text predS <+> semis ga l
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maeder
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maederinstance PrettyPrint Instance where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ Instance = text instanceS
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder printText0 _ _ = empty
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint ClassItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ClassItem d l _) = printText0 ga d $$
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder if null l then empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder else braces (semis ga l)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint ClassDecl where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (ClassDecl l _) = commas ga l
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (SubclassDecl l s _) = commas ga l <> text lessS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder <> printText0 ga s
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (ClassDefn n c _) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> printText0 ga c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (DownsetDefn c v t _) =
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder let pv = printText0 ga v in
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga c
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> braces (pv <> text dotS <> pv
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> text lessS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maederinstance PrettyPrint TypeItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypeDecl l k _) = commas ga l <>
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printKind ga k
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga (SubtypeDecl l t _) = commas ga l <+> text lessS
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder <+> printText0 ga t
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maeder printText0 ga (IsoDecl l _) = cat(punctuate (text " = ")
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder (map (printText0 ga) l))
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga (SubtypeDefn p v t f _) = printText0 ga p
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder <+> text equalS
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maeder <+> braces (printText0 ga v
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <+> text dotS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga f)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (AliasType p k t _) = (printText0 ga p <>
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printKind ga k)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text assignS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (Datatype t) = printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint OpItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (OpDecl l t as _) = commas ga l <+> colon
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> (printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> (if null as then empty else comma)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> commas ga as)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (OpDefn n ps s p t _) = (printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> fcat (map (printText0 ga) ps))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> (colon <> if p == Partial
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder then text quMark else empty)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> printText0 ga s
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint PredItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PredDecl l t _) = commas ga l <+> colon <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PredDefn n ps f _) = (printText0 ga n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> fcat (map (printText0 ga) ps))
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> text equivS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> printText0 ga f
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint BinOpAttr where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ Assoc = text assocS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 _ Comm = text commS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 _ Idem = text idemS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint OpAttr where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (BinOpAttr a _) = printText0 ga a
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (UnitOpAttr t _) = text unitS <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint DatatypeDecl where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (DatatypeDecl p k as d _) = (printText0 ga p <>
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printKind ga k)
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder <+> text defnS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder <+> vcat(punctuate (text " | ")
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder (map (printText0 ga) as))
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> case d of { Nothing -> empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder ; Just c -> text derivingS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga c
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder }
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Alternative where
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (Constructor n cs p _) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> fcat (map (printText0 ga) cs)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> (case p of {Partial -> text quMark;
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder _ -> empty})
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (Subtype l _) = text typeS <+> commas ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Components where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (Selector n p t _ _) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> colon <> (case p of { Partial ->text quMark;
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder _ -> empty }
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (NoSelector t) = printText0 ga t
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (NestedComponents l _) = parens $ semis ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint OpName where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (OpName n ts) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> fcat(map (printText0 ga) ts)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder