summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 18:32:41 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-09-11 18:32:41 -0400
commit42944f71120301ea2dff0e93f3a0f2e7df4a44b0 (patch)
tree527e676197eaa7c1c4377678e5e6d9731fb11a98 /src
parent48b9d4dae3d1ca6ff39e71571a6db3a43497c9f9 (diff)
Crud list works
Diffstat (limited to 'src')
-rw-r--r--src/disjoint.sml2
-rw-r--r--src/elab_ops.sml60
-rw-r--r--src/elaborate.sml45
3 files changed, 65 insertions, 42 deletions
diff --git a/src/disjoint.sml b/src/disjoint.sml
index 069d3ec2..5602c8d2 100644
--- a/src/disjoint.sml
+++ b/src/disjoint.sml
@@ -199,6 +199,8 @@ fun decomposeRow (env, denv) c =
| _ => (Unknown cAll :: acc, gs)
end
in
+ (*Print.prefaces "decomposeRow'" [("c", ElabPrint.p_con env c),
+ ("c'", ElabPrint.p_con env (#1 (hnormCon (env, denv) c)))];*)
case #1 (#1 (hnormCon (env, denv) c)) of
CApp (
(CApp (
diff --git a/src/elab_ops.sml b/src/elab_ops.sml
index 50c95ac7..6c75768b 100644
--- a/src/elab_ops.sml
+++ b/src/elab_ops.sml
@@ -98,36 +98,40 @@ fun hnormCon env (cAll as (c, loc)) =
("sc", p_con env sc)];*)
sc
end
- | CApp (c', i) =>
- (case #1 (hnormCon env c') of
- CApp (c', f) =>
- (case #1 (hnormCon env c') of
- CFold ks =>
- (case #1 (hnormCon env c2) of
- CRecord (_, []) => hnormCon env i
- | CRecord (k, (x, c) :: rest) =>
- hnormCon env
- (CApp ((CApp ((CApp (f, x), loc), c), loc),
+ | c1' as CApp (c', i) =>
+ let
+ fun default () = (CApp ((c1', loc), hnormCon env c2), loc)
+ in
+ case #1 (hnormCon env c') of
+ CApp (c', f) =>
+ (case #1 (hnormCon env c') of
+ CFold ks =>
+ (case #1 (hnormCon env c2) of
+ CRecord (_, []) => hnormCon env i
+ | CRecord (k, (x, c) :: rest) =>
+ hnormCon env
+ (CApp ((CApp ((CApp (f, x), loc), c), loc),
(CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- (CRecord (k, rest), loc)), loc)), loc)
- | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
- let
- val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
-
- (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
+ (CRecord (k, rest), loc)), loc)), loc)
+ | CConcat ((CRecord (k, (x, c) :: rest), _), rest') =>
+ let
+ val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc)
+
+ (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc),
+ (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
+ rest''), loc)), loc)*)
+ in
+ (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
+ hnormCon env
+ (CApp ((CApp ((CApp (f, x), loc), c), loc),
(CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- rest''), loc)), loc)*)
- in
- (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*)
- hnormCon env
- (CApp ((CApp ((CApp (f, x), loc), c), loc),
- (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc),
- rest''), loc)), loc)
- end
- | _ => cAll)
- | _ => cAll)
- | _ => cAll)
- | _ => cAll)
+ rest''), loc)), loc)
+ end
+ | _ => default ())
+ | _ => default ())
+ | _ => default ()
+ end
+ | c1' => (CApp ((c1', loc), hnormCon env c2), loc))
| CConcat (c1, c2) =>
(case (hnormCon env c1, hnormCon env c2) of
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5109feb4..8564b2dd 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -896,17 +896,28 @@ and guessFold (env, denv) (c1, c2, gs, ex) =
end
and unifyCons' (env, denv) c1 c2 =
- let
- val (c1, gs1) = hnormCon (env, denv) c1
- val (c2, gs2) = hnormCon (env, denv) c2
- in
+ case (#1 c1, #1 c2) of
+ (L'.TDisjoint (x1, y1, t1), L'.TDisjoint (x2, y2, t2)) =>
let
- val gs3 = unifyCons'' (env, denv) c1 c2
+ val gs1 = unifyCons' (env, denv) x1 x2
+ val gs2 = unifyCons' (env, denv) y1 y2
+ val (denv', gs3) = D.assert env denv (x1, y1)
+ val gs4 = unifyCons' (env, denv') t1 t2
in
- gs1 @ gs2 @ gs3
+ gs1 @ gs2 @ gs3 @ gs4
+ end
+ | _ =>
+ let
+ val (c1, gs1) = hnormCon (env, denv) c1
+ val (c2, gs2) = hnormCon (env, denv) c2
+ in
+ let
+ val gs3 = unifyCons'' (env, denv) c1 c2
+ in
+ gs1 @ gs2 @ gs3
+ end
+ handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
end
- handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex)
- end
and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) =
let
@@ -1116,12 +1127,18 @@ fun foldType (dom, loc) =
(L'.TCFun (L'.Explicit, "v", dom,
(L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc),
(L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc),
- (L'.CApp ((L'.CRel 3, loc),
- recCons (dom,
- (L'.CRel 2, loc),
- (L'.CRel 1, loc),
- (L'.CRel 0, loc),
- loc)), loc)), loc)),
+ (L'.TDisjoint ((L'.CRecord
+ ((L'.KUnit, loc),
+ [((L'.CRel 2, loc),
+ (L'.CUnit, loc))]), loc),
+ (L'.CRel 0, loc),
+ (L'.CApp ((L'.CRel 3, loc),
+ recCons (dom,
+ (L'.CRel 2, loc),
+ (L'.CRel 1, loc),
+ (L'.CRel 0, loc),
+ loc)), loc)),
+ loc)), loc)),
loc)), loc)), loc),
(L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc),
(L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc),