comparison src/core_print.sml @ 626:230654093b51

demo/hello compiles with kind polymorphism
author Adam Chlipala <adamc@hcoop.net>
date Sun, 22 Feb 2009 17:17:01 -0500
parents 588b9d16b00a
children 70cbdcf5989b
comparison
equal deleted inserted replaced
625:47947d6e9750 626:230654093b51
36 36
37 structure E = CoreEnv 37 structure E = CoreEnv
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 "{",
103 space, 114 space,
104 string x, 115 string x,
105 space, 116 space,
106 string "::", 117 string "::",
107 space, 118 space,
108 p_kind k, 119 p_kind env k,
109 space, 120 space,
110 string "=>", 121 string "=>",
111 space, 122 space,
112 p_con (E.pushCRel env x k) c]) 123 p_con (E.pushCRel env x k) c])
113 124
121 space, 132 space,
122 string "=", 133 string "=",
123 space, 134 space,
124 p_con env c]) xcs, 135 p_con env c]) xcs,
125 string "]::", 136 string "]::",
126 p_kind k]) 137 p_kind env k])
127 else 138 else
128 parenIf par (box [string "[", 139 parenIf par (box [string "[",
129 p_list (fn (x, c) => 140 p_list (fn (x, c) =>
130 box [p_con env x, 141 box [p_con env x,
131 space, 142 space,
145 p_list (p_con env) cs, 156 p_list (p_con env) cs,
146 string ")"] 157 string ")"]
147 | CProj (c, n) => box [p_con env c, 158 | CProj (c, n) => box [p_con env c,
148 string ".", 159 string ".",
149 string (Int.toString n)] 160 string (Int.toString n)]
161
162 | CKAbs (x, c) => box [string x,
163 space,
164 string "==>",
165 space,
166 p_con (E.pushKRel env x) c]
167 | CKApp (c, k) => box [p_con env c,
168 string "[[",
169 p_kind env k,
170 string "]]"]
171 | TKFun (x, c) => box [string x,
172 space,
173 string "-->",
174 space,
175 p_con (E.pushKRel env x) c]
150 176
151 and p_con env = p_con' false env 177 and p_con env = p_con' false env
152 178
153 and p_name env (all as (c, _)) = 179 and p_name env (all as (c, _)) =
154 case c of 180 case c of
250 space, 276 space,
251 string x, 277 string x,
252 space, 278 space,
253 string "::", 279 string "::",
254 space, 280 space,
255 p_kind k, 281 p_kind env k,
256 space, 282 space,
257 string "=>", 283 string "=>",
258 space, 284 space,
259 p_exp (E.pushCRel env x k) e]) 285 p_exp (E.pushCRel env x k) e])
260 286
400 p_list (p_exp env) es, 426 p_list (p_exp env) es,
401 string ")[", 427 string ")[",
402 p_exp env e, 428 p_exp env e,
403 string "]"] 429 string "]"]
404 430
431 | EKAbs (x, e) => box [string x,
432 space,
433 string "==>",
434 space,
435 p_exp (E.pushKRel env x) e]
436 | EKApp (e, k) => box [p_exp env e,
437 string "[[",
438 p_kind env k,
439 string "]]"]
440
405 and p_exp env = p_exp' false env 441 and p_exp env = p_exp' false env
406 442
407 fun p_named x n = 443 fun p_named x n =
408 if !debug then 444 if !debug then
409 box [string x, 445 box [string x,
478 space, 514 space,
479 xp, 515 xp,
480 space, 516 space,
481 string "::", 517 string "::",
482 space, 518 space,
483 p_kind k, 519 p_kind env k,
484 space, 520 space,
485 string "=", 521 string "=",
486 space, 522 space,
487 p_con env c] 523 p_con env c]
488 end 524 end