Mercurial > urweb

comparison src/reduce_local.sml @ 1272:56bd4a4f6e66

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize
author Adam Chlipala <adamc@hcoop.net>
date Thu, 03 Jun 2010 13:04:37 -0400
parents c316ca3c9ec6
children 5b5c0b552f59
comparison
equal deleted inserted replaced
1271:503d4ec93494 1272:56bd4a4f6e66
1 (* Copyright (c) 2008, Adam Chlipala 1 (* Copyright (c) 2008-2010, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
41 41
42 datatype env_item = 42 datatype env_item =
43 Unknown 43 Unknown
44 | Known of exp 44 | Known of exp
45 45
46 | Lift of int 46 | UnknownC
47 | KnownC of con
48
49 | Lift of int * int
47 50
48 type env = env_item list 51 type env = env_item list
49 52
50 val deKnown = List.filter (fn Known _ => false 53 val deKnown = List.filter (fn Known _ => false
54 | KnownC _ => false
51 | _ => true) 55 | _ => true)
52 56
53 datatype result = Yes of env | No | Maybe 57 datatype result = Yes of env | No | Maybe
54 58
55 fun match (env, p : pat, e : exp) = 59 fun match (env, p : pat, e : exp) =
118 | _ => Maybe 122 | _ => Maybe
119 in 123 in
120 match (env, p, e) 124 match (env, p, e)
121 end 125 end
122 126
127 fun con env (all as (c, loc)) =
128 ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*)
129 case c of
130 TFun (c1, c2) => (TFun (con env c1, con env c2), loc)
131 | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc)
132 | TKFun (x, c2) => (TKFun (x, con env c2), loc)
133 | TRecord c => (TRecord (con env c), loc)
134
135 | CRel n =>
136 let
137 fun find (n', env, nudge, liftC) =
138 case env of
139 [] => raise Fail "Reduce.con: CRel"
140 | Unknown :: rest => find (n', rest, nudge, liftC)
141 | Known _ :: rest => find (n', rest, nudge, liftC)
142 | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC',
143 liftC + liftC')
144 | UnknownC :: rest =>
145 if n' = 0 then
146 (CRel (n + nudge), loc)
147 else
148 find (n' - 1, rest, nudge, liftC + 1)
149 | KnownC c :: rest =>
150 if n' = 0 then
151 con (Lift (liftC, 0) :: rest) c
152 else
153 find (n' - 1, rest, nudge - 1, liftC)
154 in
155 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
156 find (n, env, 0, 0)
157 end
158 | CNamed _ => all
159 | CFfi _ => all
160 | CApp (c1, c2) =>
161 let
162 val c1 = con env c1
163 val c2 = con env c2
164 in
165 case #1 c1 of
166 CAbs (_, _, b) =>
167 con (KnownC c2 :: deKnown env) b
168
169 | CApp ((CMap (dom, ran), _), f) =>
170 (case #1 c2 of
171 CRecord (_, []) => (CRecord (ran, []), loc)
172 | CRecord (_, (x, c) :: rest) =>
173 con (deKnown env)
174 (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc),
175 (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc)
176 | _ => (CApp (c1, c2), loc))
177
178 | _ => (CApp (c1, c2), loc)
179 end
180 | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc)
181
182 | CKApp (c1, k) =>
183 let
184 val c1 = con env c1
185 in
186 case #1 c1 of
187 CKAbs (_, b) =>
188 con (deKnown env) b
189
190 | _ => (CKApp (c1, k), loc)
191 end
192 | CKAbs (x, b) => (CKAbs (x, con env b), loc)
193
194 | CName _ => all
195
196 | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc)
197 | CConcat (c1, c2) =>
198 let
199 val c1 = con env c1
200 val c2 = con env c2
201 in
202 case (#1 c1, #1 c2) of
203 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
204 (CRecord (k, xcs1 @ xcs2), loc)
205 | (CRecord (_, []), _) => c2
206 | (_, CRecord (_, [])) => c1
207 | _ => (CConcat (c1, c2), loc)
208 end
209 | CMap _ => all
210
211 | CUnit => all
212
213 | CTuple cs => (CTuple (map (con env) cs), loc)
214 | CProj (c, n) =>
215 let
216 val c = con env c
217 in
218 case #1 c of
219 CTuple cs => List.nth (cs, n - 1)
220 | _ => (CProj (c, n), loc)
221 end)
222
223 fun patCon pc =
224 case pc of
225 PConVar _ => pc
226 | PConFfi {mod = m, datatyp, params, con = c, arg, kind} =>
227 PConFfi {mod = m, datatyp = datatyp, params = params, con = c,
228 arg = Option.map (con (map (fn _ => UnknownC) params)) arg,
229 kind = kind}
230
123 fun exp env (all as (e, loc)) = 231 fun exp env (all as (e, loc)) =
124 case e of 232 case e of
125 EPrim _ => all 233 EPrim _ => all
126 | ERel n => 234 | ERel n =>
127 let 235 let
128 fun find (n', env, nudge, lift) = 236 fun find (n', env, nudge, liftC, liftE) =
129 case env of 237 case env of
130 [] => (ERel (n + nudge), loc) 238 [] => (ERel (n + nudge), loc)
131 | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift') 239 | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE')
240 | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE)
241 | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE)
132 | Unknown :: rest => 242 | Unknown :: rest =>
133 if n' = 0 then 243 if n' = 0 then
134 (ERel (n + nudge), loc) 244 (ERel (n + nudge), loc)
135 else 245 else
136 find (n' - 1, rest, nudge, lift + 1) 246 find (n' - 1, rest, nudge, liftC, liftE + 1)
137 | Known e :: rest => 247 | Known e :: rest =>
138 if n' = 0 then 248 if n' = 0 then
139 ((*print "SUBSTITUTING\n";*) 249 ((*print "SUBSTITUTING\n";*)
140 exp (Lift lift :: rest) e) 250 exp (Lift (liftC, liftE) :: rest) e)
141 else 251 else
142 find (n' - 1, rest, nudge - 1, lift) 252 find (n' - 1, rest, nudge - 1, liftC, liftE)
143 in 253 in
144 find (n, env, 0, 0) 254 find (n, env, 0, 0, 0)
145 end 255 end
146 | ENamed _ => all 256 | ENamed _ => all
147 | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc) 257 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) cs, Option.map (exp env) eo), loc)
148 | EFfi _ => all 258 | EFfi _ => all
149 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) 259 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
150
151 | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _,
152 (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _),
153 t), _), e) =>
154 (ECon (dk, pc, [t], SOME (exp env e)), loc)
155 260
156 | EApp (e1, e2) => 261 | EApp (e1, e2) =>
157 let 262 let
158 val e1 = exp env e1 263 val e1 = exp env e1
159 val e2 = exp env e2 264 val e2 = exp env e2
161 case #1 e1 of 266 case #1 e1 of
162 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b 267 EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b
163 | _ => (EApp (e1, e2), loc) 268 | _ => (EApp (e1, e2), loc)
164 end 269 end
165 270
166 | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) 271 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc)
167 272
168 | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) => 273 | ECApp (e, c) =>
169 (ECon (dk, pc, [t], NONE), loc) 274 let
170 275 val e = exp env e
171 | ECApp (e, c) => (ECApp (exp env e, c), loc) 276 val c = con env c
172 | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) 277 in
278 case #1 e of
279 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
280 | _ => (ECApp (e, c), loc)
281 end
282
283 | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc)
173 284
174 | EKApp (e, k) => (EKApp (exp env e, k), loc) 285 | EKApp (e, k) => (EKApp (exp env e, k), loc)
175 | EKAbs (x, e) => (EKAbs (x, exp env e), loc) 286 | EKAbs (x, e) => (EKAbs (x, exp env e), loc)
176 287
177 | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc) 288 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
178 | EField (e, c, others) => 289 | EField (e, c, others) =>
179 let 290 let
180 val e = exp env e 291 val e = exp env e
292 val c = con env c
181 293
182 fun default () = (EField (e, c, others), loc) 294 fun default () = (EField (e, c, others), loc)
183 in 295 in
184 case (#1 e, #1 c) of 296 case (#1 e, #1 c) of
185 (ERecord xcs, CName x) => 297 (ERecord xcs, CName x) =>
187 NONE => default () 299 NONE => default ()
188 | SOME (_, e, _) => e) 300 | SOME (_, e, _) => e)
189 | _ => default () 301 | _ => default ()
190 end 302 end
191 303
192 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc) 304 | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc)
193 | ECut (e, c, others) => (ECut (exp env e, c, others), loc) 305 | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e,
194 | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) 306 con env c,
195 307 {field = con env f, rest = con env r}), loc)
196 | ECase (e, pes, others) => 308 | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc)
197 let 309
310 | ECase (e, pes, {disc = d, result = r}) =>
311 let
312 val others = {disc = con env d, result = con env r}
313
198 fun patBinds (p, _) = 314 fun patBinds (p, _) =
199 case p of 315 case p of
200 PWild => 0 316 PWild => 0
201 | PVar _ => 1 317 | PVar _ => 1
202 | PPrim _ => 0 318 | PPrim _ => 0
203 | PCon (_, _, _, NONE) => 0 319 | PCon (_, _, _, NONE) => 0
204 | PCon (_, _, _, SOME p) => patBinds p 320 | PCon (_, _, _, SOME p) => patBinds p
205 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts 321 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
206 322
323 fun pat (all as (p, loc)) =
324 case p of
325 PWild => all
326 | PVar (x, t) => (PVar (x, con env t), loc)
327 | PPrim _ => all
328 | PCon (dk, pc, cs, po) =>
329 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
330 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
331
207 fun push () = 332 fun push () =
208 (ECase (exp env e, 333 (ECase (exp env e,
209 map (fn (p, e) => (p, 334 map (fn (p, e) => (pat p,
210 exp (List.tabulate (patBinds p, 335 exp (List.tabulate (patBinds p,
211 fn _ => Unknown) @ env) e)) 336 fn _ => Unknown) @ env) e))
212 pes, others), loc) 337 pes, others), loc)
213 338
214 fun search pes = 339 fun search pes =
224 end 349 end
225 350
226 | EWrite e => (EWrite (exp env e), loc) 351 | EWrite e => (EWrite (exp env e), loc)
227 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) 352 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
228 353
229 | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) 354 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc)
230 355
231 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc) 356 | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc)
232 357
233 fun reduce file = 358 fun reduce file =
234 let 359 let
235 fun doDecl (d as (_, loc)) = 360 fun doDecl (d as (_, loc)) =
236 case #1 d of 361 case #1 d of