Mercurial > urweb

comparison src/elaborate.sml @ 326:950320f33232

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Crud list works
author Adam Chlipala <adamc@hcoop.net>
date Thu, 11 Sep 2008 18:32:41 -0400
parents e457d8972ff1
children 3a57f3b3a3f8
comparison
equal deleted inserted replaced
325:e457d8972ff1 326:950320f33232
894 unfold (dom, ran, f, i, r, c1) 894 unfold (dom, ran, f, i, r, c1)
895 | _ => raise ex 895 | _ => raise ex
896 end 896 end
897 897
898 and unifyCons' (env, denv) c1 c2 = 898 and unifyCons' (env, denv) c1 c2 =
899 let 899 case (#1 c1, #1 c2) of
900 val (c1, gs1) = hnormCon (env, denv) c1 900 (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) =>
901 val (c2, gs2) = hnormCon (env, denv) c2 901 let
902 in 902 val gs1 = unifyCons' (env, denv) x1 x2
903 let 903 val gs2 = unifyCons' (env, denv) y1 y2
904 val gs3 = unifyCons'' (env, denv) c1 c2 904 val (denv', gs3) = D.assert env denv (x1, y1)
905 in 905 val gs4 = unifyCons' (env, denv') t1 t2
906 gs1 @ gs2 @ gs3 906 in
907 end 907 gs1 @ gs2 @ gs3 @ gs4
908 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) 908 end
909 end 909 | _ =>
910 let
911 val (c1, gs1) = hnormCon (env, denv) c1
912 val (c2, gs2) = hnormCon (env, denv) c2
913 in
914 let
915 val gs3 = unifyCons'' (env, denv) c1 c2
916 in
917 gs1 @ gs2 @ gs3
918 end
919 handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
920 end
910 921
911 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = 922 and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
912 let 923 let
913 fun err f = raise CUnify' (f (c1All, c2All)) 924 fun err f = raise CUnify' (f (c1All, c2All))
914 925
1114 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), 1125 (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc),
1115 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), 1126 (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc),
1116 (L'.TCFun (L'.Explicit, "v", dom, 1127 (L'.TCFun (L'.Explicit, "v", dom,
1117 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), 1128 (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
1118 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), 1129 (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
1119 (L'.CApp ((L'.CRel 3, loc), 1130 (L'.TDisjoint ((L'.CRecord
1120 recCons (dom, 1131 ((L'.KUnit, loc),
1121 (L'.CRel 2, loc), 1132 [((L'.CRel 2, loc),
1122 (L'.CRel 1, loc), 1133 (L'.CUnit, loc))]), loc),
1123 (L'.CRel 0, loc), 1134 (L'.CRel 0, loc),
1124 loc)), loc)), loc)), 1135 (L'.CApp ((L'.CRel 3, loc),
1136 recCons (dom,
1137 (L'.CRel 2, loc),
1138 (L'.CRel 1, loc),
1139 (L'.CRel 0, loc),
1140 loc)), loc)),
1141 loc)), loc)),
1125 loc)), loc)), loc), 1142 loc)), loc)), loc),
1126 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), 1143 (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
1127 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), 1144 (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),
1128 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), 1145 (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)),
1129 loc)), loc)), loc) 1146 loc)), loc)), loc)