adamc@412: (* Copyright (c) 2008, Adam Chlipala adamc@445: * All rights reserved. adamc@445: * adamc@445: * Redistribution and use in source and binary forms, with or without adamc@445: * modification, are permitted provided that the following conditions are met: adamc@445: * adamc@445: * - Redistributions of source code must retain the above copyright notice, adamc@445: * this list of conditions and the following disclaimer. adamc@445: * - Redistributions in binary form must reproduce the above copyright notice, adamc@445: * this list of conditions and the following disclaimer in the documentation adamc@445: * and/or other materials provided with the distribution. adamc@445: * - The names of contributors may not be used to endorse or promote products adamc@445: * derived from this software without specific prior written permission. adamc@445: * adamc@445: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@445: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@445: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@445: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@445: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@445: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@445: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@445: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@445: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@445: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@445: * POSSIBILITY OF SUCH DAMAGE. adamc@445: *) adamc@403: adamc@403: structure Elaborate :> ELABORATE = struct adamc@403: adamc@403: structure P = Prim adamc@403: structure L = Source adamc@403: structure L' = Elab adamc@403: structure E = ElabEnv adamc@403: structure U = ElabUtil adamc@403: structure D = Disjoint adamc@403: adamc@403: open Print adamc@403: open ElabPrint adamc@403: open ElabErr adamc@403: adamc@819: structure IS = IntBinarySet adamc@403: structure IM = IntBinaryMap adamc@403: adamc@403: structure SK = struct adamc@403: type ord_key = string adamc@403: val compare = String.compare adamc@403: end adamc@403: adamc@403: structure SS = BinarySetFn(SK) adamc@403: structure SM = BinaryMapFn(SK) adamc@403: adamc@403: val basis_r = ref 0 adamc@633: val top_r = ref 0 adamc@403: adamc@403: fun elabExplicitness e = adamc@403: case e of adamc@403: L.Explicit => L'.Explicit adamc@403: | L.Implicit => L'.Implicit adamc@403: adamc@403: fun occursKind r = adamc@403: U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' adamc@403: | _ => false) adamc@403: adamc@403: exception KUnify' of kunify_error adamc@403: adamc@623: fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = adamc@403: let adamc@403: fun err f = raise KUnify' (f (k1All, k2All)) adamc@403: in adamc@403: case (k1, k2) of adamc@403: (L'.KType, L'.KType) => () adamc@403: | (L'.KUnit, L'.KUnit) => () adamc@403: adamc@403: | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => adamc@623: (unifyKinds' env d1 d2; adamc@623: unifyKinds' env r1 r2) adamc@403: | (L'.KName, L'.KName) => () adamc@623: | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2 adamc@403: | (L'.KTuple ks1, L'.KTuple ks2) => adamc@623: ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2)) adamc@403: handle ListPair.UnequalLengths => err KIncompatible) adamc@403: adamc@623: | (L'.KRel n1, L'.KRel n2) => adamc@623: if n1 = n2 then adamc@623: () adamc@623: else adamc@623: err KIncompatible adamc@623: | (L'.KFun (x, k1), L'.KFun (_, k2)) => adamc@623: unifyKinds' (E.pushKRel env x) k1 k2 adamc@623: adamc@403: | (L'.KError, _) => () adamc@403: | (_, L'.KError) => () adamc@403: adamc@623: | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All adamc@623: | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All adamc@403: adamc@403: | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => adamc@403: if r1 = r2 then adamc@403: () adamc@403: else adamc@403: r1 := SOME k2All adamc@403: adamc@403: | (L'.KUnif (_, _, r), _) => adamc@403: if occursKind r k2All then adamc@403: err KOccursCheckFailed adamc@403: else adamc@403: r := SOME k2All adamc@403: | (_, L'.KUnif (_, _, r)) => adamc@403: if occursKind r k1All then adamc@403: err KOccursCheckFailed adamc@403: else adamc@403: r := SOME k1All adamc@403: adamc@403: | _ => err KIncompatible adamc@403: end adamc@403: adamc@403: exception KUnify of L'.kind * L'.kind * kunify_error adamc@403: adamc@623: fun unifyKinds env k1 k2 = adamc@623: unifyKinds' env k1 k2 adamc@403: handle KUnify' err => raise KUnify (k1, k2, err) adamc@403: adamc@403: fun checkKind env c k1 k2 = adamc@623: unifyKinds env k1 k2 adamc@403: handle KUnify (k1, k2, err) => adamc@403: conError env (WrongKind (c, k1, k2, err)) adamc@403: adamc@403: val dummy = ErrorMsg.dummySpan adamc@403: adamc@403: val ktype = (L'.KType, dummy) adamc@403: val kname = (L'.KName, dummy) adamc@403: val ktype_record = (L'.KRecord ktype, dummy) adamc@403: adamc@403: val cerror = (L'.CError, dummy) adamc@403: val kerror = (L'.KError, dummy) adamc@403: val eerror = (L'.EError, dummy) adamc@403: val sgnerror = (L'.SgnError, dummy) adamc@403: val strerror = (L'.StrError, dummy) adamc@403: adamc@403: val int = ref cerror adamc@403: val float = ref cerror adamc@403: val string = ref cerror adamc@821: val char = ref cerror adamc@403: val table = ref cerror adamc@403: adamc@403: local adamc@403: val count = ref 0 adamc@403: in adamc@403: adamc@403: fun resetKunif () = count := 0 adamc@403: adamc@403: fun kunif loc = adamc@403: let adamc@403: val n = !count adamc@403: val s = if n <= 26 then adamc@403: str (chr (ord #"A" + n)) adamc@403: else adamc@403: "U" ^ Int.toString (n - 26) adamc@403: in adamc@403: count := n + 1; adamc@838: (L'.KUnif (loc, s, ref NONE), loc) adamc@403: end adamc@403: adamc@403: end adamc@403: adamc@403: local adamc@403: val count = ref 0 adamc@403: in adamc@403: adamc@403: fun resetCunif () = count := 0 adamc@403: adamc@403: fun cunif (loc, k) = adamc@403: let adamc@403: val n = !count adamc@712: val s = if n < 26 then adamc@403: str (chr (ord #"A" + n)) adamc@403: else adamc@403: "U" ^ Int.toString (n - 26) adamc@403: in adamc@403: count := n + 1; adamc@838: (L'.CUnif (loc, k, s, ref NONE), loc) adamc@403: end adamc@403: adamc@403: end adamc@403: adamc@623: fun elabKind env (k, loc) = adamc@403: case k of adamc@403: L.KType => (L'.KType, loc) adamc@623: | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc) adamc@403: | L.KName => (L'.KName, loc) adamc@623: | L.KRecord k => (L'.KRecord (elabKind env k), loc) adamc@403: | L.KUnit => (L'.KUnit, loc) adamc@623: | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) adamc@403: | L.KWild => kunif loc adamc@403: adamc@623: | L.KVar s => (case E.lookupK env s of adamc@623: NONE => adamc@623: (kindError env (UnboundKind (loc, s)); adamc@623: kerror) adamc@623: | SOME n => (L'.KRel n, loc)) adamc@623: | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc) adamc@623: adamc@621: fun mapKind (dom, ran, loc)= adamc@621: (L'.KArrow ((L'.KArrow (dom, ran), loc), adamc@621: (L'.KArrow ((L'.KRecord dom, loc), adamc@621: (L'.KRecord ran, loc)), loc)), loc) adamc@403: adamc@403: fun hnormKind (kAll as (k, _)) = adamc@403: case k of adamc@403: L'.KUnif (_, _, ref (SOME k)) => hnormKind k adamc@403: | _ => kAll adamc@403: adamc@623: open ElabOps adamc@623: adamc@623: fun elabConHead (c as (_, loc)) k = adamc@623: let adamc@623: fun unravel (k, c) = adamc@623: case hnormKind k of adamc@623: (L'.KFun (x, k'), _) => adamc@623: let adamc@623: val u = kunif loc adamc@623: adamc@623: val k'' = subKindInKind (0, u) k' adamc@623: in adamc@623: unravel (k'', (L'.CKApp (c, u), loc)) adamc@623: end adamc@623: | _ => (c, k) adamc@623: in adamc@623: unravel (k, c) adamc@623: end adamc@623: adamc@403: fun elabCon (env, denv) (c, loc) = adamc@403: case c of adamc@403: L.CAnnot (c, k) => adamc@403: let adamc@623: val k' = elabKind env k adamc@403: val (c', ck, gs) = elabCon (env, denv) c adamc@403: in adamc@403: checkKind env c' ck k'; adamc@403: (c', k', gs) adamc@403: end adamc@403: adamc@403: | L.TFun (t1, t2) => adamc@403: let adamc@403: val (t1', k1, gs1) = elabCon (env, denv) t1 adamc@403: val (t2', k2, gs2) = elabCon (env, denv) t2 adamc@403: in adamc@403: checkKind env t1' k1 ktype; adamc@403: checkKind env t2' k2 ktype; adamc@403: ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2) adamc@403: end adamc@403: | L.TCFun (e, x, k, t) => adamc@403: let adamc@403: val e' = elabExplicitness e adamc@623: val k' = elabKind env k adamc@403: val env' = E.pushCRel env x k' adamc@403: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@403: in adamc@403: checkKind env t' tk ktype; adamc@403: ((L'.TCFun (e', x, k', t'), loc), ktype, gs) adamc@403: end adamc@623: | L.TKFun (x, t) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (t', tk, gs) = elabCon (env', denv) t adamc@623: in adamc@623: checkKind env t' tk ktype; adamc@623: ((L'.TKFun (x, t'), loc), ktype, gs) adamc@623: end adamc@628: | L.TDisjoint (c1, c2, c) => adamc@403: let adamc@403: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@403: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@403: adamc@403: val ku1 = kunif loc adamc@403: val ku2 = kunif loc adamc@403: adamc@628: val denv' = D.assert env denv (c1', c2') adamc@403: val (c', k, gs4) = elabCon (env, denv') c adamc@403: in adamc@403: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@403: checkKind env c2' k2 (L'.KRecord ku2, loc); adamc@403: adamc@628: ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs4) adamc@403: end adamc@403: | L.TRecord c => adamc@403: let adamc@403: val (c', ck, gs) = elabCon (env, denv) c adamc@403: val k = (L'.KRecord ktype, loc) adamc@403: in adamc@403: checkKind env c' ck k; adamc@403: ((L'.TRecord c', loc), ktype, gs) adamc@403: end adamc@403: adamc@403: | L.CVar ([], s) => adamc@403: (case E.lookupC env s of adamc@403: E.NotBound => adamc@403: (conError env (UnboundCon (loc, s)); adamc@403: (cerror, kerror, [])) adamc@403: | E.Rel (n, k) => adamc@623: let adamc@623: val (c, k) = elabConHead (L'.CRel n, loc) k adamc@623: in adamc@623: (c, k, []) adamc@623: end adamc@403: | E.Named (n, k) => adamc@623: let adamc@623: val (c, k) = elabConHead (L'.CNamed n, loc) k adamc@623: in adamc@623: (c, k, []) adamc@623: end) adamc@403: | L.CVar (m1 :: ms, s) => adamc@403: (case E.lookupStr env m1 of adamc@403: NONE => (conError env (UnboundStrInCon (loc, m1)); adamc@403: (cerror, kerror, [])) adamc@403: | SOME (n, sgn) => adamc@403: let adamc@403: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@403: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@403: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@403: (strerror, sgnerror)) adamc@403: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@403: ((L'.StrVar n, loc), sgn) ms adamc@403: adamc@403: val k = case E.projectCon env {sgn = sgn, str = str, field = s} of adamc@403: NONE => (conError env (UnboundCon (loc, s)); adamc@403: kerror) adamc@403: | SOME (k, _) => k adamc@403: in adamc@403: ((L'.CModProj (n, ms, s), loc), k, []) adamc@403: end) adamc@403: adamc@403: | L.CApp (c1, c2) => adamc@403: let adamc@403: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@403: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@403: val dom = kunif loc adamc@403: val ran = kunif loc adamc@403: in adamc@403: checkKind env c1' k1 (L'.KArrow (dom, ran), loc); adamc@403: checkKind env c2' k2 dom; adamc@403: ((L'.CApp (c1', c2'), loc), ran, gs1 @ gs2) adamc@403: end adamc@403: | L.CAbs (x, ko, t) => adamc@403: let adamc@403: val k' = case ko of adamc@403: NONE => kunif loc adamc@623: | SOME k => elabKind env k adamc@403: val env' = E.pushCRel env x k' adamc@403: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@403: in adamc@403: ((L'.CAbs (x, k', t'), loc), adamc@403: (L'.KArrow (k', tk), loc), adamc@403: gs) adamc@403: end adamc@623: | L.CKAbs (x, t) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (t', tk, gs) = elabCon (env', denv) t adamc@623: in adamc@623: ((L'.CKAbs (x, t'), loc), adamc@623: (L'.KFun (x, tk), loc), adamc@623: gs) adamc@623: end adamc@403: adamc@403: | L.CName s => adamc@403: ((L'.CName s, loc), kname, []) adamc@403: adamc@403: | L.CRecord xcs => adamc@403: let adamc@403: val k = kunif loc adamc@403: adamc@403: val (xcs', gs) = ListUtil.foldlMap (fn ((x, c), gs) => adamc@403: let adamc@403: val (x', xk, gs1) = elabCon (env, denv) x adamc@403: val (c', ck, gs2) = elabCon (env, denv) c adamc@403: in adamc@403: checkKind env x' xk kname; adamc@403: checkKind env c' ck k; adamc@403: ((x', c'), gs1 @ gs2 @ gs) adamc@403: end) [] xcs adamc@403: adamc@403: val rc = (L'.CRecord (k, xcs'), loc) adamc@403: (* Add duplicate field checking later. *) adamc@403: adamc@403: fun prove (xcs, ds) = adamc@403: case xcs of adamc@403: [] => ds adamc@403: | xc :: rest => adamc@403: let adamc@403: val r1 = (L'.CRecord (k, [xc]), loc) adamc@403: val ds = foldl (fn (xc', ds) => adamc@403: let adamc@403: val r2 = (L'.CRecord (k, [xc']), loc) adamc@403: in adamc@403: D.prove env denv (r1, r2, loc) @ ds adamc@403: end) adamc@403: ds rest adamc@403: in adamc@403: prove (rest, ds) adamc@403: end adamc@403: in adamc@403: (rc, (L'.KRecord k, loc), prove (xcs', gs)) adamc@403: end adamc@403: | L.CConcat (c1, c2) => adamc@403: let adamc@403: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@403: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@403: val ku = kunif loc adamc@403: val k = (L'.KRecord ku, loc) adamc@403: in adamc@403: checkKind env c1' k1 k; adamc@403: checkKind env c2' k2 k; adamc@403: ((L'.CConcat (c1', c2'), loc), k, adamc@403: D.prove env denv (c1', c2', loc) @ gs1 @ gs2) adamc@403: end adamc@621: | L.CMap => adamc@403: let adamc@403: val dom = kunif loc adamc@403: val ran = kunif loc adamc@403: in adamc@621: ((L'.CMap (dom, ran), loc), adamc@621: mapKind (dom, ran, loc), adamc@403: []) adamc@403: end adamc@403: adamc@403: | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) adamc@403: adamc@403: | L.CTuple cs => adamc@403: let adamc@403: val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) => adamc@403: let adamc@403: val (c', k, gs') = elabCon (env, denv) c adamc@403: in adamc@403: (c' :: cs', k :: ks, gs' @ gs) adamc@403: end) ([], [], []) cs adamc@403: in adamc@403: ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs) adamc@403: end adamc@403: | L.CProj (c, n) => adamc@403: let adamc@403: val (c', k, gs) = elabCon (env, denv) c adamc@403: in adamc@403: case hnormKind k of adamc@403: (L'.KTuple ks, _) => adamc@403: if n <= 0 orelse n > length ks then adamc@403: (conError env (ProjBounds (c', n)); adamc@83: (cerror, kerror, [])) adamc@403: else adamc@403: ((L'.CProj (c', n), loc), List.nth (ks, n - 1), gs) adamc@403: | k => (conError env (ProjMismatch (c', k)); adamc@403: (cerror, kerror, [])) adamc@403: end adamc@403: adamc@403: | L.CWild k => adamc@403: let adamc@623: val k' = elabKind env k adamc@403: in adamc@403: (cunif (loc, k'), k', []) adamc@403: end adamc@403: adamc@403: fun kunifsRemain k = adamc@403: case k of adamc@403: L'.KUnif (_, _, ref NONE) => true adamc@403: | _ => false adamc@403: fun cunifsRemain c = adamc@403: case c of adamc@710: L'.CUnif (loc, _, _, ref NONE) => SOME loc adamc@403: | _ => NONE adamc@403: adamc@403: val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, adamc@403: con = fn _ => false, adamc@403: exp = fn _ => false, adamc@403: sgn_item = fn _ => false, adamc@403: sgn = fn _ => false, adamc@403: str = fn _ => false, adamc@403: decl = fn _ => false} adamc@403: adamc@403: val cunifsInDecl = U.Decl.search {kind = fn _ => NONE, adamc@403: con = cunifsRemain, adamc@403: exp = fn _ => NONE, adamc@403: sgn_item = fn _ => NONE, adamc@403: sgn = fn _ => NONE, adamc@403: str = fn _ => NONE, adamc@403: decl = fn _ => NONE} adamc@403: adamc@403: fun occursCon r = adamc@403: U.Con.exists {kind = fn _ => false, adamc@403: con = fn L'.CUnif (_, _, _, r') => r = r' adamc@403: | _ => false} adamc@403: adamc@403: exception CUnify' of cunify_error adamc@403: adamc@403: exception SynUnif = E.SynUnif adamc@403: adamc@403: type record_summary = { adamc@403: fields : (L'.con * L'.con) list, adamc@403: unifs : (L'.con * L'.con option ref) list, adamc@403: others : L'.con list adamc@403: } adamc@403: adamc@403: fun summaryToCon {fields, unifs, others} = adamc@403: let adamc@403: val c = (L'.CRecord (ktype, []), dummy) adamc@403: val c = List.foldr (fn (c', c) => (L'.CConcat (c', c), dummy)) c others adamc@403: val c = List.foldr (fn ((c', _), c) => (L'.CConcat (c', c), dummy)) c unifs adamc@403: in adamc@403: (L'.CConcat ((L'.CRecord (ktype, fields), dummy), c), dummy) adamc@403: end adamc@403: adamc@403: fun p_summary env s = p_con env (summaryToCon s) adamc@403: adamc@403: exception CUnify of L'.con * L'.con * cunify_error adamc@403: adamc@403: fun kindof env (c, loc) = adamc@403: case c of adamc@403: L'.TFun _ => ktype adamc@403: | L'.TCFun _ => ktype adamc@403: | L'.TRecord _ => ktype adamc@628: | L'.TDisjoint _ => ktype adamc@403: adamc@403: | L'.CRel xn => #2 (E.lookupCRel env xn) adamc@403: | L'.CNamed xn => #2 (E.lookupCNamed env xn) adamc@403: | L'.CModProj (n, ms, x) => adamc@403: let adamc@403: val (_, sgn) = E.lookupStrNamed env n adamc@403: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@403: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@403: NONE => raise Fail "kindof: Unknown substructure" adamc@403: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@403: ((L'.StrVar n, loc), sgn) ms adamc@403: in adamc@403: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@403: NONE => raise Fail "kindof: Unknown con in structure" adamc@403: | SOME (k, _) => k adamc@403: end adamc@403: adamc@403: | L'.CApp (c, _) => adamc@403: (case hnormKind (kindof env c) of adamc@403: (L'.KArrow (_, k), _) => k adamc@403: | (L'.KError, _) => kerror adamc@413: | k => raise CUnify' (CKindof (k, c, "arrow"))) adamc@403: | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) adamc@628: adamc@403: adamc@403: | L'.CName _ => kname adamc@403: adamc@403: | L'.CRecord (k, _) => (L'.KRecord k, loc) adamc@403: | L'.CConcat (c, _) => kindof env c adamc@621: | L'.CMap (dom, ran) => mapKind (dom, ran, loc) adamc@403: adamc@403: | L'.CUnit => (L'.KUnit, loc) adamc@403: adamc@403: | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) adamc@403: | L'.CProj (c, n) => adamc@403: (case hnormKind (kindof env c) of adamc@403: (L'.KTuple ks, _) => List.nth (ks, n - 1) adamc@413: | k => raise CUnify' (CKindof (k, c, "tuple"))) adamc@403: adamc@403: | L'.CError => kerror adamc@403: | L'.CUnif (_, k, _, _) => k adamc@403: adamc@623: | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) adamc@623: | L'.CKApp (c, k) => adamc@623: (case hnormKind (kindof env c) of adamc@623: (L'.KFun (_, k'), _) => subKindInKind (0, k) k' adamc@623: | k => raise CUnify' (CKindof (k, c, "kapp"))) adamc@623: | L'.TKFun _ => ktype adamc@403: adamc@621: exception GuessFailure adamc@403: adamc@513: fun isUnitCon env (c, loc) = adamc@513: case c of adamc@513: L'.TFun _ => false adamc@513: | L'.TCFun _ => false adamc@513: | L'.TRecord _ => false adamc@628: | L'.TDisjoint _ => false adamc@513: adamc@513: | L'.CRel xn => #1 (#2 (E.lookupCRel env xn)) = L'.KUnit adamc@513: | L'.CNamed xn => #1 (#2 (E.lookupCNamed env xn)) = L'.KUnit adamc@518: | L'.CModProj (n, ms, x) => false adamc@518: (*let adamc@513: val (_, sgn) = E.lookupStrNamed env n adamc@513: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@513: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@513: NONE => raise Fail "kindof: Unknown substructure" adamc@513: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@513: ((L'.StrVar n, loc), sgn) ms adamc@513: in adamc@513: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@513: NONE => raise Fail "kindof: Unknown con in structure" adamc@513: | SOME ((k, _), _) => k = L'.KUnit adamc@518: end*) adamc@518: adamc@518: | L'.CApp (c, _) => false adamc@518: (*(case hnormKind (kindof env c) of adamc@513: (L'.KArrow (_, k), _) => #1 k = L'.KUnit adamc@513: | (L'.KError, _) => false adamc@518: | k => raise CUnify' (CKindof (k, c, "arrow")))*) adamc@513: | L'.CAbs _ => false adamc@513: adamc@513: | L'.CName _ => false adamc@513: adamc@513: | L'.CRecord _ => false adamc@513: | L'.CConcat _ => false adamc@621: | L'.CMap _ => false adamc@513: adamc@513: | L'.CUnit => true adamc@513: adamc@513: | L'.CTuple _ => false adamc@518: | L'.CProj (c, n) => false adamc@518: (*(case hnormKind (kindof env c) of adamc@513: (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit adamc@518: | k => raise CUnify' (CKindof (k, c, "tuple")))*) adamc@513: adamc@513: | L'.CError => false adamc@513: | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit adamc@513: adamc@623: | L'.CKAbs _ => false adamc@623: | L'.CKApp _ => false adamc@623: | L'.TKFun _ => false adamc@623: adamc@709: val recdCounter = ref 0 adamc@709: adamc@713: val mayDelay = ref false adamc@777: val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) adamc@777: adamc@830: val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list) adamc@830: adamc@777: fun unifyRecordCons env (loc, c1, c2) = adamc@403: let adamc@403: fun rkindof c = adamc@403: case hnormKind (kindof env c) of adamc@403: (L'.KRecord k, _) => k adamc@403: | (L'.KError, _) => kerror adamc@753: | (L'.KUnif (_, _, r), _) => adamc@753: let adamc@753: val k = kunif (#2 c) adamc@753: in adamc@753: r := SOME (L'.KRecord k, #2 c); adamc@753: k adamc@753: end adamc@413: | k => raise CUnify' (CKindof (k, c, "record")) adamc@403: adamc@403: val k1 = rkindof c1 adamc@403: val k2 = rkindof c2 adamc@403: adamc@628: val r1 = recordSummary env c1 adamc@628: val r2 = recordSummary env c2 adamc@403: in adamc@623: unifyKinds env k1 k2; adamc@777: unifySummaries env (loc, k1, r1, r2) adamc@403: end adamc@403: adamc@777: and normalizeRecordSummary env (r : record_summary) = adamc@777: recordSummary env (summaryToCon r) adamc@777: adamc@628: and recordSummary env c = adamc@403: let adamc@628: val c = hnormCon env c adamc@628: adamc@628: val sum = adamc@403: case c of adamc@628: (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []} adamc@403: | (L'.CConcat (c1, c2), _) => adamc@403: let adamc@628: val s1 = recordSummary env c1 adamc@628: val s2 = recordSummary env c2 adamc@403: in adamc@628: {fields = #fields s1 @ #fields s2, adamc@628: unifs = #unifs s1 @ #unifs s2, adamc@628: others = #others s1 @ #others s2} adamc@403: end adamc@628: | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c adamc@628: | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} adamc@628: | c' => {fields = [], unifs = [], others = [c']} adamc@403: in adamc@628: sum adamc@403: end adamc@403: adamc@628: and consEq env (c1, c2) = adamc@777: let adamc@777: val mayDelay' = !mayDelay adamc@777: in adamc@777: (mayDelay := false; adamc@777: unifyCons env c1 c2; adamc@777: mayDelay := mayDelay'; adamc@777: true) adamc@777: handle CUnify _ => (mayDelay := mayDelay'; false) adamc@777: end adamc@403: adamc@403: and consNeq env (c1, c2) = adamc@628: case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of adamc@403: (L'.CName x1, L'.CName x2) => x1 <> x2 adamc@403: | _ => false adamc@403: adamc@777: and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = adamc@403: let adamc@848: (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), adamc@848: ("#1", p_summary env s1), adamc@848: ("#2", p_summary env s2)]*) adamc@403: adamc@403: fun eatMatching p (ls1, ls2) = adamc@403: let adamc@403: fun em (ls1, ls2, passed1) = adamc@403: case ls1 of adamc@403: [] => (rev passed1, ls2) adamc@403: | h1 :: t1 => adamc@403: let adamc@403: fun search (ls2', passed2) = adamc@403: case ls2' of adamc@403: [] => em (t1, ls2, h1 :: passed1) adamc@403: | h2 :: t2 => adamc@403: if p (h1, h2) then adamc@403: em (t1, List.revAppend (passed2, t2), passed1) adamc@403: else adamc@403: search (t2, h2 :: passed2) adamc@403: in adamc@403: search (ls2, []) adamc@403: end adamc@403: in adamc@403: em (ls1, ls2, []) adamc@403: end adamc@403: adamc@403: val (fs1, fs2) = eatMatching (fn ((x1, c1), (x2, c2)) => adamc@403: not (consNeq env (x1, x2)) adamc@628: andalso consEq env (c1, c2) adamc@628: andalso consEq env (x1, x2)) adamc@403: (#fields s1, #fields s2) adamc@403: (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), adamc@403: ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) adamc@646: adamc@403: val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) adamc@646: adamc@628: val (others1, others2) = eatMatching (consEq env) (#others s1, #others s2) adamc@403: (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@403: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@709: fun unsummarize {fields, unifs, others} = adamc@709: let adamc@709: val c = (L'.CRecord (k, fields), loc) adamc@709: adamc@709: val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc)) adamc@709: c unifs adamc@709: in adamc@709: foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) adamc@709: c others adamc@709: end adamc@709: adamc@710: val empties = ([], [], [], [], [], []) adamc@710: adamc@709: val (unifs1, fs1, others1, unifs2, fs2, others2) = adamc@709: case (unifs1, fs1, others1, unifs2, fs2, others2) of adamc@709: orig as ([(_, r)], [], [], _, _, _) => adamc@709: let adamc@709: val c = unsummarize {fields = fs2, others = others2, unifs = unifs2} adamc@709: in adamc@709: if occursCon r c then adamc@709: orig adamc@709: else adamc@709: (r := SOME c; adamc@710: empties) adamc@709: end adamc@709: | orig as (_, _, _, [(_, r)], [], []) => adamc@709: let adamc@709: val c = unsummarize {fields = fs1, others = others1, unifs = unifs1} adamc@709: in adamc@709: if occursCon r c then adamc@709: orig adamc@709: else adamc@709: (r := SOME c; adamc@710: empties) adamc@709: end adamc@710: | orig as ([(_, r1 as ref NONE)], _, [], [(_, r2 as ref NONE)], _, []) => adamc@710: if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then adamc@710: let adamc@838: val kr = (L'.KRecord k, loc) adamc@710: val u = cunif (loc, kr) adamc@710: in adamc@710: r1 := SOME (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc); adamc@710: r2 := SOME (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc); adamc@710: empties adamc@710: end adamc@710: else adamc@710: orig adamc@709: | orig => orig adamc@709: adamc@403: (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@777: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@753: fun isGuessable (other, fs, unifs) = adamc@753: let adamc@753: val c = (L'.CRecord (k, fs), loc) adamc@753: val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs adamc@753: in adamc@753: (guessMap env (other, c, GuessFailure); adamc@753: true) adamc@753: handle GuessFailure => false adamc@753: end adamc@403: adamc@754: val (fs1, fs2, others1, others2, unifs1, unifs2) = adamc@753: case (fs1, fs2, others1, others2, unifs1, unifs2) of adamc@753: ([], _, [other1], [], [], _) => adamc@753: if isGuessable (other1, fs2, unifs2) then adamc@754: ([], [], [], [], [], []) adamc@403: else adamc@754: (fs1, fs2, others1, others2, unifs1, unifs2) adamc@753: | (_, [], [], [other2], _, []) => adamc@777: if isGuessable (other2, fs1, unifs1) then adamc@777: ([], [], [], [], [], []) adamc@777: else adamc@777: (fs1, fs2, others1, others2, unifs1, unifs2) adamc@754: | _ => (fs1, fs2, others1, others2, unifs1, unifs2) adamc@403: adamc@403: (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@646: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@838: val empty = (L'.CRecord (k, []), loc) adamc@713: fun failure () = raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) adamc@709: in adamc@777: (case (unifs1, fs1, others1, unifs2, fs2, others2) of adamc@777: (_, [], [], [], [], []) => adamc@777: app (fn (_, r) => r := SOME empty) unifs1 adamc@777: | ([], [], [], _, [], []) => adamc@777: app (fn (_, r) => r := SOME empty) unifs2 adamc@777: | _ => adamc@777: if !mayDelay then adamc@777: delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs adamc@777: else adamc@777: failure ()) adamc@777: adamc@777: (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), adamc@777: ("#2", p_summary env (normalizeRecordSummary env s2))]*) adamc@403: end adamc@403: adamc@628: and guessMap env (c1, c2, ex) = adamc@403: let adamc@403: val loc = #2 c1 adamc@403: adamc@621: fun unfold (dom, ran, f, r, c) = adamc@403: let adamc@621: fun unfold (r, c) = adamc@754: case #1 (hnormCon env c) of adamc@628: L'.CRecord (_, []) => unifyCons env r (L'.CRecord (dom, []), loc) adamc@628: | L'.CRecord (_, [(x, v)]) => adamc@628: let adamc@628: val v' = case dom of adamc@628: (L'.KUnit, _) => (L'.CUnit, loc) adamc@628: | _ => cunif (loc, dom) adamc@628: in adamc@628: unifyCons env v (L'.CApp (f, v'), loc); adamc@628: unifyCons env r (L'.CRecord (dom, [(x, v')]), loc) adamc@628: end adamc@628: | L'.CRecord (_, (x, v) :: rest) => adamc@628: let adamc@628: val r1 = cunif (loc, (L'.KRecord dom, loc)) adamc@628: val r2 = cunif (loc, (L'.KRecord dom, loc)) adamc@628: in adamc@628: unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)); adamc@628: unfold (r2, (L'.CRecord (ran, rest), loc)); adamc@628: unifyCons env r (L'.CConcat (r1, r2), loc) adamc@628: end adamc@628: | L'.CConcat (c1', c2') => adamc@628: let adamc@628: val r1 = cunif (loc, (L'.KRecord dom, loc)) adamc@628: val r2 = cunif (loc, (L'.KRecord dom, loc)) adamc@628: in adamc@628: unfold (r1, c1'); adamc@628: unfold (r2, c2'); adamc@628: unifyCons env r (L'.CConcat (r1, r2), loc) adamc@628: end adamc@754: | L'.CUnif (_, _, _, ur) => adamc@777: ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) adamc@628: | _ => raise ex adamc@403: in adamc@621: unfold (r, c) adamc@403: end adamc@632: handle _ => raise ex adamc@403: in adamc@403: case (#1 c1, #1 c2) of adamc@621: (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) => adamc@621: unfold (dom, ran, f, r, c2) adamc@621: | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => adamc@621: unfold (dom, ran, f, r, c1) adamc@403: | _ => raise ex adamc@403: end adamc@403: adamc@628: and unifyCons' env c1 c2 = adamc@628: if isUnitCon env c1 andalso isUnitCon env c2 then adamc@628: () adamc@628: else adamc@403: let adamc@628: (*val befor = Time.now () adamc@628: val old1 = c1 adamc@628: val old2 = c2*) adamc@628: val c1 = hnormCon env c1 adamc@628: val c2 = hnormCon env c2 adamc@403: in adamc@628: unifyCons'' env c1 c2 adamc@628: handle ex => guessMap env (c1, c2, ex) adamc@403: end adamc@628: adamc@628: and unifyCons'' env (c1All as (c1, loc)) (c2All as (c2, _)) = adamc@403: let adamc@403: fun err f = raise CUnify' (f (c1All, c2All)) adamc@403: adamc@706: fun projSpecial1 (c1, n1, onFail) = adamc@403: let adamc@632: fun trySnd () = adamc@632: case #1 (hnormCon env c2All) of adamc@632: L'.CProj (c2, n2) => adamc@632: let adamc@632: fun tryNormal () = adamc@632: if n1 = n2 then adamc@632: unifyCons' env c1 c2 adamc@632: else adamc@706: onFail () adamc@632: in adamc@632: case #1 (hnormCon env c2) of adamc@632: L'.CUnif (_, k, _, r) => adamc@632: (case #1 (hnormKind k) of adamc@632: L'.KTuple ks => adamc@632: let adamc@632: val loc = #2 c2 adamc@632: val us = map (fn k => cunif (loc, k)) ks adamc@632: in adamc@632: r := SOME (L'.CTuple us, loc); adamc@632: unifyCons' env c1All (List.nth (us, n2 - 1)) adamc@632: end adamc@632: | _ => tryNormal ()) adamc@632: | _ => tryNormal () adamc@632: end adamc@706: | _ => onFail () adamc@403: in adamc@632: case #1 (hnormCon env c1) of adamc@632: L'.CUnif (_, k, _, r) => adamc@632: (case #1 (hnormKind k) of adamc@632: L'.KTuple ks => adamc@632: let adamc@632: val loc = #2 c1 adamc@632: val us = map (fn k => cunif (loc, k)) ks adamc@632: in adamc@632: r := SOME (L'.CTuple us, loc); adamc@632: unifyCons' env (List.nth (us, n1 - 1)) c2All adamc@632: end adamc@632: | _ => trySnd ()) adamc@632: | _ => trySnd () adamc@403: end adamc@632: adamc@706: fun projSpecial2 (c2, n2, onFail) = adamc@706: case #1 (hnormCon env c2) of adamc@706: L'.CUnif (_, k, _, r) => adamc@706: (case #1 (hnormKind k) of adamc@706: L'.KTuple ks => adamc@706: let adamc@706: val loc = #2 c2 adamc@706: val us = map (fn k => cunif (loc, k)) ks adamc@706: in adamc@706: r := SOME (L'.CTuple us, loc); adamc@706: unifyCons' env c1All (List.nth (us, n2 - 1)) adamc@706: end adamc@706: | _ => onFail ()) adamc@706: | _ => onFail () adamc@706: adamc@777: fun isRecord' () = unifyRecordCons env (loc, c1All, c2All) adamc@706: adamc@706: fun isRecord () = adamc@706: case (c1, c2) of adamc@706: (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') adamc@706: | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') adamc@706: | _ => isRecord' () adamc@706: in adamc@706: (*eprefaces "unifyCons''" [("c1All", p_con env c1All), adamc@706: ("c2All", p_con env c2All)];*) adamc@706: adamc@706: case (c1, c2) of adamc@706: (L'.CError, _) => () adamc@706: | (_, L'.CError) => () adamc@403: adamc@705: | (L'.CRecord _, _) => isRecord () adamc@705: | (_, L'.CRecord _) => isRecord () adamc@705: | (L'.CConcat _, _) => isRecord () adamc@705: | (_, L'.CConcat _) => isRecord () adamc@705: adamc@705: | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => adamc@705: if r1 = r2 then adamc@705: () adamc@705: else adamc@705: (unifyKinds env k1 k2; adamc@705: r1 := SOME c2All) adamc@705: adamc@705: | (L'.CUnif (_, _, _, r), _) => adamc@705: if occursCon r c2All then adamc@705: err COccursCheckFailed adamc@705: else adamc@705: r := SOME c2All adamc@705: | (_, L'.CUnif (_, _, _, r)) => adamc@705: if occursCon r c1All then adamc@705: err COccursCheckFailed adamc@705: else adamc@705: r := SOME c1All adamc@705: adamc@705: | (L'.CUnit, L'.CUnit) => () adamc@705: adamc@705: | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => adamc@705: (unifyCons' env d1 d2; adamc@705: unifyCons' env r1 r2) adamc@705: | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => adamc@705: if expl1 <> expl2 then adamc@705: err CExplicitness adamc@705: else adamc@705: (unifyKinds env d1 d2; adamc@705: let adamc@705: (*val befor = Time.now ()*) adamc@705: val env' = E.pushCRel env x1 d1 adamc@705: in adamc@705: (*TextIO.print ("E.pushCRel: " adamc@705: ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) adamc@705: ^ "\n");*) adamc@705: unifyCons' env' r1 r2 adamc@705: end) adamc@705: | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 adamc@705: | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => adamc@705: (unifyCons' env c1 c2; adamc@705: unifyCons' env d1 d2; adamc@705: unifyCons' env e1 e2) adamc@705: adamc@705: | (L'.CRel n1, L'.CRel n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: | (L'.CNamed n1, L'.CNamed n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => adamc@705: (unifyCons' env d1 d2; adamc@705: unifyCons' env r1 r2) adamc@705: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => adamc@705: (unifyKinds env k1 k2; adamc@705: unifyCons' (E.pushCRel env x1 k1) c1 c2) adamc@705: adamc@705: | (L'.CName n1, L'.CName n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => adamc@705: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CTuple cs1, L'.CTuple cs2) => adamc@705: ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) adamc@705: handle ListPair.UnequalLengths => err CIncompatible) adamc@705: adamc@706: | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible) adamc@706: | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible) adamc@706: adamc@623: | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => adamc@623: (unifyKinds env dom1 dom2; adamc@628: unifyKinds env ran1 ran2) adamc@623: adamc@623: | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => adamc@628: unifyCons' (E.pushKRel env x) c1 c2 adamc@623: | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => adamc@623: (unifyKinds env k1 k2; adamc@628: unifyCons' env c1 c2) adamc@623: | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => adamc@628: unifyCons' (E.pushKRel env x) c1 c2 adamc@628: adamc@403: | _ => err CIncompatible adamc@403: end adamc@403: adamc@628: and unifyCons env c1 c2 = adamc@628: unifyCons' env c1 c2 adamc@403: handle CUnify' err => raise CUnify (c1, c2, err) adamc@403: | KUnify args => raise CUnify (c1, c2, CKind args) adamc@403: adamc@628: fun checkCon env e c1 c2 = adamc@628: unifyCons env c1 c2 adamc@403: handle CUnify (c1, c2, err) => adamc@628: expError env (Unify (e, c1, c2, err)) adamc@628: adamc@628: fun checkPatCon env p c1 c2 = adamc@628: unifyCons env c1 c2 adamc@403: handle CUnify (c1, c2, err) => adamc@628: expError env (PatUnify (p, c1, c2, err)) adamc@71: adamc@403: fun primType env p = adamc@403: case p of adamc@403: P.Int _ => !int adamc@403: | P.Float _ => !float adamc@403: | P.String _ => !string adamc@821: | P.Char _ => !char adamc@623: adamc@403: datatype constraint = adamc@403: Disjoint of D.goal adamc@403: | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span adamc@403: adamc@403: val enD = map Disjoint adamc@403: adamc@634: fun isClassOrFolder env cl = adamc@634: E.isClass env cl adamc@634: orelse case hnormCon env cl of adamc@634: (L'.CKApp (cl, _), _) => adamc@634: (case hnormCon env cl of adamc@634: (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r adamc@634: | _ => false) adamc@634: | _ => false adamc@634: adamc@629: fun elabHead (env, denv) infer (e as (_, loc)) t = adamc@403: let adamc@898: fun unravelKind (t, e) = adamc@898: case hnormCon env t of adamc@898: (L'.TKFun (x, t'), _) => adamc@898: let adamc@898: val u = kunif loc adamc@898: adamc@898: val t'' = subKindInCon (0, u) t' adamc@898: in adamc@898: unravelKind (t'', (L'.EKApp (e, u), loc)) adamc@898: end adamc@898: | t => (e, t, []) adamc@898: adamc@403: fun unravel (t, e) = adamc@628: case hnormCon env t of adamc@628: (L'.TKFun (x, t'), _) => adamc@628: let adamc@628: val u = kunif loc adamc@628: adamc@628: val t'' = subKindInCon (0, u) t' adamc@628: in adamc@628: unravel (t'', (L'.EKApp (e, u), loc)) adamc@628: end adamc@628: | (L'.TCFun (L'.Implicit, x, k, t'), _) => adamc@628: let adamc@628: val u = cunif (loc, k) adamc@628: adamc@628: val t'' = subConInCon (0, u) t' adamc@628: in adamc@628: unravel (t'', (L'.ECApp (e, u), loc)) adamc@628: end adamc@633: | (L'.TFun (dom, ran), _) => adamc@628: let adamc@633: fun default () = (e, t, []) adamc@750: adamc@750: fun isInstance () = adamc@750: if infer <> L.TypesOnly then adamc@750: let adamc@750: val r = ref NONE adamc@750: val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) adamc@750: in adamc@750: (e, t, TypeClass (env, dom, r, loc) :: gs) adamc@750: end adamc@750: else adamc@750: default () adamc@750: adamc@750: fun hasInstance c = adamc@753: case hnormCon env c of adamc@753: (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false, adamc@753: con = fn c => adamc@753: E.isClass env (hnormCon env (c, loc))} c adamc@753: | c => adamc@750: let adamc@753: fun findHead c = adamc@753: case #1 c of adamc@753: L'.CApp (f, _) => findHead f adamc@753: | _ => c adamc@753: adamc@753: val cl = hnormCon env (findHead c) adamc@750: in adamc@750: isClassOrFolder env cl adamc@750: end adamc@628: in adamc@750: if hasInstance dom then adamc@750: isInstance () adamc@750: else adamc@750: default () adamc@628: end adamc@629: | (L'.TDisjoint (r1, r2, t'), loc) => adamc@629: if infer <> L.TypesOnly then adamc@629: let adamc@792: val gs = D.prove env denv (r1, r2, #2 e) adamc@629: val (e, t, gs') = unravel (t', e) adamc@629: in adamc@629: (e, t, enD gs @ gs') adamc@629: end adamc@629: else adamc@629: (e, t, []) adamc@628: | t => (e, t, []) adamc@704: in adamc@704: case infer of adamc@898: L.DontInfer => unravelKind (t, e) adamc@704: | _ => unravel (t, e) adamc@704: end adamc@15: adamc@628: fun elabPat (pAll as (p, loc), (env, 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@628: val ((p', pt), (env, bound)) = elabPat (p, (env, 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@628: ignore (checkPatCon env 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@628: val ((p', t), (env, bound)) = elabPat (p, (env, 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@822: adamc@822: | L.PAnnot (p, t) => adamc@822: let adamc@822: val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) adamc@822: val (t', k, _) = elabCon (env, D.empty) t adamc@822: in adamc@822: checkPatCon env p' pt t'; adamc@822: ((p', t'), (env, bound)) adamc@822: end adamc@171: end adamc@171: adamc@819: (* This exhaustiveness checking follows Luc Maranget's paper "Warnings for pattern matching." *) adamc@819: fun exhaustive (env, t, ps, loc) = adamc@819: let adamc@819: fun fail n = raise Fail ("Elaborate.exhaustive: Impossible " ^ Int.toString n) adamc@819: adamc@819: fun patConNum pc = adamc@819: case pc of adamc@819: L'.PConVar n => n adamc@819: | L'.PConProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@819: NONE => raise Fail "exhaustive: Can't project datatype" adamc@819: | SOME (_, n, _, _, _) => n adamc@819: end adamc@819: adamc@819: fun nameOfNum (t, n) = adamc@819: case t of adamc@819: L'.CModProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@819: NONE => raise Fail "exhaustive: Can't project datatype" adamc@819: | SOME (_, cons) => adamc@819: case ListUtil.search (fn (name, n', _) => adamc@819: if n' = n then adamc@819: SOME name adamc@819: else adamc@819: NONE) cons of adamc@819: NONE => fail 9 adamc@819: | SOME name => L'.PConProj (m1, ms, name) adamc@819: end adamc@819: | _ => L'.PConVar n adamc@819: adamc@819: fun S (args, c, P) = adamc@819: List.mapPartial adamc@819: (fn [] => fail 1 adamc@819: | p1 :: ps => adamc@819: let adamc@819: val loc = #2 p1 adamc@819: adamc@819: fun wild () = adamc@819: SOME (map (fn _ => (L'.PWild, loc)) args @ ps) adamc@819: in adamc@819: case #1 p1 of adamc@819: L'.PPrim _ => NONE adamc@819: | L'.PCon (_, c', _, NONE) => adamc@819: if patConNum c' = c then adamc@819: SOME ps adamc@819: else adamc@819: NONE adamc@819: | L'.PCon (_, c', _, SOME p) => adamc@819: if patConNum c' = c then adamc@819: SOME (p :: ps) adamc@819: else adamc@819: NONE adamc@819: | L'.PRecord xpts => adamc@819: SOME (map (fn x => adamc@819: case ListUtil.search (fn (x', p, _) => adamc@819: if x = x' then adamc@819: SOME p adamc@819: else adamc@819: NONE) xpts of adamc@819: NONE => (L'.PWild, loc) adamc@819: | SOME p => p) args @ ps) adamc@819: | L'.PWild => wild () adamc@819: | L'.PVar _ => wild () adamc@819: end) adamc@819: P adamc@819: adamc@819: fun D P = adamc@819: List.mapPartial adamc@819: (fn [] => fail 2 adamc@819: | (p1, _) :: ps => adamc@819: case p1 of adamc@819: L'.PWild => SOME ps adamc@819: | L'.PVar _ => SOME ps adamc@819: | L'.PPrim _ => NONE adamc@819: | L'.PCon _ => NONE adamc@819: | L'.PRecord _ => NONE) adamc@819: P adamc@819: adamc@819: fun I (P, q) = adamc@819: (*(prefaces "I" [("P", p_list (fn P' => box [PD.string "[", p_list (p_pat env) P', PD.string "]"]) P), adamc@819: ("q", p_list (p_con env) q)];*) adamc@819: case q of adamc@819: [] => (case P of adamc@819: [] => SOME [] adamc@819: | _ => NONE) adamc@819: | q1 :: qs => adamc@819: let adamc@819: val loc = #2 q1 adamc@819: adamc@819: fun unapp (t, acc) = adamc@830: case #1 t of adamc@830: L'.CApp (t, arg) => unapp (t, arg :: acc) adamc@819: | _ => (t, rev acc) adamc@819: adamc@830: val (t1, args) = unapp (hnormCon env q1, []) adamc@830: val t1 = hnormCon env t1 adamc@819: fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args adamc@819: adamc@819: fun dtype (dtO, names) = adamc@819: let adamc@819: val nameSet = IS.addList (IS.empty, names) adamc@819: val nameSet = foldl (fn (ps, nameSet) => adamc@819: case ps of adamc@819: [] => fail 4 adamc@819: | (L'.PCon (_, pc, _, _), _) :: _ => adamc@819: (IS.delete (nameSet, patConNum pc) adamc@819: handle NotFound => nameSet) adamc@819: | _ => nameSet) adamc@819: nameSet P adamc@819: in adamc@819: nameSet adamc@819: end adamc@819: adamc@819: fun default () = (NONE, IS.singleton 0, []) adamc@819: adamc@819: val (dtO, unused, cons) = adamc@830: case #1 t1 of adamc@819: L'.CNamed n => adamc@819: let adamc@819: val dt = E.lookupDatatype env n adamc@819: val cons = E.constructors dt adamc@819: in adamc@819: (SOME dt, adamc@819: dtype (SOME dt, map #2 cons), adamc@819: map (fn (_, n, co) => adamc@819: (n, adamc@819: case co of adamc@819: NONE => [] adamc@819: | SOME t => [("", doSub t)])) cons) adamc@819: end adamc@819: | L'.CModProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@819: NONE => default () adamc@819: | SOME (_, cons) => adamc@819: (NONE, adamc@819: dtype (NONE, map #2 cons), adamc@819: map (fn (s, _, co) => adamc@819: (patConNum (L'.PConProj (m1, ms, s)), adamc@819: case co of adamc@819: NONE => [] adamc@819: | SOME t => [("", doSub t)])) cons) adamc@819: end adamc@830: | L'.TRecord t => adamc@830: (case #1 (hnormCon env t) of adamc@830: L'.CRecord (_, xts) => adamc@830: let adamc@830: val xts = map (fn ((L'.CName x, _), co) => SOME (x, co) adamc@830: | _ => NONE) xts adamc@830: in adamc@830: if List.all Option.isSome xts then adamc@830: let adamc@830: val xts = List.mapPartial (fn x => x) xts adamc@830: val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) => adamc@830: String.compare (x1, x2) = GREATER) xts adamc@830: in adamc@830: (NONE, IS.empty, [(0, xts)]) adamc@830: end adamc@830: else adamc@830: default () adamc@830: end adamc@830: | _ => default ()) adamc@819: | _ => default () adamc@819: in adamc@819: if IS.isEmpty unused then adamc@819: let adamc@819: fun recurse cons = adamc@819: case cons of adamc@819: [] => NONE adamc@819: | (name, args) :: cons => adamc@819: case I (S (map #1 args, name, P), adamc@819: map #2 args @ qs) of adamc@819: NONE => recurse cons adamc@819: | SOME ps => adamc@819: let adamc@819: val nargs = length args adamc@819: val argPs = List.take (ps, nargs) adamc@819: val restPs = List.drop (ps, nargs) adamc@819: adamc@819: val p = case name of adamc@819: 0 => L'.PRecord (ListPair.map adamc@819: (fn ((name, t), p) => (name, p, t)) adamc@819: (args, argPs)) adamc@830: | _ => L'.PCon (L'.Default, nameOfNum (#1 t1, name), [], adamc@819: case argPs of adamc@819: [] => NONE adamc@819: | [p] => SOME p adamc@819: | _ => fail 3) adamc@819: in adamc@819: SOME ((p, loc) :: restPs) adamc@819: end adamc@819: in adamc@819: recurse cons adamc@819: end adamc@819: else adamc@819: case I (D P, qs) of adamc@819: NONE => NONE adamc@819: | SOME ps => adamc@819: let adamc@819: val p = case cons of adamc@819: [] => L'.PWild adamc@819: | (0, _) :: _ => L'.PWild adamc@819: | _ => adamc@819: case IS.find (fn _ => true) unused of adamc@819: NONE => fail 6 adamc@819: | SOME name => adamc@819: case ListUtil.search (fn (name', args) => adamc@819: if name = name' then adamc@819: SOME (name', args) adamc@819: else adamc@819: NONE) cons of adamc@819: SOME (n, []) => adamc@830: L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], NONE) adamc@819: | SOME (n, [_]) => adamc@830: L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], SOME (L'.PWild, loc)) adamc@819: | _ => fail 7 adamc@819: in adamc@819: SOME ((p, loc) :: ps) adamc@819: end adamc@819: end adamc@819: in adamc@819: case I (map (fn x => [x]) ps, [t]) of adamc@819: NONE => NONE adamc@819: | SOME [p] => SOME p adamc@819: | _ => fail 7 adamc@819: end adamc@819: 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@721: fun normClassKey env c = adamc@467: let adamc@721: val c = hnormCon env c adamc@467: in adamc@467: case #1 c of adamc@467: L'.CApp (c1, c2) => adamc@467: let adamc@721: val c1 = normClassKey env c1 adamc@721: val c2 = normClassKey env c2 adamc@467: in adamc@467: (L'.CApp (c1, c2), #2 c) adamc@467: end adamc@721: | L'.CRecord (k, xcs) => (L'.CRecord (k, map (fn (x, c) => (normClassKey env x, adamc@721: normClassKey env c)) xcs), #2 c) adamc@721: | _ => unmodCon env c adamc@467: end adamc@467: adamc@467: fun normClassConstraint env (c, loc) = adamc@217: case c of adamc@217: L'.CApp (f, x) => adamc@217: let adamc@721: val f = normClassKey env f adamc@467: val x = normClassKey env x adamc@217: in adamc@467: (L'.CApp (f, x), loc) adamc@217: end adamc@674: | L'.TFun (c1, c2) => adamc@674: let adamc@674: val c1 = normClassConstraint env c1 adamc@674: val c2 = normClassConstraint env c2 adamc@674: in adamc@674: (L'.TFun (c1, c2), loc) adamc@674: end adamc@674: | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) adamc@467: | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c adamc@721: | _ => unmodCon env (c, loc) adamc@216: adamc@92: fun elabExp (env, denv) (eAll as (e, loc)) = adamc@91: let adamc@848: (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) adamc@514: (*val befor = Time.now ()*) 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: in adamc@628: checkCon env e' et t'; adamc@628: (e', t', gs1 @ enD gs2) adamc@91: end adamc@34: adamc@91: | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) adamc@403: | L.EVar ([], s, infer) => adamc@91: (case E.lookupE env s of adamc@91: E.NotBound => adamc@91: (expError env (UnboundExp (loc, s)); adamc@91: (eerror, cerror, [])) adamc@629: | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t adamc@629: | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t) adamc@403: | L.EVar (m1 :: ms, s, infer) => 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@629: elabHead (env, denv) infer (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@403: val (e2', t2, gs2) = elabExp (env, denv) e2 adamc@71: adamc@91: val dom = cunif (loc, ktype) adamc@91: val ran = cunif (loc, ktype) adamc@838: val t = (L'.TFun (dom, ran), loc) adamc@91: in adamc@628: checkCon env e1' t1 t; adamc@628: checkCon env e2' t2 dom; adamc@628: ((L'.EApp (e1', e2'), loc), ran, gs1 @ gs2) 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@467: val dom = normClassConstraint env t' adamc@467: val (e', et, gs2) = 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@467: enD gs1 @ gs2) 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@403: val (c', ck, gs2) = elabCon (env, denv) c adamc@628: val (et', _) = hnormCon env 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@628: ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2) 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@623: val k' = elabKind env 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@623: | L.EKAbs (x, e) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (e', et, gs) = elabExp (env', denv) e adamc@623: in adamc@623: ((L'.EKAbs (x, e'), loc), adamc@623: (L'.TKFun (x, et), loc), adamc@623: gs) adamc@623: 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@628: val denv' = D.assert env denv (c1', c2') adamc@628: val (e', t, gs3) = 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@628: (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3) adamc@91: end adamc@629: | L.EDisjointApp e => adamc@629: let adamc@629: val (e', t, gs1) = elabExp (env, denv) e adamc@629: adamc@629: val k1 = kunif loc adamc@629: val c1 = cunif (loc, (L'.KRecord k1, loc)) adamc@629: val k2 = kunif loc adamc@629: val c2 = cunif (loc, (L'.KRecord k2, loc)) adamc@629: val t' = cunif (loc, ktype) adamc@629: val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) adamc@629: val gs2 = D.prove env denv (c1, c2, loc) adamc@629: in adamc@629: (e', t', enD gs2 @ gs1) adamc@629: 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@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (first, rest), loc), loc); adamc@628: val gs3 = D.prove env denv (first, rest, loc) adamc@91: in adamc@628: ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3) adamc@91: end adamc@91: adamc@445: | L.EConcat (e1, e2) => adamc@339: let adamc@339: val (e1', e1t, gs1) = elabExp (env, denv) e1 adamc@445: val (e2', e2t, gs2) = elabExp (env, denv) e2 adamc@445: adamc@445: val r1 = cunif (loc, ktype_record) adamc@445: val r2 = cunif (loc, ktype_record) adamc@445: adamc@629: val () = checkCon env e1' e1t (L'.TRecord r1, loc) adamc@629: val () = checkCon env e2' e2t (L'.TRecord r2, loc) adamc@629: adamc@628: val gs3 = D.prove env denv (r1, r2, loc) adamc@339: in adamc@445: ((L'.EConcat (e1', r1, e2', r2), loc), adamc@445: (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), adamc@628: gs1 @ gs2 @ enD gs3) 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@629: adamc@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@149: adamc@628: val gs3 = 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@628: gs1 @ enD gs2 @ enD gs3) adamc@149: end adamc@493: | L.ECutMulti (e, c) => adamc@493: let adamc@493: val (e', et, gs1) = elabExp (env, denv) e adamc@493: val (c', ck, gs2) = elabCon (env, denv) c adamc@493: adamc@493: val rest = cunif (loc, ktype_record) adamc@629: adamc@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (c', rest), loc), loc) adamc@493: adamc@628: val gs3 = D.prove env denv (c', rest, loc) adamc@493: in adamc@493: ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), adamc@628: gs1 @ enD gs2 @ enD gs3) adamc@493: end adamc@149: 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@628: val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) adamc@628: adamc@629: val (e', et', gs1) = elabExp (env, denv) e adamc@171: in adamc@628: checkPatCon env p' pt et; adamc@629: checkCon env e' et' result; adamc@628: ((p', e'), gs1 @ gs) adamc@171: end) adamc@171: gs1 pes adamc@171: in adamc@819: case exhaustive (env, et, map #1 pes', loc) of adamc@819: NONE => () adamc@830: | SOME p => if !mayDelay then adamc@830: delayedExhaustives := (env, et, map #1 pes', loc) :: !delayedExhaustives adamc@830: else adamc@830: expError env (Inexhaustive (loc, p)); adamc@172: adamc@628: ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) adamc@171: end adamc@447: adamc@447: | L.ELet (eds, e) => adamc@447: let adamc@447: val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds adamc@447: val (e, t, gs2) = elabExp (env, denv) e adamc@447: in adamc@825: ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2) adamc@447: end adamc@280: in adamc@819: (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) adamc@280: r adamc@91: end adamc@31: adamc@628: and elabEdecl denv (dAll as (d, loc), (env, gs)) = adamc@447: let adamc@447: val r = adamc@447: case d of adamc@825: L.EDVal (p, e) => adamc@447: let adamc@825: val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty)) adamc@825: val (e', et, gs1) = elabExp (env, denv) e adamc@825: adamc@825: val () = checkCon env e' et pt adamc@825: adamc@825: val pt = normClassConstraint env pt adamc@447: in adamc@830: case exhaustive (env, et, [p'], loc) of adamc@830: NONE => () adamc@830: | SOME p => if !mayDelay then adamc@830: delayedExhaustives := (env, et, [p'], loc) :: !delayedExhaustives adamc@830: else adamc@830: expError env (Inexhaustive (loc, p)); adamc@830: adamc@825: ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs)) adamc@447: end adamc@447: | L.EDValRec vis => adamc@447: let adamc@447: fun allowable (e, _) = adamc@447: case e of adamc@447: L.EAbs _ => true adamc@447: | L.ECAbs (_, _, _, e) => allowable e adamc@623: | L.EKAbs (_, e) => allowable e adamc@447: | L.EDisjoint (_, _, e) => allowable e adamc@447: | _ => false adamc@447: adamc@447: val (vis, gs) = ListUtil.foldlMap adamc@447: (fn ((x, co, e), gs) => adamc@447: let adamc@447: val (c', _, gs1) = case co of adamc@447: NONE => (cunif (loc, ktype), ktype, []) adamc@447: | SOME c => elabCon (env, denv) c adamc@447: in adamc@447: ((x, c', e), enD gs1 @ gs) adamc@447: end) gs vis adamc@447: adamc@447: val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis adamc@447: adamc@447: val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) => adamc@447: let adamc@447: val (e', et, gs1) = elabExp (env, denv) e adamc@447: in adamc@628: checkCon env e' et c'; adamc@447: if allowable e then adamc@447: () adamc@447: else adamc@447: expError env (IllegalRec (x, e')); adamc@628: ((x, c', e'), gs1 @ gs) adamc@447: end) gs vis adamc@447: in adamc@447: ((L'.EDValRec vis, loc), (env, gs)) adamc@447: end adamc@447: in adamc@447: r adamc@447: end adamc@447: 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@754: fun viewOf () = (L'.CModProj (!basis_r, [], "sql_view"), ErrorMsg.dummySpan) adamc@754: fun queryOf () = (L'.CModProj (!basis_r, [], "sql_query"), ErrorMsg.dummySpan) adamc@459: fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) adamc@718: fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan) adamc@205: adamc@469: fun dopenConstraints (loc, env, denv) {str, strs} = adamc@469: case E.lookupStr env str of adamc@469: NONE => (strError env (UnboundStr (loc, str)); adamc@469: denv) adamc@469: | SOME (n, sgn) => adamc@469: let adamc@469: val (st, sgn) = foldl (fn (m, (str, sgn)) => adamc@469: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@469: NONE => (strError env (UnboundStr (loc, m)); adamc@469: (strerror, sgnerror)) adamc@469: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@469: ((L'.StrVar n, loc), sgn) strs adamc@469: adamc@469: val cso = E.projectConstraints env {sgn = sgn, str = st} adamc@469: in adamc@628: case cso of adamc@628: NONE => (strError env (UnboundStr (loc, str)); adamc@628: denv) adamc@628: | SOME cs => foldl (fn ((c1, c2), denv) => adamc@628: D.assert env denv (c1, c2)) denv cs adamc@469: end adamc@469: 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@623: val k' = elabKind env 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@623: | SOME k => elabKind env 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@805: | L.SgiDatatype dts => adamc@157: let adamc@157: val k = (L'.KType, loc) adamc@805: adamc@805: val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) => adamc@805: let adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@805: val (env, n) = E.pushCNamed env x k' NONE adamc@805: in adamc@805: ((x, n, xs, xcs), env) adamc@805: end) adamc@805: env dts adamc@805: adamc@805: val (dts, env) = ListUtil.foldlMap adamc@805: (fn ((x, n, xs, xcs), env) => adamc@805: let adamc@805: val t = (L'.CNamed n, loc) adamc@805: val nxs = length xs - 1 adamc@805: val t = ListUtil.foldli (fn (i, _, t) => adamc@805: (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@805: adamc@805: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@805: (E.pushCRel env' x k, adamc@805: D.enter denv')) (env, denv) xs adamc@805: adamc@805: val (xcs, (used, env, gs)) = adamc@805: ListUtil.foldlMap adamc@805: (fn ((x, to), (used, env, gs)) => adamc@805: let adamc@805: val (to, t, gs') = case to of adamc@805: NONE => (NONE, t, gs) adamc@805: | SOME t' => adamc@805: let adamc@805: val (t', tk, gs') = adamc@805: elabCon (env', denv') t' adamc@805: in adamc@805: checkKind env' t' tk k; adamc@805: (SOME t', adamc@805: (L'.TFun (t', t), loc), adamc@805: gs' @ gs) adamc@805: end adamc@805: val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@805: t xs adamc@805: adamc@805: val (env, n') = E.pushENamed env x t adamc@805: in adamc@805: if SS.member (used, x) then adamc@805: strError env (DuplicateConstructor (x, loc)) adamc@805: else adamc@805: (); adamc@805: ((x, n', to), (SS.add (used, x), env, gs')) adamc@805: end) adamc@805: (SS.empty, env, []) xcs adamc@805: in adamc@805: ((x, n, xs, xcs), E.pushDatatype env n xs xcs) adamc@805: end) adamc@805: env dts adamc@157: in adamc@805: ([(L'.SgiDatatype dts, 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@628: case hnormCon env (L'.CModProj (n, ms, s), loc) of adamc@628: (L'.CModProj (n, ms, s), _) => adamc@161: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@161: NONE => (conError env (UnboundDatatype (loc, s)); adamc@628: ([], (env, denv, []))) 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@628: ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, [])) 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@721: val old = c' adamc@711: val c' = normClassConstraint env c' adamc@76: val (env', n) = E.pushENamed env x c' adamc@76: in adamc@623: (unifyKinds env ck ktype adamc@706: handle KUnify ue => strError env (NotType (loc, ck, ue))); adamc@31: adamc@467: ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@707: | L.SgiTable (x, c, pe, ce) => adamc@706: let adamc@706: val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) adamc@706: val x' = x ^ "_hidden_constraints" adamc@706: val (env', hidden_n) = E.pushCNamed env x' cstK NONE adamc@706: val hidden = (L'.CNamed hidden_n, loc) adamc@706: adamc@706: val (c', ck, gs') = elabCon (env, denv) c adamc@707: val pkey = cunif (loc, cstK) adamc@706: val visible = cunif (loc, cstK) adamc@706: val uniques = (L'.CConcat (visible, hidden), loc) adamc@706: adamc@706: val ct = tableOf () adamc@706: val ct = (L'.CApp (ct, c'), loc) adamc@707: val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) adamc@707: adamc@707: val (pe', pet, gs'') = elabExp (env', denv) pe adamc@707: val gs'' = List.mapPartial (fn Disjoint x => SOME x adamc@707: | _ => NONE) gs'' adamc@707: adamc@707: val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) adamc@707: val pst = (L'.CApp (pst, c'), loc) adamc@707: val pst = (L'.CApp (pst, pkey), loc) adamc@706: adamc@706: val (env', n) = E.pushENamed env' x ct adamc@706: adamc@707: val (ce', cet, gs''') = elabExp (env', denv) ce adamc@707: val gs''' = List.mapPartial (fn Disjoint x => SOME x adamc@707: | _ => NONE) gs''' adamc@706: adamc@706: val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) adamc@706: val cst = (L'.CApp (cst, c'), loc) adamc@706: val cst = (L'.CApp (cst, visible), loc) adamc@706: in adamc@706: checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); adamc@707: checkCon env' pe' pet pst; adamc@707: checkCon env' ce' cet cst; adamc@706: adamc@706: ([(L'.SgiConAbs (x', hidden_n, cstK), loc), adamc@707: (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) adamc@706: end adamc@706: 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@628: val denv = 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@628: ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) adamc@76: end adamc@31: adamc@563: | L.SgiClassAbs (x, k) => adamc@211: let adamc@623: val k = elabKind env k adamc@711: val (env, n) = E.pushCNamed env x k NONE adamc@211: val env = E.pushClass env n adamc@211: in adamc@563: ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) adamc@211: end adamc@211: adamc@563: | L.SgiClass (x, k, c) => adamc@211: let adamc@623: val k = elabKind env k adamc@211: val (c', ck, gs) = elabCon (env, denv) c adamc@711: val (env, n) = E.pushCNamed env x k (SOME c') adamc@211: val env = E.pushClass env n adamc@211: in adamc@711: checkKind env c' ck k; adamc@563: ([(L'.SgiClass (x, n, k, 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@805: | L'.SgiDatatype dts => adamc@156: let adamc@805: val (cons, vals) = adamc@805: let adamc@805: fun doOne ((x, _, _, xncs), (cons, vals)) = adamc@805: let adamc@805: val vals = foldl (fn ((x, _, _), vals) => adamc@805: (if SS.member (vals, x) then adamc@805: sgnError env (DuplicateVal (loc, x)) adamc@805: else adamc@805: (); adamc@805: SS.add (vals, x))) adamc@805: vals xncs adamc@805: in adamc@805: if SS.member (cons, x) then adamc@805: sgnError env (DuplicateCon (loc, x)) adamc@805: else adamc@805: (); adamc@805: (SS.add (cons, x), vals) adamc@805: end adamc@805: in adamc@805: foldl doOne (cons, vals) dts adamc@805: end adamc@156: in adamc@805: (cons, 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@563: | 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@563: | L'.SgiClass (x, _, _, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@460: (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@469: val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []} adamc@469: 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@623: (unifyKinds env 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@706: and 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@805: (L'.SgnConst (ListUtil.mapConcat (fn (L'.SgiConAbs (x, n, k), loc) => adamc@805: [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adamc@805: | (L'.SgiDatatype dts, loc) => adamc@805: map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts adamc@563: | (L'.SgiClassAbs (x, n, k), loc) => adamc@805: [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adamc@66: | (L'.SgiStr (x, n, sgn), loc) => adamc@805: [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] adamc@805: | 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@706: and 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@706: and dopen env {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@805: ListUtil.foldlMapConcat adamc@805: (fn ((sgi, loc), env') => adamc@805: let adamc@805: val d = adamc@805: case sgi of adamc@805: L'.SgiConAbs (x, n, k) => adamc@805: let adamc@805: val c = (L'.CModProj (str, strs, x), loc) adamc@805: in adamc@805: [(L'.DCon (x, n, k, c), loc)] adamc@805: end adamc@805: | L'.SgiCon (x, n, k, c) => adamc@805: [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adamc@805: | L'.SgiDatatype dts => adamc@805: map (fn (x, n, xs, xncs) => (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts adamc@805: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@805: [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)] adamc@805: | L'.SgiVal (x, n, t) => adamc@805: [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] adamc@805: | L'.SgiStr (x, n, sgn) => adamc@805: [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] adamc@805: | L'.SgiSgn (x, n, sgn) => adamc@805: [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)] adamc@805: | L'.SgiConstraint (c1, c2) => adamc@805: [(L'.DConstraint (c1, c2), loc)] adamc@805: | L'.SgiClassAbs (x, n, k) => adamc@805: let adamc@805: val c = (L'.CModProj (str, strs, x), loc) adamc@805: in adamc@805: [(L'.DCon (x, n, k, c), loc)] adamc@805: end adamc@805: | L'.SgiClass (x, n, k, _) => adamc@805: let adamc@805: val c = (L'.CModProj (str, strs, x), loc) adamc@805: in adamc@805: [(L'.DCon (x, n, k, c), loc)] adamc@805: end adamc@805: in adamc@805: (d, foldl (fn (d, env') => E.declBinds env' d) env' d) adamc@805: end) adamc@805: env sgis adamc@66: | _ => (strError env (UnOpenable sgn); adamc@628: ([], env)) adamc@66: end adamc@66: adamc@706: and 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@707: | L'.DTable (tn, x, n, c, _, pc, _, cc) => adamc@707: [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), adamc@707: (L'.CConcat (pc, cc), loc)), loc)), loc)] adamc@460: | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] adamc@754: | L'.DView (tn, x, n, _, c) => adamc@754: [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)] adamc@563: | L'.DClass (x, n, k, c) => [(L'.SgiClass (x, n, k, c), loc)] adamc@271: | L'.DDatabase _ => [] adamc@460: | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] adamc@720: | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] adamc@88: adamc@838: and subSgn' counterparts env sgn1 (sgn2 as (_, loc2)) = adamc@469: ((*prefaces "subSgn" [("sgn1", p_sgn env sgn1), adamc@469: ("sgn2", p_sgn env sgn2)];*) 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@362: (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1), adamc@362: ("sgn2", p_sgn env sgn2), adamc@362: ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), adamc@362: ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) adamc@362: adamc@838: fun cpart n = IM.find (!counterparts, n) adamc@838: fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1) adamc@838: adamc@838: val sub2 = U.Con.map {kind = fn k => k, adamc@838: con = fn c => adamc@838: case c of adamc@838: L'.CNamed n2 => adamc@838: (case cpart n2 of adamc@838: NONE => c adamc@838: | SOME n1 => L'.CNamed n1) adamc@838: | _ => c} adamc@838: adamc@628: fun folder (sgi2All as (sgi, loc), env) = adamc@31: let adamc@362: (*val () = prefaces "folder" [("sgis1", p_sgn env (L'.SgnConst sgis1, loc2))]*) adamc@362: adamc@805: fun seek' f p = adamc@31: let adamc@628: fun seek env ls = adamc@31: case ls of adamc@805: [] => f env adamc@31: | h :: t => adamc@469: case p (env, h) of adamc@469: NONE => adamc@469: let adamc@469: val env = case #1 h of adamc@469: L'.SgiCon (x, n, k, c) => adamc@471: if E.checkENamed env n then adamc@471: env adamc@471: else adamc@471: E.pushCNamedAs env x n k (SOME c) adamc@469: | L'.SgiConAbs (x, n, k) => adamc@471: if E.checkENamed env n then adamc@471: env adamc@471: else adamc@471: E.pushCNamedAs env x n k NONE adamc@469: | _ => env adamc@469: in adamc@628: seek (E.sgiBinds env h) t adamc@469: end adamc@88: | SOME envs => envs adamc@31: in adamc@628: seek env sgis1 adamc@31: end adamc@805: adamc@805: val seek = seek' (fn env => (sgnError env (UnmatchedSgi sgi2All); adamc@805: env)) adamc@31: in adamc@31: case sgi of adamc@31: L'.SgiConAbs (x, n2, k2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@31: let adamc@41: fun found (x', n1, k1, co1) = adamc@41: if x = x' then adamc@41: let adamc@623: val () = unifyKinds env 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@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))) 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@805: | L'.SgiDatatype dts => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@805: adamc@805: fun search dts = adamc@805: case dts of adamc@805: [] => NONE adamc@805: | (x', n1, xs, _) :: dts => adamc@805: let adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@805: in adamc@805: case found (x', n1, k', NONE) of adamc@805: NONE => search dts adamc@805: | x => x adamc@805: end adamc@191: in adamc@805: search dts 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@711: | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE) adamc@711: | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c) adamc@31: | _ => NONE adamc@31: end) adamc@31: adamc@31: | L'.SgiCon (x, n2, k2, c2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@211: let adamc@211: fun found (x', n1, k1, c1) = adamc@211: if x = x' then adamc@211: let adamc@838: val c2 = sub2 c2 adamc@838: 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@839: (cparts (n2, n1); adamc@839: E.pushCNamedAs env x n1 k1 (SOME c1)) adamc@327: in adamc@628: SOME env adamc@327: end adamc@211: in adamc@628: (unifyCons env c1 c2; adamc@628: good ()) 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@711: | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: adamc@805: | L'.SgiDatatype dts2 => adamc@805: let adamc@805: fun found' (sgi1All, (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = adamc@805: if x1 <> x2 then adamc@805: NONE adamc@805: else adamc@805: let adamc@805: fun mismatched ue = adamc@805: (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); adamc@805: SOME env) adamc@805: adamc@805: val k = (L'.KType, loc) adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 adamc@805: adamc@805: fun good () = adamc@805: let adamc@805: val env = E.sgiBinds env sgi1All adamc@805: val env = if n1 = n2 then adamc@805: env adamc@805: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x1 n2 k' adamc@838: (SOME (L'.CNamed n1, loc))) adamc@805: in adamc@805: SOME env adamc@805: end adamc@805: adamc@805: val env = E.pushCNamedAs env x1 n1 k' NONE adamc@805: val env = if n1 = n2 then adamc@805: env adamc@805: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))) adamc@805: val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 adamc@805: fun xncBad ((x1, _, t1), (x2, _, t2)) = adamc@805: String.compare (x1, x2) <> EQUAL adamc@805: orelse case (t1, t2) of adamc@805: (NONE, NONE) => false adamc@805: | (SOME t1, SOME t2) => adamc@838: (unifyCons env t1 (sub2 t2); false) adamc@805: | _ => true adamc@805: in adamc@805: (if xs1 <> xs2 adamc@805: orelse length xncs1 <> length xncs2 adamc@805: orelse ListPair.exists xncBad (xncs1, xncs2) then adamc@805: mismatched NONE adamc@160: else adamc@805: good ()) adamc@805: handle CUnify ue => mismatched (SOME ue) adamc@805: end adamc@805: in adamc@805: seek' adamc@805: (fn _ => adamc@805: let adamc@805: fun seekOne (dt2, env) = adamc@805: seek (fn (env, sgi1All as (sgi1, _)) => adamc@805: case sgi1 of adamc@805: L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => adamc@805: found' (sgi1All, (x', n1, xs, xncs1), dt2, env) adamc@805: | _ => NONE) adamc@805: adamc@805: fun seekAll (dts, env) = adamc@805: case dts of adamc@805: [] => env adamc@805: | dt :: dts => seekAll (dts, seekOne (dt, env)) adamc@805: in adamc@805: seekAll (dts2, env) adamc@805: end) adamc@805: (fn (env, sgi1All as (sgi1, _)) => adamc@805: let adamc@805: fun found dts1 = adamc@805: let adamc@805: fun iter (dts1, dts2, env) = adamc@805: case (dts1, dts2) of adamc@805: ([], []) => SOME env adamc@805: | (dt1 :: dts1, dt2 :: dts2) => adamc@805: (case found' (sgi1All, dt1, dt2, env) of adamc@805: NONE => NONE adamc@805: | SOME env => iter (dts1, dts2, env)) adamc@805: | _ => NONE adamc@805: in adamc@805: iter (dts1, dts2, env) adamc@805: end adamc@805: in adamc@805: case sgi1 of adamc@805: L'.SgiDatatype dts1 => found dts1 adamc@805: | _ => NONE adamc@805: end) adamc@805: end adamc@156: adamc@191: | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => adamc@469: seek (fn (env, 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@838: cparts (n2, n1); adamc@628: SOME env adamc@158: end adamc@158: in adamc@628: (unifyCons env t1 t2; adamc@628: good ()) 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@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@32: case sgi1 of adamc@41: L'.SgiVal (x', n1, c1) => adamc@41: if x = x' then adamc@838: ((*prefaces "val" [("x", PD.string x), adamc@838: ("n1", PD.string (Int.toString n1)), adamc@838: ("c1", p_con env c1), adamc@838: ("c2", p_con env c2), adamc@838: ("c2'", p_con env (sub2 c2))];*) adamc@838: unifyCons env c1 (sub2 c2); adamc@628: SOME env) adamc@86: handle CUnify (c1, c2, err) => adamc@86: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@628: SOME env) adamc@41: else adamc@41: NONE adamc@32: | _ => NONE) adamc@32: adamc@33: | L'.SgiStr (x, n2, sgn2) => adamc@469: seek (fn (env, 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@838: val () = subSgn' counterparts env 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@628: SOME env adamc@66: end adamc@41: else adamc@41: NONE adamc@33: | _ => NONE) adamc@59: adamc@59: | L'.SgiSgn (x, n2, sgn2) => adamc@469: seek (fn (env, 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@838: val () = subSgn' counterparts env sgn1 sgn2 adamc@838: val () = subSgn' counterparts env 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@838: (cparts (n2, n1); adamc@838: E.pushSgnNamedAs env x n1 sgn2) adamc@65: in adamc@628: SOME env adamc@65: end adamc@59: else adamc@59: NONE adamc@59: | _ => NONE) adamc@88: adamc@88: | L'.SgiConstraint (c2, d2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@88: case sgi1 of adamc@88: L'.SgiConstraint (c1, d1) => adamc@628: if consEq env (c1, c2) andalso consEq env (d1, d2) then adamc@628: SOME env adamc@88: else adamc@88: NONE adamc@88: | _ => NONE) adamc@203: adamc@563: | L'.SgiClassAbs (x, n2, k2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@211: let adamc@563: fun found (x', n1, k1, co) = adamc@211: if x = x' then adamc@211: let adamc@623: val () = unifyKinds env k1 k2 adamc@563: handle KUnify (k1, k2, err) => adamc@563: sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) adamc@563: adamc@711: val env = E.pushCNamedAs env x n1 k1 co adamc@211: in adamc@211: SOME (if n1 = n2 then adamc@211: env adamc@211: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2)))) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@563: L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE) adamc@563: | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c) adamc@211: | _ => NONE adamc@211: end) adamc@563: | L'.SgiClass (x, n2, k2, c2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@211: let adamc@563: fun found (x', n1, k1, c1) = adamc@211: if x = x' then adamc@211: let adamc@623: val () = unifyKinds env k1 k2 adamc@563: handle KUnify (k1, k2, err) => adamc@563: sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) adamc@563: adamc@838: val c2 = sub2 c2 adamc@838: adamc@218: fun good () = adamc@218: let adamc@711: val env = E.pushCNamedAs env x n2 k2 (SOME c2) adamc@218: val env = if n1 = n2 then adamc@218: env adamc@218: else adamc@839: (cparts (n2, n1); adamc@839: E.pushCNamedAs env x n1 k2 (SOME c1)) adamc@218: in adamc@628: SOME env adamc@218: end adamc@211: in adamc@628: (unifyCons env c1 c2; adamc@628: good ()) 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@563: L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: end adamc@31: in adamc@628: ignore (foldl folder env sgis2) adamc@31: end adamc@31: adamc@41: | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => adamc@43: let adamc@480: val ran2 = adamc@43: if n1 = n2 then adamc@480: ran2 adamc@43: else adamc@480: subStrInSgn (n2, n1) ran2 adamc@43: in adamc@838: subSgn' counterparts env dom2 dom1; adamc@838: subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2 adamc@43: end adamc@41: adamc@469: | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) adamc@41: adamc@838: and subSgn env = subSgn' (ref IM.empty) env adamc@61: adamc@706: and 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@628: | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@623: | CKAbs _ => false adamc@623: | TKFun _ => false adamc@623: 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@621: | CMap => 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@628: | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@623: | CKAbs _ => false adamc@623: | TKFun _ => false adamc@623: 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@621: | CMap => 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@706: and 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@493: fun decompileKind (k, loc) = adamc@493: case k of adamc@493: L'.KType => SOME (L.KType, loc) adamc@493: | L'.KArrow (k1, k2) => adamc@493: (case (decompileKind k1, decompileKind k2) of adamc@493: (SOME k1, SOME k2) => SOME (L.KArrow (k1, k2), loc) adamc@493: | _ => NONE) adamc@493: | L'.KName => SOME (L.KName, loc) adamc@493: | L'.KRecord k => adamc@493: (case decompileKind k of adamc@493: SOME k => SOME (L.KRecord k, loc) adamc@493: | _ => NONE) adamc@493: | L'.KUnit => SOME (L.KUnit, loc) adamc@493: | L'.KTuple ks => adamc@493: let adamc@493: val ks' = List.mapPartial decompileKind ks adamc@493: in adamc@493: if length ks' = length ks then adamc@493: SOME (L.KTuple ks', loc) adamc@493: else adamc@493: NONE adamc@493: end adamc@493: adamc@493: | L'.KError => NONE adamc@493: | L'.KUnif (_, _, ref (SOME k)) => decompileKind k adamc@493: | L'.KUnif _ => NONE adamc@493: adamc@623: | L'.KRel _ => NONE adamc@623: | L'.KFun _ => NONE adamc@623: 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@913: | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c adamc@325: adamc@325: | _ => NONE adamc@325: adamc@469: val (neededC, constraints, neededV, _) = adamc@469: foldl (fn ((sgi, loc), (neededC, constraints, neededV, env')) => adamc@325: let adamc@469: val (needed, constraints, neededV) = adamc@325: case sgi of adamc@913: L'.SgiCon (x, _, k, c) => (SM.insert (neededC, x, (k, SOME c)), adamc@913: constraints, neededV) adamc@913: | L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, (k, NONE)), constraints, neededV) adamc@469: | L'.SgiConstraint cs => (neededC, (env', cs, loc) :: constraints, neededV) adamc@469: adamc@469: | L'.SgiVal (x, _, t) => adamc@469: let adamc@469: fun default () = (neededC, constraints, neededV) adamc@469: adamc@469: val t = normClassConstraint env' t adamc@469: in adamc@469: case #1 t of adamc@469: L'.CApp (f, _) => adamc@634: if isClassOrFolder env' f then adamc@469: (neededC, constraints, SS.add (neededV, x)) adamc@469: else adamc@469: default () adamc@469: | _ => default () adamc@469: end adamc@469: adamc@469: | _ => (neededC, constraints, neededV) adamc@325: in adamc@469: (needed, constraints, neededV, E.sgiBinds env' (sgi, loc)) adamc@325: end) adamc@493: (SM.empty, [], SS.empty, env) sgis adamc@325: adamc@634: val (neededC, neededV) = adamc@634: foldl (fn ((d, _), needed as (neededC, neededV)) => adamc@634: case d of adamc@634: L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) adamc@634: handle NotFound => adamc@634: needed) adamc@634: | L.DClass (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) adamc@634: handle NotFound => needed) adamc@634: | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) adamc@634: handle NotFound => needed) adamc@634: | L.DOpen _ => (SM.empty, SS.empty) adamc@634: | _ => needed) adamc@634: (neededC, neededV) ds adamc@469: adamc@469: val ds' = 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@469: adamc@469: val ds' = adamc@469: case SS.listItems neededV of adamc@469: [] => ds' adamc@469: | xs => adamc@469: let adamc@469: val ewild = (L.EWild, #2 str) adamc@469: val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs adamc@469: in adamc@469: ds'' @ ds' adamc@469: end adamc@469: adamc@469: val ds' = adamc@493: case SM.listItemsi neededC of adamc@469: [] => ds' adamc@469: | xs => adamc@469: let adamc@913: val ds'' = map (fn (x, (k, co)) => adamc@493: let adamc@493: val k = adamc@493: case decompileKind k of adamc@493: NONE => (L.KWild, #2 str) adamc@493: | SOME k => k adamc@913: adamc@493: val cwild = (L.CWild k, #2 str) adamc@913: val c = adamc@913: case co of adamc@913: NONE => cwild adamc@913: | SOME c => adamc@913: case decompileCon env c of adamc@913: NONE => cwild adamc@913: | SOME c' => c' adamc@493: in adamc@913: (L.DCon (x, NONE, c), #2 str) adamc@493: end) xs adamc@469: in adamc@469: ds'' @ ds' adamc@469: end adamc@325: in adamc@469: (L.StrConst (ds @ ds'), #2 str) adamc@325: end adamc@325: | _ => str) adamc@325: | _ => str adamc@325: adamc@706: and elabDecl (dAll as (d, loc), (env, denv, gs)) = adamc@255: let adamc@904: (*val () = preface ("elabDecl", SourcePrint.p_decl dAll)*) adamc@514: (*val befor = Time.now ()*) 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@623: | SOME k => elabKind env 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@805: | L.DDatatype dts => adamc@255: let adamc@255: val k = (L'.KType, loc) adamc@805: adamc@805: val (dts, env) = ListUtil.foldlMap adamc@805: (fn ((x, xs, xcs), env) => adamc@805: let adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@805: val (env, n) = E.pushCNamed env x k' NONE adamc@805: in adamc@805: ((x, n, xs, xcs), env) adamc@805: end) adamc@805: env dts adamc@805: adamc@805: val (dts, (env, gs')) = ListUtil.foldlMap adamc@805: (fn ((x, n, xs, xcs), (env, gs')) => adamc@805: let adamc@805: val t = (L'.CNamed n, loc) adamc@805: val nxs = length xs - 1 adamc@805: val t = ListUtil.foldli adamc@805: (fn (i, _, t) => adamc@805: (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@805: adamc@805: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@805: (E.pushCRel env' x k, adamc@805: D.enter denv')) (env, denv) xs adamc@805: adamc@805: val (xcs, (used, env, gs')) = adamc@805: ListUtil.foldlMap adamc@805: (fn ((x, to), (used, env, gs)) => adamc@805: let adamc@805: val (to, t, gs') = case to of adamc@805: NONE => (NONE, t, gs) adamc@805: | SOME t' => adamc@805: let adamc@805: val (t', tk, gs') = elabCon (env', denv') t' adamc@805: in adamc@805: checkKind env' t' tk k; adamc@805: (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) adamc@805: end adamc@805: val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@805: adamc@805: val (env, n') = E.pushENamed env x t adamc@805: in adamc@805: if SS.member (used, x) then adamc@805: strError env (DuplicateConstructor (x, loc)) adamc@805: else adamc@805: (); adamc@805: ((x, n', to), (SS.add (used, x), env, gs')) adamc@805: end) adamc@805: (SS.empty, env, gs') xcs adamc@805: in adamc@805: ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs')) adamc@805: end) adamc@805: (env, []) dts adamc@255: in adamc@805: ([(L'.DDatatype dts, loc)], (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@628: case hnormCon env (L'.CModProj (n, ms, s), loc) of adamc@628: (L'.CModProj (n, ms, s), _) => 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@844: val nxs = length xs adamc@844: val t = ListUtil.foldli (fn (i, _, t) => adamc@844: (L'.CApp (t, (L'.CRel (nxs - 1 - i), loc)), loc)) adamc@844: t xs 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@628: ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, 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@629: adamc@629: val () = checkCon env e' et c' adamc@629: adamc@674: val c' = normClassConstraint env c' adamc@255: val (env', n) = E.pushENamed env x c' adamc@255: in adamc@255: (*prefaces "DVal" [("x", Print.PD.string x), adamc@362: ("c'", p_con env c')];*) adamc@628: ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ 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@623: | L.EKAbs (_, 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@674: val c' = normClassConstraint env 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: in adamc@628: checkCon env e' et c'; adamc@255: if allowable e then adamc@255: () adamc@255: else adamc@255: expError env (IllegalRec (x, e')); adamc@628: ((x, n, c', e'), gs1 @ 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@628: subSgn env (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@834: val denv' = adamc@834: case #1 str' of adamc@834: L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} adamc@834: | _ => denv 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@834: ([(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@628: val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} adamc@628: 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@628: val denv' = 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@628: ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ 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@628: case hnormCon env ran of adamc@628: (L'.CApp (tf, arg), _) => adamc@628: (case (hnormCon env tf, hnormCon env arg) of adamc@628: ((L'.CModProj (basis, [], "transaction"), _), adamc@720: (L'.CApp (tf, arg3), _)) => adamc@325: (case (basis = !basis_r, adamc@720: hnormCon env tf, hnormCon env arg3) of adamc@325: (true, adamc@720: (L'.CApp (tf, arg2), _), adamc@628: ((L'.CRecord (_, []), _))) => adamc@720: (case (hnormCon env tf) of adamc@720: (L'.CApp (tf, arg1), _) => adamc@720: (case (hnormCon env tf, adamc@720: hnormCon env arg1, adamc@720: hnormCon env arg2) of adamc@720: (tf, arg1, adamc@720: (L'.CRecord (_, []), _)) => adamc@720: let adamc@720: val t = (L'.CApp (tf, arg1), loc) adamc@720: val t = (L'.CApp (t, arg2), loc) adamc@720: val t = (L'.CApp (t, arg3), loc) adamc@720: val t = (L'.CApp ( adamc@720: (L'.CModProj adamc@720: (basis, [], "transaction"), loc), adamc@325: t), loc) adamc@720: in adamc@720: (L'.SgiVal (x, n, makeRes t), loc) adamc@720: end adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all adamc@325: in adamc@628: case hnormCon env t of adamc@628: (L'.TFun (dom, ran), _) => adamc@628: (case hnormCon env dom of adamc@628: (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@707: | L.DTable (x, c, pe, ce) => adamc@255: let adamc@707: val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) adamc@707: adamc@255: val (c', k, gs') = elabCon (env, denv) c adamc@707: val pkey = cunif (loc, cstK) adamc@707: val uniques = cunif (loc, cstK) adamc@705: adamc@705: val ct = tableOf () adamc@705: val ct = (L'.CApp (ct, c'), loc) adamc@707: val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) adamc@705: adamc@705: val (env, n) = E.pushENamed env x ct adamc@707: val (pe', pet, gs'') = elabExp (env, denv) pe adamc@707: val (ce', cet, gs''') = elabExp (env, denv) ce adamc@707: adamc@707: val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) adamc@707: val pst = (L'.CApp (pst, c'), loc) adamc@707: val pst = (L'.CApp (pst, pkey), loc) adamc@704: adamc@704: val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) adamc@704: val cst = (L'.CApp (cst, c'), loc) adamc@705: val cst = (L'.CApp (cst, uniques), loc) adamc@255: in adamc@255: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@707: checkCon env pe' pet pst; adamc@707: checkCon env ce' cet cst; adamc@707: ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)], adamc@707: (env, denv, gs''' @ gs'' @ 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@754: | L.DView (x, e) => adamc@754: let adamc@754: val (e', t, gs') = elabExp (env, denv) e adamc@754: adamc@754: val k = (L'.KRecord (L'.KType, loc), loc) adamc@754: val fs = cunif (loc, k) adamc@754: val ts = cunif (loc, (L'.KRecord k, loc)) adamc@754: val tf = (L'.CApp ((L'.CMap (k, k), loc), adamc@754: (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc) adamc@754: val ts = (L'.CApp (tf, ts), loc) adamc@754: adamc@754: val cv = viewOf () adamc@754: val cv = (L'.CApp (cv, fs), loc) adamc@754: val (env', n) = E.pushENamed env x cv adamc@754: adamc@754: val ct = queryOf () adamc@754: val ct = (L'.CApp (ct, ts), loc) adamc@754: val ct = (L'.CApp (ct, fs), loc) adamc@754: in adamc@754: checkCon env e' t ct; adamc@754: ([(L'.DView (!basis_r, x, n, e', fs), loc)], adamc@754: (env', denv, gs' @ gs)) adamc@754: end adamc@255: adamc@563: | L.DClass (x, k, c) => adamc@255: let adamc@623: val k = elabKind env k adamc@280: val (c', ck, gs') = elabCon (env, denv) c adamc@711: val (env, n) = E.pushCNamed env x k (SOME c') adamc@255: val env = E.pushClass env n adamc@255: in adamc@711: checkKind env c' ck k; adamc@563: ([(L'.DClass (x, n, k, 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@459: | L.DCookie (x, c) => adamc@459: let adamc@459: val (c', k, gs') = elabCon (env, denv) c adamc@459: val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) adamc@459: in adamc@459: checkKind env c' k (L'.KType, loc); adamc@459: ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@459: end adamc@720: | L.DStyle x => adamc@718: let adamc@720: val (env, n) = E.pushENamed env x (styleOf ()) adamc@718: in adamc@720: ([(L'.DStyle (!basis_r, x, n), loc)], (env, denv, gs)) adamc@718: end adamc@459: adamc@280: (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) adamc@255: in adamc@904: (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll)];*) 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@805: | L'.SgiDatatype dts => adamc@156: let adamc@805: fun doOne ((x, n, xs, xncs), (cons, vals)) = adamc@805: let adamc@805: val (cons, x) = adamc@805: if SS.member (cons, x) then adamc@805: (cons, "?" ^ x) adamc@156: else adamc@805: (SS.add (cons, x), x) adamc@805: adamc@805: val (xncs, vals) = adamc@805: ListUtil.foldlMap adamc@805: (fn ((x, n, t), vals) => adamc@805: if SS.member (vals, x) then adamc@805: (("?" ^ x, n, t), vals) adamc@805: else adamc@805: ((x, n, t), SS.add (vals, x))) adamc@805: vals xncs adamc@805: in adamc@805: ((x, n, xs, xncs), (cons, vals)) adamc@805: end adamc@805: adamc@805: val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts adamc@156: in adamc@805: ((L'.SgiDatatype dts, 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@563: | L'.SgiClassAbs (x, n, k) => adamc@211: let 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@563: ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) adamc@211: end adamc@563: | L'.SgiClass (x, n, k, c) => adamc@211: let 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@563: ((L'.SgiClass (x, n, k, 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@834: val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []} adamc@834: 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@834: val (ran', gs) = elabSgn (env', denv') ran adamc@41: in adamc@628: subSgn env' 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@628: (subSgn env 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@833: fun resolveClass env = E.resolveClass (hnormCon env) (consEq env) env adamc@833: adamc@325: fun elabFile basis topStr topSgn env file = adamc@56: let adamc@713: val () = mayDelay := true adamc@713: val () = delayedUnifs := [] adamc@830: val () = delayedExhaustives := [] adamc@713: 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@628: val (ds, env') = dopen env' {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@821: val () = discoverC char "char" 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@720: ("c2", p_con env c2)]; adamc@478: raise Fail "Unresolved constraint in top.ur")) adamc@564: | TypeClass (env, c, r, loc) => adamc@564: let adamc@564: val c = normClassKey env c adamc@564: in adamc@833: case resolveClass env c of adamc@564: SOME e => r := SOME e adamc@564: | NONE => expError env (Unresolvable (loc, c)) adamc@634: end) gs adamc@564: adamc@720: val () = subSgn env' topSgn' topSgn adamc@720: adamc@325: val (env', top_n) = E.pushStrNamed env' "Top" topSgn adamc@633: val () = top_r := top_n adamc@325: adamc@628: val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} adamc@325: adamc@713: val checks = ref ([] : (unit -> unit) list) adamc@713: 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@713: checks := adamc@713: (fn () => adamc@713: (if List.exists kunifsInDecl ds then adamc@713: declError env (KunifsRemain ds) adamc@713: else adamc@713: (); adamc@713: adamc@713: case ListUtil.search cunifsInDecl ds of adamc@713: NONE => () adamc@713: | SOME loc => adamc@713: declError env (CunifsRemain ds))) adamc@713: :: !checks; adamc@76: adamc@83: (ds, (env, gs)) adamc@76: end adamc@76: adamc@83: val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file adamc@753: adamc@777: fun oneSummaryRound () = adamc@777: if ErrorMsg.anyErrors () then adamc@777: () adamc@777: else adamc@777: let adamc@777: val delayed = !delayedUnifs adamc@777: in adamc@777: delayedUnifs := []; adamc@777: app (fn (loc, env, k, s1, s2) => adamc@777: unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) adamc@777: delayed adamc@777: end adamc@56: in adamc@777: oneSummaryRound (); adamc@753: adamc@753: if ErrorMsg.anyErrors () then adamc@753: () adamc@753: else adamc@753: let adamc@753: fun solver gs = adamc@753: let adamc@753: val (gs, solved) = adamc@753: ListUtil.foldlMapPartial adamc@753: (fn (g, solved) => adamc@753: case g of adamc@753: Disjoint (loc, env, denv, c1, c2) => adamc@753: (case D.prove env denv (c1, c2, loc) of adamc@753: [] => (NONE, true) adamc@753: | _ => (SOME g, solved)) adamc@753: | TypeClass (env, c, r, loc) => adamc@753: let adamc@753: fun default () = (SOME g, solved) adamc@753: adamc@753: val c = normClassKey env c adamc@753: in adamc@833: case resolveClass env c of adamc@753: SOME e => (r := SOME e; adamc@753: (NONE, true)) adamc@753: | NONE => adamc@753: case #1 (hnormCon env c) of adamc@753: L'.CApp (f, x) => adamc@753: (case (#1 (hnormCon env f), #1 (hnormCon env x)) of adamc@753: (L'.CKApp (f, _), L'.CRecord (k, xcs)) => adamc@753: (case #1 (hnormCon env f) of adamc@753: L'.CModProj (top_n', [], "folder") => adamc@753: if top_n' = top_n then adamc@753: let adamc@753: val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) adamc@753: val e = (L'.EKApp (e, k), loc) adamc@753: adamc@753: val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => adamc@753: let adamc@753: val e = (L'.EModProj (top_n, ["Folder"], adamc@753: "cons"), loc) adamc@753: val e = (L'.EKApp (e, k), loc) adamc@753: val e = (L'.ECApp (e, adamc@753: (L'.CRecord (k, xcs), adamc@753: loc)), loc) adamc@753: val e = (L'.ECApp (e, x), loc) adamc@753: val e = (L'.ECApp (e, c), loc) adamc@753: val e = (L'.EApp (e, folder), loc) adamc@753: in adamc@753: (e, (x, c) :: xcs) adamc@753: end) adamc@753: (e, []) xcs adamc@753: in adamc@753: (r := SOME folder; adamc@753: (NONE, true)) adamc@753: end adamc@753: else adamc@753: default () adamc@753: | _ => default ()) adamc@753: | _ => default ()) adamc@753: | _ => default () adamc@753: end) adamc@753: false gs adamc@753: in adamc@753: case (gs, solved) of adamc@753: ([], _) => () adamc@777: | (_, true) => (oneSummaryRound (); solver gs) adamc@753: | _ => adamc@753: app (fn Disjoint (loc, env, denv, c1, c2) => adamc@753: ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; adamc@753: eprefaces' [("Con 1", p_con env c1), adamc@753: ("Con 2", p_con env c2), adamc@753: ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), adamc@753: ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) adamc@753: | TypeClass (env, c, r, loc) => adamc@753: expError env (Unresolvable (loc, c))) adamc@753: gs adamc@753: end adamc@753: in adamc@753: solver gs adamc@753: end; adamc@753: adamc@713: mayDelay := false; adamc@713: adamc@777: if ErrorMsg.anyErrors () then adamc@777: () adamc@777: else adamc@777: (app (fn (loc, env, k, s1, s2) => adamc@777: unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) adamc@777: handle CUnify' err => (ErrorMsg.errorAt loc "Error in final record unification"; adamc@777: cunifyError env err)) adamc@777: (!delayedUnifs); adamc@777: delayedUnifs := []); adamc@713: adamc@713: if ErrorMsg.anyErrors () then adamc@713: () adamc@713: else adamc@750: app (fn f => f ()) (!checks); adamc@750: adamc@830: if ErrorMsg.anyErrors () then adamc@830: () adamc@830: else adamc@837: app (fn all as (env, _, _, loc) => adamc@830: case exhaustive all of adamc@830: NONE => () adamc@830: | SOME p => expError env (Inexhaustive (loc, p))) adamc@830: (!delayedExhaustives); adamc@830: adamc@799: (*preface ("file", p_file env' file);*) adamc@799: 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