summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2012-05-19 11:32:24 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2012-05-19 11:32:24 -0400
commit2a2a9f56384d8914561d000d50b6b900ad474597 (patch)
tree1e70503e18823b764b2d3eb3ff889b52a3804953
parentdf475a9256347564d3adc1fafc53c4d93b4e73f7 (diff)
parent5da2212753a33c1865a6595d12d4c8bfb41db99e (diff)
Merge
-rw-r--r--src/elaborate.sml122
1 files changed, 77 insertions, 45 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 07a1d976..8436c975 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -1444,7 +1444,7 @@
case hnormCon env c of
(L'.TRecord c, _) => U.Con.exists {kind = fn _ => false,
con = fn c =>
- E.isClass env (hnormCon env (c, loc))} c
+ isClassOrFolder env (hnormCon env (c, loc))} c
| c =>
let
fun findHead c =
@@ -4591,11 +4591,11 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
()
else
let
- fun solver gs =
+ fun solver (gs : constraint list) =
let
val (gs, solved) =
ListUtil.foldlMapPartial
- (fn (g, solved) =>
+ (fn (g : constraint, solved) =>
case g of
Disjoint (loc, env, denv, c1, c2) =>
(case D.prove env denv (c1, c2, loc) of
@@ -4604,48 +4604,80 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
| TypeClass (env, c, r, loc) =>
let
fun default () = (SOME g, solved)
-
- val c = normClassKey env c
+
+ fun resolver r c =
+ let
+ val c = normClassKey env c
+ in
+ case resolveClass env c of
+ SOME e => (r := SOME e;
+ (NONE, true))
+ | NONE =>
+ case #1 (hnormCon env c) of
+ L'.CApp (f, x) =>
+ (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
+ (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
+ (case #1 (hnormCon env f) of
+ L'.CModProj (top_n', [], "folder") =>
+ if top_n' = top_n then
+ let
+ val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
+ val e = (L'.EKApp (e, k), loc)
+
+ val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
+ let
+ val e = (L'.EModProj (top_n, ["Folder"],
+ "cons"), loc)
+ val e = (L'.EKApp (e, k), loc)
+ val e = (L'.ECApp (e,
+ (L'.CRecord (k, xcs),
+ loc)), loc)
+ val e = (L'.ECApp (e, x), loc)
+ val e = (L'.ECApp (e, c), loc)
+ val e = (L'.EApp (e, folder), loc)
+ in
+ (e, (x, c) :: xcs)
+ end)
+ (e, []) xcs
+ in
+ (r := SOME folder;
+ (NONE, true))
+ end
+ else
+ default ()
+ | _ => default ())
+ | _ => default ())
+
+ | L'.TRecord c' =>
+ (case #1 (hnormCon env c') of
+ L'.CRecord (_, xts) =>
+ let
+ val witnesses = map (fn (x, t) =>
+ let
+ val r = ref NONE
+ val (opt, _) = resolver r t
+ in
+ case opt of
+ SOME _ => NONE
+ | NONE =>
+ case !r of
+ NONE => NONE
+ | SOME e =>
+ SOME (x, e, t)
+ end) xts
+ in
+ if List.all Option.isSome witnesses then
+ (r := SOME (L'.ERecord (map valOf witnesses), loc);
+ (NONE, true))
+ else
+ (SOME g, solved)
+ end
+ | _ => (SOME g, solved))
+
+ | _ => default ()
+ end
in
- case resolveClass env c of
- SOME e => (r := SOME e;
- (NONE, true))
- | NONE =>
- case #1 (hnormCon env c) of
- L'.CApp (f, x) =>
- (case (#1 (hnormCon env f), #1 (hnormCon env x)) of
- (L'.CKApp (f, _), L'.CRecord (k, xcs)) =>
- (case #1 (hnormCon env f) of
- L'.CModProj (top_n', [], "folder") =>
- if top_n' = top_n then
- let
- val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc)
- val e = (L'.EKApp (e, k), loc)
-
- val (folder, _) = foldr (fn ((x, c), (folder, xcs)) =>
- let
- val e = (L'.EModProj (top_n, ["Folder"],
- "cons"), loc)
- val e = (L'.EKApp (e, k), loc)
- val e = (L'.ECApp (e,
- (L'.CRecord (k, xcs),
- loc)), loc)
- val e = (L'.ECApp (e, x), loc)
- val e = (L'.ECApp (e, c), loc)
- val e = (L'.EApp (e, folder), loc)
- in
- (e, (x, c) :: xcs)
- end)
- (e, []) xcs
- in
- (r := SOME folder;
- (NONE, true))
- end
- else
- default ()
- | _ => default ())
- | _ => default ())
- | _ => default ()
+ resolver r c
end)
false gs
in
@@ -4685,7 +4717,7 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file =
val c = normClassKey env c
in
case resolveClass env c of
- SOME _ => ()
+ SOME e => r := SOME e
| NONE => expError env (Unresolvable (loc, c))
end)
gs)