Mercurial > urweb

comparison src/elaborate.sml @ 514:0fc08d1750e1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove unnecessary lifts in ElabEnv.pushCRel
author Adam Chlipala <adamc@hcoop.net>
date Thu, 27 Nov 2008 10:40:29 -0500
parents 5fc269f744ee
children 685d232bd1a5
comparison
equal deleted inserted replaced
513:5fc269f744ee 514:0fc08d1750e1
873 | _ => 873 | _ =>
874 if isUnitCon env c1 andalso isUnitCon env c2 then 874 if isUnitCon env c1 andalso isUnitCon env c2 then
875 [] 875 []
876 else 876 else
877 let 877 let
878 (*val befor = Time.now ()
879 val old1 = c1
880 val old2 = c2*)
878 val (c1, gs1) = hnormCon (env, denv) c1 881 val (c1, gs1) = hnormCon (env, denv) c1
879 val (c2, gs2) = hnormCon (env, denv) c2 882 val (c2, gs2) = hnormCon (env, denv) c2
880 in 883 in
881 let 884 let
882 val gs3 = unifyCons'' (env, denv) c1 c2 885 val gs3 = unifyCons'' (env, denv) c1 c2
883 in 886 in
887 (*prefaces "unifyCons'" [("c1", p_con env old1),
888 ("c2", p_con env old2),
889 ("t", PD.string (LargeReal.toString (Time.toReal
890 (Time.- (Time.now (), befor)))))];*)
884 gs1 @ gs2 @ gs3 891 gs1 @ gs2 @ gs3
885 end 892 end
886 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) 893 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
887 end 894 end
888 895
904 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => 911 | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) =>
905 if expl1 <> expl2 then 912 if expl1 <> expl2 then
906 err CExplicitness 913 err CExplicitness
907 else 914 else
908 (unifyKinds d1 d2; 915 (unifyKinds d1 d2;
909 unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2) 916 let
917 val denv' = D.enter denv
918 (*val befor = Time.now ()*)
919 val env' = E.pushCRel env x1 d1
920 in
921 (*TextIO.print ("E.pushCRel: "
922 ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))
923 ^ "\n");*)
924 unifyCons' (env', denv') r1 r2
925 end)
910 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2 926 | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2
911 927
912 | (L'.CRel n1, L'.CRel n2) => 928 | (L'.CRel n1, L'.CRel n2) =>
913 if n1 = n2 then 929 if n1 = n2 then
914 [] 930 []
1476 end 1492 end
1477 1493
1478 fun elabExp (env, denv) (eAll as (e, loc)) = 1494 fun elabExp (env, denv) (eAll as (e, loc)) =
1479 let 1495 let
1480 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) 1496 (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*)
1497 (*val befor = Time.now ()*)
1481 1498
1482 val r = case e of 1499 val r = case e of
1483 L.EAnnot (e, t) => 1500 L.EAnnot (e, t) =>
1484 let 1501 let
1485 val (e', et, gs1) = elabExp (env, denv) e 1502 val (e', et, gs1) = elabExp (env, denv) e
1768 in 1785 in
1769 ((L'.ELet (eds, e), loc), t, gs1 @ gs2) 1786 ((L'.ELet (eds, e), loc), t, gs1 @ gs2)
1770 end 1787 end
1771 in 1788 in
1772 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), 1789 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
1773 ("t", PD.string (LargeInt.toString (Time.toMilliseconds (Time.- (Time.now (), befor)))))];*) 1790 ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*)
1774 r 1791 r
1775 end 1792 end
1776 1793
1777 and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = 1794 and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) =
1778 let 1795 let
2911 | _ => str 2928 | _ => str
2912 2929
2913 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2930 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2914 let 2931 let
2915 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2932 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2933 (*val befor = Time.now ()*)
2916 2934
2917 val r = 2935 val r =
2918 case d of 2936 case d of
2919 L.DCon (x, ko, c) => 2937 L.DCon (x, ko, c) =>
2920 let 2938 let
3291 end 3309 end
3292 3310
3293 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) 3311 (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*)
3294 in 3312 in
3295 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), 3313 (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll),
3296 ("t", PD.string (LargeInt.toString (Time.toMilliseconds 3314 ("t", PD.string (LargeReal.toString (Time.toReal
3297 (Time.- (Time.now (), befor)))))];*) 3315 (Time.- (Time.now (), befor)))))];*)
3298 3316
3299 r 3317 r
3300 end 3318 end
3301 3319
3302 and elabStr (env, denv) (str, loc) = 3320 and elabStr (env, denv) (str, loc) =