Cross Reference: /hets/HasCASL/PrintAs.hs
PrintAs.hs revision 5dcec414fdc0d68ebcd5188e418c1fae9b32e738
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
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 = fsep $ 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 Maederinstance PrettyPrint Type where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TypeConstrAppl name kind args _) = printText0 ga name
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> (case kind of
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder Kind [] (Intersection [] _) _ -> empty
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ -> space <> colon <> printText0 ga kind)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <> if null args then empty
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder else parens (commas ga args)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (TypeToken t) = printText0 ga t
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (BracketType k l _) = bracket k $ commas ga l
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (KindedType t kind _) = printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> (case kind of
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder Kind [] (Intersection [] _) _ -> empty
a2149e576afc5770597d033a1884da0627df0a4eChristian Maeder _ -> space <> colon <> printText0 ga kind)
a2149e576afc5770597d033a1884da0627df0a4eChristian Maeder printText0 ga (MixfixType ts) = fsep (map (printText0 ga) ts)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (TupleType args _) = parens $ commas ga args
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (LazyType t _) = text quMark <+> printText0 ga (t)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ProductType ts _) = fsep (punctuate (space <> text timesS)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (map (printText0 ga) ts))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (FunType t1 arr t2 _) = printText0 ga t1
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <+> printText0 ga arr
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t2
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder-- no curried notation for bound variables
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint TypeScheme where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (SimpleTypeScheme t) = printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypeScheme vs t _) = text forallS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> semis ga vs
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> text dotS
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder <+> printText0 ga t
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint Partiality where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ Partial = text quMark
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ Total = text exMark
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint Arrow where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ FunArr = text funS
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ PFunArr = text pFun
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ ContFunArr = text contFun
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ PContFunArr = text pContFun
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint Quantifier where
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ Universal = text forallS
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder printText0 _ Existential = text existsS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ Unique = text $ existsS ++ exMark
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint TypeQual where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ OfType = colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ AsType = text asS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ InType = text inS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint LogOp where
fe883661c9d1a5a8b42ac4e8673ec133d9dad354Christian Maeder printText0 _ NotOp = text notS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ AndOp = text lAnd
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ OrOp = text lOr
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ ImplOp = text implS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 _ EquivOp = text equivS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint EqOp where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ EqualOp = text equalS
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 _ ExEqualOp = text exEqual
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint Formula where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TermFormula t) = printText0 ga t
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (ConnectFormula o fs _) = parens $
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder fsep (punctuate (space <> printText0 ga o) (map (printText0 ga) fs))
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (EqFormula o t1 t2 _) = printText0 ga t1
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga o
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t2
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (DefFormula t _) = text defS <+> printText0 ga t
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (QuantifiedFormula q vs f _) =
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga q <+> semis ga vs <+> text dotS <+> printText0 ga f
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian 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
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga f
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> text elseS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga t2
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (QualVar v t _) = parens $ text varS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga v
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> colon
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (QualOp n t _) = parens $
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder text opS
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga n
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> colon
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga t
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (ApplTerm t1 t2 _) = printText0 ga t1
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> parens (printText0 ga t2)
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (TupleTerm ts _) = parens $ commas ga ts
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 ga (TypedTerm term q typ _) = printText0 ga term
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga q
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder <+> printText0 ga typ
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (QuantifiedTerm q vs t _) = printText0 ga q
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> semis ga vs
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text dotS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (LambdaTerm ps q t _) = text lamS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> (if length ps == 1 then
86c119e3e74ba4b1b4ca728531282e9100789939Christian 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
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Total -> text $ dotS ++ exMark)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (CaseTerm t es _ ) = text caseS
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text ofS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> vcat (punctuate (text " | ")
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (map (printEq0 ga funS) es))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (LetTerm es t _) = text letS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> vcat (punctuate semi
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (map (printEq0 ga equalS) es))
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text inS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TermToken t) = printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (MixfixTerm ts) = fsep $ map (printText0 ga) ts
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (BracketTerm k l _) = bracket k $ commas ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint Pattern where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PatternVars vs _) = semis ga vs
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder printText0 ga (PatternConstr n t args _) = printText0 ga n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> colon
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> fcat (map (parens.printText0 ga) args)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (PatternToken t) = printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian 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)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TypedPattern p t _) = printText0 ga p
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (AsPattern v p _) = printText0 ga v
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> text asP
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga p
e05956d1da3c97e4d808926f97c6841c4a561991Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian 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]
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint VarDecl where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (VarDecl v t _ _) = printText0 ga v <+> colon
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint TypeVarDecl where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (TypeVarDecl v c _ _) = printText0 ga v <+>
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder case c of
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder Downset t ->
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder text lessS <+> printText0 ga t
dc808c58c91f82311454b4b66d206cd813d0aa70Christian Maeder _ -> colon <+> printText0 ga c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint GenVarDecl where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (GenVarDecl v) = printText0 ga v
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (GenTypeVarDecl tv) = printText0 ga tv
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint TypeArg where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (TypeArg v c _ _) = printText0 ga v <> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> printText0 ga c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maederinstance PrettyPrint Variance where
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder printText0 _ CoVar = text plusS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ ContraVar = text minusS
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder printText0 _ InVar = empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint ExtClass where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ExtClass c v _) = printText0 ga c <> printText0 ga v
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> space
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint ProdClass where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ProdClass l _) = fcat $ punctuate (text timesS)
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder (map (printText0 ga) l)
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maederinstance PrettyPrint Kind where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (Kind l c _) = (if null l then empty else
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder (fcat $ punctuate (text funS)
a05bca7a10260c19581dff325389de3f8edefa5eChristian Maeder (map (printText0 ga) l))
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> text funS)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <> printText0 ga c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Class where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (Downset t) = braces $ text lessS <+> printText0 ga t
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (Intersection c _) = if null c then empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder else if null $ tail c then printText0 ga $ head c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder else parens $ commas ga c
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederinstance PrettyPrint Types where
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (Types l _) = Pretty.brackets $ commas ga l
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint InstOpName where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (InstOpName n l) = printText0 ga n
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <> fcat(map (printText0 ga) l)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder------------------------------------------------------------------------
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder-- item stuff
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder------------------------------------------------------------------------
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint PseudoType where
f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder printText0 ga (SimplePseudoType t) = printText0 ga t
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (PseudoType l t _) = text lamS
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <+> fcat(map (printText0 ga) l)
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder <+> text dotS <+> printText0 ga t
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint TypeArgs where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (TypeArgs l _) = semis ga l
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint TypeVarDecls where
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maeder printText0 ga (TypeVarDecls l _) = Pretty.brackets $ semis ga l
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder
a64a0692ffff29e0846ca325b1811266a9f105e0Christian Maederinstance PrettyPrint BasicSpec where
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (BasicSpec l) = vcat (map (printText0 ga) l)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maederinstance PrettyPrint ProgEq where
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga = printEq0 ga equalS
880ba2a650103f63739485d0ed2b7d39052aeb15Christian Maeder
5dcec414fdc0d68ebcd5188e418c1fae9b32e738Christian Maederinstance PrettyPrint BasicItem where
5dcec414fdc0d68ebcd5188e418c1fae9b32e738Christian Maeder printText0 ga (SigItems s) = printText0 ga s
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ProgItems l _) = text programS <+> semis ga l
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (ClassItems i l _) = text classS <+> printText0 ga i
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> semis ga l
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (GenVarItems l _) = text varS <+> semis ga l
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder printText0 ga (FreeDatatype l _) = text freeS <+> text typeS
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder <+> semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (GenItems l _) = text generatedS <+> braces (semis ga l)
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder printText0 ga (AxiomItems vs fs _) = (if null vs then empty
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder else text forallS <+> semis ga vs)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder $$ vcat (map
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder (\x -> text dotS <+> printText0 ga x)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian 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
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (OpItems l _) = text opS <+> semis ga l
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (PredItems l _) = text predS <+> semis ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint Instance where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 _ Instance = text instanceS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ _ = empty
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint ClassItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ClassItem d l _) = printText0 ga d $$
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder if null l then empty
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder else braces (semis ga l)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint ClassDecl where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (ClassDecl l _) = commas ga l
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (SubclassDecl l s _) = commas ga l <> text lessS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> printText0 ga s
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (ClassDefn n c _) = printText0 ga n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> printText0 ga c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (DownsetDefn c v t _) = printText0 ga c
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> braces (printText0 ga v
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maeder <> text dotS
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maeder <> printText0 ga v
d24cb84dba35006c81c22c0fc4215f63c22858efChristian Maeder <> (text lessS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t))
c0467970183fa3dc894edea3caf9ca05d3a09fa8Christian Maeder
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maederinstance PrettyPrint TypeItem where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (TypeDecl l k _) = commas ga l <>
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder case k of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Kind [] (Intersection [] _) _ -> empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder _ -> space <> colon <> printText0 ga k
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (SubtypeDecl l t _) = commas ga l <+> text lessS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> printText0 ga t
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (IsoDecl l _) = cat(punctuate (text " = ")
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder (map (printText0 ga) l))
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder printText0 ga (SubtypeDefn p v t f _) = printText0 ga p
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> text equalS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> braces (printText0 ga v
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> colon
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text dotS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> printText0 ga f)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (AliasType p k t _) = (printText0 ga p <>
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder case k of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Kind [] (Intersection [] _) _ -> empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder _ -> space <> colon <> printText0 ga k)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text assignS
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (Datatype t) = printText0 ga t
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maederinstance PrettyPrint OpItem where
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga (OpDecl l t as _) = commas ga l <+> colon
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maeder <+> (printText0 ga t
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder <> (if null as then empty else comma)
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder <> commas ga as)
078dd2f6a402c8d9804616dc9616b27ce380a2eaChristian Maeder printText0 ga (OpDefn n ps s p t _) = (printText0 ga n
ae464ac109d82566feab1acbc98eab3bf1f10bb3Christian Maeder <> fcat (map (printText0 ga) ps))
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> (colon <> if p == Partial
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder then text quMark else empty)
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder <+> printText0 ga s
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> text equalS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint PredItem where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (PredDecl l t _) = commas ga l <+> colon <+> printText0 ga t
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (PredDefn n ps f _) = (printText0 ga n
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> fcat (map (printText0 ga) ps))
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> text equivS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <+> printText0 ga f
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint BinOpAttr where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 _ Assoc = text assocS
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 _ Comm = text commS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 _ Idem = text idemS
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint OpAttr where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (BinOpAttr a _) = printText0 ga a
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (UnitOpAttr t _) = text unitS <+> printText0 ga t
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint DatatypeDecl where
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (DatatypeDecl p k as d _) = (printText0 ga p <>
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder case k of
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder Kind [] (Intersection [] _) _ -> empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder _ -> space <> colon <> printText0 ga k)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> text defnS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> vcat(punctuate (text " | ")
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder (map (printText0 ga) as))
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> case d of { Nothing -> empty
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder ; Just c -> text derivingS
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> printText0 ga c
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder }
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maederinstance PrettyPrint Alternative where
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder printText0 ga (Constructor n cs p _) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <> fcat (map (printText0 ga) cs)
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder <> (case p of {Partial -> text quMark;
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder _ -> empty})
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder printText0 ga (Subtype l _) = text typeS <+> commas ga l
4e1eee47e914d754644cc396647b6997a28d3704Christian Maeder
4e1eee47e914d754644cc396647b6997a28d3704Christian Maederinstance PrettyPrint Components where
4e1eee47e914d754644cc396647b6997a28d3704Christian 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
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder printText0 ga (OpName n ts) = printText0 ga n
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder <+> fcat(map (printText0 ga) ts)
aae7a026a323021c5364aef85a0e03d586e5a5c3Christian Maeder
86c119e3e74ba4b1b4ca728531282e9100789939Christian Maeder