Ur/Web: src/elaborate.sml comparison

comparison src/elaborate.sml @ 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	588b9d16b00a
children	e68de2a5506b

comparison

equal deleted inserted replaced

-:f4f2b09a533a
+:12b73f3c108e
 case k of
 L'.KUnif (_, _, ref (SOME k)) => hnormKind k
 | _ => kAll
 open ElabOps
-val hnormCon = D.hnormCon
 fun elabConHead (c as (_, loc)) k =
 let
 fun unravel (k, c) =
 case hnormKind k of
 val (t', tk, gs) = elabCon (env', denv) t
 in
 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
 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
 val (c', ck, gs) = elabCon (env, denv) c
 val k = (L'.KRecord ktype, loc)
 fun kindof env (c, loc) =
 case c of
 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)
 | L'.CModProj (n, ms, x) =>
 let
 (case hnormKind (kindof env c) of
 (L'.KArrow (_, k), _) => k
 | (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
 | L'.CRecord (k, _) => (L'.KRecord k, loc)
 | L'.CConcat (c, _) => kindof env c
 (case hnormKind (kindof env c) of
 (L'.KFun (_, k'), _) => subKindInKind (0, k) k'
 | 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) =
 case c of
 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
 | L'.CModProj (n, ms, x) => false
 (*let
 (*(case hnormKind (kindof env c) of
 (L'.KArrow (_, k), _) => #1 k = L'.KUnit
 | (L'.KError, _) => false
 | k => raise CUnify' (CKindof (k, c, "arrow")))*)
 | L'.CAbs _ => false
-| L'.CDisjoint (_, _, _, c) => false(*isUnitCon env c*)
 | L'.CName _ => false
 | L'.CRecord _ => false
 | L'.CConcat _ => false
 | L'.CKAbs _ => false
 | 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
 (L'.KRecord k, _) => k
 | (L'.KError, _) => kerror
 | k => raise CUnify' (CKindof (k, c, "record"))
 val k1 = rkindof c1
 val k2 = rkindof c2
-val (r1, gs1) = recordSummary (env, denv) c1
+val r1 = recordSummary env c1
-val (r2, gs2) = recordSummary (env, denv) c2
+val r2 = recordSummary env c2
 in
 unifyKinds env k1 k2;
-unifySummaries (env, denv) (k1, r1, r2);
+unifySummaries env (k1, r1, r2)
-gs1 @ gs2
 end
-and recordSummary (env, denv) c =
+and recordSummary env c =
 let
-val (c, gs) = hnormCon (env, denv) c
+val c = hnormCon env c
-val (sum, gs') =
+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 s1 = recordSummary env c1
-val (s2, gs2) = recordSummary (env, denv) c2
+val s2 = recordSummary env c2
 in
-({fields = #fields s1 @ #fields s2,
+{fields = #fields s1 @ #fields s2,
 unifs = #unifs s1 @ #unifs s2,
-others = #others s1 @ #others s2},
+others = #others s1 @ #others s2}
-gs1 @ gs2)
 end
-| (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c
+| (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c
-| c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, [])
+| c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []}
-| c' => ({fields = [], unifs = [], others = [c']}, [])
+| c' => {fields = [], unifs = [], others = [c']}
 in
-(sum, gs @ gs')
+sum
 end
-and consEq (env, denv) (c1, c2) =
+and consEq env (c1, c2) =
-let
+(unifyCons env c1 c2;
-val gs = unifyCons (env, denv) c1 c2
+true)
-in
-List.all (fn (loc, env, denv, c1, c2) =>
-case D.prove env denv (c1, c2, loc) of
-[] => true
-| _ => false) gs
-end
 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),
 ("#2", p_summary env s2)]*)
 em (ls1, ls2, [])
 end
 val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) =>
 not (consNeq env (x1, x2))
-andalso consEq (env, denv) (c1, c2)
+andalso consEq env (c1, c2)
-andalso consEq (env, denv) (x1, x2))
+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})]*)
 fun unifFields (fs, others, unifs) =
 case (fs, others, unifs) of
 (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}),
 ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*)
 fun isGuessable (other, fs) =
