summaryrefslogtreecommitdiff
path: root/src/elaborate.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-12 11:08:00 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-12 11:08:00 -0400
commit0f0d418e2290cdf5e6e392f65579756b37661be9 (patch)
treed4d5c202be4912da6d99166ecc5d1de3413f4c93 /src/elaborate.sml
parent30eeaff2c92fb1d0ba029a7688fc7b547a60c150 (diff)
hello compiles with CSS
Diffstat (limited to 'src/elaborate.sml')
-rw-r--r--src/elaborate.sml65
1 files changed, 42 insertions, 23 deletions
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 922c9c32..792ab315 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -3284,30 +3284,40 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) =
(L'.CApp (tf, arg), _) =>
(case (hnormCon env tf, hnormCon env arg) of
((L'.CModProj (basis, [], "transaction"), _),
- (L'.CApp (tf, arg3), _)) =>
+ (L'.CApp (tf, arg4), _)) =>
(case (basis = !basis_r,
- hnormCon env tf, hnormCon env arg3) of
+ hnormCon env tf, hnormCon env arg4) of
(true,
- (L'.CApp (tf, arg2), _),
+ (L'.CApp (tf, arg3), _),
((L'.CRecord (_, []), _))) =>
- (case (hnormCon env tf) of
- (L'.CApp (tf, arg1), _) =>
- (case (hnormCon env tf,
- hnormCon env arg1,
- hnormCon env arg2) of
- (tf, arg1,
- (L'.CRecord (_, []), _)) =>
- let
- val t = (L'.CApp (tf, arg1), loc)
- val t = (L'.CApp (t, arg2), loc)
- val t = (L'.CApp (t, arg3), loc)
- val t = (L'.CApp (
- (L'.CModProj
- (basis, [], "transaction"), loc),
+ (case hnormCon env tf of
+ (L'.CApp (tf, arg2), _) =>
+ (case hnormCon env tf of
+ (L'.CApp (tf, arg1), _) =>
+ (case (hnormCon env tf,
+ hnormCon env arg1,
+ hnormCon env arg2,
+ hnormCon env arg3,
+ hnormCon env arg4) of
+ (tf,
+ arg1,
+ (L'.CRecord (_, []), _),
+ arg2,
+ arg4) =>
+ let
+ val t = (L'.CApp (tf, arg1), loc)
+ val t = (L'.CApp (t, arg2), loc)
+ val t = (L'.CApp (t, arg3), loc)
+ val t = (L'.CApp (t, arg4), loc)
+
+ val t = (L'.CApp (
+ (L'.CModProj
+ (basis, [], "transaction"), loc),
t), loc)
- in
- (L'.SgiVal (x, n, makeRes t), loc)
- end
+ in
+ (L'.SgiVal (x, n, makeRes t), loc)
+ end
+ | _ => all)
| _ => all)
| _ => all)
| _ => all)
@@ -3622,6 +3632,16 @@ fun elabFile basis topStr topSgn env file =
[] => ()
| _ => raise Fail "Unresolved disjointness constraints in top.urs"
val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan)
+
+ val () = subSgn env' topSgn' topSgn
+
+ val () = app (fn (env, k, s1, s2) =>
+ unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)
+ handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in Top final record unification";
+ cunifyError env err))
+ (!delayedUnifs)
+ val () = delayedUnifs := []
+
val () = case gs of
[] => ()
| _ => app (fn Disjoint (loc, env, denv, c1, c2) =>
@@ -3631,7 +3651,8 @@ fun elabFile basis topStr topSgn env file =
(prefaces "Unresolved constraint in top.ur"
[("loc", PD.string (ErrorMsg.spanToString loc)),
("c1", p_con env c1),
- ("c2", p_con env c2)];
+ ("c2", p_con env c2),
+ ("topStr", p_str env topStr)];
raise Fail "Unresolved constraint in top.ur"))
| TypeClass (env, c, r, loc) =>
let
@@ -3642,8 +3663,6 @@ fun elabFile basis topStr topSgn env file =
| NONE => expError env (Unresolvable (loc, c))
end) gs
- val () = subSgn env' topSgn' topSgn
-
val (env', top_n) = E.pushStrNamed env' "Top" topSgn
val () = top_r := top_n