Mercurial > urweb

comparison src/elab_print.sml @ 623:588b9d16b00a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 16:10:25 -0500
parents 8998114760c1
children 354800878b4d
comparison
equal deleted inserted replaced
622:d64533157f40 623:588b9d16b00a
36 36
37 structure E = ElabEnv 37 structure E = ElabEnv
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 | KError => string "<ERROR>" 56 | KError => string "<ERROR>"
57 | KUnif (_, _, ref (SOME k)) => p_kind' par k 57 | KUnif (_, _, ref (SOME k)) => p_kind' par env k
58 | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">") 58 | KUnif (_, s, _) => string ("<UNIF:" ^ s ^ ">")
59
60 | KRel n => ((if !debug then
61 string (E.lookupKRel env n ^ "_" ^ Int.toString n)
62 else
63 string (E.lookupKRel env n))
64 handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n))
65 | KFun (x, k) => box [string x,
66 space,
67 string "-->",
68 space,
69 p_kind (E.pushKRel env x) k]
59 70
60 and p_kind k = p_kind' false k 71 and p_kind k = p_kind' false k
61 72
62 fun p_explicitness e = 73 fun p_explicitness e =
63 case e of 74 case e of
64 Explicit => string "::" 75 Explicit => string "::"
65 | Implicit => string ":::" 76 | Implicit => string ":::"
66 77
67 fun p_con' par env (c, _) = 78 fun p_con' par env (c, _) =
68 case c of 79 case c of
69 TFun (t1, t2) => parenIf par (box [p_con' true env t1, 80 TFun (t1, t2) => parenIf true (box [p_con' true env t1,
70 space, 81 space,
71 string "->", 82 string "->",
72 space, 83 space,
73 p_con env t2]) 84 p_con env t2])
74 | TCFun (e, x, k, c) => parenIf par (box [string x, 85 | TCFun (e, x, k, c) => parenIf par (box [string x,
75 space, 86 space,
76 p_explicitness e, 87 p_explicitness e,
77 space, 88 space,
78 p_kind k, 89 p_kind env k,
79 space, 90 space,
80 string "->", 91 string "->",
81 space, 92 space,
82 p_con (E.pushCRel env x k) c]) 93 p_con (E.pushCRel env x k) c])
83 | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1, 94 | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1,
84 space, 95 space,
85 string "~", 96 string (case ai of
86 space, 97 Instantiate => "~"
87 p_con env c2, 98 | LeaveAlone => "~~"),
88 space, 99 space,
89 string "=>", 100 p_con env c2,
90 space, 101 space,
91 p_con env c3]) 102 string "=>",
103 space,
104 p_con env c3])
92 | TRecord (CRecord (_, xcs), _) => box [string "{", 105 | TRecord (CRecord (_, xcs), _) => box [string "{",
93 p_list (fn (x, c) => 106 p_list (fn (x, c) =>
94 box [p_name env x, 107 box [p_name env x,
95 space, 108 space,
96 string ":", 109 string ":",
132 space, 145 space,
133 string x, 146 string x,
134 space, 147 space,
135 string "::", 148 string "::",
136 space, 149 space,
137 p_kind k, 150 p_kind env k,
138 space, 151 space,
139 string "=>", 152 string "=>",
140 space, 153 space,
141 p_con (E.pushCRel env x k) c]) 154 p_con (E.pushCRel env x k) c])
142 155
150 space, 163 space,
151 string "=", 164 string "=",
152 space, 165 space,
153 p_con env c]) xcs, 166 p_con env c]) xcs,
154 string "]::", 167 string "]::",
155 p_kind k]) 168 p_kind env k])
156 else 169 else
157 parenIf par (box [string "[", 170 parenIf par (box [string "[",
158 p_list (fn (x, c) => 171 p_list (fn (x, c) =>
159 box [p_con env x, 172 box [p_con env x,
160 space, 173 space,
179 string (Int.toString n)] 192 string (Int.toString n)]
180 193
181 | CError => string "<ERROR>" 194 | CError => string "<ERROR>"
182 | CUnif (_, _, _, ref (SOME c)) => p_con' par env c 195 | CUnif (_, _, _, ref (SOME c)) => p_con' par env c
183 | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"), 196 | CUnif (_, k, s, _) => box [string ("<UNIF:" ^ s ^ "::"),
184 p_kind k, 197 p_kind env k,
185 string ">"] 198 string ">"]
199
200 | CKAbs (x, c) => box [string x,
201 space,
202 string "==>",
203 space,
204 p_con (E.pushKRel env x) c]
205 | CKApp (c, k) => box [p_con env c,
206 string "[[",
207 p_kind env k,
208 string "]]"]
209 | TKFun (x, c) => box [string x,
210 space,
211 string "-->",
212 space,
213 p_con (E.pushKRel env x) c]
214
186 215
187 and p_con env = p_con' false env 216 and p_con env = p_con' false env
188 217
189 and p_name env (all as (c, _)) = 218 and p_name env (all as (c, _)) =
190 case c of 219 case c of
284 space, 313 space,
285 string x, 314 string x,
286 space, 315 space,
287 p_explicitness exp, 316 p_explicitness exp,
288 space, 317 space,
289 p_kind k, 318 p_kind env k,
290 space, 319 space,
291 string "=>", 320 string "=>",
292 space, 321 space,
293 p_exp (E.pushCRel env x k) e]) 322 p_exp (E.pushCRel env x k) e])
294 323
374 box [p_exp' true env e, 403 box [p_exp' true env e,
375 space, 404 space,
376 string "---", 405 string "---",
377 space, 406 space,
378 p_con' true env c]) 407 p_con' true env c])
379
380 | EFold _ => string "fold"
381 408
382 | ECase (e, pes, _) => parenIf par (box [string "case", 409 | ECase (e, pes, _) => parenIf par (box [string "case",
383 space, 410 space,
384 p_exp env e, 411 p_exp env e,
385 space, 412 space,
412 newline, 439 newline,
413 box [p_exp env e], 440 box [p_exp env e],
414 newline, 441 newline,
415 string "end"] 442 string "end"]
416 end 443 end
444
445 | EKAbs (x, e) => box [string x,
446 space,
447 string "==>",
448 space,
449 p_exp (E.pushKRel env x) e]
450 | EKApp (e, k) => box [p_exp env e,
451 string "[[",
452 p_kind env k,
453 string "]]"]
417 454
418 and p_exp env = p_exp' false env 455 and p_exp env = p_exp' false env
419 456
420 and p_edecl env (dAll as (d, _)) = 457 and p_edecl env (dAll as (d, _)) =
421 case d of 458 case d of
476 space, 513 space,
477 p_named x n, 514 p_named x n,
478 space, 515 space,
479 string "::", 516 string "::",
480 space, 517 space,
481 p_kind k] 518 p_kind env k]
482 | SgiCon (x, n, k, c) => box [string "con", 519 | SgiCon (x, n, k, c) => box [string "con",
483 space, 520 space,
484 p_named x n, 521 p_named x n,
485 space, 522 space,
486 string "::", 523 string "::",
487 space, 524 space,
488 p_kind k, 525 p_kind env k,
489 space, 526 space,
490 string "=", 527 string "=",
491 space, 528 space,
492 p_con env c] 529 p_con env c]
493 | SgiDatatype x => p_datatype env x 530 | SgiDatatype x => p_datatype env x
538 space, 575 space,
539 p_named x n, 576 p_named x n,
540 space, 577 space,
541 string "::", 578 string "::",
542 space, 579 space,
543 p_kind k] 580 p_kind env k]
544 | SgiClass (x, n, k, c) => box [string "class", 581 | SgiClass (x, n, k, c) => box [string "class",
545 space, 582 space,
546 p_named x n, 583 p_named x n,
547 space, 584 space,
548 string "::", 585 string "::",
549 space, 586 space,
550 p_kind k, 587 p_kind env k,
551 space, 588 space,
552 string "=", 589 string "=",
553 space, 590 space,
554 p_con env c] 591 p_con env c]
555 592
625 space, 662 space,
626 p_named x n, 663 p_named x n,
627 space, 664 space,
628 string "::", 665 string "::",
629 space, 666 space,
630 p_kind k, 667 p_kind env k,
631 space, 668 space,
632 string "=", 669 string "=",
633 space, 670 space,
634 p_con env c] 671 p_con env c]
635 | DDatatype x => p_datatype env x 672 | DDatatype x => p_datatype env x
717 space, 754 space,
718 p_named x n, 755 p_named x n,
719 space, 756 space,
720 string "::", 757 string "::",
721 space, 758 space,
722 p_kind k, 759 p_kind env k,
723 space, 760 space,
724 string "=", 761 string "=",
725 space, 762 space,
726 p_con env c] 763 p_con env c]
727 | DDatabase s => box [string "database", 764 | DDatabase s => box [string "database",