Mercurial > urweb

comparison src/elaborate.sml @ 26:4ab19c19665f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Closure conversion
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Jun 2008 15:56:33 -0400
parents 9a578171de9e
children 537db4ee89f4
comparison
equal deleted inserted replaced
25:0a762c73824d 26:4ab19c19665f
695 | L'.ENamed n => #2 (E.lookupENamed env n) 695 | L'.ENamed n => #2 (E.lookupENamed env n)
696 | L'.EApp (e1, _) => 696 | L'.EApp (e1, _) =>
697 (case #1 (typeof env e1) of 697 (case #1 (typeof env e1) of
698 L'.TFun (_, c) => c 698 L'.TFun (_, c) => c
699 | _ => raise Fail "typeof: Bad EApp") 699 | _ => raise Fail "typeof: Bad EApp")
700 | L'.EAbs (x, t, e1) => (L'.TFun (t, typeof (E.pushERel env x t) e1), loc) 700 | L'.EAbs (_, _, ran, _) => ran
701 | L'.ECApp (e1, c) => 701 | L'.ECApp (e1, c) =>
702 (case #1 (typeof env e1) of 702 (case #1 (typeof env e1) of
703 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1 703 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
704 | _ => raise Fail "typeof: Bad ECApp") 704 | _ => raise Fail "typeof: Bad ECApp")
705 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) 705 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
769 checkKind env t' tk ktype; 769 checkKind env t' tk ktype;
770 t' 770 t'
771 end 771 end
772 val (e', et) = elabExp (E.pushERel env x t') e 772 val (e', et) = elabExp (E.pushERel env x t') e
773 in 773 in
774 ((L'.EAbs (x, t', e'), loc), 774 ((L'.EAbs (x, t', et, e'), loc),
775 (L'.TFun (t', et), loc)) 775 (L'.TFun (t', et), loc))
776 end 776 end
777 | L.ECApp (e, c) => 777 | L.ECApp (e, c) =>
778 let 778 let
779 val (e', et) = elabExp env e 779 val (e', et) = elabExp env e