Mercurial > urweb
comparison src/elaborate.sml @ 326:950320f33232
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) |