Mercurial > urweb

comparison src/elaborate.sml @ 334:9601c717d2f3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
queryX
author Adam Chlipala <adamc@hcoop.net>
date Sat, 13 Sep 2008 19:49:53 -0400
parents eec65c11d3e2
children e976b187d73a
comparison
equal deleted inserted replaced
333:c655eddc3795 334:9601c717d2f3
237 val (c', k, gs4) = elabCon (env, denv') c 237 val (c', k, gs4) = elabCon (env, denv') c
238 in 238 in
239 checkKind env c1' k1 (L'.KRecord ku1, loc); 239 checkKind env c1' k1 (L'.KRecord ku1, loc);
240 checkKind env c2' k2 (L'.KRecord ku2, loc); 240 checkKind env c2' k2 (L'.KRecord ku2, loc);
241 241
242 ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) 242 ((L'.TDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4)
243 end 243 end
244 | L.TRecord c => 244 | L.TRecord c =>
245 let 245 let
246 val (c', ck, gs) = elabCon (env, denv) c 246 val (c', ck, gs) = elabCon (env, denv) c
247 val k = (L'.KRecord ktype, loc) 247 val k = (L'.KRecord ktype, loc)
822 | _ => raise ex 822 | _ => raise ex
823 end 823 end
824 824
825 and unifyCons' (env, denv) c1 c2 = 825 and unifyCons' (env, denv) c1 c2 =
826 case (#1 c1, #1 c2) of 826 case (#1 c1, #1 c2) of
827 (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) => 827 (L'.TDisjoint (_, x1, y1, t1), L'.TDisjoint (_, x2, y2, t2)) =>
828 let 828 let
829 val gs1 = unifyCons' (env, denv) x1 x2 829 val gs1 = unifyCons' (env, denv) x1 x2
830 val gs2 = unifyCons' (env, denv) y1 y2 830 val gs2 = unifyCons' (env, denv) y1 y2
831 val (denv', gs3) = D.assert env denv (x1, y1) 831 val (denv', gs3) = D.assert env denv (x1, y1)
832 val gs4 = unifyCons' (env, denv') t1 t2 832 val gs4 = unifyCons' (env, denv') t1 t2
981 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), 981 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
982 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), 982 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
983 (L'.TCFun (L'.Explicit, "v", dom, 983 (L'.TCFun (L'.Explicit, "v", dom,
984 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), 984 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
985 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), 985 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
986 (L'.TDisjoint ((L'.CRecord 986 (L'.TDisjoint (L'.Instantiate,
987 (L'.CRecord
987 ((L'.KUnit, loc), 988 ((L'.KUnit, loc),
988 [((L'.CRel 2, loc), 989 [((L'.CRel 2, loc),
989 (L'.CUnit, loc))]), loc), 990 (L'.CUnit, loc))]), loc),
990 (L'.CRel 0, loc), 991 (L'.CRel 0, loc),
991 (L'.CApp ((L'.CRel 3, loc), 992 (L'.CApp ((L'.CRel 3, loc),
1521 val (e', t, gs4) = elabExp (env, denv') e 1522 val (e', t, gs4) = elabExp (env, denv') e
1522 in 1523 in
1523 checkKind env c1' k1 (L'.KRecord ku1, loc); 1524 checkKind env c1' k1 (L'.KRecord ku1, loc);
1524 checkKind env c2' k2 (L'.KRecord ku2, loc); 1525 checkKind env c2' k2 (L'.KRecord ku2, loc);
1525 1526
1526 (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) 1527 (e', (L'.TDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4)
1527 end 1528 end
1528 1529
1529 | L.ERecord xes => 1530 | L.ERecord xes =>
1530 let 1531 let
1531 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => 1532 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
2659 end 2660 end
2660 end 2661 end
2661 | _ => str) 2662 | _ => str)
2662 | _ => str 2663 | _ => str
2663 2664
2665 val makeInstantiable =
2666 let
2667 fun kind k = k
2668 fun con c =
2669 case c of
2670 L'.TDisjoint (L'.LeaveAlone, c1, c2, c) => L'.TDisjoint (L'.Instantiate, c1, c2, c)
2671 | _ => c
2672 in
2673 U.Con.map {kind = kind, con = con}
2674 end
2675
2664 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = 2676 fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) =
2665 let 2677 let
2666 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 2678 (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*)
2667 2679
2668 val r = 2680 val r =
2790 2802
2791 val (e', et, gs2) = elabExp (env, denv) e 2803 val (e', et, gs2) = elabExp (env, denv) e
2792 val gs3 = checkCon (env, denv) e' et c' 2804 val gs3 = checkCon (env, denv) e' et c'
2793 val (c', gs4) = normClassConstraint (env, denv) c' 2805 val (c', gs4) = normClassConstraint (env, denv) c'
2794 val (env', n) = E.pushENamed env x c' 2806 val (env', n) = E.pushENamed env x c'
2807 val c' = makeInstantiable c'
2795 in 2808 in
2796 (*prefaces "DVal" [("x", Print.PD.string x), 2809 (*prefaces "DVal" [("x", Print.PD.string x),
2797 ("c'", p_con env c')];*) 2810 ("c'", p_con env c')];*)
2798 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) 2811 ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs))
2799 end 2812 end
2826 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => 2839 val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) =>
2827 let 2840 let
2828 val (e', et, gs1) = elabExp (env, denv) e 2841 val (e', et, gs1) = elabExp (env, denv) e
2829 2842
2830 val gs2 = checkCon (env, denv) e' et c' 2843 val gs2 = checkCon (env, denv) e' et c'
2844
2845 val c' = makeInstantiable c'
2831 in 2846 in
2832 if allowable e then 2847 if allowable e then
2833 () 2848 ()
2834 else 2849 else
2835 expError env (IllegalRec (x, e')); 2850 expError env (IllegalRec (x, e'));