Mercurial > urweb
comparison src/reduce.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 |
---|---|
32 open Core | 32 open Core |
33 | 33 |
34 structure IM = IntBinaryMap | 34 structure IM = IntBinaryMap |
35 | 35 |
36 datatype env_item = | 36 datatype env_item = |
37 UnknownC | 37 UnknownK |
38 | KnownK of kind | |
39 | |
40 | UnknownC | |
38 | KnownC of con | 41 | KnownC of con |
39 | 42 |
40 | UnknownE | 43 | UnknownE |
41 | KnownE of exp | 44 | KnownE of exp |
42 | 45 |
43 | Lift of int * int | 46 | Lift of int * int * int |
44 | 47 |
45 type env = env_item list | 48 type env = env_item list |
46 | 49 |
47 fun ei2s ei = | 50 fun ei2s ei = |
48 case ei of | 51 case ei of |
49 UnknownC => "UC" | 52 UnknownK => "UK" |
53 | KnownK _ => "KK" | |
54 | UnknownC => "UC" | |
50 | KnownC _ => "KC" | 55 | KnownC _ => "KC" |
51 | UnknownE => "UE" | 56 | UnknownE => "UE" |
52 | KnownE _ => "KE" | 57 | KnownE _ => "KE" |
53 | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" | 58 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" |
54 | 59 |
55 fun e2s env = String.concatWith " " (map ei2s env) | 60 fun e2s env = String.concatWith " " (map ei2s env) |
56 | 61 |
57 val deKnown = List.filter (fn KnownC _ => false | 62 val deKnown = List.filter (fn KnownC _ => false |
58 | KnownE _ => false | 63 | KnownE _ => false |
64 | KnownK _ => false | |
59 | _ => true) | 65 | _ => true) |
60 | 66 |
61 fun conAndExp (namedC, namedE) = | 67 fun kindConAndExp (namedC, namedE) = |
62 let | 68 let |
69 fun kind env (all as (k, loc)) = | |
70 case k of | |
71 KType => all | |
72 | KArrow (k1, k2) => (KArrow (kind env k1, kind env k2), loc) | |
73 | KName => all | |
74 | KRecord k => (KRecord (kind env k), loc) | |
75 | KUnit => all | |
76 | KTuple ks => (KTuple (map (kind env) ks), loc) | |
77 | |
78 | KRel n => | |
79 let | |
80 fun find (n', env, nudge, lift) = | |
81 case env of | |
82 [] => raise Fail "Reduce.kind: KRel" | |
83 | UnknownC :: rest => find (n', rest, nudge, lift) | |
84 | KnownC _ :: rest => find (n', rest, nudge, lift) | |
85 | UnknownE :: rest => find (n', rest, nudge, lift) | |
86 | KnownE _ :: rest => find (n', rest, nudge, lift) | |
87 | Lift (lift', _, _) :: rest => find (n', rest, nudge + lift', lift + lift') | |
88 | UnknownK :: rest => | |
89 if n' = 0 then | |
90 (KRel (n + nudge), loc) | |
91 else | |
92 find (n' - 1, rest, nudge, lift + 1) | |
93 | KnownK k :: rest => | |
94 if n' = 0 then | |
95 kind (Lift (lift, 0, 0) :: rest) k | |
96 else | |
97 find (n' - 1, rest, nudge - 1, lift) | |
98 in | |
99 find (n, env, 0, 0) | |
100 end | |
101 | KFun (x, k) => (KFun (x, kind (UnknownK :: env) k), loc) | |
102 | |
63 fun con env (all as (c, loc)) = | 103 fun con env (all as (c, loc)) = |
64 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) | 104 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) |
65 case c of | 105 case c of |
66 TFun (c1, c2) => (TFun (con env c1, con env c2), loc) | 106 TFun (c1, c2) => (TFun (con env c1, con env c2), loc) |
67 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) | 107 | TCFun (x, k, c2) => (TCFun (x, kind env k, con (UnknownC :: env) c2), loc) |
108 | TKFun (x, c2) => (TKFun (x, con (UnknownK :: env) c2), loc) | |
68 | TRecord c => (TRecord (con env c), loc) | 109 | TRecord c => (TRecord (con env c), loc) |
69 | 110 |
70 | CRel n => | 111 | CRel n => |
71 let | 112 let |
72 fun find (n', env, nudge, lift) = | 113 fun find (n', env, nudge, liftK, liftC) = |
73 case env of | 114 case env of |
74 [] => raise Fail "Reduce.con: CRel" | 115 [] => raise Fail "Reduce.con: CRel" |
75 | UnknownE :: rest => find (n', rest, nudge, lift) | 116 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC) |
76 | KnownE _ :: rest => find (n', rest, nudge, lift) | 117 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC) |
77 | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift') | 118 | UnknownE :: rest => find (n', rest, nudge, liftK, liftC) |
119 | KnownE _ :: rest => find (n', rest, nudge, liftK, liftC) | |
120 | Lift (liftK', liftC', _) :: rest => find (n', rest, nudge + liftC', | |
121 liftK + liftK', liftC + liftC') | |
78 | UnknownC :: rest => | 122 | UnknownC :: rest => |
79 if n' = 0 then | 123 if n' = 0 then |
80 (CRel (n + nudge), loc) | 124 (CRel (n + nudge), loc) |
81 else | 125 else |
82 find (n' - 1, rest, nudge, lift + 1) | 126 find (n' - 1, rest, nudge, liftK, liftC + 1) |
83 | KnownC c :: rest => | 127 | KnownC c :: rest => |
84 if n' = 0 then | 128 if n' = 0 then |
85 con (Lift (lift, 0) :: rest) c | 129 con (Lift (liftK, liftC, 0) :: rest) c |
86 else | 130 else |
87 find (n' - 1, rest, nudge - 1, lift) | 131 find (n' - 1, rest, nudge - 1, liftK, liftC) |
88 in | 132 in |
89 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) | 133 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) |
90 find (n, env, 0, 0) | 134 find (n, env, 0, 0, 0) |
91 end | 135 end |
92 | CNamed n => | 136 | CNamed n => |
93 (case IM.find (namedC, n) of | 137 (case IM.find (namedC, n) of |
94 NONE => all | 138 NONE => all |
95 | SOME c => c) | 139 | SOME c => c) |
103 CAbs (_, _, b) => | 147 CAbs (_, _, b) => |
104 con (KnownC c2 :: deKnown env) b | 148 con (KnownC c2 :: deKnown env) b |
105 | 149 |
106 | CApp ((CMap (dom, ran), _), f) => | 150 | CApp ((CMap (dom, ran), _), f) => |
107 (case #1 c2 of | 151 (case #1 c2 of |
108 CRecord (_, []) => (CRecord (ran, []), loc) | 152 CRecord (_, []) => (CRecord (kind env ran, []), loc) |
109 | CRecord (_, (x, c) :: rest) => | 153 | CRecord (_, (x, c) :: rest) => |
110 con (deKnown env) | 154 con (deKnown env) |
111 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), | 155 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), |
112 (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc) | 156 (CApp (c1, (CRecord (kind env dom, rest), loc)), loc)), loc) |
113 | _ => (CApp (c1, c2), loc)) | 157 | _ => (CApp (c1, c2), loc)) |
114 | 158 |
115 | _ => (CApp (c1, c2), loc) | 159 | _ => (CApp (c1, c2), loc) |
116 end | 160 end |
117 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) | 161 | CAbs (x, k, b) => (CAbs (x, kind env k, con (UnknownC :: env) b), loc) |
162 | |
163 | CKApp (c1, k) => | |
164 let | |
165 val c1 = con env c1 | |
166 in | |
167 case #1 c1 of | |
168 CKAbs (_, b) => | |
169 con (KnownK k :: deKnown env) b | |
170 | |
171 | _ => (CKApp (c1, kind env k), loc) | |
172 end | |
173 | CKAbs (x, b) => (CKAbs (x, con (UnknownK :: env) b), loc) | |
118 | 174 |
119 | CName _ => all | 175 | CName _ => all |
120 | 176 |
121 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) | 177 | CRecord (k, xcs) => (CRecord (kind env k, map (fn (x, c) => (con env x, con env c)) xcs), loc) |
122 | CConcat (c1, c2) => | 178 | CConcat (c1, c2) => |
123 let | 179 let |
124 val c1 = con env c1 | 180 val c1 = con env c1 |
125 val c2 = con env c2 | 181 val c2 = con env c2 |
126 in | 182 in |
127 case (#1 c1, #1 c2) of | 183 case (#1 c1, #1 c2) of |
128 (CRecord (k, xcs1), CRecord (_, xcs2)) => | 184 (CRecord (k, xcs1), CRecord (_, xcs2)) => |
129 (CRecord (k, xcs1 @ xcs2), loc) | 185 (CRecord (kind env k, xcs1 @ xcs2), loc) |
130 | _ => (CConcat (c1, c2), loc) | 186 | _ => (CConcat (c1, c2), loc) |
131 end | 187 end |
132 | CMap _ => all | 188 | CMap (dom, ran) => (CMap (kind env dom, kind env ran), loc) |
133 | 189 |
134 | CUnit => all | 190 | CUnit => all |
135 | 191 |
136 | CTuple cs => (CTuple (map (con env) cs), loc) | 192 | CTuple cs => (CTuple (map (con env) cs), loc) |
137 | CProj (c, n) => | 193 | CProj (c, n) => |
162 ("env", Print.PD.string (e2s env))];*) | 218 ("env", Print.PD.string (e2s env))];*) |
163 case e of | 219 case e of |
164 EPrim _ => all | 220 EPrim _ => all |
165 | ERel n => | 221 | ERel n => |
166 let | 222 let |
167 fun find (n', env, nudge, liftC, liftE) = | 223 fun find (n', env, nudge, liftK, liftC, liftE) = |
168 case env of | 224 case env of |
169 [] => raise Fail "Reduce.exp: ERel" | 225 [] => raise Fail "Reduce.exp: ERel" |
170 | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) | 226 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE) |
171 | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) | 227 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) |
172 | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', | 228 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE) |
173 liftC + liftC', liftE + liftE') | 229 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) |
230 | Lift (liftK', liftC', liftE') :: rest => | |
231 find (n', rest, nudge + liftE', | |
232 liftK + liftK', liftC + liftC', liftE + liftE') | |
174 | UnknownE :: rest => | 233 | UnknownE :: rest => |
175 if n' = 0 then | 234 if n' = 0 then |
176 (ERel (n + nudge), loc) | 235 (ERel (n + nudge), loc) |
177 else | 236 else |
178 find (n' - 1, rest, nudge, liftC, liftE + 1) | 237 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1) |
179 | KnownE e :: rest => | 238 | KnownE e :: rest => |
180 if n' = 0 then | 239 if n' = 0 then |
181 ((*print "SUBSTITUTING\n";*) | 240 ((*print "SUBSTITUTING\n";*) |
182 exp (Lift (liftC, liftE) :: rest) e) | 241 exp (Lift (liftK, liftC, liftE) :: rest) e) |
183 else | 242 else |
184 find (n' - 1, rest, nudge - 1, liftC, liftE) | 243 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE) |
185 in | 244 in |
186 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) | 245 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) |
187 find (n, env, 0, 0, 0) | 246 find (n, env, 0, 0, 0, 0) |
188 end | 247 end |
189 | ENamed n => | 248 | ENamed n => |
190 (case IM.find (namedE, n) of | 249 (case IM.find (namedE, n) of |
191 NONE => all | 250 NONE => all |
192 | SOME e => e) | 251 | SOME e => e) |
215 case #1 e of | 274 case #1 e of |
216 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b | 275 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b |
217 | _ => (ECApp (e, c), loc) | 276 | _ => (ECApp (e, c), loc) |
218 end | 277 end |
219 | 278 |
220 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) | 279 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) |
280 | |
281 | EKApp (e, k) => | |
282 let | |
283 val e = exp env e | |
284 in | |
285 case #1 e of | |
286 EKAbs (_, b) => exp (KnownK k :: deKnown env) b | |
287 | _ => (EKApp (e, kind env k), loc) | |
288 end | |
289 | |
290 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) | |
221 | 291 |
222 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) | 292 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) |
223 | EField (e, c, {field, rest}) => | 293 | EField (e, c, {field, rest}) => |
224 let | 294 let |
225 val e = exp env e | 295 val e = exp env e |
351 | 421 |
352 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) | 422 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) |
353 | 423 |
354 | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc)) | 424 | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc)) |
355 in | 425 in |
356 {con = con, exp = exp} | 426 {kind = kind, con = con, exp = exp} |
357 end | 427 end |
358 | 428 |
359 fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c | 429 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k |
360 fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env e | 430 fun con namedC env c = #con (kindConAndExp (namedC, IM.empty)) env c |
431 fun exp (namedC, namedE) env e = #exp (kindConAndExp (namedC, namedE)) env e | |
361 | 432 |
362 fun reduce file = | 433 fun reduce file = |
363 let | 434 let |
364 fun doDecl (d as (_, loc), st as (namedC, namedE)) = | 435 fun doDecl (d as (_, loc), st as (namedC, namedE)) = |
365 case #1 d of | 436 case #1 d of |
366 DCon (x, n, k, c) => | 437 DCon (x, n, k, c) => |
367 let | 438 let |
439 val k = kind namedC [] k | |
368 val c = con namedC [] c | 440 val c = con namedC [] c |
369 in | 441 in |
370 ((DCon (x, n, k, c), loc), | 442 ((DCon (x, n, k, c), loc), |
371 (IM.insert (namedC, n, c), namedE)) | 443 (IM.insert (namedC, n, c), namedE)) |
372 end | 444 end |