Mercurial > urweb
comparison src/reduce.sml @ 1181:618f9f458da9
Got split1 working, but noticed a nasty type inference bug with transplanted unification variables
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sat, 06 Mar 2010 19:14:48 -0500 |
parents | c58453683bbb |
children | c316ca3c9ec6 |
comparison
equal
deleted
inserted
replaced
1180:ac3dbbc85c6e | 1181:618f9f458da9 |
---|---|
421 val e1 = exp env e1 | 421 val e1 = exp env e1 |
422 val e2 = exp env e2 | 422 val e2 = exp env e2 |
423 in | 423 in |
424 case #1 e1 of | 424 case #1 e1 of |
425 EAbs (_, _, _, b) => | 425 EAbs (_, _, _, b) => |
426 exp (KnownE e2 :: env') b | 426 let |
427 val r = exp (KnownE e2 :: env') b | |
428 in | |
429 (*Print.prefaces "eapp" [("b", CorePrint.p_exp CoreEnv.empty b), | |
430 ("env", Print.PD.string (e2s env')), | |
431 ("e2", CorePrint.p_exp CoreEnv.empty e2), | |
432 ("r", CorePrint.p_exp CoreEnv.empty r)];*) | |
433 r | |
434 end | |
427 | _ => (EApp (e1, e2), loc) | 435 | _ => (EApp (e1, e2), loc) |
428 end | 436 end |
429 | 437 |
430 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) | 438 | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) |
431 | 439 |
433 let | 441 let |
434 val e = exp env e | 442 val e = exp env e |
435 val c = con env c | 443 val c = con env c |
436 in | 444 in |
437 case #1 e of | 445 case #1 e of |
438 ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b | 446 ECAbs (_, _, b) => |
447 let | |
448 val r = exp (KnownC c :: deKnown env) b | |
449 in | |
450 (*Print.prefaces "csub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), | |
451 ("env", Print.PD.string (e2s (deKnown env))), | |
452 ("b", CorePrint.p_exp CoreEnv.empty b), | |
453 ("c", CorePrint.p_con CoreEnv.empty c), | |
454 ("r", CorePrint.p_exp CoreEnv.empty r)];*) | |
455 r | |
456 end | |
439 | _ => (ECApp (e, c), loc) | 457 | _ => (ECApp (e, c), loc) |
440 end | 458 end |
441 | 459 |
442 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) | 460 | ECAbs (x, k, e) => (ECAbs (x, kind env k, exp (UnknownC :: env) e), loc) |
443 | 461 |
444 | EKApp (e, k) => | 462 | EKApp (e, k) => |
445 let | 463 let |
446 val e = exp env e | 464 val e = exp env e |
447 in | 465 in |
448 case #1 e of | 466 case #1 e of |
449 EKAbs (_, b) => exp (KnownK k :: deKnown env) b | 467 EKAbs (_, b) => |
468 let | |
469 val r = exp (KnownK k :: deKnown env) b | |
470 in | |
471 (*Print.prefaces "ksub" [("l", Print.PD.string (ErrorMsg.spanToString loc)), | |
472 ("b", CorePrint.p_exp CoreEnv.empty b), | |
473 ("k", CorePrint.p_kind CoreEnv.empty k), | |
474 ("r", CorePrint.p_exp CoreEnv.empty r)];*) | |
475 r | |
476 end | |
450 | _ => (EKApp (e, kind env k), loc) | 477 | _ => (EKApp (e, kind env k), loc) |
451 end | 478 end |
452 | 479 |
453 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) | 480 | EKAbs (x, e) => (EKAbs (x, exp (UnknownK :: env) e), loc) |
454 | 481 |