-let
+(guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure);
-val gs = guessMap (env, denv) (other, (L'.CRecord (k, fs), loc), [], GuessFailure)
+true)
-in
-List.all (fn (loc, env, denv, c1, c2) =>
-case D.prove env denv (c1, c2, loc) of
-[] => true
-| _ => false) gs
-end
 handle GuessFailure => false
 val (fs1, fs2, others1, others2) =
 case (fs1, fs2, others1, others2) of
 ([], _, [other1], []) =>
 pairOffUnifs (unifs1, unifs2)
 (*before eprefaces "Summaries'" [("#1", p_summary env s1),
 ("#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
+case #1 c of
-val (c', gs1) = deConstraintCon (env, denv) c
+L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc)
-in
+| L'.CRecord (_, [(x, v)]) =>
-case #1 c' of
+let
-L'.CRecord (_, []) =>
+val v' = case dom of
-let
+(L'.KUnit, _) => (L'.CUnit, loc)
-val gs2 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc)
+| _ => cunif (loc, dom)
 in
-gs1 @ gs2
+unifyCons env v (L'.CApp (f, v'), loc);
-end
+unifyCons env r (L'.CRecord (dom, [(x, v')]), loc)
-| L'.CRecord (_, [(x, v)]) =>
+end
-let
+| L'.CRecord (_, (x, v) :: rest) =>
-val v' = case dom of
+let
-(L'.KUnit, _) => (L'.CUnit, loc)
+val r1 = cunif (loc, (L'.KRecord dom, loc))
-| _ => cunif (loc, dom)
+val r2 = cunif (loc, (L'.KRecord dom, loc))
-val gs2 = unifyCons (env, denv) v (L'.CApp (f, v'), loc)
+in
+unfold (r1, (L'.CRecord (ran, [(x, v)]), loc));
-val gs3 = unifyCons (env, denv) r (L'.CRecord (dom, [(x, v')]), loc)
+unfold (r2, (L'.CRecord (ran, rest), loc));
-in
+unifyCons env r (L'.CConcat (r1, r2), loc)
-gs1 @ gs2 @ gs3
+end
-end
+| L'.CConcat (c1', c2') =>
-| L'.CRecord (_, (x, v) :: rest) =>
+let
-let
+val r1 = cunif (loc, (L'.KRecord dom, loc))
-val r1 = cunif (loc, (L'.KRecord dom, loc))
+val r2 = cunif (loc, (L'.KRecord dom, loc))
-val r2 = cunif (loc, (L'.KRecord dom, loc))
+in
+unfold (r1, c1');
-val gs2 = unfold (r1, (L'.CRecord (ran, [(x, v)]), loc))
+unfold (r2, c2');
-val gs3 = unfold (r2, (L'.CRecord (ran, rest), loc))
+unifyCons env r (L'.CConcat (r1, r2), loc)
-val gs4 = unifyCons (env, denv) r (L'.CConcat (r1, r2), loc)
+end
-in
+| _ => raise ex
-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
 in
 unfold (r, c)
 end
 handle _ => (TextIO.print "Guess failure!\n"; raise ex)
 in
 | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) =>
 unfold (dom, ran, f, r, c1)
 | _ => raise ex
 end
-and unifyCons' (env, denv) c1 c2 =
+and unifyCons' env c1 c2 =
-case (#1 c1, #1 c2) of
+if isUnitCon env c1 andalso isUnitCon env c2 then
-(L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) =>
+()
+else
 let
-val gs1 = unifyCons' (env, denv) x1 x2
+(*val befor = Time.now ()
-val gs2 = unifyCons' (env, denv) y1 y2
+val old1 = c1
-val (denv', gs3) = D.assert env denv (x1, y1)
+val old2 = c2*)
-val gs4 = unifyCons' (env, denv') t1 t2
+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
+and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) =
-[]
-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, _)) =
 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 d1 d2;
-@ unifyCons' (env, denv) r1 r2
+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 d1 d2;
-unifyCons' (env, denv) r1 r2)
+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) =>
+((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2))
-let
-val gs' = unifyCons' (env, denv) c1 c2
-in
-gs' @ gs
-end) [] (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
+unifyCons' (E.pushKRel env x) c1 c2
-| (L'.CError, _) => []
+| (L'.CError, _) => ()
-| (_, L'.CError) => []
+| (_, L'.CError) => ()
 | (L'.CRecord _, _) => isRecord ()
 | (_, L'.CRecord _) => isRecord ()
 | (L'.CConcat _, _) => isRecord ()
 | (_, L'.CConcat _) => isRecord ()
 | (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 =
+and unifyCons env c1 c2 =
-unifyCons' (env, denv) 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 =
+fun checkCon env e c1 c2 =
-unifyCons (env, denv) c1 c2
+unifyCons env c1 c2
 handle CUnify (c1, c2, err) =>
-(expError env (Unify (e, c1, c2, err));
+expError env (Unify (e, c1, c2, err))
-[])
+fun checkPatCon env p c1 c2 =
-fun checkPatCon (env, denv) p c1 c2 =
+unifyCons env c1 c2
-unifyCons (env, denv) 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
 P.Int _ => !int
 | P.Float _ => !float
 Disjoint of D.goal
 | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span
 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
+case hnormCon env t of
-val (t, gs) = hnormCon (env, denv) t
+(L'.TKFun (x, t'), _) =>
-in
+let
-case t of
+val u = kunif loc
-(L'.TKFun (x, t'), _) =>
-let
+val t'' = subKindInCon (0, u) t'
-val u = kunif loc
+in
+unravel (t'', (L'.EKApp (e, u), loc))
-val t'' = subKindInCon (0, u) t'
+end
-val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc))
+| (L'.TCFun (L'.Implicit, x, k, t'), _) =>
-in
+let
-(e, t, enD gs @ gs')
+val u = cunif (loc, k)
-end
-| (L'.TCFun (L'.Implicit, x, k, t'), _) =>
+val t'' = subConInCon (0, u) t'
-let
+in
-val u = cunif (loc, k)
+unravel (t'', (L'.ECApp (e, u), loc))
+end
-val t'' = subConInCon (0, u) t'
+| (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) =>
-val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc))
+let
-in
+val cl = hnormCon env cl
-(*prefaces "Unravel" [("t'", p_con env t'),
+in
-("t''", p_con env t'')];*)
+if infer <> L.TypesOnly andalso E.isClass env cl then
-(e, t, enD gs @ gs')
+let
-end
+val r = ref NONE
-| (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) =>
+val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
-let
+in
-val cl = #1 (hnormCon (env, denv) cl)
+(e, t, TypeClass (env, dom, r, loc) :: gs)
-in
+end
-if infer <> L.TypesOnly andalso E.isClass env cl then
+else
-let
+(e, t, [])
-val r = ref NONE
+end
-val (e, t, gs') = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc))
+| t => (e, t, [])
-in
-(e, t, TypeClass (env, dom, r, loc) :: enD gs @ gs')
-end
-else
-(e, t, enD gs)
-end
-| _ => (e, t, enD gs)
-end
 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)
 val pterror = (perror, terror)
 val rerror = (pterror, (env, bound))
 (((L'.PCon (dk, pc, unifs, NONE), loc), dn),
 (env, bound))
 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
 val nxs = length unifs - 1
 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
 in
 case p of
 | L.PRecord (xps, flex) =>
 let
 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))
 else
 ();
 Wild => "Wild"
 | None => "None"
 | Datatype _ => "Datatype"
 | Record _ => "Record"
-fun exhaustive (env, denv, t, ps) =
+fun exhaustive (env, t, ps) =
 let
 fun depth (p, _) =
 case p of
 L'.PWild => 0
 | L'.PVar _ => 0
 case to of
 NONE => [Datatype (IM.insert (IM.empty, n, Wild))]
 | 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
 val cons = E.constructors dt
 in
 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
 [] => [SM.empty]
 | ((L'.CName x, _), t) :: rest =>
 r
 end
 fun isTotal (c, t) =
 case c of
-None => (false, [])
+None => false
-| Wild => (true, [])
+| Wild => true
 | Datatype cm =>
 let
-val ((t, _), gs) = hnormCon (env, denv) t
+val (t, _) = hnormCon env t
-fun dtype cons =
+val dtype =
-foldl (fn ((_, n, to), (total, gs)) =>
+List.all (fn (_, n, to) =>
 case IM.find (cm, n) of
-NONE => (false, gs)
+NONE => false
 | SOME c' =>
 case to of
-NONE => (total, gs)
+NONE => true
-| SOME t' =>
+| SOME t' => isTotal (c', t'))
-let
-val (total, gs') = isTotal (c', t')
-in
-(total, gs' @ gs)
-end)
-(true, gs) cons
 fun unapp t =
 case t of
 L'.CApp ((t, _), _) => unapp t
 | _ => t
 in
 case E.projectDatatype env {str = str, sgn = sgn, field = x} of
 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
 fun unmodCon env (c, loc) =
 end
 | _ => (c, loc)
 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) =>
 let
 val c1 = normClassKey envs c1
 (L'.CApp (f, x), loc)
 end
 | 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)];*)
 (*val befor = Time.now ()*)
 val r = case e of
 L.EAnnot (e, t) =>
 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, [])
 | L.EVar ([], s, infer) =>
 (case E.lookupE env s of
 E.NotBound =>
 (expError env (UnboundExp (loc, s));
 (eerror, cerror, []))
-| E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t
+| E.Rel (n, t) => elabHead env infer (L'.ERel n, loc) t
-| E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed 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));
 (eerror, cerror, []))
 | SOME (n, sgn) =>
 val t = case E.projectVal env {sgn = sgn, str = str, field = s} of
 NONE => (expError env (UnboundExp (loc, s));
 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 =>
 let
 val r = ref NONE
 val (e2', t2, gs2) = elabExp (env, denv) e2
 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
 val (t', gs1) = case to of
 NONE => (cunif (loc, ktype), [])
 | L.ECApp (e, c) =>
 let
 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, [])
 | L'.TCFun (_, x, k, eb) =>
 let
 ("et", p_con env oldEt),
 ("x", PD.string x),
 ("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
 | _ =>
 (expError env (WrongForm ("constructor function", e', et));
 (eerror, cerror, []))
 val (c2', k2, gs2) = elabCon (env, denv) c2
 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 (e', t, gs4) = elabExp (env, denv') e
+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 =>
 let
 val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) =>
 val ft = cunif (loc, ktype)
 val rest = cunif (loc, ktype_record)
 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
-val gs3 =
+val gs3 = D.prove env denv (first, rest, loc)
-checkCon (env, denv) e' et
-(L'.TRecord (L'.CConcat (first, rest), loc), loc)
-val gs4 = 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) =>
 let
 val (e1', e1t, gs1) = elabExp (env, denv) e1
 val (e2', e2t, gs2) = elabExp (env, denv) e2
 val r1 = cunif (loc, ktype_record)
 val r2 = cunif (loc, ktype_record)
-val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc)
+val gs3 = D.prove env denv (r1, r2, loc)
-val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc)
-val gs5 = 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
 val (e', et, gs1) = elabExp (env, denv) e
 val (c', ck, gs2) = elabCon (env, denv) c
 val ft = cunif (loc, ktype)
 val rest = cunif (loc, ktype_record)
 val first = (L'.CRecord (ktype, [(c', ft)]), loc)
-val gs3 =
+val gs3 = D.prove env denv (first, rest, loc)
-checkCon (env, denv) e' et
-(L'.TRecord (L'.CConcat (first, rest), loc), loc)
-val gs4 = 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
 val (e', et, gs1) = elabExp (env, denv) e
 val (c', ck, gs2) = elabCon (env, denv) c
 val rest = cunif (loc, ktype_record)
-val gs3 =
+val gs3 = D.prove env denv (c', rest, loc)
-checkCon (env, denv) e' et
-(L'.TRecord (L'.CConcat (c', rest), loc), loc)
-val gs4 = 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) =>
 let
 val (e', et, gs1) = elabExp (env, denv) e
 val result = cunif (loc, (L'.KType, loc))
 val (pes', gs) = ListUtil.foldlMap
 (fn ((p, e), gs) =>
 let
-val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty))
+val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty))
-val gs1 = checkPatCon (env, denv) p' pt et
+val (e', et, gs1) = elabExp (env, denv) e
-val (e', et, gs2) = elabExp (env, denv) e
-val gs3 = checkCon (env, denv) e' et result
 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) =>
 let
 val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds
 (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll),
 ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*)
 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
 L.EDVal (x, co, e) =>
 let
 val (c', _, gs1) = case co of
 NONE => (cunif (loc, ktype), ktype, [])
 | 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
 fun allowable (e, _) =
 case e of
 val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis
 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))
 end
 in
 (strerror, sgnerror))
 | SOME sgn => ((L'.StrProj (str, m), loc), sgn))
 ((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)) =
 case sgi of
 L.SgiConAbs (x, k) =>
 NONE => (conError env (UnboundStrInCon (loc, m));
 (strerror, sgnerror))
 | 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
+case hnormCon env (L'.CModProj (n, ms, s), loc) of
-((L'.CModProj (n, ms, s), _), gs) =>
+(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)
 val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs
 t xs
 in
 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, [])))
 end)
 | L.SgiConstraint (c1, c2) =>
 let
 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) =>
 let
 val k = elabKind env k
 case self str of
 NONE => sgn
 | 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
 L'.SgiConAbs (x, n, k) =>
 let
 val c = (L'.CModProj (str, strs, x), loc)
 in
 (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) =
 case d of
 L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)]
 | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)]
 | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)]
 | L'.DDatabase _ => []
 | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)]
-fun sgiBindsD (env, denv) (sgi, _) =
+fun subSgn env sgn1 (sgn2 as (_, loc2)) =
-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)) =
 ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1),
 ("sgn2", p_sgn env sgn2)];*)
 case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of
 (L'.SgnError, _) => ()
 | (_, L'.SgnError) => ()
 (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1),
 ("sgn2", p_sgn env sgn2),
 ("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 =>
 let
 val env = case #1 h of
 env
 else
 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
 L'.SgiConAbs (x, n2, k2) =>
 seek (fn (env, sgi1All as (sgi1, _)) =>
 val env = E.pushCNamedAs env x n1 k1 co1
 in
 SOME (if n1 = n2 then
 env
 else
-E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)),
+E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))
-denv)
 end
 else
 NONE
 in
 case sgi1 of
 val env = if n1 = n2 then
 env
 else
 E.pushCNamedAs env x n1 k1 (SOME c1)
 in
-SOME (env, denv)
+SOME env
 end
 in
-(case unifyCons (env, denv) c1 c2 of
+(unifyCons env c1 c2;
-[] => good ()
+good ())
-| _ => NONE)
 handle CUnify (c1, c2, err) =>
 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
 good ())
 end
 else
 let
 fun found (n1, xs1, xncs1) =
 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
 fun good () =
 env
 else
 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
 val env = if n1 = n2 then
 env
 fun xncBad ((x1, _, t1), (x2, _, t2)) =
 String.compare (x1, x2) <> EQUAL
 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
 orelse length xncs1 <> length xncs2
 orelse ListPair.exists xncBad (xncs1, xncs2) then
 fun good () =
 let
 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
+(unifyCons env t1 t2;
-[] => good ()
+good ())
-| _ => NONE)
 handle CUnify (c1, c2, err) =>
 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
 good ())
 end
 else
 | L'.SgiVal (x, n2, c2) =>
 seek (fn (env, sgi1All as (sgi1, _)) =>
 case sgi1 of
 L'.SgiVal (x', n1, c1) =>
 if x = x' then
-((*prefaces "Pre" [("c1", p_con env c1),
+(unifyCons env c1 c2;
-("c2", p_con env c2)];*)
+SOME env)
-case unifyCons (env, denv) c1 c2 of
-[] => SOME (env, denv)
-| _ => NONE)
 handle CUnify (c1, c2, err) =>
 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
-SOME (env, denv))
+SOME env)
 else
 NONE
 | _ => NONE)
 | L'.SgiStr (x, n2, sgn2) =>
 seek (fn (env, sgi1All as (sgi1, _)) =>
 case sgi1 of
 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
 else
 E.pushStrNamedAs env x n2
 (selfifyAt env {str = (L'.StrVar n1, #2 sgn2),
 sgn = sgn2})
 in
-SOME (env, denv)
+SOME env
 end
 else
 NONE
 | _ => NONE)
 seek (fn (env, sgi1All as (sgi1, _)) =>
 case sgi1 of
 L'.SgiSgn (x', n1, sgn1) =>
 if x = x' then
 let
-val () = subSgn (env, denv) sgn1 sgn2
+val () = subSgn env sgn1 sgn2
-val () = subSgn (env, denv) sgn2 sgn1
+val () = subSgn env sgn2 sgn1
 val env = E.pushSgnNamedAs env x n2 sgn2
 val env = if n1 = n2 then
 env
 else
 E.pushSgnNamedAs env x n1 sgn2
 in
-SOME (env, denv)
+SOME env
 end
 else
 NONE
 | _ => NONE)
 | L'.SgiConstraint (c2, d2) =>
 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
+if consEq env (c1, c2) andalso consEq env (d1, d2) then
-let
+SOME env
-val (denv, gs) = D.assert env denv (c2, d2)
-in
-case gs of
-[] => ()
-| _ => raise Fail "subSgn: Sub-constraints remain";
-SOME (env, denv)
-end
 else
 NONE
 | _ => NONE)
 | L'.SgiClassAbs (x, n2, k2) =>
 val env = E.pushCNamedAs env x n1 k co
 in
 SOME (if n1 = n2 then
 env
 else
-E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)),
+E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)))
-denv)
 end
 else
 NONE
 in
 case sgi1 of
 val env = if n1 = n2 then
 env
 else
 E.pushCNamedAs env x n1 k (SOME c1)
 in
-SOME (env, denv)
+SOME env
 end
 in
-(case unifyCons (env, denv) c1 c2 of
+(unifyCons env c1 c2;
-[] => good ()
+good ())
-| _ => NONE)
 handle CUnify (c1, c2, err) =>
 (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err));
 good ())
 end
 else
 L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1)
 | _ => NONE
 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)) =>
 let
 val ran2 =
 if n1 = n2 then
 ran2
 else
 subStrInSgn (n2, n1) ran2
 in
-subSgn (env, denv) dom2 dom1;
+subSgn env dom2 dom1;
-subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) ran1 ran2
+subSgn (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2
 end
 | _ => sgnError env (SgnWrongForm (sgn1, sgn2)))
 | CVar ([], x) => x <> self
 | 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
 | CName _ => true
 | TRecord c => pos c
 | 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
 | CName _ => true
 (L.StrConst (ds @ ds'), #2 str)
 end
 | _ => 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 ()*)
 val r =
 NONE => (conError env (UnboundStrInCon (loc, m));
 (strerror, sgnerror))
 | 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
+case hnormCon env (L'.CModProj (n, ms, s), loc) of
-((L'.CModProj (n, ms, s), _), gs') =>
+(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)))
 | SOME (xs, xncs) =>
 let
 t xs
 in
 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, [])))
 end)
 val (c', _, gs1) = case co of
 NONE => (cunif (loc, ktype), ktype, [])
 | 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
 fun allowable (e, _) =
 case e of
 end) env vis
 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))
 end
 | SOME (formal, gs1) =>
 let
 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
 val (env', n) = E.pushStrNamed env x sgn'
 in
 NONE => (strError env (UnboundStr (loc, m));
 (strerror, sgnerror))
 | 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 (ds, env') = dopen env {str = n, strs = ms, sgn = sgn}
-val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms}
+val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms}
 in
 (ds, (env', denv', gs))
 end)
 | L.DConstraint (c1, c2) =>
 let
 val (c1', k1, gs1) = elabCon (env, denv) c1
 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) =>
 let
 val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms}
 fun doOne (all as (sgi, _), env) =
 (case sgi of
 L'.SgiVal (x, n, t) =>
 let
 fun doPage (makeRes, ran) =
-case hnormCon (env, denv) ran of
+case hnormCon env ran of
-((L'.CApp (tf, arg), _), []) =>
+(L'.CApp (tf, arg), _) =>
-(case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of
+(case (hnormCon env tf, hnormCon env arg) of
-(((L'.CModProj (basis, [], "transaction"), _), []),
+((L'.CModProj (basis, [], "transaction"), _),
-((L'.CApp (tf, arg3), _), [])) =>
+(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'.CApp (tf, arg2), _),
-(((L'.CRecord (_, []), _), []))) =>
+((L'.CRecord (_, []), _))) =>
-(case (hnormCon (env, denv) tf) of
+(case (hnormCon env tf) of
-((L'.CApp (tf, arg1), _), []) =>
+(L'.CApp (tf, arg1), _) =>
-(case (hnormCon (env, denv) tf,
+(case (hnormCon env tf,
-hnormCon (env, denv) arg1,
+hnormCon env arg1,
-hnormCon (env, denv) arg2) of
+hnormCon env arg2) of
-((tf, []), (arg1, []),
+(tf, arg1,
-((L'.CRecord (_, []), _), [])) =>
+(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 (
 | _ => all)
 | _ => all)
 | _ => all)
 | _ => all
 in
-case hnormCon (env, denv) t of
+case hnormCon env t of
-((L'.TFun (dom, ran), _), []) =>
+(L'.TFun (dom, ran), _) =>
-(case hnormCon (env, denv) dom of
+(case hnormCon env dom of
-((L'.TRecord domR, _), []) =>
+(L'.TRecord domR, _) =>
 doPage (fn t => (L'.TFun ((L'.TRecord domR,
 loc),
 t), loc), ran)
 | _ => all)
 | _ => doPage (fn t => t, t)
 NONE => (actual, [])
 | SOME ran =>
 let
 val (ran', gs) = elabSgn (env', denv) ran
 in
-subSgn (env', denv) actual ran';
+subSgn env' actual ran';
 (ran', gs)
 end
 in
 ((L'.StrFun (m, n, dom', formal, str'), loc),
 (L'.SgnFun (m, n, dom', formal), loc),
 val (str2', sgn2, gs2) = elabStr (env, denv) str2
 in
 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 =>
 ((L'.StrApp (str1', str2'), loc),
 (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc),
 raise Fail "Unresolved disjointness constraints in Basis")
 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
 E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis")
 | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis")
 case E.resolveClass env c of
 SOME e => r := SOME e
 | 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
 val () = resetKunif ()
 val () = resetCunif ()

Mercurial > urweb

comparison src/elaborate.sml @ 628:12b73f3c108e