diff options
Diffstat (limited to 'src/elaborate.sml')
| -rw-r--r-- | src/elaborate.sml | 65 |
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 |