Mercurial > urweb

comparison src/reduce.sml @ 626:230654093b51

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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