adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * All rights reserved. adamc@2: * adamc@2: * Redistribution and use in source and binary forms, with or without adamc@2: * modification, are permitted provided that the following conditions are met: adamc@2: * adamc@2: * - Redistributions of source code must retain the above copyright notice, adamc@2: * this list of conditions and the following disclaimer. adamc@2: * - Redistributions in binary form must reproduce the above copyright notice, adamc@2: * this list of conditions and the following disclaimer in the documentation adamc@2: * and/or other materials provided with the distribution. adamc@2: * - The names of contributors may not be used to endorse or promote products adamc@2: * derived from this software without specific prior written permission. adamc@2: * adamc@2: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@2: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@2: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@2: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@2: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@2: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@2: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@2: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@2: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@2: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@2: * POSSIBILITY OF SUCH DAMAGE. adamc@2: *) adamc@2: adamc@2: structure Elaborate :> ELABORATE = struct adamc@2: adamc@14: structure P = Prim adamc@4: structure L = Source adamc@2: structure L' = Elab adamc@2: structure E = ElabEnv adamc@2: structure U = ElabUtil adamc@82: structure D = Disjoint adamc@2: adamc@3: open Print adamc@3: open ElabPrint adamc@329: open ElabErr adamc@3: adamc@172: structure IM = IntBinaryMap adamc@175: adamc@175: structure SK = struct adamc@175: type ord_key = string adamc@175: val compare = String.compare adamc@175: end adamc@175: adamc@175: structure SS = BinarySetFn(SK) adamc@175: structure SM = BinaryMapFn(SK) adamc@62: adamc@210: val basis_r = ref 0 adamc@210: adamc@2: fun elabExplicitness e = adamc@2: case e of adamc@2: L.Explicit => L'.Explicit adamc@2: | L.Implicit => L'.Implicit adamc@2: adamc@2: fun occursKind r = adamc@76: U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' adamc@2: | _ => false) adamc@2: adamc@3: exception KUnify' of kunify_error adamc@3: adamc@3: fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = adamc@2: let adamc@3: fun err f = raise KUnify' (f (k1All, k2All)) adamc@2: in adamc@2: case (k1, k2) of adamc@2: (L'.KType, L'.KType) => () adamc@82: | (L'.KUnit, L'.KUnit) => () adamc@82: adamc@2: | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => adamc@3: (unifyKinds' d1 d2; adamc@3: unifyKinds' r1 r2) adamc@2: | (L'.KName, L'.KName) => () adamc@3: | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 adamc@207: | (L'.KTuple ks1, L'.KTuple ks2) => adamc@207: ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) adamc@207: handle ListPair.UnequalLengths => err KIncompatible) adamc@2: adamc@2: | (L'.KError, _) => () adamc@2: | (_, L'.KError) => () adamc@2: adamc@76: | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All adamc@76: | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All adamc@2: adamc@76: | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => adamc@2: if r1 = r2 then adamc@2: () adamc@2: else adamc@2: r1 := SOME k2All adamc@2: adamc@76: | (L'.KUnif (_, _, r), _) => adamc@2: if occursKind r k2All then adamc@2: err KOccursCheckFailed adamc@2: else adamc@2: r := SOME k2All adamc@76: | (_, L'.KUnif (_, _, r)) => adamc@2: if occursKind r k1All then adamc@2: err KOccursCheckFailed adamc@2: else adamc@2: r := SOME k1All adamc@2: adamc@2: | _ => err KIncompatible adamc@2: end adamc@2: adamc@3: exception KUnify of L'.kind * L'.kind * kunify_error adamc@3: adamc@3: fun unifyKinds k1 k2 = adamc@3: unifyKinds' k1 k2 adamc@3: handle KUnify' err => raise KUnify (k1, k2, err) adamc@3: adamc@5: fun checkKind env c k1 k2 = adamc@3: unifyKinds k1 k2 adamc@3: handle KUnify (k1, k2, err) => adamc@5: conError env (WrongKind (c, k1, k2, err)) adamc@3: adamc@3: val dummy = ErrorMsg.dummySpan adamc@3: adamc@3: val ktype = (L'.KType, dummy) adamc@3: val kname = (L'.KName, dummy) adamc@12: val ktype_record = (L'.KRecord ktype, dummy) adamc@3: adamc@3: val cerror = (L'.CError, dummy) adamc@3: val kerror = (L'.KError, dummy) adamc@10: val eerror = (L'.EError, dummy) adamc@31: val sgnerror = (L'.SgnError, dummy) adamc@31: val strerror = (L'.StrError, dummy) adamc@3: adamc@56: val int = ref cerror adamc@56: val float = ref cerror adamc@56: val string = ref cerror adamc@203: val table = ref cerror adamc@56: adamc@3: local adamc@3: val count = ref 0 adamc@3: in adamc@3: adamc@3: fun resetKunif () = count := 0 adamc@3: adamc@76: fun kunif loc = adamc@3: let adamc@3: val n = !count adamc@3: val s = if n <= 26 then adamc@3: str (chr (ord #"A" + n)) adamc@3: else adamc@3: "U" ^ Int.toString (n - 26) adamc@3: in adamc@3: count := n + 1; adamc@76: (L'.KUnif (loc, s, ref NONE), dummy) adamc@3: end adamc@3: adamc@3: end adamc@3: adamc@10: local adamc@10: val count = ref 0 adamc@10: in adamc@10: adamc@10: fun resetCunif () = count := 0 adamc@10: adamc@76: fun cunif (loc, k) = adamc@10: let adamc@10: val n = !count adamc@10: val s = if n <= 26 then adamc@10: str (chr (ord #"A" + n)) adamc@10: else adamc@10: "U" ^ Int.toString (n - 26) adamc@10: in adamc@10: count := n + 1; adamc@76: (L'.CUnif (loc, k, s, ref NONE), dummy) adamc@10: end adamc@10: adamc@10: end adamc@10: adamc@18: fun elabKind (k, loc) = adamc@18: case k of adamc@18: L.KType => (L'.KType, loc) adamc@18: | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) adamc@18: | L.KName => (L'.KName, loc) adamc@18: | L.KRecord k => (L'.KRecord (elabKind k), loc) adamc@82: | L.KUnit => (L'.KUnit, loc) adamc@207: | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) adamc@76: | L.KWild => kunif loc adamc@18: adamc@67: fun foldKind (dom, ran, loc)= adamc@67: (L'.KArrow ((L'.KArrow ((L'.KName, loc), adamc@67: (L'.KArrow (dom, adamc@67: (L'.KArrow (ran, ran), loc)), loc)), loc), adamc@67: (L'.KArrow (ran, adamc@67: (L'.KArrow ((L'.KRecord dom, loc), adamc@67: ran), loc)), loc)), loc) adamc@67: adamc@207: fun hnormKind (kAll as (k, _)) = adamc@207: case k of adamc@207: L'.KUnif (_, _, ref (SOME k)) => hnormKind k adamc@207: | _ => kAll adamc@207: adamc@83: fun elabCon (env, denv) (c, loc) = adamc@3: case c of adamc@3: L.CAnnot (c, k) => adamc@3: let adamc@3: val k' = elabKind k adamc@83: val (c', ck, gs) = elabCon (env, denv) c adamc@3: in adamc@5: checkKind env c' ck k'; adamc@83: (c', k', gs) adamc@3: end adamc@3: adamc@3: | L.TFun (t1, t2) => adamc@3: let adamc@83: val (t1', k1, gs1) = elabCon (env, denv) t1 adamc@83: val (t2', k2, gs2) = elabCon (env, denv) t2 adamc@3: in adamc@5: checkKind env t1' k1 ktype; adamc@5: checkKind env t2' k2 ktype; adamc@83: ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2) adamc@3: end adamc@3: | L.TCFun (e, x, k, t) => adamc@3: let adamc@3: val e' = elabExplicitness e adamc@3: val k' = elabKind k adamc@3: val env' = E.pushCRel env x k' adamc@83: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@3: in adamc@5: checkKind env t' tk ktype; adamc@83: ((L'.TCFun (e', x, k', t'), loc), ktype, gs) adamc@3: end adamc@345: | L.CDisjoint (c1, c2, c) => adamc@85: let adamc@85: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@85: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@85: adamc@85: val ku1 = kunif loc adamc@85: val ku2 = kunif loc adamc@85: adamc@90: val (denv', gs3) = D.assert env denv (c1', c2') adamc@90: val (c', k, gs4) = elabCon (env, denv') c adamc@85: in adamc@85: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@85: checkKind env c2' k2 (L'.KRecord ku2, loc); adamc@85: adamc@345: ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ gs4) adamc@85: end adamc@3: | L.TRecord c => adamc@3: let adamc@83: val (c', ck, gs) = elabCon (env, denv) c adamc@3: val k = (L'.KRecord ktype, loc) adamc@3: in adamc@5: checkKind env c' ck k; adamc@83: ((L'.TRecord c', loc), ktype, gs) adamc@3: end adamc@3: adamc@34: | L.CVar ([], s) => adamc@3: (case E.lookupC env s of adamc@9: E.NotBound => adamc@5: (conError env (UnboundCon (loc, s)); adamc@83: (cerror, kerror, [])) adamc@9: | E.Rel (n, k) => adamc@83: ((L'.CRel n, loc), k, []) adamc@9: | E.Named (n, k) => adamc@83: ((L'.CNamed n, loc), k, [])) adamc@34: | L.CVar (m1 :: ms, s) => adamc@34: (case E.lookupStr env m1 of adamc@42: NONE => (conError env (UnboundStrInCon (loc, m1)); adamc@83: (cerror, kerror, [])) adamc@34: | SOME (n, sgn) => adamc@34: let adamc@34: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@34: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@34: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@34: (strerror, sgnerror)) adamc@34: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@34: ((L'.StrVar n, loc), sgn) ms adamc@34: adamc@34: val k = case E.projectCon env {sgn = sgn, str = str, field = s} of adamc@34: NONE => (conError env (UnboundCon (loc, s)); adamc@34: kerror) adamc@34: | SOME (k, _) => k adamc@34: in adamc@83: ((L'.CModProj (n, ms, s), loc), k, []) adamc@34: end) adamc@34: adamc@3: | L.CApp (c1, c2) => adamc@3: let adamc@83: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@83: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@76: val dom = kunif loc adamc@76: val ran = kunif loc adamc@3: in adamc@5: checkKind env c1' k1 (L'.KArrow (dom, ran), loc); adamc@5: checkKind env c2' k2 dom; adamc@83: ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2) adamc@3: end adamc@67: | L.CAbs (x, ko, t) => adamc@3: let adamc@67: val k' = case ko of adamc@76: NONE => kunif loc adamc@67: | SOME k => elabKind k adamc@3: val env' = E.pushCRel env x k' adamc@83: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@3: in adamc@8: ((L'.CAbs (x, k', t'), loc), adamc@83: (L'.KArrow (k', tk), loc), adamc@83: gs) adamc@3: end adamc@3: adamc@3: | L.CName s => adamc@83: ((L'.CName s, loc), kname, []) adamc@3: adamc@3: | L.CRecord xcs => adamc@3: let adamc@76: val k = kunif loc adamc@3: adamc@83: val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) => adamc@83: let adamc@83: val (x', xk, gs1) = elabCon (env, denv) x adamc@83: val (c', ck, gs2) = elabCon (env, denv) c adamc@83: in adamc@83: checkKind env x' xk kname; adamc@83: checkKind env c' ck k; adamc@83: ((x', c'), gs1 @ gs2 @ gs) adamc@83: end) [] xcs adamc@67: adamc@67: val rc = (L'.CRecord (k, xcs'), loc) adamc@67: (* Add duplicate field checking later. *) adamc@83: adamc@83: fun prove (xcs, ds) = adamc@83: case xcs of adamc@83: [] => ds adamc@83: | xc :: rest => adamc@83: let adamc@83: val r1 = (L'.CRecord (k, [xc]), loc) adamc@83: val ds = foldl (fn (xc', ds) => adamc@83: let adamc@83: val r2 = (L'.CRecord (k, [xc']), loc) adamc@83: in adamc@90: D.prove env denv (r1, r2, loc) @ ds adamc@83: end) adamc@83: ds rest adamc@83: in adamc@83: prove (rest, ds) adamc@83: end adamc@3: in adamc@83: (rc, (L'.KRecord k, loc), prove (xcs', gs)) adamc@3: end adamc@3: | L.CConcat (c1, c2) => adamc@3: let adamc@83: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@83: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@76: val ku = kunif loc adamc@3: val k = (L'.KRecord ku, loc) adamc@3: in adamc@5: checkKind env c1' k1 k; adamc@5: checkKind env c2' k2 k; adamc@83: ((L'.CConcat (c1', c2'), loc), k, adamc@90: D.prove env denv (c1', c2', loc) @ gs1 @ gs2) adamc@3: end adamc@67: | L.CFold => adamc@67: let adamc@76: val dom = kunif loc adamc@76: val ran = kunif loc adamc@67: in adamc@67: ((L'.CFold (dom, ran), loc), adamc@83: foldKind (dom, ran, loc), adamc@83: []) adamc@67: end adamc@3: adamc@83: | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) adamc@82: adamc@207: | L.CTuple cs => adamc@207: let adamc@207: val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) => adamc@207: let adamc@207: val (c', k, gs') = elabCon (env, denv) c adamc@207: in adamc@207: (c' :: cs', k :: ks, gs' @ gs) adamc@207: end) ([], [], []) cs adamc@207: in adamc@207: ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs) adamc@207: end adamc@207: | L.CProj (c, n) => adamc@207: let adamc@207: val (c', k, gs) = elabCon (env, denv) c adamc@207: in adamc@207: case hnormKind k of adamc@207: (L'.KTuple ks, _) => adamc@207: if n <= 0 orelse n > length ks then adamc@207: (conError env (ProjBounds (c', n)); adamc@207: (cerror, kerror, [])) adamc@207: else adamc@207: ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs) adamc@207: | k => (conError env (ProjMismatch (c', k)); adamc@207: (cerror, kerror, [])) adamc@207: end adamc@207: adamc@18: | L.CWild k => adamc@18: let adamc@18: val k' = elabKind k adamc@18: in adamc@83: (cunif (loc, k'), k', []) adamc@18: end adamc@18: adamc@6: fun kunifsRemain k = adamc@6: case k of adamc@76: L'.KUnif (_, _, ref NONE) => true adamc@6: | _ => false adamc@10: fun cunifsRemain c = adamc@10: case c of adamc@76: L'.CUnif (loc, _, _, ref NONE) => SOME loc adamc@76: | _ => NONE adamc@6: adamc@76: val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, adamc@76: con = fn _ => false, adamc@76: exp = fn _ => false, adamc@76: sgn_item = fn _ => false, adamc@76: sgn = fn _ => false, adamc@76: str = fn _ => false, adamc@76: decl = fn _ => false} adamc@10: adamc@76: val cunifsInDecl = U.Decl.search {kind = fn _ => NONE, adamc@76: con = cunifsRemain, adamc@76: exp = fn _ => NONE, adamc@76: sgn_item = fn _ => NONE, adamc@76: sgn = fn _ => NONE, adamc@76: str = fn _ => NONE, adamc@76: decl = fn _ => NONE} adamc@10: adamc@10: fun occursCon r = adamc@10: U.Con.exists {kind = fn _ => false, adamc@76: con = fn L'.CUnif (_, _, _, r') => r = r' adamc@10: | _ => false} adamc@10: adamc@10: exception CUnify' of cunify_error adamc@10: adamc@13: exception SynUnif = E.SynUnif adamc@12: adamc@81: open ElabOps adamc@43: adamc@12: type record_summary = { adamc@12: fields : (L'.con * L'.con) list, adamc@12: unifs : (L'.con * L'.con option ref) list, adamc@12: others : L'.con list adamc@12: } adamc@12: adamc@12: fun summaryToCon {fields, unifs, others} = adamc@12: let adamc@12: val c = (L'.CRecord (ktype, []), dummy) adamc@12: val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others adamc@12: val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs adamc@12: in adamc@12: (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy) adamc@12: end adamc@12: adamc@12: fun p_summary env s = p_con env (summaryToCon s) adamc@12: adamc@12: exception CUnify of L'.con * L'.con * cunify_error adamc@12: adamc@12: fun kindof env (c, loc) = adamc@12: case c of adamc@12: L'.TFun _ => ktype adamc@12: | L'.TCFun _ => ktype adamc@12: | L'.TRecord _ => ktype adamc@12: adamc@12: | L'.CRel xn => #2 (E.lookupCRel env xn) adamc@12: | L'.CNamed xn => #2 (E.lookupCNamed env xn) adamc@34: | L'.CModProj (n, ms, x) => adamc@34: let adamc@34: val (_, sgn) = E.lookupStrNamed env n adamc@34: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@34: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@34: NONE => raise Fail "kindof: Unknown substructure" adamc@34: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@34: ((L'.StrVar n, loc), sgn) ms adamc@34: in adamc@34: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@34: NONE => raise Fail "kindof: Unknown con in structure" adamc@34: | SOME (k, _) => k adamc@34: end adamc@34: adamc@12: | L'.CApp (c, _) => adamc@141: (case hnormKind (kindof env c) of adamc@141: (L'.KArrow (_, k), _) => k adamc@141: | (L'.KError, _) => kerror adamc@141: | k => raise CUnify' (CKindof (k, c))) adamc@12: | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) adamc@345: | L'.CDisjoint (_, _, _, c) => kindof env c adamc@12: adamc@12: | L'.CName _ => kname adamc@12: adamc@12: | L'.CRecord (k, _) => (L'.KRecord k, loc) adamc@12: | L'.CConcat (c, _) => kindof env c adamc@67: | L'.CFold (dom, ran) => foldKind (dom, ran, loc) adamc@12: adamc@82: | L'.CUnit => (L'.KUnit, loc) adamc@82: adamc@207: | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) adamc@207: | L'.CProj (c, n) => adamc@207: (case hnormKind (kindof env c) of adamc@207: (L'.KTuple ks, _) => List.nth (ks, n - 1) adamc@207: | k => raise CUnify' (CKindof (k, c))) adamc@207: adamc@12: | L'.CError => kerror adamc@76: | L'.CUnif (_, k, _, _) => k adamc@12: adamc@90: val hnormCon = D.hnormCon adamc@86: adamc@205: datatype con_summary = adamc@205: Nil adamc@205: | Cons adamc@205: | Unknown adamc@205: adamc@205: fun compatible cs = adamc@205: case cs of adamc@205: (Unknown, _) => false adamc@205: | (_, Unknown) => false adamc@205: | (s1, s2) => s1 = s2 adamc@205: adamc@205: fun summarizeCon (env, denv) c = adamc@205: let adamc@205: val (c, gs) = hnormCon (env, denv) c adamc@205: in adamc@205: case #1 c of adamc@205: L'.CRecord (_, []) => (Nil, gs) adamc@205: | L'.CRecord (_, _ :: _) => (Cons, gs) adamc@205: | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs) adamc@345: | L'.CDisjoint (_, _, _, c) => adamc@205: let adamc@205: val (s, gs') = summarizeCon (env, denv) c adamc@205: in adamc@205: (s, gs @ gs') adamc@205: end adamc@205: | _ => (Unknown, gs) adamc@205: end adamc@205: adamc@205: fun p_con_summary s = adamc@205: Print.PD.string (case s of adamc@205: Nil => "Nil" adamc@205: | Cons => "Cons" adamc@205: | Unknown => "Unknown") adamc@205: adamc@223: exception SummaryFailure adamc@223: adamc@86: fun unifyRecordCons (env, denv) (c1, c2) = adamc@12: let adamc@92: fun rkindof c = adamc@147: case hnormKind (kindof env c) of adamc@92: (L'.KRecord k, _) => k adamc@141: | (L'.KError, _) => kerror adamc@141: | k => raise CUnify' (CKindof (k, c)) adamc@92: adamc@92: val k1 = rkindof c1 adamc@92: val k2 = rkindof c2 adamc@86: adamc@86: val (r1, gs1) = recordSummary (env, denv) c1 adamc@86: val (r2, gs2) = recordSummary (env, denv) c2 adamc@12: in adamc@12: unifyKinds k1 k2; adamc@86: unifySummaries (env, denv) (k1, r1, r2); adamc@86: gs1 @ gs2 adamc@12: end adamc@12: adamc@86: and recordSummary (env, denv) c = adamc@86: let adamc@86: val (c, gs) = hnormCon (env, denv) c adamc@12: adamc@86: val (sum, gs') = adamc@86: case c of adamc@86: (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, []) adamc@86: | (L'.CConcat (c1, c2), _) => adamc@86: let adamc@86: val (s1, gs1) = recordSummary (env, denv) c1 adamc@86: val (s2, gs2) = recordSummary (env, denv) c2 adamc@86: in adamc@86: ({fields = #fields s1 @ #fields s2, adamc@86: unifs = #unifs s1 @ #unifs s2, adamc@86: others = #others s1 @ #others s2}, adamc@86: gs1 @ gs2) adamc@86: end adamc@86: | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c adamc@86: | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, []) adamc@86: | c' => ({fields = [], unifs = [], others = [c']}, []) adamc@86: in adamc@86: (sum, gs @ gs') adamc@86: end adamc@86: adamc@86: and consEq (env, denv) (c1, c2) = adamc@209: let adamc@209: val gs = unifyCons (env, denv) c1 c2 adamc@209: in adamc@209: List.all (fn (loc, env, denv, c1, c2) => adamc@209: case D.prove env denv (c1, c2, loc) of adamc@209: [] => true adamc@209: | _ => false) gs adamc@209: end adamc@12: handle CUnify _ => false adamc@12: adamc@80: and consNeq env (c1, c2) = adamc@86: case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of adamc@80: (L'.CName x1, L'.CName x2) => x1 <> x2 adamc@80: | _ => false adamc@80: adamc@86: and unifySummaries (env, denv) (k, s1 : record_summary, s2 : record_summary) = adamc@12: let adamc@223: val loc = #2 k adamc@14: (*val () = eprefaces "Summaries" [("#1", p_summary env s1), adamc@223: ("#2", p_summary env s2)]*) adamc@12: adamc@12: fun eatMatching p (ls1, ls2) = adamc@12: let adamc@12: fun em (ls1, ls2, passed1) = adamc@12: case ls1 of adamc@12: [] => (rev passed1, ls2) adamc@12: | h1 :: t1 => adamc@12: let adamc@12: fun search (ls2', passed2) = adamc@12: case ls2' of adamc@12: [] => em (t1, ls2, h1 :: passed1) adamc@12: | h2 :: t2 => adamc@12: if p (h1, h2) then adamc@12: em (t1, List.revAppend (passed2, t2), passed1) adamc@12: else adamc@12: search (t2, h2 :: passed2) adamc@12: in adamc@12: search (ls2, []) adamc@12: end adamc@12: in adamc@12: em (ls1, ls2, []) adamc@12: end adamc@12: adamc@12: val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) => adamc@80: not (consNeq env (x1, x2)) adamc@86: andalso consEq (env, denv) (c1, c2) adamc@86: andalso consEq (env, denv) (x1, x2)) adamc@79: (#fields s1, #fields s2) adamc@14: (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), adamc@223: ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) adamc@12: val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) adamc@86: val (others1, others2) = eatMatching (consEq (env, denv)) (#others s1, #others s2) adamc@223: (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@223: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@12: adamc@12: fun unifFields (fs, others, unifs) = adamc@12: case (fs, others, unifs) of adamc@12: ([], [], _) => ([], [], unifs) adamc@12: | (_, _, []) => (fs, others, []) adamc@12: | (_, _, (_, r) :: rest) => adamc@12: let adamc@12: val r' = ref NONE adamc@141: val kr = (L'.KRecord k, dummy) adamc@141: val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy) adamc@12: adamc@12: val prefix = case (fs, others) of adamc@12: ([], other :: others) => adamc@12: List.foldl (fn (other, c) => adamc@12: (L'.CConcat (c, other), dummy)) adamc@12: other others adamc@12: | (fs, []) => adamc@12: (L'.CRecord (k, fs), dummy) adamc@12: | (fs, others) => adamc@12: List.foldl (fn (other, c) => adamc@12: (L'.CConcat (c, other), dummy)) adamc@12: (L'.CRecord (k, fs), dummy) others adamc@12: in adamc@12: r := SOME (L'.CConcat (prefix, cr'), dummy); adamc@12: ([], [], (cr', r') :: rest) adamc@12: end adamc@12: adamc@12: val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2) adamc@12: val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1) adamc@12: adamc@223: (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@223: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@223: adamc@223: fun isGuessable (other, fs) = adamc@223: let adamc@223: val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure) adamc@223: in adamc@223: List.all (fn (loc, env, denv, c1, c2) => adamc@223: case D.prove env denv (c1, c2, loc) of adamc@223: [] => true adamc@223: | _ => false) gs adamc@223: end adamc@223: handle SummaryFailure => false adamc@223: adamc@223: val (fs1, fs2, others1, others2) = adamc@223: case (fs1, fs2, others1, others2) of adamc@223: ([], _, [other1], []) => adamc@223: if isGuessable (other1, fs2) then adamc@223: ([], [], [], []) adamc@223: else adamc@223: (fs1, fs2, others1, others2) adamc@348: | (_, [], [], [other2]) => adamc@348: if isGuessable (other2, fs1) then adamc@348: ([], [], [], []) adamc@348: else adamc@348: (fs1, fs2, others1, others2) adamc@223: | _ => (fs1, fs2, others1, others2) adamc@223: adamc@223: (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@348: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@223: adamc@86: val clear = case (fs1, others1, fs2, others2) of adamc@86: ([], [], [], []) => true adamc@12: | _ => false adamc@12: val empty = (L'.CRecord (k, []), dummy) adamc@223: adamc@329: fun unsummarize {fields, unifs, others} = adamc@329: let adamc@329: val c = (L'.CRecord (k, fields), loc) adamc@329: adamc@329: val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc)) adamc@329: c unifs adamc@329: in adamc@329: foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) adamc@329: c others adamc@329: end adamc@329: adamc@12: fun pairOffUnifs (unifs1, unifs2) = adamc@12: case (unifs1, unifs2) of adamc@12: ([], _) => adamc@86: if clear then adamc@12: List.app (fn (_, r) => r := SOME empty) unifs2 adamc@12: else adamc@329: raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) adamc@12: | (_, []) => adamc@86: if clear then adamc@12: List.app (fn (_, r) => r := SOME empty) unifs1 adamc@12: else adamc@329: raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) adamc@12: | ((c1, _) :: rest1, (_, r2) :: rest2) => adamc@12: (r2 := SOME c1; adamc@12: pairOffUnifs (rest1, rest2)) adamc@12: in adamc@12: pairOffUnifs (unifs1, unifs2) adamc@223: (*before eprefaces "Summaries'" [("#1", p_summary env s1), adamc@223: ("#2", p_summary env s2)]*) adamc@223: end adamc@223: adamc@223: and guessFold (env, denv) (c1, c2, gs, ex) = adamc@223: let adamc@223: val loc = #2 c1 adamc@223: adamc@223: fun unfold (dom, ran, f, i, r, c) = adamc@223: let adamc@223: val nm = cunif (loc, (L'.KName, loc)) adamc@223: val v = cunif (loc, dom) adamc@223: val rest = cunif (loc, (L'.KRecord dom, loc)) adamc@223: val acc = (L'.CFold (dom, ran), loc) adamc@223: val acc = (L'.CApp (acc, f), loc) adamc@223: val acc = (L'.CApp (acc, i), loc) adamc@223: val acc = (L'.CApp (acc, rest), loc) adamc@223: adamc@223: val (iS, gs3) = summarizeCon (env, denv) i adamc@223: adamc@223: val app = (L'.CApp (f, nm), loc) adamc@223: val app = (L'.CApp (app, v), loc) adamc@223: val app = (L'.CApp (app, acc), loc) adamc@223: val (appS, gs4) = summarizeCon (env, denv) app adamc@223: adamc@223: val (cS, gs5) = summarizeCon (env, denv) c adamc@223: in adamc@223: (*prefaces "Summaries" [("iS", p_con_summary iS), adamc@223: ("appS", p_con_summary appS), adamc@223: ("cS", p_con_summary cS)];*) adamc@223: adamc@223: if compatible (iS, appS) then adamc@223: raise ex adamc@223: else if compatible (cS, iS) then adamc@223: let adamc@223: (*val () = prefaces "Same?" [("i", p_con env i), adamc@223: ("c", p_con env c)]*) adamc@223: val gs6 = unifyCons (env, denv) i c adamc@223: (*val () = TextIO.print "Yes!\n"*) adamc@223: adamc@223: val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) adamc@223: in adamc@223: gs @ gs3 @ gs5 @ gs6 @ gs7 adamc@223: end adamc@223: else if compatible (cS, appS) then adamc@223: let adamc@223: (*val () = prefaces "Same?" [("app", p_con env app), adamc@223: ("c", p_con env c), adamc@223: ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*) adamc@223: val gs6 = unifyCons (env, denv) app c adamc@223: (*val () = TextIO.print "Yes!\n"*) adamc@223: adamc@223: val singleton = (L'.CRecord (dom, [(nm, v)]), loc) adamc@223: val concat = (L'.CConcat (singleton, rest), loc) adamc@223: (*val () = prefaces "Pre-crew" [("r", p_con env r), adamc@223: ("concat", p_con env concat)]*) adamc@223: val gs7 = unifyCons (env, denv) r concat adamc@223: in adamc@223: (*prefaces "The crew" [("nm", p_con env nm), adamc@223: ("v", p_con env v), adamc@223: ("rest", p_con env rest)];*) adamc@223: adamc@223: gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 adamc@223: end adamc@223: else adamc@223: raise ex adamc@223: end adamc@223: handle _ => raise ex adamc@223: in adamc@223: case (#1 c1, #1 c2) of adamc@223: (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) => adamc@223: unfold (dom, ran, f, i, r, c2) adamc@223: | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) => adamc@223: unfold (dom, ran, f, i, r, c1) adamc@223: | _ => raise ex adamc@12: end adamc@12: adamc@86: and unifyCons' (env, denv) c1 c2 = adamc@326: case (#1 c1, #1 c2) of adamc@345: (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) => adamc@205: let adamc@326: val gs1 = unifyCons' (env, denv) x1 x2 adamc@326: val gs2 = unifyCons' (env, denv) y1 y2 adamc@326: val (denv', gs3) = D.assert env denv (x1, y1) adamc@326: val gs4 = unifyCons' (env, denv') t1 t2 adamc@205: in adamc@326: gs1 @ gs2 @ gs3 @ gs4 adamc@205: end adamc@326: | _ => adamc@326: let adamc@326: val (c1, gs1) = hnormCon (env, denv) c1 adamc@326: val (c2, gs2) = hnormCon (env, denv) c2 adamc@326: in adamc@326: let adamc@326: val gs3 = unifyCons'' (env, denv) c1 c2 adamc@326: in adamc@326: gs1 @ gs2 @ gs3 adamc@326: end adamc@326: handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) adamc@326: end adamc@11: adamc@205: and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = adamc@10: let adamc@210: fun err f = raise CUnify' (f (c1All, c2All)) adamc@12: adamc@86: fun isRecord () = unifyRecordCons (env, denv) (c1All, c2All) adamc@10: in adamc@92: (*eprefaces "unifyCons''" [("c1All", p_con env c1All), adamc@92: ("c2All", p_con env c2All)];*) adamc@92: adamc@10: case (c1, c2) of adamc@88: (L'.CUnit, L'.CUnit) => [] adamc@88: adamc@88: | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => adamc@86: unifyCons' (env, denv) d1 d2 adamc@86: @ unifyCons' (env, denv) r1 r2 adamc@10: | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => adamc@10: if expl1 <> expl2 then adamc@10: err CExplicitness adamc@10: else adamc@10: (unifyKinds d1 d2; adamc@86: unifyCons' (E.pushCRel env x1 d1, D.enter denv) r1 r2) adamc@86: | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2 adamc@10: adamc@10: | (L'.CRel n1, L'.CRel n2) => adamc@10: if n1 = n2 then adamc@86: [] adamc@10: else adamc@10: err CIncompatible adamc@10: | (L'.CNamed n1, L'.CNamed n2) => adamc@10: if n1 = n2 then adamc@86: [] adamc@10: else adamc@10: err CIncompatible adamc@10: adamc@10: | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => adamc@86: (unifyCons' (env, denv) d1 d2; adamc@86: unifyCons' (env, denv) r1 r2) adamc@10: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => adamc@10: (unifyKinds k1 k2; adamc@86: unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) adamc@10: adamc@10: | (L'.CName n1, L'.CName n2) => adamc@10: if n1 = n2 then adamc@86: [] adamc@10: else adamc@10: err CIncompatible adamc@10: adamc@34: | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => adamc@34: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then adamc@86: [] adamc@34: else adamc@34: err CIncompatible adamc@34: adamc@207: | (L'.CTuple cs1, L'.CTuple cs2) => adamc@207: ((ListPair.foldlEq (fn (c1, c2, gs) => adamc@207: let adamc@207: val gs' = unifyCons' (env, denv) c1 c2 adamc@207: in adamc@207: gs' @ gs adamc@207: end) [] (cs1, cs2)) adamc@207: handle ListPair.UnequalLengths => err CIncompatible) adamc@348: adamc@348: | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) => adamc@348: unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All adamc@348: | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) => adamc@348: unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc) adamc@348: | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) => adamc@348: let adamc@348: val us = map (fn k => cunif (loc, k)) ks adamc@348: in adamc@348: r := SOME (L'.CTuple us, loc); adamc@348: unifyCons' (env, denv) (List.nth (us, n - 1)) c2All adamc@348: end adamc@348: | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) => adamc@348: let adamc@348: val us = map (fn k => cunif (loc, k)) ks adamc@348: in adamc@348: r := SOME (L'.CTuple us, loc); adamc@348: unifyCons' (env, denv) c1All (List.nth (us, n - 1)) adamc@348: end adamc@207: | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => adamc@207: if n1 = n2 then adamc@207: unifyCons' (env, denv) c1 c2 adamc@207: else adamc@207: err CIncompatible adamc@207: adamc@86: | (L'.CError, _) => [] adamc@86: | (_, L'.CError) => [] adamc@10: adamc@92: | (L'.CRecord _, _) => isRecord () adamc@92: | (_, L'.CRecord _) => isRecord () adamc@92: | (L'.CConcat _, _) => isRecord () adamc@92: | (_, L'.CConcat _) => isRecord () adamc@10: adamc@76: | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => adamc@10: if r1 = r2 then adamc@86: [] adamc@10: else adamc@10: (unifyKinds k1 k2; adamc@86: r1 := SOME c2All; adamc@86: []) adamc@10: adamc@76: | (L'.CUnif (_, _, _, r), _) => adamc@10: if occursCon r c2All then adamc@10: err COccursCheckFailed adamc@10: else adamc@86: (r := SOME c2All; adamc@86: []) adamc@76: | (_, L'.CUnif (_, _, _, r)) => adamc@10: if occursCon r c1All then adamc@10: err COccursCheckFailed adamc@10: else adamc@86: (r := SOME c1All; adamc@86: []) adamc@10: adamc@71: | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => adamc@71: (unifyKinds dom1 dom2; adamc@86: unifyKinds ran1 ran2; adamc@86: []) adamc@71: adamc@10: | _ => err CIncompatible adamc@10: end adamc@10: adamc@86: and unifyCons (env, denv) c1 c2 = adamc@86: unifyCons' (env, denv) c1 c2 adamc@10: handle CUnify' err => raise CUnify (c1, c2, err) adamc@10: | KUnify args => raise CUnify (c1, c2, CKind args) adamc@210: adamc@86: fun checkCon (env, denv) e c1 c2 = adamc@86: unifyCons (env, denv) c1 c2 adamc@10: handle CUnify (c1, c2, err) => adamc@86: (expError env (Unify (e, c1, c2, err)); adamc@86: []) adamc@10: adamc@171: fun checkPatCon (env, denv) p c1 c2 = adamc@171: unifyCons (env, denv) c1 c2 adamc@171: handle CUnify (c1, c2, err) => adamc@171: (expError env (PatUnify (p, c1, c2, err)); adamc@171: []) adamc@171: adamc@14: fun primType env p = adamc@56: case p of adamc@56: P.Int _ => !int adamc@56: | P.Float _ => !float adamc@56: | P.String _ => !string adamc@14: adamc@71: fun recCons (k, nm, v, rest, loc) = adamc@71: (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc), adamc@71: rest), loc) adamc@71: adamc@71: fun foldType (dom, loc) = adamc@71: (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), adamc@71: (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), adamc@71: (L'.TCFun (L'.Explicit, "v", dom, adamc@71: (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), adamc@71: (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), adamc@345: (L'.CDisjoint (L'.Instantiate, adamc@334: (L'.CRecord adamc@326: ((L'.KUnit, loc), adamc@326: [((L'.CRel 2, loc), adamc@326: (L'.CUnit, loc))]), loc), adamc@326: (L'.CRel 0, loc), adamc@326: (L'.CApp ((L'.CRel 3, loc), adamc@326: recCons (dom, adamc@326: (L'.CRel 2, loc), adamc@326: (L'.CRel 1, loc), adamc@326: (L'.CRel 0, loc), adamc@326: loc)), loc)), adamc@326: loc)), loc)), adamc@71: loc)), loc)), loc), adamc@71: (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), adamc@71: (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), adamc@71: (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), adamc@71: loc)), loc)), loc) adamc@71: adamc@228: datatype constraint = adamc@228: Disjoint of D.goal adamc@228: | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span adamc@228: adamc@228: val enD = map Disjoint adamc@228: adamc@86: fun elabHead (env, denv) (e as (_, loc)) t = adamc@15: let adamc@15: fun unravel (t, e) = adamc@86: let adamc@86: val (t, gs) = hnormCon (env, denv) t adamc@86: in adamc@86: case t of adamc@86: (L'.TCFun (L'.Implicit, x, k, t'), _) => adamc@86: let adamc@86: val u = cunif (loc, k) adamc@86: adamc@339: val t'' = subConInCon (0, u) t' adamc@339: val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc)) adamc@86: in adamc@339: (*prefaces "Unravel" [("t'", p_con env t'), adamc@339: ("t''", p_con env t'')];*) adamc@228: (e, t, enD gs @ gs') adamc@86: end adamc@228: | _ => (e, t, enD gs) adamc@86: end adamc@15: in adamc@15: unravel (t, e) adamc@15: end adamc@15: adamc@174: fun elabPat (pAll as (p, loc), (env, denv, bound)) = adamc@171: let adamc@171: val perror = (L'.PWild, loc) adamc@171: val terror = (L'.CError, loc) adamc@171: val pterror = (perror, terror) adamc@171: val rerror = (pterror, (env, bound)) adamc@171: adamc@191: fun pcon (pc, po, xs, to, dn, dk) = adamc@188: case (po, to) of adamc@188: (NONE, SOME _) => (expError env (PatHasNoArg loc); adamc@188: rerror) adamc@188: | (SOME _, NONE) => (expError env (PatHasArg loc); adamc@188: rerror) adamc@191: | (NONE, NONE) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val unifs = map (fn _ => cunif (loc, k)) xs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@191: in adamc@191: (((L'.PCon (dk, pc, unifs, NONE), loc), dn), adamc@191: (env, bound)) adamc@191: end adamc@188: | (SOME p, SOME t) => adamc@188: let adamc@188: val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) adamc@191: adamc@191: val k = (L'.KType, loc) adamc@191: val unifs = map (fn _ => cunif (loc, k)) xs adamc@194: val nxs = length unifs - 1 adamc@194: val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@188: in adamc@191: ignore (checkPatCon (env, denv) p' pt t); adamc@191: (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), adamc@188: (env, bound)) adamc@188: end adamc@171: in adamc@171: case p of adamc@171: L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))), adamc@171: (env, bound)) adamc@171: | L.PVar x => adamc@171: let adamc@171: val t = if SS.member (bound, x) then adamc@171: (expError env (DuplicatePatternVariable (loc, x)); adamc@171: terror) adamc@171: else adamc@171: cunif (loc, (L'.KType, loc)) adamc@171: in adamc@182: (((L'.PVar (x, t), loc), t), adamc@171: (E.pushERel env x t, SS.add (bound, x))) adamc@171: end adamc@173: | L.PPrim p => (((L'.PPrim p, loc), primType env p), adamc@173: (env, bound)) adamc@171: | L.PCon ([], x, po) => adamc@171: (case E.lookupConstructor env x of adamc@174: NONE => (expError env (UnboundConstructor (loc, [], x)); adamc@171: rerror) adamc@191: | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk)) adamc@174: | L.PCon (m1 :: ms, x, po) => adamc@174: (case E.lookupStr env m1 of adamc@174: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@174: rerror) adamc@174: | SOME (n, sgn) => adamc@174: let adamc@174: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@174: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@182: NONE => raise Fail "elabPat: Unknown substructure" adamc@174: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@174: ((L'.StrVar n, loc), sgn) ms adamc@174: in adamc@174: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@174: NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); adamc@174: rerror) adamc@191: | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk) adamc@174: end) adamc@174: adamc@175: | L.PRecord (xps, flex) => adamc@175: let adamc@175: val (xpts, (env, bound, _)) = adamc@175: ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) => adamc@175: let adamc@175: val ((p', t), (env, bound)) = elabPat (p, (env, denv, bound)) adamc@175: in adamc@175: if SS.member (fbound, x) then adamc@175: expError env (DuplicatePatField (loc, x)) adamc@175: else adamc@175: (); adamc@175: ((x, p', t), (env, bound, SS.add (fbound, x))) adamc@175: end) adamc@175: (env, bound, SS.empty) xps adamc@175: adamc@175: val k = (L'.KType, loc) adamc@175: val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc) adamc@176: val c = adamc@175: if flex then adamc@176: (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc) adamc@175: else adamc@176: c adamc@175: in adamc@182: (((L'.PRecord xpts, loc), adamc@175: (L'.TRecord c, loc)), adamc@175: (env, bound)) adamc@175: end adamc@175: adamc@171: end adamc@171: adamc@172: datatype coverage = adamc@172: Wild adamc@173: | None adamc@172: | Datatype of coverage IM.map adamc@175: | Record of coverage SM.map list adamc@172: adamc@243: fun c2s c = adamc@243: case c of adamc@243: Wild => "Wild" adamc@243: | None => "None" adamc@243: | Datatype _ => "Datatype" adamc@243: | Record _ => "Record" adamc@243: adamc@172: fun exhaustive (env, denv, t, ps) = adamc@172: let adamc@172: fun pcCoverage pc = adamc@172: case pc of adamc@172: L'.PConVar n => n adamc@174: | L'.PConProj (m1, ms, x) => adamc@174: let adamc@174: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@174: in adamc@174: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@174: NONE => raise Fail "exhaustive: Can't project constructor" adamc@191: | SOME (_, n, _, _, _) => n adamc@174: end adamc@172: adamc@172: fun coverage (p, _) = adamc@172: case p of adamc@172: L'.PWild => Wild adamc@172: | L'.PVar _ => Wild adamc@173: | L'.PPrim _ => None adamc@191: | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) adamc@191: | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) adamc@182: | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => adamc@182: SM.insert (fmap, x, coverage p)) SM.empty xps] adamc@176: adamc@172: fun merge (c1, c2) = adamc@172: case (c1, c2) of adamc@173: (None, _) => c2 adamc@173: | (_, None) => c1 adamc@173: adamc@173: | (Wild, _) => Wild adamc@172: | (_, Wild) => Wild adamc@172: adamc@172: | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2)) adamc@172: adamc@175: | (Record fm1, Record fm2) => Record (fm1 @ fm2) adamc@175: adamc@175: | _ => None adamc@175: adamc@172: fun combinedCoverage ps = adamc@172: case ps of adamc@172: [] => raise Fail "Empty pattern list for coverage checking" adamc@172: | [p] => coverage p adamc@172: | p :: ps => merge (coverage p, combinedCoverage ps) adamc@172: adamc@175: fun enumerateCases t = adamc@175: let adamc@175: fun dtype cons = adamc@175: ListUtil.mapConcat (fn (_, n, to) => adamc@175: case to of adamc@175: NONE => [Datatype (IM.insert (IM.empty, n, Wild))] adamc@175: | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) adamc@175: (enumerateCases t)) cons adamc@175: in adamc@175: case #1 (#1 (hnormCon (env, denv) t)) of adamc@175: L'.CNamed n => adamc@175: (let adamc@175: val dt = E.lookupDatatype env n adamc@175: val cons = E.constructors dt adamc@175: in adamc@175: dtype cons adamc@175: end handle E.UnboundNamed _ => [Wild]) adamc@175: | L'.TRecord c => adamc@175: (case #1 (#1 (hnormCon (env, denv) c)) of adamc@175: L'.CRecord (_, xts) => adamc@175: let adamc@175: val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) x), t)) xts adamc@175: adamc@175: fun exponentiate fs = adamc@175: case fs of adamc@175: [] => [SM.empty] adamc@175: | ((L'.CName x, _), t) :: rest => adamc@175: let adamc@175: val this = enumerateCases t adamc@175: val rest = exponentiate rest adamc@175: in adamc@175: ListUtil.mapConcat (fn fmap => adamc@175: map (fn c => SM.insert (fmap, x, c)) this) rest adamc@175: end adamc@175: | _ => raise Fail "exponentiate: Not CName" adamc@175: in adamc@175: if List.exists (fn ((L'.CName _, _), _) => false adamc@175: | (c, _) => true) xts then adamc@175: [Wild] adamc@175: else adamc@175: map (fn ls => Record [ls]) (exponentiate xts) adamc@175: end adamc@175: | _ => [Wild]) adamc@175: | _ => [Wild] adamc@175: end adamc@175: adamc@175: fun coverageImp (c1, c2) = adamc@243: let adamc@243: val r = adamc@243: case (c1, c2) of adamc@243: (Wild, _) => true adamc@243: adamc@243: | (Datatype cmap1, Datatype cmap2) => adamc@243: List.all (fn (n, c2) => adamc@243: case IM.find (cmap1, n) of adamc@243: NONE => false adamc@243: | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2) adamc@243: | (Datatype cmap1, Wild) => adamc@243: List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1) adamc@243: adamc@243: | (Record fmaps1, Record fmaps2) => adamc@243: List.all (fn fmap2 => adamc@243: List.exists (fn fmap1 => adamc@243: List.all (fn (x, c2) => adamc@243: case SM.find (fmap1, x) of adamc@243: NONE => true adamc@243: | SOME c1 => coverageImp (c1, c2)) adamc@243: (SM.listItemsi fmap2)) adamc@243: fmaps1) fmaps2 adamc@243: adamc@243: | (Record fmaps1, Wild) => adamc@243: List.exists (fn fmap1 => adamc@243: List.all (fn (x, c1) => coverageImp (c1, Wild)) adamc@243: (SM.listItemsi fmap1)) fmaps1 adamc@243: adamc@243: | _ => false adamc@243: in adamc@243: (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*) adamc@243: r adamc@243: end adamc@175: adamc@172: fun isTotal (c, t) = adamc@172: case c of adamc@173: None => (false, []) adamc@173: | Wild => (true, []) adamc@172: | Datatype cm => adamc@172: let adamc@172: val ((t, _), gs) = hnormCon (env, denv) t adamc@174: adamc@174: fun dtype cons = adamc@174: foldl (fn ((_, n, to), (total, gs)) => adamc@174: case IM.find (cm, n) of adamc@174: NONE => (false, gs) adamc@174: | SOME c' => adamc@174: case to of adamc@174: NONE => (total, gs) adamc@174: | SOME t' => adamc@174: let adamc@174: val (total, gs') = isTotal (c', t') adamc@174: in adamc@174: (total, gs' @ gs) adamc@174: end) adamc@174: (true, gs) cons adamc@191: adamc@191: fun unapp t = adamc@191: case t of adamc@191: L'.CApp ((t, _), _) => unapp t adamc@191: | _ => t adamc@172: in adamc@191: case unapp t of adamc@172: L'.CNamed n => adamc@172: let adamc@172: val dt = E.lookupDatatype env n adamc@172: val cons = E.constructors dt adamc@172: in adamc@174: dtype cons adamc@174: end adamc@174: | L'.CModProj (m1, ms, x) => adamc@174: let adamc@174: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@174: in adamc@174: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@174: NONE => raise Fail "isTotal: Can't project datatype" adamc@191: | SOME (_, cons) => dtype cons adamc@172: end adamc@172: | L'.CError => (true, gs) adamc@341: | c => adamc@341: (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; adamc@341: raise Fail "isTotal: Not a datatype") adamc@172: end adamc@175: | Record _ => (List.all (fn c2 => coverageImp (c, c2)) (enumerateCases t), []) adamc@172: in adamc@172: isTotal (combinedCoverage ps, t) adamc@172: end adamc@172: adamc@217: fun unmodCon env (c, loc) = adamc@217: case c of adamc@217: L'.CNamed n => adamc@217: (case E.lookupCNamed env n of adamc@217: (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc)) adamc@217: | L'.CModProj (m1, ms, x) => adamc@217: let adamc@217: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@217: in adamc@217: case E.projectCon env {str = str, sgn = sgn, field = x} of adamc@217: NONE => raise Fail "unmodCon: Can't projectCon" adamc@217: | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc) adamc@217: end adamc@217: | _ => (c, loc) adamc@217: adamc@217: fun normClassConstraint envs (c, loc) = adamc@217: case c of adamc@217: L'.CApp (f, x) => adamc@217: let adamc@217: val f = unmodCon (#1 envs) f adamc@217: val (x, gs) = hnormCon envs x adamc@217: in adamc@217: ((L'.CApp (f, x), loc), gs) adamc@217: end adamc@217: | _ => ((c, loc), []) adamc@216: adamc@92: fun elabExp (env, denv) (eAll as (e, loc)) = adamc@91: let adamc@280: (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) adamc@280: adamc@280: val r = case e of adamc@91: L.EAnnot (e, t) => adamc@91: let adamc@91: val (e', et, gs1) = elabExp (env, denv) e adamc@91: val (t', _, gs2) = elabCon (env, denv) t adamc@91: val gs3 = checkCon (env, denv) e' et t' adamc@91: in adamc@228: (e', t', gs1 @ enD gs2 @ enD gs3) adamc@91: end adamc@34: adamc@91: | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) adamc@91: | L.EVar ([], s) => adamc@91: (case E.lookupE env s of adamc@91: E.NotBound => adamc@91: (expError env (UnboundExp (loc, s)); adamc@91: (eerror, cerror, [])) adamc@91: | E.Rel (n, t) => ((L'.ERel n, loc), t, []) adamc@191: | E.Named (n, t) => adamc@191: if Char.isUpper (String.sub (s, 0)) then adamc@191: elabHead (env, denv) (L'.ENamed n, loc) t adamc@191: else adamc@191: ((L'.ENamed n, loc), t, [])) adamc@91: | L.EVar (m1 :: ms, s) => adamc@91: (case E.lookupStr env m1 of adamc@91: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@91: (eerror, cerror, [])) adamc@91: | SOME (n, sgn) => adamc@91: let adamc@91: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@91: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@91: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@91: (strerror, sgnerror)) adamc@91: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@91: ((L'.StrVar n, loc), sgn) ms adamc@10: adamc@91: val t = case E.projectVal env {sgn = sgn, str = str, field = s} of adamc@91: NONE => (expError env (UnboundExp (loc, s)); adamc@91: cerror) adamc@91: | SOME t => t adamc@91: in adamc@91: ((L'.EModProj (n, ms, s), loc), t, []) adamc@91: end) adamc@86: adamc@349: | L.EWild => adamc@210: let adamc@349: val r = ref NONE adamc@349: val c = cunif (loc, (L'.KType, loc)) adamc@210: in adamc@349: ((L'.EUnif r, loc), c, [TypeClass (env, c, r, loc)]) adamc@210: end adamc@210: adamc@91: | L.EApp (e1, e2) => adamc@91: let adamc@91: val (e1', t1, gs1) = elabExp (env, denv) e1 adamc@91: val (e1', t1, gs2) = elabHead (env, denv) e1' t1 adamc@91: val (e2', t2, gs3) = elabExp (env, denv) e2 adamc@71: adamc@91: val dom = cunif (loc, ktype) adamc@91: val ran = cunif (loc, ktype) adamc@91: val t = (L'.TFun (dom, ran), dummy) adamc@91: adamc@91: val gs4 = checkCon (env, denv) e1' t1 t adamc@91: val gs5 = checkCon (env, denv) e2' t2 dom adamc@205: adamc@228: val gs = gs1 @ gs2 @ gs3 @ enD gs4 @ enD gs5 adamc@91: in adamc@205: ((L'.EApp (e1', e2'), loc), ran, gs) adamc@91: end adamc@91: | L.EAbs (x, to, e) => adamc@91: let adamc@91: val (t', gs1) = case to of adamc@91: NONE => (cunif (loc, ktype), []) adamc@91: | SOME t => adamc@91: let adamc@91: val (t', tk, gs) = elabCon (env, denv) t adamc@91: in adamc@91: checkKind env t' tk ktype; adamc@91: (t', gs) adamc@91: end adamc@256: val (dom, gs2) = normClassConstraint (env, denv) t' adamc@256: val (e', et, gs3) = elabExp (E.pushERel env x dom, denv) e adamc@91: in adamc@91: ((L'.EAbs (x, t', et, e'), loc), adamc@91: (L'.TFun (t', et), loc), adamc@256: enD gs1 @ enD gs2 @ gs3) adamc@91: end adamc@91: | L.ECApp (e, c) => adamc@91: let adamc@91: val (e', et, gs1) = elabExp (env, denv) e adamc@328: val oldEt = et adamc@91: val (e', et, gs2) = elabHead (env, denv) e' et adamc@91: val (c', ck, gs3) = elabCon (env, denv) c adamc@91: val ((et', _), gs4) = hnormCon (env, denv) et adamc@91: in adamc@91: case et' of adamc@91: L'.CError => (eerror, cerror, []) adamc@328: | L'.TCFun (_, x, k, eb) => adamc@91: let adamc@91: val () = checkKind env c' ck k adamc@91: val eb' = subConInCon (0, c') eb adamc@339: handle SynUnif => (expError env (Unif ("substitution", loc, eb)); adamc@91: cerror) adamc@91: in adamc@328: (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), adamc@328: ("et", p_con env oldEt), adamc@328: ("x", PD.string x), adamc@328: ("eb", p_con (E.pushCRel env x k) eb), adamc@328: ("c", p_con env c'), adamc@328: ("eb'", p_con env eb')];*) adamc@228: ((L'.ECApp (e', c'), loc), eb', gs1 @ gs2 @ enD gs3 @ enD gs4) adamc@91: end adamc@91: adamc@91: | _ => adamc@91: (expError env (WrongForm ("constructor function", e', et)); adamc@91: (eerror, cerror, [])) adamc@91: end adamc@91: | L.ECAbs (expl, x, k, e) => adamc@91: let adamc@91: val expl' = elabExplicitness expl adamc@91: val k' = elabKind k adamc@328: adamc@328: val env' = E.pushCRel env x k' adamc@328: val (e', et, gs) = elabExp (env', D.enter denv) e adamc@91: in adamc@91: ((L'.ECAbs (expl', x, k', e'), loc), adamc@91: (L'.TCFun (expl', x, k', et), loc), adamc@91: gs) adamc@91: end adamc@91: adamc@91: | L.EDisjoint (c1, c2, e) => adamc@91: let adamc@91: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@91: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@91: adamc@91: val ku1 = kunif loc adamc@91: val ku2 = kunif loc adamc@91: adamc@91: val (denv', gs3) = D.assert env denv (c1', c2') adamc@91: val (e', t, gs4) = elabExp (env, denv') e adamc@91: in adamc@91: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@91: checkKind env c2' k2 (L'.KRecord ku2, loc); adamc@91: adamc@345: (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) adamc@91: end adamc@91: adamc@91: | L.ERecord xes => adamc@91: let adamc@91: val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => adamc@91: let adamc@91: val (x', xk, gs1) = elabCon (env, denv) x adamc@91: val (e', et, gs2) = elabExp (env, denv) e adamc@91: in adamc@91: checkKind env x' xk kname; adamc@228: ((x', e', et), enD gs1 @ gs2 @ gs) adamc@91: end) adamc@91: [] xes adamc@91: adamc@91: val k = (L'.KType, loc) adamc@91: adamc@91: fun prove (xets, gs) = adamc@91: case xets of adamc@91: [] => gs adamc@91: | (x, _, t) :: rest => adamc@91: let adamc@91: val xc = (x, t) adamc@91: val r1 = (L'.CRecord (k, [xc]), loc) adamc@91: val gs = foldl (fn ((x', _, t'), gs) => adamc@91: let adamc@91: val xc' = (x', t') adamc@91: val r2 = (L'.CRecord (k, [xc']), loc) adamc@91: in adamc@91: D.prove env denv (r1, r2, loc) @ gs adamc@91: end) adamc@91: gs rest adamc@91: in adamc@91: prove (rest, gs) adamc@91: end adamc@228: adamc@228: val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs adamc@228: val gsO = List.filter (fn Disjoint _ => false | _ => true) gs adamc@91: in adamc@255: (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*) adamc@91: ((L'.ERecord xes', loc), adamc@91: (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc), adamc@228: enD (prove (xes', gsD)) @ gsO) adamc@91: end adamc@91: adamc@91: | L.EField (e, c) => adamc@91: let adamc@91: val (e', et, gs1) = elabExp (env, denv) e adamc@91: val (c', ck, gs2) = elabCon (env, denv) c adamc@91: adamc@91: val ft = cunif (loc, ktype) adamc@91: val rest = cunif (loc, ktype_record) adamc@91: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@91: adamc@91: val gs3 = adamc@91: checkCon (env, denv) e' et adamc@91: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@91: val gs4 = D.prove env denv (first, rest, loc) adamc@91: in adamc@228: ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) adamc@91: end adamc@91: adamc@339: | L.EWith (e1, c, e2) => adamc@339: let adamc@339: val (e1', e1t, gs1) = elabExp (env, denv) e1 adamc@339: val (c', ck, gs2) = elabCon (env, denv) c adamc@339: val (e2', e2t, gs3) = elabExp (env, denv) e2 adamc@339: adamc@339: val rest = cunif (loc, ktype_record) adamc@339: val first = (L'.CRecord (ktype, [(c', e2t)]), loc) adamc@339: adamc@339: val gs4 = checkCon (env, denv) e1' e1t (L'.TRecord rest, loc) adamc@339: val gs5 = D.prove env denv (first, rest, loc) adamc@339: in adamc@339: ((L'.EWith (e1', c', e2', {field = e2t, rest = rest}), loc), adamc@339: (L'.TRecord ((L'.CConcat (first, rest), loc)), loc), adamc@339: gs1 @ enD gs2 @ gs3 @ enD gs4 @ enD gs5) adamc@339: end adamc@149: | L.ECut (e, c) => adamc@149: let adamc@149: val (e', et, gs1) = elabExp (env, denv) e adamc@149: val (c', ck, gs2) = elabCon (env, denv) c adamc@149: adamc@149: val ft = cunif (loc, ktype) adamc@149: val rest = cunif (loc, ktype_record) adamc@149: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@149: adamc@149: val gs3 = adamc@149: checkCon (env, denv) e' et adamc@149: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@149: val gs4 = D.prove env denv (first, rest, loc) adamc@149: in adamc@228: ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), adamc@228: gs1 @ enD gs2 @ enD gs3 @ enD gs4) adamc@149: end adamc@149: adamc@91: | L.EFold => adamc@91: let adamc@91: val dom = kunif loc adamc@91: in adamc@91: ((L'.EFold dom, loc), foldType (dom, loc), []) adamc@91: end adamc@170: adamc@171: | L.ECase (e, pes) => adamc@171: let adamc@171: val (e', et, gs1) = elabExp (env, denv) e adamc@171: val result = cunif (loc, (L'.KType, loc)) adamc@171: val (pes', gs) = ListUtil.foldlMap adamc@171: (fn ((p, e), gs) => adamc@171: let adamc@174: val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty)) adamc@171: adamc@171: val gs1 = checkPatCon (env, denv) p' pt et adamc@171: val (e', et, gs2) = elabExp (env, denv) e adamc@171: val gs3 = checkCon (env, denv) e' et result adamc@171: in adamc@228: ((p', e'), enD gs1 @ gs2 @ enD gs3 @ gs) adamc@171: end) adamc@171: gs1 pes adamc@172: adamc@172: val (total, gs') = exhaustive (env, denv, et, map #1 pes') adamc@171: in adamc@172: if total then adamc@172: () adamc@172: else adamc@172: expError env (Inexhaustive loc); adamc@172: adamc@228: ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) adamc@171: end adamc@280: adamc@280: (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 r)*) adamc@280: in adamc@280: (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), adamc@280: ("|tcs|", PD.string (Int.toString (length tcs)))];*) adamc@280: r adamc@91: end adamc@31: adamc@42: val hnormSgn = E.hnormSgn adamc@31: adamc@210: fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) adamc@338: fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) adamc@205: adamc@88: fun elabSgn_item ((sgi, loc), (env, denv, gs)) = adamc@76: case sgi of adamc@76: L.SgiConAbs (x, k) => adamc@76: let adamc@76: val k' = elabKind k adamc@31: adamc@76: val (env', n) = E.pushCNamed env x k' NONE adamc@76: in adamc@88: ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) adamc@76: end adamc@31: adamc@76: | L.SgiCon (x, ko, c) => adamc@76: let adamc@76: val k' = case ko of adamc@76: NONE => kunif loc adamc@76: | SOME k => elabKind k adamc@31: adamc@83: val (c', ck, gs') = elabCon (env, denv) c adamc@76: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@76: in adamc@76: checkKind env c' ck k'; adamc@31: adamc@88: ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@191: | L.SgiDatatype (x, xs, xcs) => adamc@157: let adamc@157: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: val (env, n) = E.pushCNamed env x k' NONE adamc@157: val t = (L'.CNamed n, loc) adamc@194: val nxs = length xs - 1 adamc@194: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@157: adamc@284: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@284: (E.pushCRel env' x k, adamc@284: D.enter denv')) (env, denv) xs adamc@284: adamc@157: val (xcs, (used, env, gs)) = adamc@157: ListUtil.foldlMap adamc@157: (fn ((x, to), (used, env, gs)) => adamc@157: let adamc@157: val (to, t, gs') = case to of adamc@157: NONE => (NONE, t, gs) adamc@157: | SOME t' => adamc@157: let adamc@284: val (t', tk, gs') = elabCon (env', denv') t' adamc@157: in adamc@284: checkKind env' t' tk k; adamc@157: (SOME t', (L'.TFun (t', t), loc), gs' @ gs) adamc@157: end adamc@191: val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@157: adamc@157: val (env, n') = E.pushENamed env x t adamc@157: in adamc@157: if SS.member (used, x) then adamc@157: strError env (DuplicateConstructor (x, loc)) adamc@157: else adamc@157: (); adamc@157: ((x, n', to), (SS.add (used, x), env, gs')) adamc@157: end) adamc@157: (SS.empty, env, []) xcs adamc@191: adamc@191: val env = E.pushDatatype env n xs xcs adamc@157: in adamc@191: ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) adamc@157: end adamc@156: adamc@158: | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" adamc@158: adamc@158: | L.SgiDatatypeImp (x, m1 :: ms, s) => adamc@158: (case E.lookupStr env m1 of adamc@158: NONE => (strError env (UnboundStr (loc, m1)); adamc@158: ([], (env, denv, gs))) adamc@158: | SOME (n, sgn) => adamc@158: let adamc@158: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@158: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@158: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@158: (strerror, sgnerror)) adamc@158: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@158: ((L'.StrVar n, loc), sgn) ms adamc@158: in adamc@161: case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of adamc@161: ((L'.CModProj (n, ms, s), _), gs) => adamc@161: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@161: NONE => (conError env (UnboundDatatype (loc, s)); adamc@161: ([], (env, denv, gs))) adamc@191: | SOME (xs, xncs) => adamc@161: let adamc@161: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: adamc@161: val t = (L'.CModProj (n, ms, s), loc) adamc@191: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@191: val env = E.pushDatatype env n' xs xncs adamc@158: adamc@161: val t = (L'.CNamed n', loc) adamc@161: val env = foldl (fn ((x, n, to), env) => adamc@161: let adamc@161: val t = case to of adamc@161: NONE => t adamc@161: | SOME t' => (L'.TFun (t', t), loc) adamc@191: adamc@191: val t = foldr (fn (x, t) => adamc@191: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@191: t xs adamc@161: in adamc@161: E.pushENamedAs env x n t adamc@161: end) env xncs adamc@161: in adamc@191: ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) adamc@161: end) adamc@161: | _ => (strError env (NotDatatype loc); adamc@161: ([], (env, denv, []))) adamc@158: end) adamc@156: adamc@76: | L.SgiVal (x, c) => adamc@76: let adamc@83: val (c', ck, gs') = elabCon (env, denv) c adamc@31: adamc@76: val (env', n) = E.pushENamed env x c' adamc@218: val (c', gs'') = normClassConstraint (env, denv) c' adamc@76: in adamc@76: (unifyKinds ck ktype adamc@76: handle KUnify ue => strError env (NotType (ck, ue))); adamc@31: adamc@218: ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs'' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiStr (x, sgn) => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: val (env', n) = E.pushStrNamed env x sgn' adamc@76: in adamc@88: ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiSgn (x, sgn) => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: val (env', n) = E.pushSgnNamed env x sgn' adamc@76: in adamc@88: ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiInclude sgn => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: in adamc@76: case #1 (hnormSgn env sgn') of adamc@76: L'.SgnConst sgis => adamc@88: (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) adamc@76: | _ => (sgnError env (NotIncludable sgn'); adamc@88: ([], (env, denv, []))) adamc@88: end adamc@88: adamc@88: | L.SgiConstraint (c1, c2) => adamc@88: let adamc@88: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@88: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@88: adamc@90: val (denv, gs3) = D.assert env denv (c1', c2') adamc@88: in adamc@88: checkKind env c1' k1 (L'.KRecord (kunif loc), loc); adamc@88: checkKind env c2' k2 (L'.KRecord (kunif loc), loc); adamc@88: adamc@90: ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) adamc@76: end adamc@31: adamc@203: | L.SgiTable (x, c) => adamc@203: let adamc@203: val (c', k, gs) = elabCon (env, denv) c adamc@210: val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) adamc@203: in adamc@203: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@210: ([(L'.SgiTable (!basis_r, x, n, c'), loc)], (env, denv, gs)) adamc@203: end adamc@203: adamc@338: | L.SgiSequence x => adamc@338: let adamc@338: val (env, n) = E.pushENamed env x (sequenceOf ()) adamc@338: in adamc@338: ([(L'.SgiSequence (!basis_r, x, n), loc)], (env, denv, gs)) adamc@338: end adamc@338: adamc@211: | L.SgiClassAbs x => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val (env, n) = E.pushCNamed env x k NONE adamc@211: val env = E.pushClass env n adamc@211: in adamc@211: ([(L'.SgiClassAbs (x, n), loc)], (env, denv, [])) adamc@211: end adamc@211: adamc@211: | L.SgiClass (x, c) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val (c', ck, gs) = elabCon (env, denv) c adamc@211: val (env, n) = E.pushCNamed env x k (SOME c') adamc@211: val env = E.pushClass env n adamc@211: in adamc@211: checkKind env c' ck k; adamc@211: ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) adamc@211: end adamc@211: adamc@83: and elabSgn (env, denv) (sgn, loc) = adamc@31: case sgn of adamc@31: L.SgnConst sgis => adamc@31: let adamc@88: val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis adamc@62: adamc@62: val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => adamc@62: case sgi of adamc@62: L'.SgiConAbs (x, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiCon (x, _, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@191: | L'.SgiDatatype (x, _, _, xncs) => adamc@156: let adamc@156: val vals = foldl (fn ((x, _, _), vals) => adamc@156: (if SS.member (vals, x) then adamc@156: sgnError env (DuplicateVal (loc, x)) adamc@156: else adamc@156: (); adamc@156: SS.add (vals, x))) adamc@156: vals xncs adamc@156: in adamc@156: if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => adamc@156: (if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiVal (x, _, _) => adamc@62: (if SS.member (vals, x) then adamc@62: sgnError env (DuplicateVal (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, SS.add (vals, x), sgns, strs)) adamc@62: | L'.SgiSgn (x, _, _) => adamc@62: (if SS.member (sgns, x) then adamc@62: sgnError env (DuplicateSgn (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, vals, SS.add (sgns, x), strs)) adamc@62: | L'.SgiStr (x, _, _) => adamc@62: (if SS.member (strs, x) then adamc@62: sgnError env (DuplicateStr (loc, x)) adamc@62: else adamc@62: (); adamc@88: (cons, vals, sgns, SS.add (strs, x))) adamc@203: | L'.SgiConstraint _ => (cons, vals, sgns, strs) adamc@205: | L'.SgiTable (_, x, _, _) => adamc@203: (if SS.member (vals, x) then adamc@203: sgnError env (DuplicateVal (loc, x)) adamc@203: else adamc@203: (); adamc@211: (cons, SS.add (vals, x), sgns, strs)) adamc@338: | L'.SgiSequence (_, x, _) => adamc@338: (if SS.member (vals, x) then adamc@338: sgnError env (DuplicateVal (loc, x)) adamc@338: else adamc@338: (); adamc@338: (cons, SS.add (vals, x), sgns, strs)) adamc@211: | L'.SgiClassAbs (x, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@211: (SS.add (cons, x), vals, sgns, strs)) adamc@211: | L'.SgiClass (x, _, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@211: (SS.add (cons, x), vals, sgns, strs))) adamc@62: (SS.empty, SS.empty, SS.empty, SS.empty) sgis' adamc@31: in adamc@83: ((L'.SgnConst sgis', loc), gs) adamc@31: end adamc@31: | L.SgnVar x => adamc@31: (case E.lookupSgn env x of adamc@31: NONE => adamc@31: (sgnError env (UnboundSgn (loc, x)); adamc@83: ((L'.SgnError, loc), [])) adamc@83: | SOME (n, sgis) => ((L'.SgnVar n, loc), [])) adamc@41: | L.SgnFun (m, dom, ran) => adamc@41: let adamc@83: val (dom', gs1) = elabSgn (env, denv) dom adamc@41: val (env', n) = E.pushStrNamed env m dom' adamc@83: val (ran', gs2) = elabSgn (env', denv) ran adamc@41: in adamc@83: ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2) adamc@41: end adamc@42: | L.SgnWhere (sgn, x, c) => adamc@42: let adamc@83: val (sgn', ds1) = elabSgn (env, denv) sgn adamc@83: val (c', ck, ds2) = elabCon (env, denv) c adamc@42: in adamc@42: case #1 (hnormSgn env sgn') of adamc@83: L'.SgnError => (sgnerror, []) adamc@42: | L'.SgnConst sgis => adamc@75: if List.exists (fn (L'.SgiConAbs (x', _, k), _) => adamc@75: x' = x andalso adamc@75: (unifyKinds k ck adamc@75: handle KUnify x => sgnError env (WhereWrongKind x); adamc@42: true) adamc@42: | _ => false) sgis then adamc@83: ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2) adamc@42: else adamc@42: (sgnError env (UnWhereable (sgn', x)); adamc@83: (sgnerror, [])) adamc@42: | _ => (sgnError env (UnWhereable (sgn', x)); adamc@83: (sgnerror, [])) adamc@42: end adamc@59: | L.SgnProj (m, ms, x) => adamc@59: (case E.lookupStr env m of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@83: (sgnerror, [])) adamc@59: | SOME (n, sgn) => adamc@59: let adamc@59: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@59: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@59: (strerror, sgnerror)) adamc@59: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@59: ((L'.StrVar n, loc), sgn) ms adamc@59: in adamc@59: case E.projectSgn env {sgn = sgn, str = str, field = x} of adamc@59: NONE => (sgnError env (UnboundSgn (loc, x)); adamc@83: (sgnerror, [])) adamc@83: | SOME _ => ((L'.SgnProj (n, ms, x), loc), []) adamc@59: end) adamc@59: adamc@31: adamc@66: fun selfify env {str, strs, sgn} = adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnError => sgn adamc@66: | L'.SgnVar _ => sgn adamc@66: adamc@66: | L'.SgnConst sgis => adamc@66: (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => adamc@66: (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | (L'.SgiDatatype (x, n, xs, xncs), loc) => adamc@191: (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@218: | (L'.SgiClassAbs (x, n), loc) => adamc@218: (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc) adamc@66: | (L'.SgiStr (x, n, sgn), loc) => adamc@66: (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) adamc@66: | x => x) sgis), #2 sgn) adamc@66: | L'.SgnFun _ => sgn adamc@66: | L'.SgnWhere _ => sgn adamc@66: | L'.SgnProj (m, ms, x) => adamc@66: case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar m, #2 sgn) ms, adamc@66: sgn = #2 (E.lookupStrNamed env m), adamc@66: field = x} of adamc@66: NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" adamc@66: | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} adamc@66: adamc@66: fun selfifyAt env {str, sgn} = adamc@66: let adamc@66: fun self (str, _) = adamc@66: case str of adamc@66: L'.StrVar x => SOME (x, []) adamc@66: | L'.StrProj (str, x) => adamc@66: (case self str of adamc@66: NONE => NONE adamc@66: | SOME (m, ms) => SOME (m, ms @ [x])) adamc@66: | _ => NONE adamc@66: in adamc@66: case self str of adamc@66: NONE => sgn adamc@66: | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} adamc@66: end adamc@66: adamc@88: fun dopen (env, denv) {str, strs, sgn} = adamc@66: let adamc@66: val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar str, #2 sgn) strs adamc@66: in adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnConst sgis => adamc@88: ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => adamc@162: let adamc@162: val d = adamc@162: case sgi of adamc@162: L'.SgiConAbs (x, n, k) => adamc@162: let adamc@162: val c = (L'.CModProj (str, strs, x), loc) adamc@162: in adamc@162: (L'.DCon (x, n, k, c), loc) adamc@162: end adamc@162: | L'.SgiCon (x, n, k, c) => adamc@162: (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | L'.SgiDatatype (x, n, xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) adamc@162: | L'.SgiVal (x, n, t) => adamc@162: (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiStr (x, n, sgn) => adamc@162: (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) adamc@162: | L'.SgiSgn (x, n, sgn) => adamc@162: (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiConstraint (c1, c2) => adamc@162: (L'.DConstraint (c1, c2), loc) adamc@205: | L'.SgiTable (_, x, n, c) => adamc@210: (L'.DVal (x, n, (L'.CApp (tableOf (), c), loc), adamc@203: (L'.EModProj (str, strs, x), loc)), loc) adamc@338: | L'.SgiSequence (_, x, n) => adamc@338: (L'.DVal (x, n, sequenceOf (), adamc@338: (L'.EModProj (str, strs, x), loc)), loc) adamc@211: | L'.SgiClassAbs (x, n) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@211: (L'.DCon (x, n, k, c), loc) adamc@211: end adamc@211: | L'.SgiClass (x, n, _) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@211: (L'.DCon (x, n, k, c), loc) adamc@211: end adamc@162: in adamc@162: (d, (E.declBinds env' d, denv')) adamc@162: end) adamc@88: (env, denv) sgis adamc@66: | _ => (strError env (UnOpenable sgn); adamc@88: ([], (env, denv))) adamc@66: end adamc@66: adamc@88: fun dopenConstraints (loc, env, denv) {str, strs} = adamc@88: case E.lookupStr env str of adamc@88: NONE => (strError env (UnboundStr (loc, str)); adamc@88: denv) adamc@88: | SOME (n, sgn) => adamc@88: let adamc@88: val (st, sgn) = foldl (fn (m, (str, sgn)) => adamc@88: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@88: NONE => (strError env (UnboundStr (loc, m)); adamc@88: (strerror, sgnerror)) adamc@88: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@88: ((L'.StrVar n, loc), sgn) strs adamc@88: adamc@88: val cso = E.projectConstraints env {sgn = sgn, str = st} adamc@88: adamc@88: val denv = case cso of adamc@88: NONE => (strError env (UnboundStr (loc, str)); adamc@88: denv) adamc@90: | SOME cs => foldl (fn ((c1, c2), denv) => adamc@90: let adamc@90: val (denv, gs) = D.assert env denv (c1, c2) adamc@90: in adamc@90: case gs of adamc@90: [] => () adamc@90: | _ => raise Fail "dopenConstraints: Sub-constraints remain"; adamc@90: adamc@90: denv adamc@90: end) denv cs adamc@88: in adamc@88: denv adamc@88: end adamc@88: adamc@31: fun sgiOfDecl (d, loc) = adamc@31: case d of adamc@123: L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] adamc@156: | L'.DDatatype x => [(L'.SgiDatatype x, loc)] adamc@156: | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] adamc@123: | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] adamc@123: | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis adamc@123: | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] adamc@123: | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] adamc@123: | L'.DExport _ => [] adamc@205: | L'.DTable (tn, x, n, c) => [(L'.SgiTable (tn, x, n, c), loc)] adamc@338: | L'.DSequence (tn, x, n) => [(L'.SgiSequence (tn, x, n), loc)] adamc@213: | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, c), loc)] adamc@271: | L'.DDatabase _ => [] adamc@88: adamc@88: fun sgiBindsD (env, denv) (sgi, _) = adamc@88: case sgi of adamc@90: L'.SgiConstraint (c1, c2) => adamc@90: (case D.assert env denv (c1, c2) of adamc@90: (denv, []) => denv adamc@90: | _ => raise Fail "sgiBindsD: Sub-constraints remain") adamc@88: | _ => denv adamc@31: adamc@86: fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = adamc@35: case (#1 (hnormSgn env sgn1), #1 (hnormSgn env sgn2)) of adamc@31: (L'.SgnError, _) => () adamc@31: | (_, L'.SgnError) => () adamc@31: adamc@31: | (L'.SgnConst sgis1, L'.SgnConst sgis2) => adamc@31: let adamc@156: fun folder (sgi2All as (sgi, loc), (env, denv)) = adamc@31: let adamc@31: fun seek p = adamc@31: let adamc@88: fun seek (env, denv) ls = adamc@31: case ls of adamc@31: [] => (sgnError env (UnmatchedSgi sgi2All); adamc@88: (env, denv)) adamc@31: | h :: t => adamc@31: case p h of adamc@88: NONE => seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t adamc@88: | SOME envs => envs adamc@31: in adamc@88: seek (env, denv) sgis1 adamc@31: end adamc@31: in adamc@31: case sgi of adamc@31: L'.SgiConAbs (x, n2, k2) => adamc@31: seek (fn sgi1All as (sgi1, _) => adamc@31: let adamc@41: fun found (x', n1, k1, co1) = adamc@41: if x = x' then adamc@41: let adamc@41: val () = unifyKinds k1 k2 adamc@41: handle KUnify (k1, k2, err) => adamc@41: sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) adamc@41: val env = E.pushCNamedAs env x n1 k1 co1 adamc@41: in adamc@41: SOME (if n1 = n2 then adamc@41: env adamc@41: else adamc@88: E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)), adamc@88: denv) adamc@41: end adamc@41: else adamc@41: NONE adamc@31: in adamc@31: case sgi1 of adamc@41: L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) adamc@41: | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) adamc@191: | L'.SgiDatatype (x', n1, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', NONE) adamc@191: end adamc@191: | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) adamc@191: end adamc@211: | L'.SgiClassAbs (x', n1) => found (x', n1, adamc@218: (L'.KArrow ((L'.KType, loc), adamc@218: (L'.KType, loc)), loc), adamc@218: NONE) adamc@211: | L'.SgiClass (x', n1, c) => found (x', n1, adamc@211: (L'.KArrow ((L'.KType, loc), adamc@211: (L'.KType, loc)), loc), adamc@211: SOME c) adamc@31: | _ => NONE adamc@31: end) adamc@31: adamc@31: | L'.SgiCon (x, n2, k2, c2) => adamc@31: seek (fn sgi1All as (sgi1, _) => adamc@211: let adamc@211: fun found (x', n1, k1, c1) = adamc@211: if x = x' then adamc@211: let adamc@327: fun good () = adamc@327: let adamc@327: val env = E.pushCNamedAs env x n2 k2 (SOME c2) adamc@327: val env = if n1 = n2 then adamc@327: env adamc@327: else adamc@327: E.pushCNamedAs env x n1 k1 (SOME c1) adamc@327: in adamc@327: SOME (env, denv) adamc@327: end adamc@211: in adamc@211: (case unifyCons (env, denv) c1 c2 of adamc@211: [] => good () adamc@211: | _ => NONE) adamc@211: handle CUnify (c1, c2, err) => adamc@211: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | L'.SgiClass (x', n1, c1) => adamc@211: found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: adamc@191: | L'.SgiDatatype (x, n2, xs2, xncs2) => adamc@156: seek (fn sgi1All as (sgi1, _) => adamc@160: let adamc@191: fun found (n1, xs1, xncs1) = adamc@160: let adamc@160: fun mismatched ue = adamc@160: (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); adamc@160: SOME (env, denv)) adamc@156: adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 adamc@191: adamc@160: fun good () = adamc@160: let adamc@160: val env = E.sgiBinds env sgi2All adamc@160: val env = if n1 = n2 then adamc@160: env adamc@160: else adamc@160: E.pushCNamedAs env x n1 (L'.KType, loc) adamc@160: (SOME (L'.CNamed n1, loc)) adamc@160: in adamc@160: SOME (env, denv) adamc@160: end adamc@156: adamc@191: val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 adamc@160: fun xncBad ((x1, _, t1), (x2, _, t2)) = adamc@160: String.compare (x1, x2) <> EQUAL adamc@160: orelse case (t1, t2) of adamc@160: (NONE, NONE) => false adamc@160: | (SOME t1, SOME t2) => adamc@160: not (List.null (unifyCons (env, denv) t1 t2)) adamc@160: | _ => true adamc@160: in adamc@191: (if xs1 <> xs2 adamc@191: orelse length xncs1 <> length xncs2 adamc@160: orelse ListPair.exists xncBad (xncs1, xncs2) then adamc@160: mismatched NONE adamc@160: else adamc@160: good ()) adamc@160: handle CUnify ue => mismatched (SOME ue) adamc@160: end adamc@160: in adamc@160: case sgi1 of adamc@191: L'.SgiDatatype (x', n1, xs, xncs1) => adamc@160: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@160: else adamc@160: NONE adamc@191: | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => adamc@162: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@162: else adamc@162: NONE adamc@160: | _ => NONE adamc@160: end) adamc@156: adamc@191: | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => adamc@158: seek (fn sgi1All as (sgi1, _) => adamc@158: case sgi1 of adamc@191: L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => adamc@158: if x = x' then adamc@158: let adamc@158: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@158: val t1 = (L'.CModProj (m11, ms1, s1), loc) adamc@158: val t2 = (L'.CModProj (m12, ms2, s2), loc) adamc@158: adamc@158: fun good () = adamc@158: let adamc@191: val env = E.pushCNamedAs env x n1 k' (SOME t1) adamc@191: val env = E.pushCNamedAs env x n2 k' (SOME t2) adamc@158: in adamc@158: SOME (env, denv) adamc@158: end adamc@158: in adamc@158: (case unifyCons (env, denv) t1 t2 of adamc@158: [] => good () adamc@158: | _ => NONE) adamc@158: handle CUnify (c1, c2, err) => adamc@158: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@158: good ()) adamc@158: end adamc@158: else adamc@158: NONE adamc@158: adamc@158: | _ => NONE) adamc@156: adamc@32: | L'.SgiVal (x, n2, c2) => adamc@32: seek (fn sgi1All as (sgi1, _) => adamc@32: case sgi1 of adamc@41: L'.SgiVal (x', n1, c1) => adamc@41: if x = x' then adamc@86: (case unifyCons (env, denv) c1 c2 of adamc@88: [] => SOME (env, denv) adamc@86: | _ => NONE) adamc@86: handle CUnify (c1, c2, err) => adamc@86: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@88: SOME (env, denv)) adamc@41: else adamc@41: NONE adamc@205: | L'.SgiTable (_, x', n1, c1) => adamc@203: if x = x' then adamc@210: (case unifyCons (env, denv) (L'.CApp (tableOf (), c1), loc) c2 of adamc@203: [] => SOME (env, denv) adamc@203: | _ => NONE) adamc@203: handle CUnify (c1, c2, err) => adamc@203: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@203: SOME (env, denv)) adamc@203: else adamc@203: NONE adamc@338: | L'.SgiSequence (_, x', n1) => adamc@338: if x = x' then adamc@338: (case unifyCons (env, denv) (sequenceOf ()) c2 of adamc@338: [] => SOME (env, denv) adamc@338: | _ => NONE) adamc@338: handle CUnify (c1, c2, err) => adamc@338: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@338: SOME (env, denv)) adamc@338: else adamc@338: NONE adamc@32: | _ => NONE) adamc@32: adamc@33: | L'.SgiStr (x, n2, sgn2) => adamc@33: seek (fn sgi1All as (sgi1, _) => adamc@33: case sgi1 of adamc@41: L'.SgiStr (x', n1, sgn1) => adamc@41: if x = x' then adamc@66: let adamc@86: val () = subSgn (env, denv) sgn1 sgn2 adamc@66: val env = E.pushStrNamedAs env x n1 sgn1 adamc@66: val env = if n1 = n2 then adamc@66: env adamc@66: else adamc@66: E.pushStrNamedAs env x n2 adamc@66: (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), adamc@66: sgn = sgn2}) adamc@66: in adamc@88: SOME (env, denv) adamc@66: end adamc@41: else adamc@41: NONE adamc@33: | _ => NONE) adamc@59: adamc@59: | L'.SgiSgn (x, n2, sgn2) => adamc@59: seek (fn sgi1All as (sgi1, _) => adamc@59: case sgi1 of adamc@59: L'.SgiSgn (x', n1, sgn1) => adamc@59: if x = x' then adamc@65: let adamc@86: val () = subSgn (env, denv) sgn1 sgn2 adamc@86: val () = subSgn (env, denv) sgn2 sgn1 adamc@65: adamc@65: val env = E.pushSgnNamedAs env x n2 sgn2 adamc@65: val env = if n1 = n2 then adamc@65: env adamc@65: else adamc@65: E.pushSgnNamedAs env x n1 sgn2 adamc@65: in adamc@88: SOME (env, denv) adamc@65: end adamc@59: else adamc@59: NONE adamc@59: | _ => NONE) adamc@88: adamc@88: | L'.SgiConstraint (c2, d2) => adamc@88: seek (fn sgi1All as (sgi1, _) => adamc@88: case sgi1 of adamc@88: L'.SgiConstraint (c1, d1) => adamc@88: if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then adamc@90: let adamc@90: val (denv, gs) = D.assert env denv (c2, d2) adamc@90: in adamc@90: case gs of adamc@90: [] => () adamc@90: | _ => raise Fail "subSgn: Sub-constraints remain"; adamc@90: adamc@90: SOME (env, denv) adamc@90: end adamc@88: else adamc@88: NONE adamc@88: | _ => NONE) adamc@203: adamc@205: | L'.SgiTable (_, x, n2, c2) => adamc@203: seek (fn sgi1All as (sgi1, _) => adamc@203: case sgi1 of adamc@205: L'.SgiTable (_, x', n1, c1) => adamc@203: if x = x' then adamc@203: (case unifyCons (env, denv) c1 c2 of adamc@203: [] => SOME (env, denv) adamc@203: | _ => NONE) adamc@203: handle CUnify (c1, c2, err) => adamc@203: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@203: SOME (env, denv)) adamc@203: else adamc@203: NONE adamc@203: | _ => NONE) adamc@211: adamc@338: | L'.SgiSequence (_, x, n2) => adamc@338: seek (fn sgi1All as (sgi1, _) => adamc@338: case sgi1 of adamc@338: L'.SgiSequence (_, x', n1) => adamc@338: if x = x' then adamc@338: SOME (env, denv) adamc@338: else adamc@338: NONE adamc@338: | _ => NONE) adamc@338: adamc@211: | L'.SgiClassAbs (x, n2) => adamc@211: seek (fn sgi1All as (sgi1, _) => adamc@211: let adamc@211: fun found (x', n1, co) = adamc@211: if x = x' then adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val env = E.pushCNamedAs env x n1 k co adamc@211: in adamc@211: SOME (if n1 = n2 then adamc@211: env adamc@211: else adamc@211: E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)), adamc@211: denv) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiClassAbs (x', n1) => found (x', n1, NONE) adamc@211: | L'.SgiClass (x', n1, c) => found (x', n1, SOME c) adamc@211: | _ => NONE adamc@211: end) adamc@211: | L'.SgiClass (x, n2, c2) => adamc@211: seek (fn sgi1All as (sgi1, _) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: fun found (x', n1, c1) = adamc@211: if x = x' then adamc@211: let adamc@218: fun good () = adamc@218: let adamc@218: val env = E.pushCNamedAs env x n2 k (SOME c2) adamc@218: val env = if n1 = n2 then adamc@218: env adamc@218: else adamc@218: E.pushCNamedAs env x n1 k (SOME c1) adamc@218: in adamc@218: SOME (env, denv) adamc@218: end adamc@211: in adamc@211: (case unifyCons (env, denv) c1 c2 of adamc@211: [] => good () adamc@211: | _ => NONE) adamc@211: handle CUnify (c1, c2, err) => adamc@211: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiClass (x', n1, c1) => found (x', n1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: end adamc@31: in adamc@88: ignore (foldl folder (env, denv) sgis2) adamc@31: end adamc@31: adamc@41: | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => adamc@43: let adamc@43: val ran1 = adamc@43: if n1 = n2 then adamc@43: ran1 adamc@43: else adamc@43: subStrInSgn (n1, n2) ran1 adamc@43: in adamc@86: subSgn (env, denv) dom2 dom1; adamc@86: subSgn (E.pushStrNamedAs env m2 n2 dom2, denv) ran1 ran2 adamc@43: end adamc@41: adamc@41: | _ => sgnError env (SgnWrongForm (sgn1, sgn2)) adamc@41: adamc@61: adamc@312: fun positive self = adamc@312: let adamc@312: open L adamc@312: adamc@312: fun none (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => none c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso none c2 adamc@312: | TCFun (_, _, _, c) => none c adamc@312: | TRecord c => none c adamc@312: adamc@312: | CVar ([], x) => x <> self adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => none c1 andalso none c2 adamc@312: | CAbs _ => false adamc@312: | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs adamc@312: | CConcat (c1, c2) => none c1 andalso none c2 adamc@312: | CFold => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all none cs adamc@312: | CProj (c, _) => none c adamc@312: adamc@312: | CWild _ => false adamc@312: adamc@312: fun pos (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => pos c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso pos c2 adamc@312: | TCFun (_, _, _, c) => pos c adamc@312: | TRecord c => pos c adamc@312: adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => pos c1 andalso none c2 adamc@312: | CAbs _ => false adamc@312: | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs adamc@312: | CConcat (c1, c2) => pos c1 andalso pos c2 adamc@312: | CFold => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all pos cs adamc@312: | CProj (c, _) => pos c adamc@312: adamc@312: | CWild _ => false adamc@312: in adamc@312: pos adamc@312: end adamc@312: adamc@325: fun wildifyStr env (str, sgn) = adamc@325: case #1 (hnormSgn env sgn) of adamc@325: L'.SgnConst sgis => adamc@325: (case #1 str of adamc@325: L.StrConst ds => adamc@325: let adamc@325: fun decompileCon env (c, loc) = adamc@325: case c of adamc@325: L'.CRel i => adamc@325: let adamc@325: val (s, _) = E.lookupCRel env i adamc@325: in adamc@325: SOME (L.CVar ([], s), loc) adamc@325: end adamc@325: | L'.CNamed i => adamc@325: let adamc@325: val (s, _, _) = E.lookupCNamed env i adamc@325: in adamc@325: SOME (L.CVar ([], s), loc) adamc@325: end adamc@325: | L'.CModProj (m1, ms, x) => adamc@325: let adamc@325: val (s, _) = E.lookupStrNamed env m1 adamc@325: in adamc@325: SOME (L.CVar (s :: ms, x), loc) adamc@325: end adamc@325: | L'.CName s => SOME (L.CName s, loc) adamc@325: | L'.CRecord (_, xcs) => adamc@325: let adamc@325: fun fields xcs = adamc@325: case xcs of adamc@325: [] => SOME [] adamc@325: | (x, t) :: xcs => adamc@325: case (decompileCon env x, decompileCon env t, fields xcs) of adamc@325: (SOME x, SOME t, SOME xcs) => SOME ((x, t) :: xcs) adamc@325: | _ => NONE adamc@325: in adamc@325: Option.map (fn xcs => (L.CRecord xcs, loc)) adamc@325: (fields xcs) adamc@325: end adamc@325: | L'.CConcat (c1, c2) => adamc@325: (case (decompileCon env c1, decompileCon env c2) of adamc@325: (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc) adamc@325: | _ => NONE) adamc@325: | L'.CUnit => SOME (L.CUnit, loc) adamc@325: adamc@325: | _ => NONE adamc@325: adamc@325: val (needed, constraints, _) = adamc@325: foldl (fn ((sgi, loc), (needed, constraints, env')) => adamc@325: let adamc@325: val (needed, constraints) = adamc@325: case sgi of adamc@325: L'.SgiConAbs (x, _, _) => (SS.add (needed, x), constraints) adamc@325: | L'.SgiConstraint cs => (needed, (env', cs, loc) :: constraints) adamc@325: | _ => (needed, constraints) adamc@325: in adamc@325: (needed, constraints, E.sgiBinds env' (sgi, loc)) adamc@325: end) adamc@325: (SS.empty, [], env) sgis adamc@325: adamc@325: val needed = foldl (fn ((d, _), needed) => adamc@325: case d of adamc@325: L.DCon (x, _, _) => (SS.delete (needed, x) adamc@325: handle NotFound => adamc@325: needed) adamc@325: | L.DClass (x, _) => (SS.delete (needed, x) adamc@325: handle NotFound => needed) adamc@325: | L.DOpen _ => SS.empty adamc@325: | _ => needed) adamc@325: needed ds adamc@325: adamc@325: val cds = List.mapPartial (fn (env', (c1, c2), loc) => adamc@325: case (decompileCon env' c1, decompileCon env' c2) of adamc@325: (SOME c1, SOME c2) => adamc@325: SOME (L.DConstraint (c1, c2), loc) adamc@325: | _ => NONE) constraints adamc@325: in adamc@325: case SS.listItems needed of adamc@325: [] => (L.StrConst (ds @ cds), #2 str) adamc@325: | xs => adamc@325: let adamc@325: val kwild = (L.KWild, #2 str) adamc@325: val cwild = (L.CWild kwild, #2 str) adamc@325: val ds' = map (fn x => (L.DCon (x, NONE, cwild), #2 str)) xs adamc@325: in adamc@325: (L.StrConst (ds @ ds' @ cds), #2 str) adamc@325: end adamc@325: end adamc@325: | _ => str) adamc@325: | _ => str adamc@325: adamc@334: val makeInstantiable = adamc@334: let adamc@334: fun kind k = k adamc@334: fun con c = adamc@334: case c of adamc@345: L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c) adamc@334: | _ => c adamc@334: in adamc@334: U.Con.map {kind = kind, con = con} adamc@334: end adamc@334: adamc@280: fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = adamc@255: let adamc@255: (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) adamc@255: adamc@255: val r = adamc@255: case d of adamc@255: L.DCon (x, ko, c) => adamc@255: let adamc@255: val k' = case ko of adamc@255: NONE => kunif loc adamc@255: | SOME k => elabKind k adamc@255: adamc@255: val (c', ck, gs') = elabCon (env, denv) c adamc@255: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@255: in adamc@255: checkKind env c' ck k'; adamc@255: adamc@255: ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: | L.DDatatype (x, xs, xcs) => adamc@255: let adamc@312: val positive = List.all (fn (_, to) => adamc@312: case to of adamc@312: NONE => true adamc@312: | SOME t => positive x t) xcs adamc@312: adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val (env, n) = E.pushCNamed env x k' NONE adamc@255: val t = (L'.CNamed n, loc) adamc@255: val nxs = length xs - 1 adamc@255: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@255: adamc@255: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@255: (E.pushCRel env' x k, adamc@255: D.enter denv')) (env, denv) xs adamc@255: adamc@255: val (xcs, (used, env, gs')) = adamc@255: ListUtil.foldlMap adamc@255: (fn ((x, to), (used, env, gs)) => adamc@255: let adamc@255: val (to, t, gs') = case to of adamc@255: NONE => (NONE, t, gs) adamc@255: | SOME t' => adamc@255: let adamc@255: val (t', tk, gs') = elabCon (env', denv') t' adamc@255: in adamc@255: checkKind env' t' tk k; adamc@255: (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) adamc@255: end adamc@255: val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@255: adamc@255: val (env, n') = E.pushENamed env x t adamc@255: in adamc@255: if SS.member (used, x) then adamc@255: strError env (DuplicateConstructor (x, loc)) adamc@255: else adamc@255: (); adamc@255: ((x, n', to), (SS.add (used, x), env, gs')) adamc@255: end) adamc@255: (SS.empty, env, []) xcs adamc@255: adamc@255: val env = E.pushDatatype env n xs xcs adamc@312: val d' = (L'.DDatatype (x, n, xs, xcs), loc) adamc@255: in adamc@312: if positive then adamc@312: () adamc@312: else adamc@312: declError env (Nonpositive d'); adamc@312: adamc@312: ([d'], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" adamc@255: adamc@255: | L.DDatatypeImp (x, m1 :: ms, s) => adamc@255: (case E.lookupStr env m1 of adamc@255: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@255: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: in adamc@255: case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of adamc@255: ((L'.CModProj (n, ms, s), _), gs') => adamc@255: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@255: NONE => (conError env (UnboundDatatype (loc, s)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (xs, xncs) => adamc@255: let adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val t = (L'.CModProj (n, ms, s), loc) adamc@255: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@255: val env = E.pushDatatype env n' xs xncs adamc@255: adamc@255: val t = (L'.CNamed n', loc) adamc@255: val env = foldl (fn ((x, n, to), env) => adamc@255: let adamc@255: val t = case to of adamc@255: NONE => t adamc@255: | SOME t' => (L'.TFun (t', t), loc) adamc@255: adamc@255: val t = foldr (fn (x, t) => adamc@255: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@255: t xs adamc@255: in adamc@255: E.pushENamedAs env x n t adamc@255: end) env xncs adamc@255: in adamc@255: ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs)) adamc@255: end) adamc@255: | _ => (strError env (NotDatatype loc); adamc@255: ([], (env, denv, []))) adamc@255: end) adamc@255: adamc@255: | L.DVal (x, co, e) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adamc@255: NONE => (cunif (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@255: adamc@255: val (e', et, gs2) = elabExp (env, denv) e adamc@255: val gs3 = checkCon (env, denv) e' et c' adamc@255: val (c', gs4) = normClassConstraint (env, denv) c' adamc@255: val (env', n) = E.pushENamed env x c' adamc@334: val c' = makeInstantiable c' adamc@255: in adamc@255: (*prefaces "DVal" [("x", Print.PD.string x), adamc@255: ("c'", p_con env c')];*) adamc@255: ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ enD gs4 @ gs)) adamc@255: end adamc@255: | L.DValRec vis => adamc@255: let adamc@255: fun allowable (e, _) = adamc@255: case e of adamc@255: L.EAbs _ => true adamc@255: | L.ECAbs (_, _, _, e) => allowable e adamc@255: | L.EDisjoint (_, _, e) => allowable e adamc@255: | _ => false adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap adamc@255: (fn ((x, co, e), gs) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adamc@255: NONE => (cunif (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@255: in adamc@255: ((x, c', e), enD gs1 @ gs) adamc@280: end) gs vis adamc@255: adamc@255: val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => adamc@255: let adamc@255: val (env, n) = E.pushENamed env x c' adamc@255: in adamc@255: ((x, n, c', e), env) adamc@255: end) env vis adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => adamc@255: let adamc@255: val (e', et, gs1) = elabExp (env, denv) e adamc@255: adamc@255: val gs2 = checkCon (env, denv) e' et c' adamc@334: adamc@334: val c' = makeInstantiable c' adamc@255: in adamc@255: if allowable e then adamc@255: () adamc@255: else adamc@255: expError env (IllegalRec (x, e')); adamc@255: ((x, n, c', e'), gs1 @ enD gs2 @ gs) adamc@255: end) gs vis adamc@255: in adamc@255: ([(L'.DValRec vis, loc)], (env, denv, gs)) adamc@255: end adamc@255: adamc@255: | L.DSgn (x, sgn) => adamc@255: let adamc@255: val (sgn', gs') = elabSgn (env, denv) sgn adamc@255: val (env', n) = E.pushSgnNamed env x sgn' adamc@255: in adamc@255: ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DStr (x, sgno, str) => adamc@255: let adamc@255: val () = if x = "Basis" then adamc@255: raise Fail "Not allowed to redefine structure 'Basis'" adamc@255: else adamc@255: () adamc@255: adamc@255: val formal = Option.map (elabSgn (env, denv)) sgno adamc@255: adamc@255: val (str', sgn', gs') = adamc@255: case formal of adamc@255: NONE => adamc@255: let adamc@255: val (str', actual, gs') = elabStr (env, denv) str adamc@255: in adamc@255: (str', selfifyAt env {str = str', sgn = actual}, gs') adamc@255: end adamc@255: | SOME (formal, gs1) => adamc@255: let adamc@325: val str = wildifyStr env (str, formal) adamc@255: val (str', actual, gs2) = elabStr (env, denv) str adamc@255: in adamc@255: subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal; adamc@255: (str', formal, enD gs1 @ gs2) adamc@255: end adamc@255: adamc@255: val (env', n) = E.pushStrNamed env x sgn' adamc@255: in adamc@255: case #1 (hnormSgn env sgn') of adamc@255: L'.SgnFun _ => adamc@255: (case #1 str' of adamc@255: L'.StrFun _ => () adamc@255: | _ => strError env (FunctorRebind loc)) adamc@255: | _ => (); adamc@255: adamc@255: ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DFfiStr (x, sgn) => adamc@255: let adamc@255: val (sgn', gs') = elabSgn (env, denv) sgn adamc@255: adamc@255: val (env', n) = E.pushStrNamed env x sgn' adamc@255: in adamc@255: ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpen (m, ms) => adamc@255: (case E.lookupStr env m of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (_, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: adamc@255: val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} adamc@255: val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} adamc@255: in adamc@255: (ds, (env', denv', gs)) adamc@255: end) adamc@255: adamc@255: | L.DConstraint (c1, c2) => adamc@255: let adamc@255: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@255: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@255: val gs3 = D.prove env denv (c1', c2', loc) adamc@255: adamc@255: val (denv', gs4) = D.assert env denv (c1', c2') adamc@255: in adamc@255: checkKind env c1' k1 (L'.KRecord (kunif loc), loc); adamc@255: checkKind env c2' k2 (L'.KRecord (kunif loc), loc); adamc@255: adamc@255: ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpenConstraints (m, ms) => adamc@255: let adamc@255: val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} adamc@255: in adamc@255: ([], (env, denv, gs)) adamc@255: end adamc@255: adamc@255: | L.DExport str => adamc@255: let adamc@255: val (str', sgn, gs') = elabStr (env, denv) str adamc@255: adamc@255: val sgn = adamc@255: case #1 (hnormSgn env sgn) of adamc@255: L'.SgnConst sgis => adamc@255: let adamc@255: fun doOne (all as (sgi, _), env) = adamc@255: (case sgi of adamc@255: L'.SgiVal (x, n, t) => adamc@325: let adamc@325: fun doPage (makeRes, ran) = adamc@325: case hnormCon (env, denv) ran of adamc@325: ((L'.CApp (tf, arg), _), []) => adamc@325: (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of adamc@325: (((L'.CModProj (basis, [], "transaction"), _), []), adamc@325: ((L'.CApp (tf, arg3), _), [])) => adamc@325: (case (basis = !basis_r, adamc@325: hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of adamc@325: (true, adamc@325: ((L'.CApp (tf, arg2), _), []), adamc@325: (((L'.CRecord (_, []), _), []))) => adamc@325: (case (hnormCon (env, denv) tf) of adamc@325: ((L'.CApp (tf, arg1), _), []) => adamc@325: (case (hnormCon (env, denv) tf, adamc@325: hnormCon (env, denv) arg1, adamc@325: hnormCon (env, denv) arg2) of adamc@325: ((tf, []), (arg1, []), adamc@325: ((L'.CRecord (_, []), _), [])) => adamc@325: let adamc@325: val t = (L'.CApp (tf, arg1), loc) adamc@325: val t = (L'.CApp (t, arg2), loc) adamc@325: val t = (L'.CApp (t, arg3), loc) adamc@325: val t = (L'.CApp ( adamc@325: (L'.CModProj adamc@325: (basis, [], "transaction"), loc), adamc@325: t), loc) adamc@325: in adamc@325: (L'.SgiVal (x, n, makeRes t), loc) adamc@325: end adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all adamc@325: in adamc@325: case hnormCon (env, denv) t of adamc@325: ((L'.TFun (dom, ran), _), []) => adamc@325: (case hnormCon (env, denv) dom of adamc@325: ((L'.TRecord domR, _), []) => adamc@325: doPage (fn t => (L'.TFun ((L'.TRecord domR, adamc@325: loc), adamc@325: t), loc), ran) adamc@325: | _ => all) adamc@325: | _ => doPage (fn t => t, t) adamc@325: end adamc@255: | _ => all, adamc@255: E.sgiBinds env all) adamc@255: in adamc@255: (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) adamc@255: end adamc@255: | _ => sgn adamc@255: in adamc@255: ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DTable (x, c) => adamc@255: let adamc@255: val (c', k, gs') = elabCon (env, denv) c adamc@255: val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) adamc@255: in adamc@255: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@255: ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@255: end adamc@338: | L.DSequence x => adamc@338: let adamc@338: val (env, n) = E.pushENamed env x (sequenceOf ()) adamc@338: in adamc@338: ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) adamc@338: end adamc@255: adamc@255: | L.DClass (x, c) => adamc@255: let adamc@255: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@280: val (c', ck, gs') = elabCon (env, denv) c adamc@255: val (env, n) = E.pushCNamed env x k (SOME c') adamc@255: val env = E.pushClass env n adamc@255: in adamc@255: checkKind env c' ck k; adamc@280: ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@255: end adamc@271: adamc@280: | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) adamc@280: adamc@280: (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) adamc@255: in adamc@280: (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), adamc@280: ("|tcs|", PD.string (Int.toString (length tcs)))];*) adamc@280: adamc@255: r adamc@255: end adamc@211: adamc@83: and elabStr (env, denv) (str, loc) = adamc@31: case str of adamc@31: L.StrConst ds => adamc@31: let adamc@88: val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds adamc@123: val sgis = ListUtil.mapConcat sgiOfDecl ds' adamc@63: adamc@63: val (sgis, _, _, _, _) = adamc@64: foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => adamc@63: case sgi of adamc@64: L'.SgiConAbs (x, n, k) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiCon (x, n, k, c) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@191: | L'.SgiDatatype (x, n, xs, xncs) => adamc@156: let adamc@156: val (cons, x) = adamc@156: if SS.member (cons, x) then adamc@156: (cons, "?" ^ x) adamc@156: else adamc@156: (SS.add (cons, x), x) adamc@156: adamc@156: val (xncs, vals) = adamc@156: ListUtil.foldlMap adamc@156: (fn ((x, n, t), vals) => adamc@156: if SS.member (vals, x) then adamc@156: (("?" ^ x, n, t), vals) adamc@156: else adamc@156: ((x, n, t), SS.add (vals, x))) adamc@156: vals xncs adamc@156: in adamc@191: ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@156: let adamc@156: val (cons, x) = adamc@156: if SS.member (cons, x) then adamc@156: (cons, "?" ^ x) adamc@156: else adamc@156: (SS.add (cons, x), x) adamc@156: in adamc@191: ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@64: | L'.SgiVal (x, n, c) => adamc@64: let adamc@64: val (vals, x) = adamc@64: if SS.member (vals, x) then adamc@64: (vals, "?" ^ x) adamc@64: else adamc@64: (SS.add (vals, x), x) adamc@64: in adamc@64: ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiSgn (x, n, sgn) => adamc@64: let adamc@64: val (sgns, x) = adamc@64: if SS.member (sgns, x) then adamc@64: (sgns, "?" ^ x) adamc@64: else adamc@64: (SS.add (sgns, x), x) adamc@64: in adamc@64: ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: adamc@64: | L'.SgiStr (x, n, sgn) => adamc@64: let adamc@64: val (strs, x) = adamc@64: if SS.member (strs, x) then adamc@64: (strs, "?" ^ x) adamc@64: else adamc@64: (SS.add (strs, x), x) adamc@64: in adamc@64: ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@88: end adamc@203: | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) adamc@205: | L'.SgiTable (tn, x, n, c) => adamc@203: let adamc@203: val (vals, x) = adamc@203: if SS.member (vals, x) then adamc@203: (vals, "?" ^ x) adamc@203: else adamc@203: (SS.add (vals, x), x) adamc@203: in adamc@205: ((L'.SgiTable (tn, x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@211: end adamc@338: | L'.SgiSequence (tn, x, n) => adamc@338: let adamc@338: val (vals, x) = adamc@338: if SS.member (vals, x) then adamc@338: (vals, "?" ^ x) adamc@338: else adamc@338: (SS.add (vals, x), x) adamc@338: in adamc@338: ((L'.SgiSequence (tn, x, n), loc) :: sgis, cons, vals, sgns, strs) adamc@338: end adamc@211: | L'.SgiClassAbs (x, n) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@211: ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs) adamc@211: end adamc@211: | L'.SgiClass (x, n, c) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@211: ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@203: end) adamc@64: adamc@63: ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis adamc@31: in adamc@83: ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) adamc@31: end adamc@31: | L.StrVar x => adamc@31: (case E.lookupStr env x of adamc@31: NONE => adamc@31: (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, [])) adamc@34: | L.StrProj (str, x) => adamc@34: let adamc@83: val (str', sgn, gs) = elabStr (env, denv) str adamc@34: in adamc@34: case E.projectStr env {str = str', sgn = sgn, field = x} of adamc@34: NONE => (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs) adamc@34: end adamc@41: | L.StrFun (m, dom, ranO, str) => adamc@41: let adamc@83: val (dom', gs1) = elabSgn (env, denv) dom adamc@41: val (env', n) = E.pushStrNamed env m dom' adamc@83: val (str', actual, gs2) = elabStr (env', denv) str adamc@41: adamc@83: val (formal, gs3) = adamc@41: case ranO of adamc@83: NONE => (actual, []) adamc@41: | SOME ran => adamc@41: let adamc@83: val (ran', gs) = elabSgn (env', denv) ran adamc@41: in adamc@86: subSgn (env', denv) actual ran'; adamc@83: (ran', gs) adamc@41: end adamc@41: in adamc@41: ((L'.StrFun (m, n, dom', formal, str'), loc), adamc@83: (L'.SgnFun (m, n, dom', formal), loc), adamc@228: enD gs1 @ gs2 @ enD gs3) adamc@41: end adamc@44: | L.StrApp (str1, str2) => adamc@44: let adamc@83: val (str1', sgn1, gs1) = elabStr (env, denv) str1 adamc@325: val str2 = adamc@325: case sgn1 of adamc@325: (L'.SgnFun (_, _, dom, _), _) => adamc@325: wildifyStr env (str2, dom) adamc@325: | _ => str2 adamc@83: val (str2', sgn2, gs2) = elabStr (env, denv) str2 adamc@44: in adamc@44: case #1 (hnormSgn env sgn1) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnFun (m, n, dom, ran) => adamc@86: (subSgn (env, denv) sgn2 dom; adamc@44: case #1 (hnormSgn env ran) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnConst sgis => adamc@44: ((L'.StrApp (str1', str2'), loc), adamc@83: (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), adamc@83: gs1 @ gs2) adamc@44: | _ => raise Fail "Unable to hnormSgn in functor application") adamc@44: | _ => (strError env (NotFunctor sgn1); adamc@83: (strerror, sgnerror, [])) adamc@44: end adamc@31: adamc@325: fun elabFile basis topStr topSgn env file = adamc@56: let adamc@83: val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) adamc@83: val () = case gs of adamc@83: [] => () adamc@207: | _ => (app (fn (_, env, _, c1, c2) => adamc@207: prefaces "Unresolved" adamc@207: [("c1", p_con env c1), adamc@207: ("c2", p_con env c2)]) gs; adamc@207: raise Fail "Unresolved disjointness constraints in Basis") adamc@83: adamc@56: val (env', basis_n) = E.pushStrNamed env "Basis" sgn adamc@210: val () = basis_r := basis_n adamc@56: adamc@88: val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} adamc@56: adamc@56: fun discoverC r x = adamc@56: case E.lookupC env' x of adamc@56: E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") adamc@56: | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis") adamc@56: | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc) adamc@56: adamc@56: val () = discoverC int "int" adamc@56: val () = discoverC float "float" adamc@56: val () = discoverC string "string" adamc@203: val () = discoverC table "sql_table" adamc@56: adamc@325: val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@325: | _ => raise Fail "Unresolved disjointness constraints in top.urs" adamc@325: val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@329: | _ => app (fn Disjoint (loc, env, denv, c1, c2) => adamc@329: (case D.prove env denv (c1, c2, loc) of adamc@329: [] => () adamc@329: | _ => adamc@329: (prefaces "Unresolved constraint in top.ur" adamc@329: [("loc", PD.string (ErrorMsg.spanToString loc)), adamc@329: ("c1", p_con env c1), adamc@329: ("c2", p_con env c2)]; adamc@329: raise Fail "Unresolve constraint in top.ur")) adamc@329: | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs adamc@325: val () = subSgn (env', D.empty) topSgn' topSgn adamc@325: adamc@325: val (env', top_n) = E.pushStrNamed env' "Top" topSgn adamc@325: adamc@325: val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn} adamc@325: adamc@83: fun elabDecl' (d, (env, gs)) = adamc@76: let adamc@76: val () = resetKunif () adamc@76: val () = resetCunif () adamc@88: val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) adamc@76: in adamc@76: if ErrorMsg.anyErrors () then adamc@76: () adamc@76: else ( adamc@76: if List.exists kunifsInDecl ds then adamc@91: declError env (KunifsRemain ds) adamc@76: else adamc@76: (); adamc@76: adamc@76: case ListUtil.search cunifsInDecl ds of adamc@76: NONE => () adamc@76: | SOME loc => adamc@91: declError env (CunifsRemain ds) adamc@76: ); adamc@76: adamc@83: (ds, (env, gs)) adamc@76: end adamc@76: adamc@83: val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file adamc@56: in adamc@84: if ErrorMsg.anyErrors () then adamc@84: () adamc@84: else adamc@228: app (fn Disjoint (loc, env, denv, c1, c2) => adamc@228: (case D.prove env denv (c1, c2, loc) of adamc@228: [] => () adamc@228: | _ => adamc@228: (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; adamc@228: eprefaces' [("Con 1", p_con env c1), adamc@228: ("Con 2", p_con env c2), adamc@228: ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), adamc@228: ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) adamc@228: | TypeClass (env, c, r, loc) => adamc@349: let adamc@349: val c = ElabOps.hnormCon env c adamc@349: in adamc@349: case E.resolveClass env c of adamc@349: SOME e => r := SOME e adamc@349: | NONE => expError env (Unresolvable (loc, c)) adamc@349: end) gs; adamc@83: adamc@325: (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) adamc@325: :: ds adamc@325: @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) adamc@325: :: ds' @ file adamc@56: end adamc@2: adamc@2: end