Mercurial > urweb

comparison src/reduce.sml @ 909:1d3f60e74ec7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixed bug in reduce bind-commutation
author Adam Chlipala <adamc@hcoop.net>
date Sat, 22 Aug 2009 16:32:31 -0400
parents ed06e25c70ef
children 8e540df3294d
comparison
equal deleted inserted replaced
908:ed06e25c70ef 909:1d3f60e74ec7
39 if n = 0 then 39 if n = 0 then
40 e 40 e
41 else 41 else
42 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e) 42 multiLiftExpInExp (n - 1) (E.liftExpInExp 0 e)
43 43
44 val dangling =
45 CoreUtil.Exp.existsB {kind = fn _ => false,
46 con = fn _ => false,
47 exp = fn (n, e) =>
48 case e of
49 ERel n' => n' >= n
50 | _ => false,
51 bind = fn (n, b) =>
52 case b of
53 CoreUtil.Exp.RelE _ => n + 1
54 | _ => n}
55
44 datatype env_item = 56 datatype env_item =
45 UnknownK 57 UnknownK
46 | KnownK of kind 58 | KnownK of kind
47 59
48 | UnknownC 60 | UnknownC
50 62
51 | UnknownE 63 | UnknownE
52 | KnownE of exp 64 | KnownE of exp
53 65
54 | Lift of int * int * int 66 | Lift of int * int * int
67
68 val edepth = foldl (fn (UnknownE, n) => n + 1
69 | (KnownE _, n) => n + 1
70 | (_, n) => n) 0
71
72 val edepth' = foldl (fn (UnknownE, n) => n + 1
73 | (KnownE _, n) => n + 1
74 | (Lift (_, _, n'), n) => n + n'
75 | (_, n) => n) 0
55 76
56 type env = env_item list 77 type env = env_item list
57 78
58 fun ei2s ei = 79 fun ei2s ei =
59 case ei of 80 case ei of
65 | KnownE _ => "KE" 86 | KnownE _ => "KE"
66 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" 87 | Lift (_, n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")"
67 88
68 fun e2s env = String.concatWith " " (map ei2s env) 89 fun e2s env = String.concatWith " " (map ei2s env)
69 90
70 val deKnown = List.filter (fn KnownC _ => false 91 (*val deKnown = List.filter (fn KnownC _ => false
71 | KnownE _ => false 92 | KnownE _ => false
72 | KnownK _ => false 93 | KnownK _ => false
73 | _ => true) 94 | _ => true)*)
95
96 val deKnown = ListUtil.mapConcat (fn KnownC _ => []
97 | KnownE _ => []
98 | KnownK _ => []
99 | Lift (nk, nc, ne) => List.tabulate (nk, fn _ => UnknownK)
100 @ List.tabulate (nc, fn _ => UnknownC)
101 @ List.tabulate (ne, fn _ => UnknownE)
102 | x => [x])
74 103
75 fun kindConAndExp (namedC, namedE) = 104 fun kindConAndExp (namedC, namedE) =
76 let 105 let
77 fun kind env (all as (k, loc)) = 106 fun kind env (all as (k, loc)) =
78 case k of 107 case k of
220 fun doPart e (this as (x, t), rest) = 249 fun doPart e (this as (x, t), rest) =
221 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), 250 ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t),
222 this :: rest) 251 this :: rest)
223 252
224 fun exp env (all as (e, loc)) = 253 fun exp env (all as (e, loc)) =
225 ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), 254 let
226 ("env", Print.PD.string (e2s env))];*) 255 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
227 case e of 256 ("env", Print.PD.string (e2s env))]*)
228 EPrim _ => all 257 (*val () = if dangling (edepth env) all then
229 | ERel n => 258 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
230 let 259 ("env", Print.PD.string (e2s env))];
231 fun find (n', env, nudge, liftK, liftC, liftE) = 260 raise Fail "!")
232 case env of 261 else
233 [] => raise Fail "Reduce.exp: ERel" 262 ()*)
234 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE) 263
235 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) 264 val r = case e of
236 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE) 265 EPrim _ => all
237 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE) 266 | ERel n =>
238 | Lift (liftK', liftC', liftE') :: rest => 267 let
239 find (n', rest, nudge + liftE', 268 fun find (n', env, nudge, liftK, liftC, liftE) =
240 liftK + liftK', liftC + liftC', liftE + liftE') 269 case env of
241 | UnknownE :: rest => 270 [] => raise Fail ("Reduce.exp: ERel (" ^ ErrorMsg.spanToString loc ^ ")")
242 if n' = 0 then 271 | UnknownK :: rest => find (n', rest, nudge, liftK + 1, liftC, liftE)
243 (ERel (n + nudge), loc) 272 | KnownK _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
244 else 273 | UnknownC :: rest => find (n', rest, nudge, liftK, liftC + 1, liftE)
245 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1) 274 | KnownC _ :: rest => find (n', rest, nudge, liftK, liftC, liftE)
246 | KnownE e :: rest => 275 | Lift (liftK', liftC', liftE') :: rest =>
247 if n' = 0 then 276 find (n', rest, nudge + liftE',
248 ((*print "SUBSTITUTING\n";*) 277 liftK + liftK', liftC + liftC', liftE + liftE')
249 exp (Lift (liftK, liftC, liftE) :: rest) e) 278 | UnknownE :: rest =>
250 else 279 if n' = 0 then
251 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE) 280 (ERel (n + nudge), loc)
252 in 281 else
253 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) 282 find (n' - 1, rest, nudge, liftK, liftC, liftE + 1)
254 find (n, env, 0, 0, 0, 0) 283 | KnownE e :: rest =>
255 end 284 if n' = 0 then
256 | ENamed n => 285 ((*print "SUBSTITUTING\n";*)
257 (case IM.find (namedE, n) of 286 exp (Lift (liftK, liftC, liftE) :: rest) e)
258 NONE => all 287 else
259 | SOME e => e) 288 find (n' - 1, rest, nudge - 1, liftK, liftC, liftE)
260 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, 289 in
261 map (con env) cs, Option.map (exp env) eo), loc) 290 (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*)
262 | EFfi _ => all 291 find (n, env, 0, 0, 0, 0)
263 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) 292 end
264 293 | ENamed n =>
265 | EApp ( 294 (case IM.find (namedE, n) of
266 (EApp 295 NONE => all
267 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), 296 | SOME e => e)
268 _), _), 297 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
269 (EApp ( 298 map (con env) cs, Option.map (exp env) eo), loc)
270 (EApp ( 299 | EFfi _ => all
271 (ECApp ( 300 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
272 (ECApp ((EFfi ("Basis", "return"), _), _), _), 301
273 _), _), 302 | EApp (
274 _), _), v), _)), _), trans2) => exp env (EApp (trans2, v), loc) 303 (EApp
275 304 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
276 (*| EApp ( 305 _), _),
277 (EApp 306 (EApp (
278 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), 307 (EApp (
279 (EFfi ("Basis", "transaction_monad"), _)), _), 308 (ECApp (
280 (ECase (ed, pes, {disc, ...}), _)), _), 309 (ECApp ((EFfi ("Basis", "return"), _), _), _),
281 trans2) => 310 _), _),
282 let 311 _), _), v), _)), _), trans2) => exp env (EApp (trans2, v), loc)
283 val e' = (EFfi ("Basis", "bind"), loc) 312
284 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) 313 (*| EApp (
285 val e' = (ECApp (e', t1), loc) 314 (EApp
286 val e' = (ECApp (e', t2), loc) 315 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
287 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) 316 (EFfi ("Basis", "transaction_monad"), _)), _),
288 317 (ECase (ed, pes, {disc, ...}), _)), _),
289 val pes = map (fn (p, e) => 318 trans2) =>
290 let 319 let
291 val e' = (EApp (e', e), loc) 320 val e' = (EFfi ("Basis", "bind"), loc)
292 val e' = (EApp (e', 321 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
293 multiLiftExpInExp (E.patBindsN p) 322 val e' = (ECApp (e', t1), loc)
294 trans2), loc) 323 val e' = (ECApp (e', t2), loc)
295 val e' = exp env e' 324 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
296 in 325
297 (p, e') 326 val pes = map (fn (p, e) =>
298 end) pes 327 let
299 in 328 val e' = (EApp (e', e), loc)
300 (ECase (exp env ed, 329 val e' = (EApp (e',
301 pes, 330 multiLiftExpInExp (E.patBindsN p)
302 {disc = con env disc, 331 trans2), loc)
303 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}), 332 val e' = exp env e'
304 loc) 333 in
305 end*) 334 (p, e')
306 335 end) pes
307 | EApp ( 336 in
308 (EApp 337 (ECase (exp env ed,
309 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), 338 pes,
310 (EFfi ("Basis", "transaction_monad"), _)), _), 339 {disc = con env disc,
311 (EServerCall (n, es, ke, dom, ran), _)), _), 340 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
312 trans2) => 341 loc)
313 let 342 end*)
314 val e' = (EFfi ("Basis", "bind"), loc) 343
315 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) 344 | EApp (
316 val e' = (ECApp (e', dom), loc) 345 (EApp
317 val e' = (ECApp (e', t2), loc) 346 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
318 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) 347 (EFfi ("Basis", "transaction_monad"), _)), _),
319 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc) 348 (EServerCall (n, es, ke, dom, ran), _)), _),
320 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc) 349 trans2) =>
321 val e' = (EAbs ("x", dom, t2, e'), loc) 350 let
322 val e' = (EServerCall (n, es, e', dom, t2), loc) 351 val e' = (EFfi ("Basis", "bind"), loc)
323 in 352 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
324 exp env e' 353 val e' = (ECApp (e', dom), loc)
325 end 354 val e' = (ECApp (e', t2), loc)
326 355 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
327 | EApp ( 356 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
328 (EApp 357 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
329 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), _), _), t3), _), 358 val e' = (EAbs ("x", dom, t2, e'), loc)
330 (EFfi ("Basis", "transaction_monad"), _)), _), 359 val e' = (EServerCall (n, es, e', dom, t2), loc)
331 (EApp ((EApp 360 in
332 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _), 361 exp env e'
333 (EFfi ("Basis", "transaction_monad"), _)), _), 362 end
334 trans1), _), trans2), _)), _), 363
335 trans3) => 364 | EApp (
336 let 365 (EApp
337 val e'' = (EFfi ("Basis", "bind"), loc) 366 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt), _), _), _), t3), _),
338 val e'' = (ECApp (e'', (CFfi ("Basis", "transaction"), loc)), loc) 367 me), _),
339 val e'' = (ECApp (e'', t2), loc) 368 (EApp ((EApp
340 val e'' = (ECApp (e'', t3), loc) 369 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
341 val e'' = (EApp (e'', (EFfi ("Basis", "transaction_monad"), loc)), loc) 370 _), _),
342 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc) 371 trans1), _), trans2), _)), _),
343 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc) 372 trans3) =>
344 val e'' = (EAbs ("x", t1, (CApp ((CFfi ("Basis", "transaction"), loc), t3), loc), e''), loc) 373 let
345 374 val e'' = (EFfi ("Basis", "bind"), loc)
346 val e' = (EFfi ("Basis", "bind"), loc) 375 val e'' = (ECApp (e'', mt), loc)
347 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc) 376 val e'' = (ECApp (e'', t2), loc)
348 val e' = (ECApp (e', t1), loc) 377 val e'' = (ECApp (e'', t3), loc)
349 val e' = (ECApp (e', t3), loc) 378 val e'' = (EApp (e'', me), loc)
350 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc) 379 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
351 val e' = (EApp (e', trans1), loc) 380 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
352 val e' = (EApp (e', e''), loc) 381 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
353 in 382
354 exp env e' 383 val e' = (EFfi ("Basis", "bind"), loc)
355 end 384 val e' = (ECApp (e', mt), loc)
356 385 val e' = (ECApp (e', t1), loc)
357 | EApp (e1, e2) => 386 val e' = (ECApp (e', t3), loc)
358 let 387 val e' = (EApp (e', me), loc)
359 val e1 = exp env e1 388 val e' = (EApp (e', trans1), loc)
360 val e2 = exp env e2 389 val e' = (EApp (e', e''), loc)
361 in 390 (*val () = print "Before\n"*)
362 case #1 e1 of 391 val ee' = exp env e'
363 EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b 392 (*val () = print "After\n"*)
364 | _ => (EApp (e1, e2), loc) 393 in
365 end 394 (*Print.prefaces "Commute" [("Pre", CorePrint.p_exp CoreEnv.empty (e, loc)),
366 395 ("Mid", CorePrint.p_exp CoreEnv.empty e'),
367 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) 396 ("env", Print.PD.string (e2s env)),
368 397 ("Post", CorePrint.p_exp CoreEnv.empty ee')];*)
369 | ECApp (e, c) => 398 ee'
370 let 399 end
371 val e = exp env e 400
372 val c = con env c 401 | EApp (e1, e2) =>
373 in 402 let
374 case #1 e of 403 val e1 = exp env e1
375 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b 404 val e2 = exp env e2
376 | _ => (ECApp (e, c), loc) 405 in
377 end 406 case #1 e1 of
378 407 EAbs (_, _, _, b) =>
379 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) 408 ((*Print.preface ("Body", CorePrint.p_exp CoreEnv.empty b);*)
380 409 exp (KnownE e2 :: deKnown env) b)
381 | EKApp (e, k) => 410 | _ => (EApp (e1, e2), loc)
382 let 411 end
383 val e = exp env e 412
384 in 413 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
385 case #1 e of 414
386 EKAbs (_, b) => exp (KnownK k :: deKnown env) b 415 | ECApp (e, c) =>
387 | _ => (EKApp (e, kind env k), loc) 416 let
388 end 417 val e = exp env e
389 418 val c = con env c
390 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) 419 in
391 420 case #1 e of
392 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) 421 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b
393 | EField (e, c, {field, rest}) => 422 | _ => (ECApp (e, c), loc)
394 let 423 end
395 val e = exp env e 424
396 val c = con env c 425 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc)
397 426
398 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc) 427 | EKApp (e, k) =>
399 in 428 let
400 case (#1 e, #1 c) of 429 val e = exp env e
401 (ERecord xcs, CName x) => 430 in
402 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of 431 case #1 e of
403 NONE => default () 432 EKAbs (_, b) => exp (KnownK k :: deKnown env) b
404 | SOME (_, e, _) => e) 433 | _ => (EKApp (e, kind env k), loc)
405 | _ => default () 434 end
406 end 435
407 436 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc)
408 | EConcat (e1, c1, e2, c2) => 437
409 let 438 | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc)
410 val e1 = exp env e1 439 | EField (e, c, {field, rest}) =>
411 val e2 = exp env e2 440 let
412 in 441 val e = exp env e
413 case (#1 e1, #1 e2) of 442 val c = con env c
414 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc) 443
415 | _ => 444 fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc)
416 let 445 in
417 val c1 = con env c1 446 case (#1 e, #1 c) of
418 val c2 = con env c2 447 (ERecord xcs, CName x) =>
419 in 448 (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of
420 case (#1 c1, #1 c2) of 449 NONE => default ()
421 (CRecord (k, xcs1), CRecord (_, xcs2)) => 450 | SOME (_, e, _) => e)
422 let 451 | _ => default ()
423 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 452 end
424 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 453
425 in 454 | EConcat (e1, c1, e2, c2) =>
426 exp (deKnown env) (ERecord (xes1 @ xes2), loc) 455 let
427 end 456 val e1 = exp env e1
428 | _ => (EConcat (e1, c1, e2, c2), loc) 457 val e2 = exp env e2
429 end 458 in
430 end 459 case (#1 e1, #1 e2) of
431 460 (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc)
432 | ECut (e, c, {field, rest}) => 461 | _ =>
433 let 462 let
434 val e = exp env e 463 val c1 = con env c1
435 val c = con env c 464 val c2 = con env c2
436 465 in
437 fun default () = 466 case (#1 c1, #1 c2) of
438 let 467 (CRecord (k, xcs1), CRecord (_, xcs2)) =>
439 val rest = con env rest 468 let
440 in 469 val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1
441 case #1 rest of 470 val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2
442 CRecord (k, xcs) => 471 in
443 let 472 exp (deKnown env) (ERecord (xes1 @ xes2), loc)
444 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs 473 end
445 in 474 | _ => (EConcat (e1, c1, e2, c2), loc)
446 exp (deKnown env) (ERecord xes, loc) 475 end
447 end 476 end
448 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) 477
449 end 478 | ECut (e, c, {field, rest}) =>
450 in 479 let
451 case (#1 e, #1 c) of 480 val e = exp env e
452 (ERecord xes, CName x) => 481 val c = con env c
453 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then 482
454 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x 483 fun default () =
455 | _ => raise Fail "Reduce: ECut") xes), loc) 484 let
456 else 485 val rest = con env rest
457 default () 486 in
458 | _ => default () 487 case #1 rest of
459 end 488 CRecord (k, xcs) =>
460 489 let
461 | ECutMulti (e, c, {rest}) => 490 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
462 let 491 in
463 val e = exp env e 492 exp (deKnown env) (ERecord xes, loc)
464 val c = con env c 493 end
465 494 | _ => (ECut (e, c, {field = con env field, rest = rest}), loc)
466 fun default () = 495 end
467 let 496 in
468 val rest = con env rest 497 case (#1 e, #1 c) of
469 in 498 (ERecord xes, CName x) =>
470 case #1 rest of 499 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then
471 CRecord (k, xcs) => 500 (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x
472 let 501 | _ => raise Fail "Reduce: ECut") xes), loc)
473 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs 502 else
474 in 503 default ()
475 exp (deKnown env) (ERecord xes, loc) 504 | _ => default ()
476 end 505 end
477 | _ => (ECutMulti (e, c, {rest = rest}), loc) 506
478 end 507 | ECutMulti (e, c, {rest}) =>
479 in 508 let
480 case (#1 e, #1 c) of 509 val e = exp env e
481 (ERecord xes, CRecord (_, xcs)) => 510 val c = con env c
482 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes 511
483 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then 512 fun default () =
484 (ERecord (List.filter (fn ((CName x', _), _, _) => 513 let
485 List.all (fn ((CName x, _), _) => x' <> x 514 val rest = con env rest
486 | _ => raise Fail "Reduce: ECutMulti [1]") xcs 515 in
487 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc) 516 case #1 rest of
488 else 517 CRecord (k, xcs) =>
489 default () 518 let
490 | _ => default () 519 val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs
491 end 520 in
492 521 exp (deKnown env) (ERecord xes, loc)
493 | ECase (_, [((PRecord [], _), e)], _) => exp env e 522 end
494 | ECase (_, [((PWild, _), e)], _) => exp env e 523 | _ => (ECutMulti (e, c, {rest = rest}), loc)
495 524 end
496 | ECase (e, pes, {disc, result}) => 525 in
497 let 526 case (#1 e, #1 c) of
498 fun patBinds (p, _) = 527 (ERecord xes, CRecord (_, xcs)) =>
499 case p of 528 if List.all (fn ((CName _, _), _, _) => true | _ => false) xes
500 PWild => 0 529 andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then
501 | PVar _ => 1 530 (ERecord (List.filter (fn ((CName x', _), _, _) =>
502 | PPrim _ => 0 531 List.all (fn ((CName x, _), _) => x' <> x
503 | PCon (_, _, _, NONE) => 0 532 | _ => raise Fail "Reduce: ECutMulti [1]") xcs
504 | PCon (_, _, _, SOME p) => patBinds p 533 | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc)
505 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts 534 else
506 535 default ()
507 fun pat (all as (p, loc)) = 536 | _ => default ()
508 case p of 537 end
509 PWild => all 538
510 | PVar (x, t) => (PVar (x, con env t), loc) 539 | ECase (_, [((PRecord [], _), e)], _) => exp env e
511 | PPrim _ => all 540 | ECase (_, [((PWild, _), e)], _) => exp env e
512 | PCon (dk, pc, cs, po) => 541
513 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) 542 | ECase (e, pes, {disc, result}) =>
514 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) 543 let
515 in 544 fun patBinds (p, _) =
516 (ECase (exp env e, 545 case p of
517 map (fn (p, e) => (pat p, 546 PWild => 0
518 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e)) 547 | PVar _ => 1
519 pes, {disc = con env disc, result = con env result}), loc) 548 | PPrim _ => 0
520 end 549 | PCon (_, _, _, NONE) => 0
521 550 | PCon (_, _, _, SOME p) => patBinds p
522 | EWrite e => (EWrite (exp env e), loc) 551 | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
523 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) 552
524 553 fun pat (all as (p, loc)) =
525 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) 554 case p of
526 555 PWild => all
527 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e, 556 | PVar (x, t) => (PVar (x, con env t), loc)
528 con env t1, con env t2), loc)) 557 | PPrim _ => all
558 | PCon (dk, pc, cs, po) =>
559 (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc)
560 | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc)
561 in
562 (ECase (exp env e,
563 map (fn (p, e) => (pat p,
564 exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e))
565 pes, {disc = con env disc, result = con env result}), loc)
566 end
567
568 | EWrite e => (EWrite (exp env e), loc)
569 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
570
571 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
572
573 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e,
574 con env t1, con env t2), loc)
575 in
576 (*if dangling (edepth' (deKnown env)) r then
577 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
578 ("r", CorePrint.p_exp CoreEnv.empty r)];
579 raise Fail "!!")
580 else
581 ();*)
582 r
583 end
529 in 584 in
530 {kind = kind, con = con, exp = exp} 585 {kind = kind, con = con, exp = exp}
531 end 586 end
532 587
533 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k 588 fun kind namedC env k = #kind (kindConAndExp (namedC, IM.empty)) env k