Mercurial > urweb

comparison src/expl_print.sml @ 624:354800878b4d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kind polymorphism through Explify
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:32:56 -0500
parents 588b9d16b00a
children 70cbdcf5989b
comparison
equal deleted inserted replaced
623:588b9d16b00a 624:354800878b4d
36 36
37 structure E = ExplEnv 37 structure E = ExplEnv
38 38
39 val debug = ref false 39 val debug = ref false
40 40
41 fun p_kind' par (k, _) = 41 fun p_kind' par env (k, _) =
42 case k of 42 case k of
43 KType => string "Type" 43 KType => string "Type"
44 | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, 44 | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1,
45 space, 45 space,
46 string "->", 46 string "->",
47 space, 47 space,
48 p_kind k2]) 48 p_kind env k2])
49 | KName => string "Name" 49 | KName => string "Name"
50 | KRecord k => box [string "{", p_kind k, string "}"] 50 | KRecord k => box [string "{", p_kind env k, string "}"]
51 | KUnit => string "Unit" 51 | KUnit => string "Unit"
52 | KTuple ks => box [string "(", 52 | KTuple ks => box [string "(",
53 p_list_sep (box [space, string "*", space]) p_kind ks, 53 p_list_sep (box [space, string "*", space]) (p_kind env) ks,
54 string ")"] 54 string ")"]
55 55
56 and p_kind k = p_kind' false k 56 | KRel n => ((if !debug then
57 string (E.lookupKRel env n ^ "_" ^ Int.toString n)
58 else
59 string (E.lookupKRel env n))
60 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
61 | KFun (x, k) => box [string x,
62 space,
63 string "-->",
64 space,
65 p_kind (E.pushKRel env x) k]
66
67 and p_kind env = p_kind' false env
57 68
58 fun p_con' par env (c, _) = 69 fun p_con' par env (c, _) =
59 case c of 70 case c of
60 TFun (t1, t2) => parenIf par (box [p_con' true env t1, 71 TFun (t1, t2) => parenIf par (box [p_con' true env t1,
61 space, 72 space,
64 p_con env t2]) 75 p_con env t2])
65 | TCFun (x, k, c) => parenIf par (box [string x, 76 | TCFun (x, k, c) => parenIf par (box [string x,
66 space, 77 space,
67 string "::", 78 string "::",
68 space, 79 space,
69 p_kind k, 80 p_kind env k,
70 space, 81 space,
71 string "->", 82 string "->",
72 space, 83 space,
73 p_con (E.pushCRel env x k) c]) 84 p_con (E.pushCRel env x k) c])
74 | TRecord (CRecord (_, xcs), _) => box [string "{", 85 | TRecord (CRecord (_, xcs), _) => box [string "{",
114 space, 125 space,
115 string x, 126 string x,
116 space, 127 space,
117 string "::", 128 string "::",
118 space, 129 space,
119 p_kind k, 130 p_kind env k,
120 space, 131 space,
121 string "=>", 132 string "=>",
122 space, 133 space,
123 p_con (E.pushCRel env x k) c]) 134 p_con (E.pushCRel env x k) c])
124 135
132 space, 143 space,
133 string "=", 144 string "=",
134 space, 145 space,
135 p_con env c]) xcs, 146 p_con env c]) xcs,
136 string "]::", 147 string "]::",
137 p_kind k]) 148 p_kind env k])
138 else 149 else
139 parenIf par (box [string "[", 150 parenIf par (box [string "[",
140 p_list (fn (x, c) => 151 p_list (fn (x, c) =>
141 box [p_con env x, 152 box [p_con env x,
142 space, 153 space,
156 p_list (p_con env) cs, 167 p_list (p_con env) cs,
157 string ")"] 168 string ")"]
158 | CProj (c, n) => box [p_con env c, 169 | CProj (c, n) => box [p_con env c,
159 string ".", 170 string ".",
160 string (Int.toString n)] 171 string (Int.toString n)]
172
173 | CKAbs (x, c) => box [string x,
174 space,
175 string "==>",
176 space,
177 p_con (E.pushKRel env x) c]
178 | CKApp (c, k) => box [p_con env c,
179 string "[[",
180 p_kind env k,
181 string "]]"]
182 | TKFun (x, c) => box [string x,
183 space,
184 string "-->",
185 space,
186 p_con (E.pushKRel env x) c]
161 187
162 and p_con env = p_con' false env 188 and p_con env = p_con' false env
163 189
164 and p_name env (all as (c, _)) = 190 and p_name env (all as (c, _)) =
165 case c of 191 case c of
259 space, 285 space,
260 string x, 286 string x,
261 space, 287 space,
262 string "::", 288 string "::",
263 space, 289 space,
264 p_kind k, 290 p_kind env k,
265 space, 291 space,
266 string "=>", 292 string "=>",
267 space, 293 space,
268 p_exp (E.pushCRel env x k) e]) 294 p_exp (E.pushCRel env x k) e])
269 295
395 space, 421 space,
396 string "in", 422 string "in",
397 newline, 423 newline,
398 p_exp (E.pushERel env x t) e2] 424 p_exp (E.pushERel env x t) e2]
399 425
426 | EKAbs (x, e) => box [string x,
427 space,
428 string "==>",
429 space,
430 p_exp (E.pushKRel env x) e]
431 | EKApp (e, k) => box [p_exp env e,
432 string "[[",
433 p_kind env k,
434 string "]]"]
400 435
401 436
402 and p_exp env = p_exp' false env 437 and p_exp env = p_exp' false env
403 438
404 fun p_named x n = 439 fun p_named x n =
436 space, 471 space,
437 p_named x n, 472 p_named x n,
438 space, 473 space,
439 string "::", 474 string "::",
440 space, 475 space,
441 p_kind k] 476 p_kind env k]
442 | SgiCon (x, n, k, c) => box [string "con", 477 | SgiCon (x, n, k, c) => box [string "con",
443 space, 478 space,
444 p_named x n, 479 p_named x n,
445 space, 480 space,
446 string "::", 481 string "::",
447 space, 482 space,
448 p_kind k, 483 p_kind env k,
449 space, 484 space,
450 string "=", 485 string "=",
451 space, 486 space,
452 p_con env c] 487 p_con env c]
453 | SgiDatatype x => p_datatype env x 488 | SgiDatatype x => p_datatype env x
557 space, 592 space,
558 p_named x n, 593 p_named x n,
559 space, 594 space,
560 string "::", 595 string "::",
561 space, 596 space,
562 p_kind k, 597 p_kind env k,
563 space, 598 space,
564 string "=", 599 string "=",
565 space, 600 space,
566 p_con env c] 601 p_con env c]
567 | DDatatype x => p_datatype env x 602 | DDatatype x => p_datatype env x