Mercurial > urweb

comparison src/reduce.sml @ 1181:618f9f458da9

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