Mercurial > urweb

comparison src/elaborate.sml @ 750:059074c8d2fc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
LEFT JOIN
author Adam Chlipala <adamc@hcoop.net>
date Tue, 28 Apr 2009 11:05:28 -0400
parents 9864b64b1700
children d484df4e841a
comparison
equal deleted inserted replaced
749:16bfd9e244cd 750:059074c8d2fc
1129 unravel (t'', (L'.ECApp (e, u), loc)) 1129 unravel (t'', (L'.ECApp (e, u), loc))
1130 end 1130 end
1131 | (L'.TFun (dom, ran), _) => 1131 | (L'.TFun (dom, ran), _) =>
1132 let 1132 let
1133 fun default () = (e, t, []) 1133 fun default () = (e, t, [])
1134
1135 fun isInstance () =
1136 if infer <> L.TypesOnly then
1137 let
1138 val r = ref NONE
1139 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1140 in
1141 (e, t, TypeClass (env, dom, r, loc) :: gs)
1142 end
1143 else
1144 default ()
1145
1146 fun hasInstance c =
1147 case #1 (hnormCon env c) of
1148 L'.CApp (cl, x) =>
1149 let
1150 val cl = hnormCon env cl
1151 in
1152 isClassOrFolder env cl
1153 end
1154 | L'.TRecord c => U.Con.exists {kind = fn _ => false,
1155 con = fn c =>
1156 E.isClass env (hnormCon env (c, loc))} c
1157 | _ => false
1134 in 1158 in
1135 case #1 (hnormCon env dom) of 1159 if hasInstance dom then
1136 L'.CApp (cl, x) => 1160 isInstance ()
1137 let 1161 else
1138 val cl = hnormCon env cl 1162 default ()
1139 in
1140 if infer <> L.TypesOnly then
1141 if isClassOrFolder env cl then
1142 let
1143 val r = ref NONE
1144 val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
1145 in
1146 (e, t, TypeClass (env, dom, r, loc) :: gs)
1147 end
1148 else
1149 default ()
1150 else
1151 default ()
1152 end
1153 | _ => default ()
1154 end 1163 end
1155 | (L'.TDisjoint (r1, r2, t'), loc) => 1164 | (L'.TDisjoint (r1, r2, t'), loc) =>
1156 if infer <> L.TypesOnly then 1165 if infer <> L.TypesOnly then
1157 let 1166 let
1158 val gs = D.prove env denv (r1, r2, loc) 1167 val gs = D.prove env denv (r1, r2, loc)
3636 raise Fail "Unresolved constraint in top.ur")) 3645 raise Fail "Unresolved constraint in top.ur"))
3637 | TypeClass (env, c, r, loc) => 3646 | TypeClass (env, c, r, loc) =>
3638 let 3647 let
3639 val c = normClassKey env c 3648 val c = normClassKey env c
3640 in 3649 in
3641 case E.resolveClass env c of 3650 case E.resolveClass (hnormCon env) env c of
3642 SOME e => r := SOME e 3651 SOME e => r := SOME e
3643 | NONE => expError env (Unresolvable (loc, c)) 3652 | NONE => expError env (Unresolvable (loc, c))
3644 end) gs 3653 end) gs
3645 3654
3646 val () = subSgn env' topSgn' topSgn 3655 val () = subSgn env' topSgn' topSgn
3686 delayedUnifs := []; 3695 delayedUnifs := [];
3687 3696
3688 if ErrorMsg.anyErrors () then 3697 if ErrorMsg.anyErrors () then
3689 () 3698 ()
3690 else 3699 else
3691 app (fn f => f ()) (!checks);
3692
3693 if ErrorMsg.anyErrors () then
3694 ()
3695 else
3696 app (fn Disjoint (loc, env, denv, c1, c2) => 3700 app (fn Disjoint (loc, env, denv, c1, c2) =>
3697 (case D.prove env denv (c1, c2, loc) of 3701 (case D.prove env denv (c1, c2, loc) of
3698 [] => () 3702 [] => ()
3699 | _ => 3703 | _ =>
3700 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; 3704 (ErrorMsg.errorAt loc "Couldn't prove field name disjointness";
3706 let 3710 let
3707 fun default () = expError env (Unresolvable (loc, c)) 3711 fun default () = expError env (Unresolvable (loc, c))
3708 3712
3709 val c = normClassKey env c 3713 val c = normClassKey env c
3710 in 3714 in
3711 case E.resolveClass env c of 3715 case E.resolveClass (hnormCon env) env c of
3712 SOME e => r := SOME e 3716 SOME e => r := SOME e
3713 | NONE => 3717 | NONE =>
3714 case #1 (hnormCon env c) of 3718 case #1 (hnormCon env c) of
3715 L'.CApp (f, x) => 3719 L'.CApp (f, x) =>
3716 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of 3720 (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
3745 | _ => default ()) 3749 | _ => default ())
3746 | _ => default ()) 3750 | _ => default ())
3747 | _ => default () 3751 | _ => default ()
3748 end) gs; 3752 end) gs;
3749 3753
3754 if ErrorMsg.anyErrors () then
3755 ()
3756 else
3757 app (fn f => f ()) (!checks);
3758
3750 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) 3759 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan)
3751 :: ds 3760 :: ds
3752 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) 3761 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan)
3753 :: ds' @ file 3762 :: ds' @ file
3754 end 3763 end