Mercurial > urweb
changeset 628:12b73f3c108e
Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Tue, 24 Feb 2009 12:01:24 -0500 |
| parents | f4f2b09a533a |
| children | e68de2a5506b |
| files | lib/ur/top.ur lib/ur/top.urs src/disjoint.sig src/disjoint.sml src/elab.sml src/elab_err.sml src/elab_ops.sml src/elab_print.sml src/elab_util.sml src/elaborate.sml src/explify.sml src/source.sml src/source_print.sml src/urweb.grm |
| diffstat | 14 files changed, 387 insertions(+), 549 deletions(-) [+] |
line wrap: on
line diff
--- a/lib/ur/top.ur Sun Feb 22 17:39:55 2009 -0500 +++ b/lib/ur/top.ur Tue Feb 24 12:01:24 2009 -0500 @@ -17,6 +17,18 @@ (f : nm :: Name -> v :: K -> r :: {K} -> tf r -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) (i : tf []) = f [nm] [v] [r] (fold [tf] f i) + + fun concat K (r1 ::: {K}) (r2 ::: {K}) [r1 ~ r2] + (f1 : folder r1) (f2 : folder r2) + (tf :: {K} -> Type) + (f : nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + (i : tf []) = + f1 [fn r1' [r1' ~ r2] => tf (r1' ++ r2)] 0 + (*(fn (nm :: Name) (v :: K) (r1' :: {K}) (acc : fn [r1' ~ r2] => tf (r1' ++ r2)) + [[nm] ~ r1'] [[nm = v] ++ r1' ~ r2] => + f [nm] [v] [r1' ++ r2] acc) + (f2 [tf] f i)*) end
--- a/lib/ur/top.urs Sun Feb 22 17:39:55 2009 -0500 +++ b/lib/ur/top.urs Tue Feb 24 12:01:24 2009 -0500 @@ -10,6 +10,8 @@ val nil : K --> folder (([]) :: {K}) val cons : K --> r ::: {K} -> nm :: Name -> v :: K -> fn [[nm] ~ r] => folder r -> folder ([nm = v] ++ r) + val concat : K --> r1 ::: {K} -> r2 ::: {K} + -> fn [r1 ~ r2] => folder r1 -> folder r2 -> folder (r1 ++ r2) end
--- a/src/disjoint.sig Sun Feb 22 17:39:55 2009 -0500 +++ b/src/disjoint.sig Tue Feb 24 12:01:24 2009 -0500 @@ -34,12 +34,10 @@ type goal = ErrorMsg.span * ElabEnv.env * env * Elab.con * Elab.con - val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env * goal list + val assert : ElabEnv.env -> env -> Elab.con * Elab.con -> env val prove : ElabEnv.env -> env -> Elab.con * Elab.con * ErrorMsg.span -> goal list - val hnormCon : ElabEnv.env * env -> Elab.con -> Elab.con * goal list - val p_env : env -> unit end
--- a/src/disjoint.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/disjoint.sml Tue Feb 24 12:01:24 2009 -0500 @@ -161,70 +161,65 @@ NONE => false | SOME pset => PS.member (pset, p2) -fun decomposeRow (env, denv) c = +fun decomposeRow env c = let val loc = #2 c fun decomposeProj c = let - val (c, gs) = hnormCon (env, denv) c + val c = hnormCon env c in case #1 c of CProj (c, n) => let - val (c', ns, gs') = decomposeProj c + val (c', ns) = decomposeProj c in - (c', ns @ [n], gs @ gs') + (c', ns @ [n]) end - | _ => (c, [], gs) + | _ => (c, []) end - fun decomposeName (c, (acc, gs)) = + fun decomposeName (c, acc) = let - val (cAll as (c, _), ns, gs') = decomposeProj c - - val acc = case c of - CName s => Piece (NameC s, ns) :: acc - | CRel n => Piece (NameR n, ns) :: acc - | CNamed n => Piece (NameN n, ns) :: acc - | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc - | _ => Unknown cAll :: acc + val (cAll as (c, _), ns) = decomposeProj c in - (acc, gs' @ gs) + case c of + CName s => Piece (NameC s, ns) :: acc + | CRel n => Piece (NameR n, ns) :: acc + | CNamed n => Piece (NameN n, ns) :: acc + | CModProj (m1, ms, x) => Piece (NameM (m1, ms, x), ns) :: acc + | _ => Unknown cAll :: acc end - fun decomposeRow' (c, (acc, gs)) = + fun decomposeRow' (c, acc) = let fun default () = let - val (cAll as (c, _), ns, gs') = decomposeProj c - val gs = gs' @ gs + val (cAll as (c, _), ns) = decomposeProj c in case c of - CRecord (_, xcs) => foldl (fn ((x, _), acc_gs) => decomposeName (x, acc_gs)) (acc, gs) xcs - | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, (acc, gs))) - | CRel n => (Piece (RowR n, ns) :: acc, gs) - | CNamed n => (Piece (RowN n, ns) :: acc, gs) - | CModProj (m1, ms, x) => (Piece (RowM (m1, ms, x), ns) :: acc, gs) - | _ => (Unknown cAll :: acc, gs) + CRecord (_, xcs) => foldl (fn ((x, _), acc) => decomposeName (x, acc)) acc xcs + | CConcat (c1, c2) => decomposeRow' (c1, decomposeRow' (c2, acc)) + | CRel n => Piece (RowR n, ns) :: acc + | CNamed n => Piece (RowN n, ns) :: acc + | CModProj (m1, ms, x) => Piece (RowM (m1, ms, x), ns) :: acc + | _ => Unknown cAll :: acc 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 + case #1 (hnormCon env c) of CApp ( (CApp ((CMap _, _), _), _), - r) => decomposeRow' (r, (acc, gs)) + r) => decomposeRow' (r, acc) | _ => default () end in - decomposeRow' (c, ([], [])) + decomposeRow' (c, []) end and assert env denv (c1, c2) = let - val (ps1, gs1) = decomposeRow (env, denv) c1 - val (ps2, gs2) = decomposeRow (env, denv) c2 + val ps1 = decomposeRow env c1 + val ps2 = decomposeRow env c2 val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) val ps1 = unUnknown ps1 @@ -248,13 +243,13 @@ val denv = foldl (assertPiece ps2) denv ps1 in - (foldl (assertPiece ps1) denv ps2, gs1 @ gs2) + foldl (assertPiece ps1) denv ps2 end and prove env denv (c1, c2, loc) = let - val (ps1, gs1) = decomposeRow (env, denv) c1 - val (ps2, gs2) = decomposeRow (env, denv) c2 + val ps1 = decomposeRow env c1 + val ps2 = decomposeRow env c2 val hasUnknown = List.exists (fn Unknown _ => true | _ => false) val unUnknown = List.mapPartial (fn Unknown _ => NONE | Piece p => SOME p) @@ -265,7 +260,6 @@ let val ps1 = unUnknown ps1 val ps2 = unUnknown ps2 - in (*print "Pieces1:\n"; app pp ps1; @@ -278,24 +272,8 @@ rem else (loc, env, denv, pieceToRow (p1, loc), pieceToRow (p2, loc)) :: rem) rem ps2) - (gs1 @ gs2) ps1 + [] ps1 end end -and hnormCon (env, denv) c = - let - val cAll as (c, loc) = ElabOps.hnormCon env c - - fun doDisj (c1, c2, c) = - let - val (c, gs) = hnormCon (env, denv) c - in - (c, prove env denv (c1, c2, loc) @ gs) - end - in - case c of - CDisjoint (Instantiate, c1, c2, c) => doDisj (c1, c2, c) - | _ => (cAll, []) - end - end
--- a/src/elab.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elab.sml Tue Feb 24 12:01:24 2009 -0500 @@ -49,21 +49,17 @@ Explicit | Implicit -datatype auto_instantiate = - Instantiate - | LeaveAlone - datatype con' = TFun of con * con | TCFun of explicitness * string * kind * con | TRecord of con + | TDisjoint of con * con * con | CRel of int | CNamed of int | CModProj of int * string list * string | CApp of con * con | CAbs of string * kind * con - | CDisjoint of auto_instantiate * con * con * con | CKAbs of string * con | CKApp of con * kind
--- a/src/elab_err.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elab_err.sml Tue Feb 24 12:01:24 2009 -0500 @@ -40,7 +40,7 @@ con = fn env => fn c => let val c = (c, ErrorMsg.dummySpan) - val (c', _) = Disjoint.hnormCon (env, Disjoint.empty) c + val c' = ElabOps.hnormCon env c in (*prefaces "simpl" [("c", P.p_con env c), ("c'", P.p_con env c')];*)
--- a/src/elab_ops.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elab_ops.sml Tue Feb 24 12:01:24 2009 -0500 @@ -194,7 +194,7 @@ let fun unconstraint c = case hnormCon env c of - (CDisjoint (_, _, _, c), _) => unconstraint c + (TDisjoint (_, _, c), _) => unconstraint c | c => c fun tryDistributivity () =
--- a/src/elab_print.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elab_print.sml Tue Feb 24 12:01:24 2009 -0500 @@ -91,17 +91,17 @@ string "->", space, p_con (E.pushCRel env x k) c]) - | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1, - space, - string (case ai of - Instantiate => "~" - | LeaveAlone => "~~"), - space, - p_con env c2, - space, - string "=>", - space, - p_con env c3]) + | TDisjoint (c1, c2, c3) => parenIf par (box [string "[", + p_con env c1, + space, + string "~", + space, + p_con env c2, + string "]", + space, + string "=>", + space, + p_con env c3]) | TRecord (CRecord (_, xcs), _) => box [string "{", p_list (fn (x, c) => box [p_name env x,
--- a/src/elab_util.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elab_util.sml Tue Feb 24 12:01:24 2009 -0500 @@ -136,14 +136,14 @@ S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) - | CDisjoint (ai, c1, c2, c3) => + | TDisjoint (c1, c2, c3) => S.bind2 (mfc ctx c1, fn c1' => S.bind2 (mfc ctx c2, fn c2' => S.map2 (mfc ctx c3, fn c3' => - (CDisjoint (ai, c1', c2', c3'), loc)))) + (TDisjoint (c1', c2', c3'), loc)))) | TRecord c => S.map2 (mfc ctx c, fn c' =>
--- a/src/elaborate.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/elaborate.sml Tue Feb 24 12:01:24 2009 -0500 @@ -208,7 +208,6 @@ | _ => kAll open ElabOps - val hnormCon = D.hnormCon fun elabConHead (c as (_, loc)) k = let @@ -265,7 +264,7 @@ checkKind env t' tk ktype; ((L'.TKFun (x, t'), loc), ktype, gs) end - | L.CDisjoint (c1, c2, c) => + | L.TDisjoint (c1, c2, c) => let val (c1', k1, gs1) = elabCon (env, denv) c1 val (c2', k2, gs2) = elabCon (env, denv) c2 @@ -273,13 +272,13 @@ val ku1 = kunif loc val ku2 = kunif loc - val (denv', gs3) = D.assert env denv (c1', c2') + val denv' = D.assert env denv (c1', c2') val (c', k, gs4) = elabCon (env, denv') c in checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) + ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs4) end | L.TRecord c => let @@ -515,6 +514,7 @@ L'.TFun _ => ktype | L'.TCFun _ => ktype | L'.TRecord _ => ktype + | L'.TDisjoint _ => ktype | L'.CRel xn => #2 (E.lookupCRel env xn) | L'.CNamed xn => #2 (E.lookupCNamed env xn) @@ -538,7 +538,7 @@ | (L'.KError, _) => kerror | k => raise CUnify' (CKindof (k, c, "arrow"))) | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) - | L'.CDisjoint (_, _, _, c) => kindof env c + | L'.CName _ => kname @@ -564,20 +564,6 @@ | k => raise CUnify' (CKindof (k, c, "kapp"))) | L'.TKFun _ => ktype - fun deConstraintCon (env, denv) c = - let - val (c, gs) = hnormCon (env, denv) c - in - case #1 c of - L'.CDisjoint (_, _, _, c) => - let - val (c', gs') = deConstraintCon (env, denv) c - in - (c', gs @ gs') - end - | _ => (c, gs) - end - exception GuessFailure fun isUnitCon env (c, loc) = @@ -585,6 +571,7 @@ L'.TFun _ => false | L'.TCFun _ => false | L'.TRecord _ => false + | L'.TDisjoint _ => false | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit @@ -608,7 +595,6 @@ | (L'.KError, _) => false | k => raise CUnify' (CKindof (k, c, "arrow")))*) | L'.CAbs _ => false - | L'.CDisjoint (_, _, _, c) => false(*isUnitCon env c*) | L'.CName _ => false @@ -631,7 +617,7 @@ | L'.CKApp _ => false | L'.TKFun _ => false - fun unifyRecordCons (env, denv) (c1, c2) = + fun unifyRecordCons env (c1, c2) = let fun rkindof c = case hnormKind (kindof env c) of @@ -642,55 +628,47 @@ val k1 = rkindof c1 val k2 = rkindof c2 - val (r1, gs1) = recordSummary (env, denv) c1 - val (r2, gs2) = recordSummary (env, denv) c2 + val r1 = recordSummary env c1 + val r2 = recordSummary env c2 in unifyKinds env k1 k2; - unifySummaries (env, denv) (k1, r1, r2); - gs1 @ gs2 + unifySummaries env (k1, r1, r2) end - and recordSummary (env, denv) c = + and recordSummary env c = let - val (c, gs) = hnormCon (env, denv) c - - val (sum, gs') = + val c = hnormCon env c + + val sum = case c of - (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, []) + (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []} | (L'.CConcat (c1, c2), _) => let - val (s1, gs1) = recordSummary (env, denv) c1 - val (s2, gs2) = recordSummary (env, denv) c2 + val s1 = recordSummary env c1 + val s2 = recordSummary env c2 in - ({fields = #fields s1 @ #fields s2, - unifs = #unifs s1 @ #unifs s2, - others = #others s1 @ #others s2}, - gs1 @ gs2) + {fields = #fields s1 @ #fields s2, + unifs = #unifs s1 @ #unifs s2, + others = #others s1 @ #others s2} end - | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c - | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, []) - | c' => ({fields = [], unifs = [], others = [c']}, []) + | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c + | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} + | c' => {fields = [], unifs = [], others = [c']} in - (sum, gs @ gs') + sum end - and consEq (env, denv) (c1, c2) = - let - val gs = unifyCons (env, denv) c1 c2 - in - List.all (fn (loc, env, denv, c1, c2) => - case D.prove env denv (c1, c2, loc) of - [] => true - | _ => false) gs - end + and consEq env (c1, c2) = + (unifyCons env c1 c2; + true) handle CUnify _ => false and consNeq env (c1, c2) = - case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of + case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of (L'.CName x1, L'.CName x2) => x1 <> x2 | _ => false - and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) = + and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = let val loc = #2 k (*val () = eprefaces "Summaries" [("#1", p_summary env s1), @@ -720,13 +698,13 @@ val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) => not (consNeq env (x1, x2)) - andalso consEq (env, denv) (c1, c2) - andalso consEq (env, denv) (x1, x2)) + andalso consEq env (c1, c2) + andalso consEq env (x1, x2)) (#fields s1, #fields s2) (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) - val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2) + val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) @@ -763,14 +741,8 @@ ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) fun isGuessable (other, fs) = - let - val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure) - in - List.all (fn (loc, env, denv, c1, c2) => - case D.prove env denv (c1, c2, loc) of - [] => true - | _ => false) gs - end + (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure); + true) handle GuessFailure => false val (fs1, fs2, others1, others2) = @@ -827,58 +799,43 @@ ("#2", p_summary env s2)]*) end - and guessMap (env, denv) (c1, c2, gs, ex) = + and guessMap env (c1, c2, ex) = let val loc = #2 c1 fun unfold (dom, ran, f, r, c) = let fun unfold (r, c) = - let - val (c', gs1) = deConstraintCon (env, denv) c - in - case #1 c' of - L'.CRecord (_, []) => - let - val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) - in - gs1 @ gs2 - end - | L'.CRecord (_, [(x, v)]) => - let - val v' = case dom of - (L'.KUnit, _) => (L'.CUnit, loc) - | _ => cunif (loc, dom) - val gs2 = unifyCons (env, denv) v (L'.CApp (f, v'), loc) - - val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc) - in - gs1 @ gs2 @ gs3 - end - | L'.CRecord (_, (x, v) :: rest) => - let - val r1 = cunif (loc, (L'.KRecord dom, loc)) - val r2 = cunif (loc, (L'.KRecord dom, loc)) - - val gs2 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)) - val gs3 = unfold (r2, (L'.CRecord (ran, rest), loc)) - val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) - in - gs1 @ gs2 @ gs3 @ gs4 - end - | L'.CConcat (c1', c2') => - let - val r1 = cunif (loc, (L'.KRecord dom, loc)) - val r2 = cunif (loc, (L'.KRecord dom, loc)) - - val gs2 = unfold (r1, c1') - val gs3 = unfold (r2, c2') - val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc) - in - gs1 @ gs2 @ gs3 @ gs4 - end - | _ => raise ex - end + case #1 c of + L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc) + | L'.CRecord (_, [(x, v)]) => + let + val v' = case dom of + (L'.KUnit, _) => (L'.CUnit, loc) + | _ => cunif (loc, dom) + in + unifyCons env v (L'.CApp (f, v'), loc); + unifyCons env r (L'.CRecord (dom, [(x, v')]), loc) + end + | L'.CRecord (_, (x, v) :: rest) => + let + val r1 = cunif (loc, (L'.KRecord dom, loc)) + val r2 = cunif (loc, (L'.KRecord dom, loc)) + in + unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)); + unfold (r2, (L'.CRecord (ran, rest), loc)); + unifyCons env r (L'.CConcat (r1, r2), loc) + end + | L'.CConcat (c1', c2') => + let + val r1 = cunif (loc, (L'.KRecord dom, loc)) + val r2 = cunif (loc, (L'.KRecord dom, loc)) + in + unfold (r1, c1'); + unfold (r2, c2'); + unifyCons env r (L'.CConcat (r1, r2), loc) + end + | _ => raise ex in unfold (r, c) end @@ -892,151 +849,128 @@ | _ => raise ex end - and unifyCons' (env, denv) c1 c2 = - case (#1 c1, #1 c2) of - (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) => + and unifyCons' env c1 c2 = + if isUnitCon env c1 andalso isUnitCon env c2 then + () + else let - 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 + (*val befor = Time.now () + val old1 = c1 + val old2 = c2*) + val c1 = hnormCon env c1 + val c2 = hnormCon env c2 in - gs1 @ gs2 @ gs3 @ gs4 + unifyCons'' env c1 c2 + handle ex => guessMap env (c1, c2, ex) end - | _ => - if isUnitCon env c1 andalso isUnitCon env c2 then - [] - else - let - (*val befor = Time.now () - val old1 = c1 - val old2 = c2*) - val (c1, gs1) = hnormCon (env, denv) c1 - val (c2, gs2) = hnormCon (env, denv) c2 - in - let - (*val () = prefaces "unifyCons'" [("old1", p_con env old1), - ("old2", p_con env old2), - ("c1", p_con env c1), - ("c2", p_con env c2)]*) - - val gs3 = unifyCons'' (env, denv) c1 c2 - in - gs1 @ gs2 @ gs3 - end - handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex) - end - - and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = + + and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) = let fun err f = raise CUnify' (f (c1All, c2All)) - fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) + fun isRecord () = unifyRecordCons env (c1All, c2All) in (*eprefaces "unifyCons''" [("c1All", p_con env c1All), ("c2All", p_con env c2All)];*) case (c1, c2) of - (L'.CUnit, L'.CUnit) => [] + (L'.CUnit, L'.CUnit) => () | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => - unifyCons' (env, denv) d1 d2 - @ unifyCons' (env, denv) r1 r2 + (unifyCons' env d1 d2; + unifyCons' env r1 r2) | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => if expl1 <> expl2 then err CExplicitness else (unifyKinds env d1 d2; let - val denv' = D.enter denv (*val befor = Time.now ()*) val env' = E.pushCRel env x1 d1 in (*TextIO.print ("E.pushCRel: " ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) ^ "\n");*) - unifyCons' (env', denv') r1 r2 + unifyCons' env' r1 r2 end) - | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2 + | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 + | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => + (unifyCons' env c1 c2; + unifyCons' env d1 d2; + unifyCons' env e1 e2) | (L'.CRel n1, L'.CRel n2) => if n1 = n2 then - [] + () else err CIncompatible | (L'.CNamed n1, L'.CNamed n2) => if n1 = n2 then - [] + () else err CIncompatible | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => - (unifyCons' (env, denv) d1 d2; - unifyCons' (env, denv) r1 r2) + (unifyCons' env d1 d2; + unifyCons' env r1 r2) | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => (unifyKinds env k1 k2; - unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) + unifyCons' (E.pushCRel env x1 k1) c1 c2) | (L'.CName n1, L'.CName n2) => if n1 = n2 then - [] + () else err CIncompatible | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then - [] + () else err CIncompatible | (L'.CTuple cs1, L'.CTuple cs2) => - ((ListPair.foldlEq (fn (c1, c2, gs) => - let - val gs' = unifyCons' (env, denv) c1 c2 - in - gs' @ gs - end) [] (cs1, cs2)) + ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) handle ListPair.UnequalLengths => err CIncompatible) | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) => - unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All + unifyCons' env (L'.CProj (c1, n1), loc) c2All | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) => - unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc) + unifyCons' env c1All (L'.CProj (c2, n2), loc) | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) => let val us = map (fn k => cunif (loc, k)) ks in r := SOME (L'.CTuple us, loc); - unifyCons' (env, denv) (List.nth (us, n - 1)) c2All + unifyCons' env (List.nth (us, n - 1)) c2All end | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) => let val us = map (fn k => cunif (loc, k)) ks in r := SOME (L'.CTuple us, loc); - unifyCons' (env, denv) c1All (List.nth (us, n - 1)) + unifyCons' env c1All (List.nth (us, n - 1)) end | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => if n1 = n2 then - unifyCons' (env, denv) c1 c2 + unifyCons' env c1 c2 else err CIncompatible | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => (unifyKinds env dom1 dom2; - unifyKinds env ran1 ran2; - []) + unifyKinds env ran1 ran2) | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => - unifyCons' (E.pushKRel env x, denv) c1 c2 + unifyCons' (E.pushKRel env x) c1 c2 | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => (unifyKinds env k1 k2; - unifyCons' (env, denv) c1 c2) + unifyCons' env c1 c2) | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => - unifyCons' (E.pushKRel env x, denv) c1 c2 - - | (L'.CError, _) => [] - | (_, L'.CError) => [] + unifyCons' (E.pushKRel env x) c1 c2 + + | (L'.CError, _) => () + | (_, L'.CError) => () | (L'.CRecord _, _) => isRecord () | (_, L'.CRecord _) => isRecord () @@ -1045,44 +979,39 @@ | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => if r1 = r2 then - [] + () else (unifyKinds env k1 k2; - r1 := SOME c2All; - []) + r1 := SOME c2All) | (L'.CUnif (_, _, _, r), _) => if occursCon r c2All then err COccursCheckFailed else - (r := SOME c2All; - []) + r := SOME c2All | (_, L'.CUnif (_, _, _, r)) => if occursCon r c1All then err COccursCheckFailed else - (r := SOME c1All; - []) + r := SOME c1All | _ => err CIncompatible end - and unifyCons (env, denv) c1 c2 = - unifyCons' (env, denv) c1 c2 + and unifyCons env c1 c2 = + unifyCons' env c1 c2 handle CUnify' err => raise CUnify (c1, c2, err) | KUnify args => raise CUnify (c1, c2, CKind args) - fun checkCon (env, denv) e c1 c2 = - unifyCons (env, denv) c1 c2 + fun checkCon env e c1 c2 = + unifyCons env c1 c2 handle CUnify (c1, c2, err) => - (expError env (Unify (e, c1, c2, err)); - []) - - fun checkPatCon (env, denv) p c1 c2 = - unifyCons (env, denv) c1 c2 + expError env (Unify (e, c1, c2, err)) + + fun checkPatCon env p c1 c2 = + unifyCons env c1 c2 handle CUnify (c1, c2, err) => - (expError env (PatUnify (p, c1, c2, err)); - []) + expError env (PatUnify (p, c1, c2, err)) fun primType env p = case p of @@ -1096,56 +1025,48 @@ val enD = map Disjoint - fun elabHead (env, denv) infer (e as (_, loc)) t = + fun elabHead env infer (e as (_, loc)) t = let fun unravel (t, e) = - let - val (t, gs) = hnormCon (env, denv) t - in - case t of - (L'.TKFun (x, t'), _) => - let - val u = kunif loc - - val t'' = subKindInCon (0, u) t' - val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc)) - in - (e, t, enD gs @ gs') - end - | (L'.TCFun (L'.Implicit, x, k, t'), _) => - let - val u = cunif (loc, k) - - val t'' = subConInCon (0, u) t' - val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc)) - in - (*prefaces "Unravel" [("t'", p_con env t'), - ("t''", p_con env t'')];*) - (e, t, enD gs @ gs') - end - | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) => - let - val cl = #1 (hnormCon (env, denv) cl) - in - if infer <> L.TypesOnly andalso E.isClass env cl then - let - val r = ref NONE - val (e, t, gs') = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) - in - (e, t, TypeClass (env, dom, r, loc) :: enD gs @ gs') - end - else - (e, t, enD gs) - end - | _ => (e, t, enD gs) - end + case hnormCon env t of + (L'.TKFun (x, t'), _) => + let + val u = kunif loc + + val t'' = subKindInCon (0, u) t' + in + unravel (t'', (L'.EKApp (e, u), loc)) + end + | (L'.TCFun (L'.Implicit, x, k, t'), _) => + let + val u = cunif (loc, k) + + val t'' = subConInCon (0, u) t' + in + unravel (t'', (L'.ECApp (e, u), loc)) + end + | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) => + let + val cl = hnormCon env cl + in + if infer <> L.TypesOnly andalso E.isClass env cl then + let + val r = ref NONE + val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) + in + (e, t, TypeClass (env, dom, r, loc) :: gs) + end + else + (e, t, []) + end + | t => (e, t, []) in case infer of L.DontInfer => (e, t, []) | _ => unravel (t, e) end -fun elabPat (pAll as (p, loc), (env, denv, bound)) = +fun elabPat (pAll as (p, loc), (env, bound)) = let val perror = (L'.PWild, loc) val terror = (L'.CError, loc) @@ -1169,7 +1090,7 @@ end | (SOME p, SOME t) => let - val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) + val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) val k = (L'.KType, loc) val unifs = map (fn _ => cunif (loc, k)) xs @@ -1177,7 +1098,7 @@ val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in - ignore (checkPatCon (env, denv) p' pt t); + ignore (checkPatCon env p' pt t); (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), (env, bound)) end @@ -1226,7 +1147,7 @@ val (xpts, (env, bound, _)) = ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) => let - val ((p', t), (env, bound)) = elabPat (p, (env, denv, bound)) + val ((p', t), (env, bound)) = elabPat (p, (env, bound)) in if SS.member (fbound, x) then expError env (DuplicatePatField (loc, x)) @@ -1264,7 +1185,7 @@ | Datatype _ => "Datatype" | Record _ => "Record" -fun exhaustive (env, denv, t, ps) = +fun exhaustive (env, t, ps) = let fun depth (p, _) = case p of @@ -1331,7 +1252,7 @@ | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) (enumerateCases (depth-1) t)) cons in - case #1 (#1 (hnormCon (env, denv) t)) of + case #1 (hnormCon env t) of L'.CNamed n => (let val dt = E.lookupDatatype env n @@ -1340,10 +1261,10 @@ dtype cons end handle E.UnboundNamed _ => [Wild]) | L'.TRecord c => - (case #1 (#1 (hnormCon (env, denv) c)) of + (case #1 (hnormCon env c) of L'.CRecord (_, xts) => let - val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts + val xts = map (fn (x, t) => (hnormCon env x, t)) xts fun exponentiate fs = case fs of @@ -1405,26 +1326,20 @@ fun isTotal (c, t) = case c of - None => (false, []) - | Wild => (true, []) + None => false + | Wild => true | Datatype cm => let - val ((t, _), gs) = hnormCon (env, denv) t - - fun dtype cons = - foldl (fn ((_, n, to), (total, gs)) => - case IM.find (cm, n) of - NONE => (false, gs) - | SOME c' => - case to of - NONE => (total, gs) - | SOME t' => - let - val (total, gs') = isTotal (c', t') - in - (total, gs' @ gs) - end) - (true, gs) cons + val (t, _) = hnormCon env t + + val dtype = + List.all (fn (_, n, to) => + case IM.find (cm, n) of + NONE => false + | SOME c' => + case to of + NONE => true + | SOME t' => isTotal (c', t')) fun unapp t = case t of @@ -1447,12 +1362,12 @@ NONE => raise Fail "isTotal: Can't project datatype" | SOME (_, cons) => dtype cons end - | L'.CError => (true, gs) + | L'.CError => true | c => (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; raise Fail "isTotal: Not a datatype") end - | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t), []) + | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t) in isTotal (combinedCoverage ps, t) end @@ -1476,7 +1391,7 @@ fun normClassKey envs c = let - val c = ElabOps.hnormCon envs c + val c = hnormCon envs c in case #1 c of L'.CApp (c1, c2) => @@ -1501,18 +1416,6 @@ | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c | _ => (c, loc) - -val makeInstantiable = - let - fun kind k = k - fun con c = - case c of - L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c) - | _ => c - in - U.Con.map {kind = kind, con = con} - end - fun elabExp (env, denv) (eAll as (e, loc)) = let (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) @@ -1523,9 +1426,9 @@ let val (e', et, gs1) = elabExp (env, denv) e val (t', _, gs2) = elabCon (env, denv) t - val gs3 = checkCon (env, denv) e' et t' in - (e', t', gs1 @ enD gs2 @ enD gs3) + checkCon env e' et t'; + (e', t', gs1 @ enD gs2) end | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) @@ -1534,8 +1437,8 @@ E.NotBound => (expError env (UnboundExp (loc, s)); (eerror, cerror, [])) - | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t - | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t) + | E.Rel (n, t) => elabHead env infer (L'.ERel n, loc) t + | E.Named (n, t) => elabHead env infer (L'.ENamed n, loc) t) | L.EVar (m1 :: ms, s, infer) => (case E.lookupStr env m1 of NONE => (expError env (UnboundStrInExp (loc, m1)); @@ -1554,7 +1457,7 @@ cerror) | SOME t => t in - elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t + elabHead env infer (L'.EModProj (n, ms, s), loc) t end) | L.EWild => @@ -1573,13 +1476,10 @@ val dom = cunif (loc, ktype) val ran = cunif (loc, ktype) val t = (L'.TFun (dom, ran), dummy) - - val gs3 = checkCon (env, denv) e1' t1 t - val gs4 = checkCon (env, denv) e2' t2 dom - - val gs = gs1 @ gs2 @ enD gs3 @ enD gs4 in - ((L'.EApp (e1', e2'), loc), ran, gs) + checkCon env e1' t1 t; + checkCon env e2' t2 dom; + ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2) end | L.EAbs (x, to, e) => let @@ -1604,7 +1504,7 @@ val (e', et, gs1) = elabExp (env, denv) e val oldEt = et val (c', ck, gs2) = elabCon (env, denv) c - val ((et', _), gs3) = hnormCon (env, denv) et + val (et', _) = hnormCon env et in case et' of L'.CError => (eerror, cerror, []) @@ -1621,7 +1521,7 @@ ("eb", p_con (E.pushCRel env x k) eb), ("c", p_con env c'), ("eb'", p_con env eb')];*) - ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2 @ enD gs3) + ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2) end | _ => @@ -1658,13 +1558,13 @@ val ku1 = kunif loc val ku2 = kunif loc - val (denv', gs3) = D.assert env denv (c1', c2') - val (e', t, gs4) = elabExp (env, denv') e + val denv' = D.assert env denv (c1', c2') + val (e', t, gs3) = elabExp (env, denv') e in checkKind env c1' k1 (L'.KRecord ku1, loc); checkKind env c2' k2 (L'.KRecord ku2, loc); - (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) + (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3) end | L.ERecord xes => @@ -1718,12 +1618,11 @@ val rest = cunif (loc, ktype_record) val first = (L'.CRecord (ktype, [(c', ft)]), loc) - val gs3 = - checkCon (env, denv) e' et - (L'.TRecord (L'.CConcat (first, rest), loc), loc) - val gs4 = D.prove env denv (first, rest, loc) + val gs3 = D.prove env denv (first, rest, loc) in - ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) + checkCon env e' et + (L'.TRecord (L'.CConcat (first, rest), loc), loc); + ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3) end | L.EConcat (e1, e2) => @@ -1734,13 +1633,13 @@ val r1 = cunif (loc, ktype_record) val r2 = cunif (loc, ktype_record) - val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc) - val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc) - val gs5 = D.prove env denv (r1, r2, loc) + val gs3 = D.prove env denv (r1, r2, loc) in + checkCon env e1' e1t (L'.TRecord r1, loc); + checkCon env e2' e2t (L'.TRecord r2, loc); ((L'.EConcat (e1', r1, e2', r2), loc), (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), - gs1 @ gs2 @ enD gs3 @ enD gs4 @ enD gs5) + gs1 @ gs2 @ enD gs3) end | L.ECut (e, c) => let @@ -1751,13 +1650,12 @@ val rest = cunif (loc, ktype_record) val first = (L'.CRecord (ktype, [(c', ft)]), loc) - val gs3 = - checkCon (env, denv) e' et - (L'.TRecord (L'.CConcat (first, rest), loc), loc) - val gs4 = D.prove env denv (first, rest, loc) + val gs3 = D.prove env denv (first, rest, loc) in + checkCon env e' et + (L'.TRecord (L'.CConcat (first, rest), loc), loc); ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), - gs1 @ enD gs2 @ enD gs3 @ enD gs4) + gs1 @ enD gs2 @ enD gs3) end | L.ECutMulti (e, c) => let @@ -1766,13 +1664,12 @@ val rest = cunif (loc, ktype_record) - val gs3 = - checkCon (env, denv) e' et - (L'.TRecord (L'.CConcat (c', rest), loc), loc) - val gs4 = D.prove env denv (c', rest, loc) + val gs3 = D.prove env denv (c', rest, loc) in + checkCon env e' et + (L'.TRecord (L'.CConcat (c', rest), loc), loc); ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), - gs1 @ enD gs2 @ enD gs3 @ enD gs4) + gs1 @ enD gs2 @ enD gs3) end | L.ECase (e, pes) => @@ -1782,24 +1679,22 @@ val (pes', gs) = ListUtil.foldlMap (fn ((p, e), gs) => let - val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty)) - - val gs1 = checkPatCon (env, denv) p' pt et - val (e', et, gs2) = elabExp (env, denv) e - val gs3 = checkCon (env, denv) e' et result + val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) + + val (e', et, gs1) = elabExp (env, denv) e in - ((p', e'), enD gs1 @ gs2 @ enD gs3 @ gs) + checkPatCon env p' pt et; + checkCon env e' et result; + ((p', e'), gs1 @ gs) end) gs1 pes - - val (total, gs') = exhaustive (env, denv, et, map #1 pes') in - if total then + if exhaustive (env, et, map #1 pes') then () else expError env (Inexhaustive loc); - ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) + ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) end | L.ELet (eds, e) => @@ -1815,7 +1710,7 @@ r end -and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = +and elabEdecl denv (dAll as (d, loc), (env, gs)) = let val r = case d of @@ -1826,12 +1721,12 @@ | SOME c => elabCon (env, denv) c val (e', et, gs2) = elabExp (env, denv) e - val gs3 = checkCon (env, denv) e' et c' + val c' = normClassConstraint env c' val env' = E.pushERel env x c' - val c' = makeInstantiable c' in - ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ gs)) + checkCon env e' et c'; + ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ gs)) end | L.EDValRec vis => let @@ -1858,16 +1753,13 @@ val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) => let val (e', et, gs1) = elabExp (env, denv) e - - val gs2 = checkCon (env, denv) e' et c' - - val c' = makeInstantiable c' in + checkCon env e' et c'; if allowable e then () else expError env (IllegalRec (x, e')); - ((x, c', e'), gs1 @ enD gs2 @ gs) + ((x, c', e'), gs1 @ gs) end) gs vis in ((L'.EDValRec vis, loc), (env, gs)) @@ -1896,22 +1788,12 @@ ((L'.StrVar n, loc), sgn) strs val cso = E.projectConstraints env {sgn = sgn, str = st} - - val denv = case cso of - NONE => (strError env (UnboundStr (loc, str)); - denv) - | SOME cs => foldl (fn ((c1, c2), denv) => - let - val (denv, gs) = D.assert env denv (c1, c2) - in - case gs of - [] => () - | _ => raise Fail "dopenConstraints: Sub-constraints remain"; - - denv - end) denv cs in - denv + case cso of + NONE => (strError env (UnboundStr (loc, str)); + denv) + | SOME cs => foldl (fn ((c1, c2), denv) => + D.assert env denv (c1, c2)) denv cs end fun elabSgn_item ((sgi, loc), (env, denv, gs)) = @@ -1997,11 +1879,11 @@ | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) ms in - case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of - ((L'.CModProj (n, ms, s), _), gs) => + case hnormCon env (L'.CModProj (n, ms, s), loc) of + (L'.CModProj (n, ms, s), _) => (case E.projectDatatype env {sgn = sgn, str = str, field = s} of NONE => (conError env (UnboundDatatype (loc, s)); - ([], (env, denv, gs))) + ([], (env, denv, []))) | SOME (xs, xncs) => let val k = (L'.KType, loc) @@ -2025,7 +1907,7 @@ E.pushENamedAs env x n t end) env xncs in - ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) + ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, [])) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -2076,12 +1958,12 @@ val (c1', k1, gs1) = elabCon (env, denv) c1 val (c2', k2, gs2) = elabCon (env, denv) c2 - val (denv, gs3) = D.assert env denv (c1', c2') + val denv = D.assert env denv (c1', c2') in checkKind env c1' k1 (L'.KRecord (kunif loc), loc); checkKind env c2' k2 (L'.KRecord (kunif loc), loc); - ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) + ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) end | L.SgiClassAbs (x, k) => @@ -2280,14 +2162,14 @@ | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} end -fun dopen (env, denv) {str, strs, sgn} = +fun dopen env {str, strs, sgn} = let val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) (L'.StrVar str, #2 sgn) strs in case #1 (hnormSgn env sgn) of L'.SgnConst sgis => - ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => + ListUtil.foldlMap (fn ((sgi, loc), env') => let val d = case sgi of @@ -2326,11 +2208,11 @@ (L'.DCon (x, n, k', c), loc) end in - (d, (E.declBinds env' d, denv')) + (d, E.declBinds env' d) end) - (env, denv) sgis + env sgis | _ => (strError env (UnOpenable sgn); - ([], (env, denv))) + ([], env)) end fun sgiOfDecl (d, loc) = @@ -2351,15 +2233,7 @@ | L'.DDatabase _ => [] | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] -fun sgiBindsD (env, denv) (sgi, _) = - case sgi of - L'.SgiConstraint (c1, c2) => - (case D.assert env denv (c1, c2) of - (denv, []) => denv - | _ => raise Fail "sgiBindsD: Sub-constraints remain") - | _ => denv - -fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = +fun subSgn env sgn1 (sgn2 as (_, loc2)) = ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), ("sgn2", p_sgn env sgn2)];*) case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of @@ -2373,16 +2247,16 @@ ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) - fun folder (sgi2All as (sgi, loc), (env, denv)) = + fun folder (sgi2All as (sgi, loc), env) = let (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) fun seek p = let - fun seek (env, denv) ls = + fun seek env ls = case ls of [] => (sgnError env (UnmatchedSgi sgi2All); - (env, denv)) + env) | h :: t => case p (env, h) of NONE => @@ -2400,11 +2274,11 @@ E.pushCNamedAs env x n k NONE | _ => env in - seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t + seek (E.sgiBinds env h) t end | SOME envs => envs in - seek (env, denv) sgis1 + seek env sgis1 end in case sgi of @@ -2422,8 +2296,7 @@ SOME (if n1 = n2 then env else - E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)), - denv) + E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2))) end else NONE @@ -2470,12 +2343,11 @@ else E.pushCNamedAs env x n1 k1 (SOME c1) in - SOME (env, denv) + SOME env end in - (case unifyCons (env, denv) c1 c2 of - [] => good () - | _ => NONE) + (unifyCons env c1 c2; + good ()) handle CUnify (c1, c2, err) => (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); good ()) @@ -2497,7 +2369,7 @@ let fun mismatched ue = (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); - SOME (env, denv)) + SOME env) val k = (L'.KType, loc) val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 @@ -2511,7 +2383,7 @@ E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc)) in - SOME (env, denv) + SOME env end val env = E.pushCNamedAs env x n1 k' NONE @@ -2525,7 +2397,7 @@ orelse case (t1, t2) of (NONE, NONE) => false | (SOME t1, SOME t2) => - not (List.null (unifyCons (env, denv) t1 t2)) + (unifyCons env t1 t2; false) | _ => true in (if xs1 <> xs2 @@ -2567,12 +2439,11 @@ val env = E.pushCNamedAs env x n1 k' (SOME t1) val env = E.pushCNamedAs env x n2 k' (SOME t2) in - SOME (env, denv) + SOME env end in - (case unifyCons (env, denv) t1 t2 of - [] => good () - | _ => NONE) + (unifyCons env t1 t2; + good ()) handle CUnify (c1, c2, err) => (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); good ()) @@ -2587,14 +2458,11 @@ case sgi1 of L'.SgiVal (x', n1, c1) => if x = x' then - ((*prefaces "Pre" [("c1", p_con env c1), - ("c2", p_con env c2)];*) - case unifyCons (env, denv) c1 c2 of - [] => SOME (env, denv) - | _ => NONE) + (unifyCons env c1 c2; + SOME env) handle CUnify (c1, c2, err) => (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); - SOME (env, denv)) + SOME env) else NONE | _ => NONE) @@ -2605,7 +2473,7 @@ L'.SgiStr (x', n1, sgn1) => if x = x' then let - val () = subSgn (env, denv) sgn1 sgn2 + val () = subSgn env sgn1 sgn2 val env = E.pushStrNamedAs env x n1 sgn1 val env = if n1 = n2 then env @@ -2614,7 +2482,7 @@ (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), sgn = sgn2}) in - SOME (env, denv) + SOME env end else NONE @@ -2626,8 +2494,8 @@ L'.SgiSgn (x', n1, sgn1) => if x = x' then let - val () = subSgn (env, denv) sgn1 sgn2 - val () = subSgn (env, denv) sgn2 sgn1 + val () = subSgn env sgn1 sgn2 + val () = subSgn env sgn2 sgn1 val env = E.pushSgnNamedAs env x n2 sgn2 val env = if n1 = n2 then @@ -2635,7 +2503,7 @@ else E.pushSgnNamedAs env x n1 sgn2 in - SOME (env, denv) + SOME env end else NONE @@ -2645,16 +2513,8 @@ seek (fn (env, sgi1All as (sgi1, _)) => case sgi1 of L'.SgiConstraint (c1, d1) => - if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then - let - val (denv, gs) = D.assert env denv (c2, d2) - in - case gs of - [] => () - | _ => raise Fail "subSgn: Sub-constraints remain"; - - SOME (env, denv) - end + if consEq env (c1, c2) andalso consEq env (d1, d2) then + SOME env else NONE | _ => NONE) @@ -2675,8 +2535,7 @@ SOME (if n1 = n2 then env else - E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)), - denv) + E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2))) end else NONE @@ -2706,12 +2565,11 @@ else E.pushCNamedAs env x n1 k (SOME c1) in - SOME (env, denv) + SOME env end in - (case unifyCons (env, denv) c1 c2 of - [] => good () - | _ => NONE) + (unifyCons env c1 c2; + good ()) handle CUnify (c1, c2, err) => (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); good ()) @@ -2725,7 +2583,7 @@ end) end in - ignore (foldl folder (env, denv) sgis2) + ignore (foldl folder env sgis2) end | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => @@ -2736,8 +2594,8 @@ else subStrInSgn (n2, n1) ran2 in - subSgn (env, denv) dom2 dom1; - subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) ran1 ran2 + subSgn env dom2 dom1; + subSgn (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2 end | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) @@ -2759,7 +2617,7 @@ | CVar _ => true | CApp (c1, c2) => none c1 andalso none c2 | CAbs _ => false - | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 | CKAbs _ => false | TKFun _ => false @@ -2788,7 +2646,7 @@ | CVar _ => true | CApp (c1, c2) => pos c1 andalso none c2 | CAbs _ => false - | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 | CKAbs _ => false | TKFun _ => false @@ -2971,7 +2829,7 @@ | _ => str) | _ => str -fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = +fun elabDecl (dAll as (d, loc), (env, denv, gs)) = let (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) (*val befor = Time.now ()*) @@ -3060,8 +2918,8 @@ | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) ms in - case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of - ((L'.CModProj (n, ms, s), _), gs') => + case hnormCon env (L'.CModProj (n, ms, s), loc) of + (L'.CModProj (n, ms, s), _) => (case E.projectDatatype env {sgn = sgn, str = str, field = s} of NONE => (conError env (UnboundDatatype (loc, s)); ([], (env, denv, gs))) @@ -3087,7 +2945,7 @@ E.pushENamedAs env x n t end) env xncs in - ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs)) + ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) end) | _ => (strError env (NotDatatype loc); ([], (env, denv, []))) @@ -3100,14 +2958,13 @@ | SOME c => elabCon (env, denv) c val (e', et, gs2) = elabExp (env, denv) e - val gs3 = checkCon (env, denv) e' et c' val c = normClassConstraint env c' val (env', n) = E.pushENamed env x c' - val c' = makeInstantiable c' in + checkCon env e' et c'; (*prefaces "DVal" [("x", Print.PD.string x), ("c'", p_con env c')];*) - ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ gs)) + ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs)) end | L.DValRec vis => let @@ -3139,16 +2996,13 @@ val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => let val (e', et, gs1) = elabExp (env, denv) e - - val gs2 = checkCon (env, denv) e' et c' - - val c' = makeInstantiable c' in + checkCon env e' et c'; if allowable e then () else expError env (IllegalRec (x, e')); - ((x, n, c', e'), gs1 @ enD gs2 @ gs) + ((x, n, c', e'), gs1 @ gs) end) gs vis in ([(L'.DValRec vis, loc)], (env, denv, gs)) @@ -3184,7 +3038,7 @@ val str = wildifyStr env (str, formal) val (str', actual, gs2) = elabStr (env, denv) str in - subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal; + subSgn env (selfifyAt env {str = str', sgn = actual}) formal; (str', formal, enD gs1 @ gs2) end @@ -3222,8 +3076,8 @@ | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) ((L'.StrVar n, loc), sgn) ms - val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} - val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} + val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} + val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms} in (ds, (env', denv', gs)) end) @@ -3234,12 +3088,12 @@ val (c2', k2, gs2) = elabCon (env, denv) c2 val gs3 = D.prove env denv (c1', c2', loc) - val (denv', gs4) = D.assert env denv (c1', c2') + val denv' = D.assert env denv (c1', c2') in checkKind env c1' k1 (L'.KRecord (kunif loc), loc); checkKind env c2' k2 (L'.KRecord (kunif loc), loc); - ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs)) + ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs)) end | L.DOpenConstraints (m, ms) => @@ -3262,23 +3116,23 @@ L'.SgiVal (x, n, t) => let fun doPage (makeRes, ran) = - case hnormCon (env, denv) ran of - ((L'.CApp (tf, arg), _), []) => - (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of - (((L'.CModProj (basis, [], "transaction"), _), []), - ((L'.CApp (tf, arg3), _), [])) => + case hnormCon env ran of + (L'.CApp (tf, arg), _) => + (case (hnormCon env tf, hnormCon env arg) of + ((L'.CModProj (basis, [], "transaction"), _), + (L'.CApp (tf, arg3), _)) => (case (basis = !basis_r, - hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of + hnormCon env tf, hnormCon env arg3) of (true, - ((L'.CApp (tf, arg2), _), []), - (((L'.CRecord (_, []), _), []))) => - (case (hnormCon (env, denv) tf) of - ((L'.CApp (tf, arg1), _), []) => - (case (hnormCon (env, denv) tf, - hnormCon (env, denv) arg1, - hnormCon (env, denv) arg2) of - ((tf, []), (arg1, []), - ((L'.CRecord (_, []), _), [])) => + (L'.CApp (tf, arg2), _), + ((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) @@ -3296,10 +3150,10 @@ | _ => all) | _ => all in - case hnormCon (env, denv) t of - ((L'.TFun (dom, ran), _), []) => - (case hnormCon (env, denv) dom of - ((L'.TRecord domR, _), []) => + case hnormCon env t of + (L'.TFun (dom, ran), _) => + (case hnormCon env dom of + (L'.TRecord domR, _) => doPage (fn t => (L'.TFun ((L'.TRecord domR, loc), t), loc), ran) @@ -3507,7 +3361,7 @@ let val (ran', gs) = elabSgn (env', denv) ran in - subSgn (env', denv) actual ran'; + subSgn env' actual ran'; (ran', gs) end in @@ -3528,7 +3382,7 @@ case #1 (hnormSgn env sgn1) of L'.SgnError => (strerror, sgnerror, []) | L'.SgnFun (m, n, dom, ran) => - (subSgn (env, denv) sgn2 dom; + (subSgn env sgn2 dom; case #1 (hnormSgn env ran) of L'.SgnError => (strerror, sgnerror, []) | L'.SgnConst sgis => @@ -3554,7 +3408,7 @@ val (env', basis_n) = E.pushStrNamed env "Basis" sgn val () = basis_r := basis_n - val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} + val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} fun discoverC r x = case E.lookupC env' x of @@ -3592,11 +3446,11 @@ | NONE => expError env (Unresolvable (loc, c)) end) gs - val () = subSgn (env', D.empty) topSgn' topSgn + val () = subSgn env' topSgn' topSgn val (env', top_n) = E.pushStrNamed env' "Top" topSgn - val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn} + val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} fun elabDecl' (d, (env, gs)) = let
--- a/src/explify.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/explify.sml Tue Feb 24 12:01:24 2009 -0500 @@ -52,7 +52,7 @@ case c of L.TFun (t1, t2) => (L'.TFun (explifyCon t1, explifyCon t2), loc) | L.TCFun (_, x, k, t) => (L'.TCFun (x, explifyKind k, explifyCon t), loc) - | L.CDisjoint (_, _, _, c) => explifyCon c + | L.TDisjoint (_, _, t) => explifyCon t | L.TRecord c => (L'.TRecord (explifyCon c), loc) | L.CRel n => (L'.CRel n, loc)
--- a/src/source.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/source.sml Tue Feb 24 12:01:24 2009 -0500 @@ -53,11 +53,11 @@ | TFun of con * con | TCFun of explicitness * string * kind * con | TRecord of con + | TDisjoint of con * con * con | CVar of string list * string | CApp of con * con | CAbs of string * kind option * con - | CDisjoint of con * con * con | CKAbs of string * con | TKFun of string * con
--- a/src/source_print.sml Sun Feb 22 17:39:55 2009 -0500 +++ b/src/source_print.sml Tue Feb 24 12:01:24 2009 -0500 @@ -98,6 +98,17 @@ string "}"] | TRecord c => box [string "$", p_con' true c] + | TDisjoint (c1, c2, c3) => parenIf par (box [string "[", + p_con c1, + space, + string "~", + space, + p_con c2, + string "]", + space, + string "=>", + space, + p_con c3]) | CVar (ss, s) => p_list_sep (string ".") string (ss @ [s]) | CApp (c1, c2) => parenIf par (box [p_con c1, @@ -121,15 +132,7 @@ string "=>", space, p_con c]) - | CDisjoint (c1, c2, c3) => parenIf par (box [p_con c1, - space, - string "~", - space, - p_con c2, - space, - string "=>", - space, - p_con c3]) + | CName s => box [string "#", string s]
--- a/src/urweb.grm Sun Feb 22 17:39:55 2009 -0500 +++ b/src/urweb.grm Tue Feb 24 12:01:24 2009 -0500 @@ -594,6 +594,7 @@ | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) + | LBRACK cexp TWIDDLE cexp RBRACK DARROW cexp (TDisjoint (cexp1, cexp2, cexp3), s (LBRACKleft, cexp3right)) | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -657,13 +658,7 @@ ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) - | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => - let - val loc = s (LBRACKleft, RBRACKright) - in - ((CDisjoint (cexp1, cexp2, c), loc), - k) - end) + path : SYMBOL ([], SYMBOL) | CSYMBOL DOT path (let val (ms, x) = path in (CSYMBOL :: ms, x) end) @@ -849,14 +844,14 @@ val loc = s (LPARENleft, RPARENright) in ((EDisjoint (cexp1, cexp2, e), loc), - (CDisjoint (cexp1, cexp2, t), loc)) + (TDisjoint (cexp1, cexp2, t), loc)) end) | LBRACK cexp TWIDDLE cexp RBRACK(fn (e, t) => let val loc = s (LBRACKleft, RBRACKright) in ((EDisjoint (cexp1, cexp2, e), loc), - (CDisjoint (cexp1, cexp2, t), loc)) + (TDisjoint (cexp1, cexp2, t), loc)) end) | CSYMBOL (fn (e, t) => let