Mercurial > urweb

comparison src/reduce.sml @ 910:8e540df3294d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
grid1 compiles but gets stuck in JS
author Adam Chlipala <adamc@hcoop.net>
date Tue, 25 Aug 2009 13:57:56 -0400
parents 1d3f60e74ec7
children 51bc7681c47e
comparison
equal deleted inserted replaced
909:1d3f60e74ec7 910:8e540df3294d
252 252
253 fun exp env (all as (e, loc)) = 253 fun exp env (all as (e, loc)) =
254 let 254 let
255 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), 255 (*val () = Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
256 ("env", Print.PD.string (e2s env))]*) 256 ("env", Print.PD.string (e2s env))]*)
257 (*val () = if dangling (edepth env) all then 257 val () = if dangling (edepth env) all then
258 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), 258 (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all),
259 ("env", Print.PD.string (e2s env))]; 259 ("env", Print.PD.string (e2s env))];
260 raise Fail "!") 260 raise Fail "!")
261 else 261 else
262 ()*) 262 ()
263 263
264 val r = case e of 264 val r = case e of
265 EPrim _ => all 265 EPrim _ => all
266 | ERel n => 266 | ERel n =>
267 let 267 let
297 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, 297 | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc,
298 map (con env) cs, Option.map (exp env) eo), loc) 298 map (con env) cs, Option.map (exp env) eo), loc)
299 | EFfi _ => all 299 | EFfi _ => all
300 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) 300 | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc)
301 301
302 | EApp (
303 (EApp
304 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
305 _), _),
306 (EApp (
307 (EApp (
308 (ECApp (
309 (ECApp ((EFfi ("Basis", "return"), _), _), _),
310 _), _),
311 _), _), v), _)), _), trans2) => exp env (EApp (trans2, v), loc)
312
313 (*| EApp ( 302 (*| EApp (
314 (EApp 303 (EApp
315 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _), 304 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
316 (EFfi ("Basis", "transaction_monad"), _)), _), 305 (EFfi ("Basis", "transaction_monad"), _)), _),
317 (ECase (ed, pes, {disc, ...}), _)), _), 306 (ECase (ed, pes, {disc, ...}), _)), _),
339 {disc = con env disc, 328 {disc = con env disc,
340 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}), 329 result = (CApp ((CFfi ("Basis", "transaction"), loc), con env t2), loc)}),
341 loc) 330 loc)
342 end*) 331 end*)
343 332
344 | EApp (
345 (EApp
346 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1), _), t2), _),
347 (EFfi ("Basis", "transaction_monad"), _)), _),
348 (EServerCall (n, es, ke, dom, ran), _)), _),
349 trans2) =>
350 let
351 val e' = (EFfi ("Basis", "bind"), loc)
352 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
353 val e' = (ECApp (e', dom), loc)
354 val e' = (ECApp (e', t2), loc)
355 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
356 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
357 val e' = (EApp (e', E.liftExpInExp 0 trans2), loc)
358 val e' = (EAbs ("x", dom, t2, e'), loc)
359 val e' = (EServerCall (n, es, e', dom, t2), loc)
360 in
361 exp env e'
362 end
363
364 | EApp (
365 (EApp
366 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt), _), _), _), t3), _),
367 me), _),
368 (EApp ((EApp
369 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _), t1), _), t2), _),
370 _), _),
371 trans1), _), trans2), _)), _),
372 trans3) =>
373 let
374 val e'' = (EFfi ("Basis", "bind"), loc)
375 val e'' = (ECApp (e'', mt), loc)
376 val e'' = (ECApp (e'', t2), loc)
377 val e'' = (ECApp (e'', t3), loc)
378 val e'' = (EApp (e'', me), loc)
379 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
380 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
381 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
382
383 val e' = (EFfi ("Basis", "bind"), loc)
384 val e' = (ECApp (e', mt), loc)
385 val e' = (ECApp (e', t1), loc)
386 val e' = (ECApp (e', t3), loc)
387 val e' = (EApp (e', me), loc)
388 val e' = (EApp (e', trans1), loc)
389 val e' = (EApp (e', e''), loc)
390 (*val () = print "Before\n"*)
391 val ee' = exp env e'
392 (*val () = print "After\n"*)
393 in
394 (*Print.prefaces "Commute" [("Pre", CorePrint.p_exp CoreEnv.empty (e, loc)),
395 ("Mid", CorePrint.p_exp CoreEnv.empty e'),
396 ("env", Print.PD.string (e2s env)),
397 ("Post", CorePrint.p_exp CoreEnv.empty ee')];*)
398 ee'
399 end
400
401 | EApp (e1, e2) => 333 | EApp (e1, e2) =>
402 let 334 let
335 val env' = deKnown env
336
337 fun reassoc e =
338 case #1 e of
339 EApp
340 ((EApp
341 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
342 t1),
343 _), t2), _),
344 (EFfi ("Basis", "transaction_monad"), _)), _),
345 (EServerCall (n, es, (EAbs (_, _, _, ke), _), dom, ran), _)), _),
346 trans3) =>
347 let
348 val e' = (EFfi ("Basis", "bind"), loc)
349 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
350 val e' = (ECApp (e', dom), loc)
351 val e' = (ECApp (e', t2), loc)
352 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
353 val e' = (EApp (e', ke), loc)
354 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
355 val e' = reassoc e'
356 val e' = (EAbs ("x", dom, t2, e'), loc)
357 val e' = (EServerCall (n, es, e', dom, t2), loc)
358 in
359 e'
360 end
361
362 | EApp
363 ((EApp
364 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _),
365 t1),
366 _), t2), _),
367 (EFfi ("Basis", "transaction_monad"), _)), _),
368 (EServerCall (n, es, ke, dom, ran), _)), _),
369 trans3) =>
370 let
371 val e' = (EFfi ("Basis", "bind"), loc)
372 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
373 val e' = (ECApp (e', dom), loc)
374 val e' = (ECApp (e', t2), loc)
375 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
376 val e' = (EApp (e', exp (UnknownE :: env')
377 (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)),
378 loc)
379 val e' = (EApp (e', E.liftExpInExp 0 trans3), loc)
380 val e' = reassoc e'
381 val e' = (EAbs ("x", dom, t2, e'), loc)
382 val e' = (EServerCall (n, es, e', dom, t2), loc)
383 in
384 e'
385 end
386
387 | EApp
388 ((EApp
389 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
390 _), _), _), t3), _),
391 me), _),
392 (EApp ((EApp
393 ((EApp ((ECApp ((ECApp ((ECApp (
394 (EFfi ("Basis", "bind"), _), _), _),
395 t1), _), t2), _),
396 _), _),
397 trans1), _), (EAbs (_, _, _, trans2), _)), _)), _),
398 trans3) =>
399 let
400 val e'' = (EFfi ("Basis", "bind"), loc)
401 val e'' = (ECApp (e'', mt), loc)
402 val e'' = (ECApp (e'', t2), loc)
403 val e'' = (ECApp (e'', t3), loc)
404 val e'' = (EApp (e'', me), loc)
405 val e'' = (EApp (e'', trans2), loc)
406 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
407 val e'' = reassoc e''
408 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
409
410 val e' = (EFfi ("Basis", "bind"), loc)
411 val e' = (ECApp (e', mt), loc)
412 val e' = (ECApp (e', t1), loc)
413 val e' = (ECApp (e', t3), loc)
414 val e' = (EApp (e', me), loc)
415 val e' = (EApp (e', trans1), loc)
416 val e' = (EApp (e', e''), loc)
417 in
418 e'
419 end
420
421 | EApp
422 ((EApp
423 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
424 _), _), _), t3), _),
425 me), _),
426 (EApp ((EApp
427 ((EApp ((ECApp ((ECApp ((ECApp (
428 (EFfi ("Basis", "bind"), _), _), _),
429 t1), _), t2), _),
430 _), _),
431 trans1), _), trans2), _)), _),
432 trans3) =>
433 let
434 val e'' = (EFfi ("Basis", "bind"), loc)
435 val e'' = (ECApp (e'', mt), loc)
436 val e'' = (ECApp (e'', t2), loc)
437 val e'' = (ECApp (e'', t3), loc)
438 val e'' = (EApp (e'', me), loc)
439 val () = print "In2\n"
440 val e'' = (EApp (e'', exp (UnknownE :: env')
441 (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)),
442 loc)),
443 loc)
444 val () = print "Out2\n"
445 val e'' = (EApp (e'', E.liftExpInExp 0 trans3), loc)
446 val e'' = reassoc e''
447 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
448
449 val e' = (EFfi ("Basis", "bind"), loc)
450 val e' = (ECApp (e', mt), loc)
451 val e' = (ECApp (e', t1), loc)
452 val e' = (ECApp (e', t3), loc)
453 val e' = (EApp (e', me), loc)
454 val e' = (EApp (e', trans1), loc)
455 val e' = (EApp (e', e''), loc)
456 in
457 e'
458 end
459
460 | _ => e
461
403 val e1 = exp env e1 462 val e1 = exp env e1
404 val e2 = exp env e2 463 val e2 = exp env e2
405 in 464 val e12 = reassoc (EApp (e1, e2), loc)
406 case #1 e1 of 465 in
407 EAbs (_, _, _, b) => 466 case #1 e12 of
467 EApp ((EAbs (_, _, _, b), _), e2) =>
408 ((*Print.preface ("Body", CorePrint.p_exp CoreEnv.empty b);*) 468 ((*Print.preface ("Body", CorePrint.p_exp CoreEnv.empty b);*)
409 exp (KnownE e2 :: deKnown env) b) 469 exp (KnownE e2 :: env') b)
410 | _ => (EApp (e1, e2), loc) 470 (*| EApp
471 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1),
472 _), t2), _),
473 _), _),
474 (EApp (
475 (EApp (
476 (ECApp (
477 (ECApp ((EFfi ("Basis", "return"), _), _), _),
478 _), _),
479 _), _), v), _)) =>
480 (ELet ("rv", con env t1, v,
481 exp (deKnown env) (EApp (E.liftExpInExp 0 e2, (ERel 0, loc)), loc)), loc)*)
482 (*| EApp
483 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), _), _), t1),
484 _), t2), _),
485 (EFfi ("Basis", "transaction_monad"), _)), _),
486 (EServerCall (n, es, ke, dom, ran), _)) =>
487 let
488 val e' = (EFfi ("Basis", "bind"), loc)
489 val e' = (ECApp (e', (CFfi ("Basis", "transaction"), loc)), loc)
490 val e' = (ECApp (e', dom), loc)
491 val e' = (ECApp (e', t2), loc)
492 val e' = (EApp (e', (EFfi ("Basis", "transaction_monad"), loc)), loc)
493 val e' = (EApp (e', (EApp (E.liftExpInExp 0 ke, (ERel 0, loc)), loc)), loc)
494 val e' = (EApp (e', E.liftExpInExp 0 (exp env e2)), loc)
495 val e' = (EAbs ("x", dom, t2, e'), loc)
496 val e' = (EServerCall (n, es, e', dom, t2), loc)
497 val e' = exp (deKnown env) e'
498 in
499 (*Print.prefaces "SC" [("Old", CorePrint.p_exp CoreEnv.empty all),
500 ("New", CorePrint.p_exp CoreEnv.empty e')]*)
501 e'
502 end
503 | EApp
504 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), loc), mt),
505 _), _), _), t3), _),
506 me), _),
507 (EApp ((EApp
508 ((EApp ((ECApp ((ECApp ((ECApp ((EFfi ("Basis", "bind"), _), _), _),
509 t1), _), t2), _),
510 _), _),
511 trans1), _), trans2), _)) =>
512 let
513 val e'' = (EFfi ("Basis", "bind"), loc)
514 val e'' = (ECApp (e'', mt), loc)
515 val e'' = (ECApp (e'', t2), loc)
516 val e'' = (ECApp (e'', t3), loc)
517 val e'' = (EApp (e'', me), loc)
518 val e'' = (EApp (e'', (EApp (E.liftExpInExp 0 trans2, (ERel 0, loc)), loc)), loc)
519 val e'' = (EApp (e'', E.liftExpInExp 0 e2), loc)
520 val e'' = (EAbs ("xb", t1, (CApp (mt, t3), loc), e''), loc)
521
522 val e' = (EFfi ("Basis", "bind"), loc)
523 val e' = (ECApp (e', mt), loc)
524 val e' = (ECApp (e', t1), loc)
525 val e' = (ECApp (e', t3), loc)
526 val e' = (EApp (e', me), loc)
527 val e' = (EApp (e', trans1), loc)
528 val e' = (EApp (e', e''), loc)
529 (*val () = Print.prefaces "Going in" [("e", CorePrint.p_exp CoreEnv.empty (e, loc)),
530 ("e1", CorePrint.p_exp CoreEnv.empty e1),
531 ("e'", CorePrint.p_exp CoreEnv.empty e')]*)
532 val ee' = exp (deKnown env) e'
533 val () = Print.prefaces "Coming out" [("ee'", CorePrint.p_exp CoreEnv.empty ee')]
534 in
535 (*Print.prefaces "Commute" [("Pre", CorePrint.p_exp CoreEnv.empty (e, loc)),
536 ("Mid", CorePrint.p_exp CoreEnv.empty e'),
537 ("env", Print.PD.string (e2s env)),
538 ("Post", CorePrint.p_exp CoreEnv.empty ee')];*)
539 ee'
540 end
541 | _ => (EApp (e1, exp env e2), loc)*)
542 | _ => e12
411 end 543 end
412 544
413 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) 545 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc)
414 546
415 | ECApp (e, c) => 547 | ECApp (e, c) =>
566 end 698 end
567 699
568 | EWrite e => (EWrite (exp env e), loc) 700 | EWrite e => (EWrite (exp env e), loc)
569 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) 701 | EClosure (n, es) => (EClosure (n, map (exp env) es), loc)
570 702
571 | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) 703 | ELet (x, t, e1, e2) =>
704 (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc)
572 705
573 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e, 706 | EServerCall (n, es, e, t1, t2) => (EServerCall (n, map (exp env) es, exp env e,
574 con env t1, con env t2), loc) 707 con env t1, con env t2), loc)
575 in 708 in
576 (*if dangling (edepth' (deKnown env)) r then 709 (*if dangling (edepth' (deKnown env)) r then
616 in 749 in
617 ((DVal (x, n, t, e, s), loc), 750 ((DVal (x, n, t, e, s), loc),
618 (namedC, IM.insert (namedE, n, e))) 751 (namedC, IM.insert (namedE, n, e)))
619 end 752 end
620 | DValRec vis => 753 | DValRec vis =>
621 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t, exp (namedC, namedE) [] e, s)) vis), loc), 754 ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC [] t,
755 exp (namedC, namedE) [] e, s)) vis), loc),
622 st) 756 st)
623 | DExport _ => (d, st) 757 | DExport _ => (d, st)
624 | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s', 758 | DTable (s, n, c, s', pe, pc, ce, cc) => ((DTable (s, n, con namedC [] c, s',
625 exp (namedC, namedE) [] pe, 759 exp (namedC, namedE) [] pe,
626 con namedC [] pc, 760 con namedC [] pc,