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@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@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@403: (L'.KUnif (loc, s, ref NONE), dummy) 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@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@403: (L'.CUnif (loc, k, s, ref NONE), dummy) 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@403: 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@628: fun unifyRecordCons env (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@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@628: unifySummaries env (k1, r1, r2) adamc@403: end adamc@403: 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@628: (unifyCons env c1 c2; adamc@628: true) adamc@403: handle CUnify _ => false 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@628: and unifySummaries env (k, s1 : record_summary, s2 : record_summary) = adamc@403: let adamc@403: val loc = #2 k adamc@403: (*val () = eprefaces "Summaries" [("#1", p_summary env s1), adamc@403: ("#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@403: val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) 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@403: fun unifFields (fs, others, unifs) = adamc@403: case (fs, others, unifs) of adamc@403: ([], [], _) => ([], [], unifs) adamc@403: | (_, _, []) => (fs, others, []) adamc@403: | (_, _, (_, r) :: rest) => adamc@403: let adamc@403: val r' = ref NONE adamc@403: val kr = (L'.KRecord k, dummy) adamc@403: val cr' = (L'.CUnif (dummy, kr, "recd", r'), dummy) adamc@403: adamc@403: val prefix = case (fs, others) of adamc@403: ([], other :: others) => adamc@403: List.foldl (fn (other, c) => adamc@403: (L'.CConcat (c, other), dummy)) adamc@403: other others adamc@403: | (fs, []) => adamc@403: (L'.CRecord (k, fs), dummy) adamc@403: | (fs, others) => adamc@403: List.foldl (fn (other, c) => adamc@403: (L'.CConcat (c, other), dummy)) adamc@403: (L'.CRecord (k, fs), dummy) others adamc@403: in adamc@403: r := SOME (L'.CConcat (prefix, cr'), dummy); adamc@403: ([], [], (cr', r') :: rest) adamc@403: end adamc@403: adamc@403: val (fs1, others1, unifs2) = unifFields (fs1, others1, unifs2) adamc@403: val (fs2, others2, unifs1) = unifFields (fs2, others2, unifs1) adamc@403: adamc@403: (*val () = eprefaces "Summaries4" [("#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@403: fun isGuessable (other, fs) = adamc@628: (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure); adamc@628: true) adamc@621: handle GuessFailure => false adamc@403: adamc@403: val (fs1, fs2, others1, others2) = adamc@403: case (fs1, fs2, others1, others2) of adamc@403: ([], _, [other1], []) => adamc@403: if isGuessable (other1, fs2) then adamc@403: ([], [], [], []) adamc@403: else adamc@403: (fs1, fs2, others1, others2) adamc@403: | (_, [], [], [other2]) => adamc@403: if isGuessable (other2, fs1) then adamc@403: ([], [], [], []) adamc@403: else adamc@403: (fs1, fs2, others1, others2) adamc@403: | _ => (fs1, fs2, others1, others2) adamc@403: adamc@403: (*val () = eprefaces "Summaries5" [("#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@403: val clear = case (fs1, others1, fs2, others2) of adamc@403: ([], [], [], []) => true adamc@403: | _ => false adamc@403: val empty = (L'.CRecord (k, []), dummy) adamc@403: adamc@403: fun unsummarize {fields, unifs, others} = adamc@403: let adamc@403: val c = (L'.CRecord (k, fields), loc) adamc@403: adamc@403: val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc)) adamc@403: c unifs adamc@403: in adamc@403: foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) adamc@403: c others adamc@403: end adamc@403: adamc@403: fun pairOffUnifs (unifs1, unifs2) = adamc@403: case (unifs1, unifs2) of adamc@403: ([], _) => adamc@403: if clear then adamc@403: List.app (fn (_, r) => r := SOME empty) unifs2 adamc@403: else adamc@403: raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) adamc@403: | (_, []) => adamc@403: if clear then adamc@403: List.app (fn (_, r) => r := SOME empty) unifs1 adamc@403: else adamc@403: raise CUnify' (CRecordFailure (unsummarize s1, unsummarize s2)) adamc@403: | ((c1, _) :: rest1, (_, r2) :: rest2) => adamc@403: (r2 := SOME c1; adamc@403: pairOffUnifs (rest1, rest2)) adamc@403: in adamc@403: pairOffUnifs (unifs1, unifs2) adamc@403: (*before eprefaces "Summaries'" [("#1", p_summary env s1), adamc@403: ("#2", p_summary 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@628: case #1 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@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@628: fun isRecord () = unifyRecordCons env (c1All, c2All) adamc@403: in adamc@403: (*eprefaces "unifyCons''" [("c1All", p_con env c1All), adamc@403: ("c2All", p_con env c2All)];*) adamc@403: adamc@403: case (c1, c2) of adamc@632: (L'.CError, _) => () adamc@632: | (_, L'.CError) => () adamc@632: adamc@632: | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => adamc@632: if r1 = r2 then adamc@632: () adamc@632: else adamc@632: (unifyKinds env k1 k2; adamc@632: r1 := SOME c2All) adamc@632: adamc@632: | (L'.CUnif (_, _, _, r), _) => adamc@632: if occursCon r c2All then adamc@632: err COccursCheckFailed adamc@632: else adamc@632: r := SOME c2All adamc@632: | (_, L'.CUnif (_, _, _, r)) => adamc@632: if occursCon r c1All then adamc@632: err COccursCheckFailed adamc@632: else adamc@632: r := SOME c1All adamc@632: adamc@632: | (L'.CUnit, L'.CUnit) => () adamc@403: adamc@403: | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => adamc@628: (unifyCons' env d1 d2; adamc@628: unifyCons' env r1 r2) adamc@403: | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => adamc@403: if expl1 <> expl2 then adamc@403: err CExplicitness adamc@403: else adamc@623: (unifyKinds env d1 d2; adamc@514: let adamc@514: (*val befor = Time.now ()*) adamc@514: val env' = E.pushCRel env x1 d1 adamc@514: in adamc@514: (*TextIO.print ("E.pushCRel: " adamc@514: ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) adamc@514: ^ "\n");*) adamc@628: unifyCons' env' r1 r2 adamc@514: end) adamc@628: | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env r1 r2 adamc@628: | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => adamc@628: (unifyCons' env c1 c2; adamc@628: unifyCons' env d1 d2; adamc@628: unifyCons' env e1 e2) adamc@403: adamc@403: | (L'.CRel n1, L'.CRel n2) => adamc@403: if n1 = n2 then adamc@628: () adamc@403: else adamc@403: err CIncompatible adamc@403: | (L'.CNamed n1, L'.CNamed n2) => adamc@403: if n1 = n2 then adamc@628: () adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => adamc@628: (unifyCons' env d1 d2; adamc@628: unifyCons' env r1 r2) adamc@403: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => adamc@623: (unifyKinds env k1 k2; adamc@628: unifyCons' (E.pushCRel env x1 k1) c1 c2) adamc@403: adamc@403: | (L'.CName n1, L'.CName n2) => adamc@403: if n1 = n2 then adamc@628: () adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => adamc@403: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then adamc@628: () adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CTuple cs1, L'.CTuple cs2) => adamc@628: ((ListPair.appEq (fn (c1, c2) => unifyCons' env c1 c2) (cs1, cs2)) adamc@403: handle ListPair.UnequalLengths => err CIncompatible) adamc@403: adamc@632: | (L'.CProj (c1, n1), _) => 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@632: err CIncompatible 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@632: | _ => err CIncompatible 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@632: | (_, L'.CProj (c2, n2)) => 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: | _ => err CIncompatible) adamc@632: | _ => err CIncompatible) adamc@403: 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: | (L'.CRecord _, _) => isRecord () adamc@403: | (_, L'.CRecord _) => isRecord () adamc@403: | (L'.CConcat _, _) => isRecord () adamc@403: | (_, L'.CConcat _) => isRecord () adamc@403: 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@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@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@628: in adamc@633: case #1 (hnormCon env dom) of adamc@633: L'.CApp (cl, x) => adamc@628: let adamc@633: val cl = hnormCon env cl adamc@628: in adamc@633: if infer <> L.TypesOnly then adamc@634: if isClassOrFolder env cl then adamc@633: let adamc@633: val r = ref NONE adamc@633: val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) adamc@633: in adamc@633: (e, t, TypeClass (env, dom, r, loc) :: gs) adamc@633: end adamc@633: else adamc@634: default () adamc@633: else adamc@633: default () adamc@628: end adamc@633: | _ => default () adamc@628: end adamc@629: | (L'.TDisjoint (r1, r2, t'), loc) => adamc@629: if infer <> L.TypesOnly then adamc@629: let adamc@629: val gs = D.prove env denv (r1, r2, loc) 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@15: in adamc@403: case infer of adamc@403: L.DontInfer => (e, t, []) adamc@403: | _ => unravel (t, e) adamc@15: 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@175: adamc@171: end adamc@171: adamc@172: datatype coverage = adamc@172: Wild adamc@173: | None adamc@172: | Datatype of coverage IM.map adamc@175: | Record of coverage SM.map list adamc@172: adamc@243: fun c2s c = adamc@243: case c of adamc@243: Wild => "Wild" adamc@243: | None => "None" adamc@243: | Datatype _ => "Datatype" adamc@243: | Record _ => "Record" adamc@243: adamc@629: fun exhaustive (env, t, ps, loc) = adamc@172: let adamc@402: fun depth (p, _) = adamc@402: case p of adamc@402: L'.PWild => 0 adamc@402: | L'.PVar _ => 0 adamc@402: | L'.PPrim _ => 0 adamc@402: | L'.PCon (_, _, _, NONE) => 1 adamc@402: | L'.PCon (_, _, _, SOME p) => 1 + depth p adamc@402: | L'.PRecord xps => foldl (fn ((_, p, _), n) => Int.max (depth p, n)) 0 xps adamc@402: adamc@402: val depth = 1 + foldl (fn (p, n) => Int.max (depth p, n)) 0 ps adamc@402: adamc@172: fun pcCoverage pc = adamc@172: case pc of adamc@172: L'.PConVar n => n adamc@174: | L'.PConProj (m1, ms, x) => adamc@174: let adamc@174: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@174: in adamc@174: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@174: NONE => raise Fail "exhaustive: Can't project constructor" adamc@191: | SOME (_, n, _, _, _) => n adamc@174: end adamc@172: adamc@172: fun coverage (p, _) = adamc@172: case p of adamc@172: L'.PWild => Wild adamc@172: | L'.PVar _ => Wild adamc@173: | L'.PPrim _ => None adamc@191: | L'.PCon (_, pc, _, NONE) => Datatype (IM.insert (IM.empty, pcCoverage pc, Wild)) adamc@191: | L'.PCon (_, pc, _, SOME p) => Datatype (IM.insert (IM.empty, pcCoverage pc, coverage p)) adamc@182: | L'.PRecord xps => Record [foldl (fn ((x, p, _), fmap) => adamc@182: SM.insert (fmap, x, coverage p)) SM.empty xps] adamc@176: adamc@172: fun merge (c1, c2) = adamc@172: case (c1, c2) of adamc@173: (None, _) => c2 adamc@173: | (_, None) => c1 adamc@173: adamc@173: | (Wild, _) => Wild adamc@172: | (_, Wild) => Wild adamc@172: adamc@172: | (Datatype cm1, Datatype cm2) => Datatype (IM.unionWith merge (cm1, cm2)) adamc@172: adamc@175: | (Record fm1, Record fm2) => Record (fm1 @ fm2) adamc@175: adamc@175: | _ => None adamc@175: adamc@172: fun combinedCoverage ps = adamc@172: case ps of adamc@172: [] => raise Fail "Empty pattern list for coverage checking" adamc@172: | [p] => coverage p adamc@172: | p :: ps => merge (coverage p, combinedCoverage ps) adamc@172: adamc@402: fun enumerateCases depth t = adamc@402: if depth = 0 then adamc@402: [Wild] adamc@402: else adamc@402: let adamc@402: fun dtype cons = adamc@402: ListUtil.mapConcat (fn (_, n, to) => adamc@402: case to of adamc@402: NONE => [Datatype (IM.insert (IM.empty, n, Wild))] adamc@402: | SOME t => map (fn c => Datatype (IM.insert (IM.empty, n, c))) adamc@402: (enumerateCases (depth-1) t)) cons adamc@402: in adamc@628: case #1 (hnormCon env t) of adamc@402: L'.CNamed n => adamc@402: (let adamc@402: val dt = E.lookupDatatype env n adamc@402: val cons = E.constructors dt adamc@175: in adamc@402: dtype cons adamc@402: end handle E.UnboundNamed _ => [Wild]) adamc@402: | L'.TRecord c => adamc@628: (case #1 (hnormCon env c) of adamc@402: L'.CRecord (_, xts) => adamc@402: let adamc@628: val xts = map (fn (x, t) => (hnormCon env x, t)) xts adamc@402: adamc@402: fun exponentiate fs = adamc@402: case fs of adamc@402: [] => [SM.empty] adamc@402: | ((L'.CName x, _), t) :: rest => adamc@402: let adamc@402: val this = enumerateCases depth t adamc@402: val rest = exponentiate rest adamc@402: in adamc@402: ListUtil.mapConcat (fn fmap => adamc@402: map (fn c => SM.insert (fmap, x, c)) this) rest adamc@402: end adamc@402: | _ => raise Fail "exponentiate: Not CName" adamc@402: in adamc@402: if List.exists (fn ((L'.CName _, _), _) => false adamc@402: | (c, _) => true) xts then adamc@402: [Wild] adamc@402: else adamc@402: map (fn ls => Record [ls]) (exponentiate xts) adamc@402: end adamc@402: | _ => [Wild]) adamc@402: | _ => [Wild] adamc@402: end adamc@175: adamc@175: fun coverageImp (c1, c2) = adamc@243: let adamc@243: val r = adamc@243: case (c1, c2) of adamc@243: (Wild, _) => true adamc@243: adamc@243: | (Datatype cmap1, Datatype cmap2) => adamc@243: List.all (fn (n, c2) => adamc@243: case IM.find (cmap1, n) of adamc@243: NONE => false adamc@243: | SOME c1 => coverageImp (c1, c2)) (IM.listItemsi cmap2) adamc@243: | (Datatype cmap1, Wild) => adamc@243: List.all (fn (n, c1) => coverageImp (c1, Wild)) (IM.listItemsi cmap1) adamc@243: adamc@243: | (Record fmaps1, Record fmaps2) => adamc@243: List.all (fn fmap2 => adamc@243: List.exists (fn fmap1 => adamc@243: List.all (fn (x, c2) => adamc@243: case SM.find (fmap1, x) of adamc@243: NONE => true adamc@243: | SOME c1 => coverageImp (c1, c2)) adamc@243: (SM.listItemsi fmap2)) adamc@243: fmaps1) fmaps2 adamc@243: adamc@243: | (Record fmaps1, Wild) => adamc@243: List.exists (fn fmap1 => adamc@243: List.all (fn (x, c1) => coverageImp (c1, Wild)) adamc@243: (SM.listItemsi fmap1)) fmaps1 adamc@243: adamc@243: | _ => false adamc@243: in adamc@243: (*TextIO.print ("coverageImp(" ^ c2s c1 ^ ", " ^ c2s c2 ^ ") = " ^ Bool.toString r ^ "\n");*) adamc@243: r adamc@243: end adamc@175: adamc@172: fun isTotal (c, t) = adamc@172: case c of adamc@628: None => false adamc@628: | Wild => true adamc@172: | Datatype cm => adamc@172: let adamc@628: val (t, _) = hnormCon env t adamc@628: adamc@628: val dtype = adamc@628: List.all (fn (_, n, to) => adamc@628: case IM.find (cm, n) of adamc@628: NONE => false adamc@628: | SOME c' => adamc@628: case to of adamc@628: NONE => true adamc@628: | SOME t' => isTotal (c', t')) adamc@191: adamc@191: fun unapp t = adamc@191: case t of adamc@191: L'.CApp ((t, _), _) => unapp t adamc@191: | _ => t adamc@172: in adamc@191: case unapp t of adamc@172: L'.CNamed n => adamc@172: let adamc@172: val dt = E.lookupDatatype env n adamc@172: val cons = E.constructors dt adamc@172: in adamc@174: dtype cons adamc@174: end adamc@174: | L'.CModProj (m1, ms, x) => adamc@174: let adamc@174: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@174: in adamc@174: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@174: NONE => raise Fail "isTotal: Can't project datatype" adamc@191: | SOME (_, cons) => dtype cons adamc@172: end adamc@628: | L'.CError => true adamc@341: | c => adamc@629: (prefaces "Not a datatype" [("loc", PD.string (ErrorMsg.spanToString loc)), adamc@629: ("c", p_con env (c, ErrorMsg.dummySpan))]; adamc@341: raise Fail "isTotal: Not a datatype") adamc@172: end adamc@628: | Record _ => List.all (fn c2 => coverageImp (c, c2)) (enumerateCases depth t) adamc@172: in adamc@172: isTotal (combinedCoverage ps, t) adamc@172: end adamc@172: adamc@217: fun unmodCon env (c, loc) = adamc@217: case c of adamc@217: L'.CNamed n => adamc@217: (case E.lookupCNamed env n of adamc@217: (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc)) adamc@217: | L'.CModProj (m1, ms, x) => adamc@217: let adamc@217: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@217: in adamc@217: case E.projectCon env {str = str, sgn = sgn, field = x} of adamc@217: NONE => raise Fail "unmodCon: Can't projectCon" adamc@217: | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc) adamc@217: end adamc@217: | _ => (c, loc) adamc@217: adamc@467: fun normClassKey envs c = adamc@467: let adamc@628: val c = hnormCon envs c adamc@467: in adamc@467: case #1 c of adamc@467: L'.CApp (c1, c2) => adamc@467: let adamc@467: val c1 = normClassKey envs c1 adamc@467: val c2 = normClassKey envs c2 adamc@467: in adamc@467: (L'.CApp (c1, c2), #2 c) adamc@467: end adamc@467: | _ => 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@467: val f = unmodCon env f adamc@467: val x = normClassKey env x adamc@217: in adamc@467: (L'.CApp (f, x), loc) adamc@217: end adamc@467: | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c adamc@467: | _ => (c, loc) adamc@216: adamc@92: fun elabExp (env, denv) (eAll as (e, loc)) = adamc@91: let adamc@280: (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)];*) adamc@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@91: val t = (L'.TFun (dom, ran), dummy) 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@629: if exhaustive (env, et, map #1 pes', loc) then adamc@172: () adamc@172: else adamc@172: expError env (Inexhaustive loc); 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@447: ((L'.ELet (eds, e), loc), t, gs1 @ gs2) adamc@447: end adamc@280: in adamc@513: (*prefaces "elabExp" [("e", SourcePrint.p_exp eAll), adamc@514: ("t", PD.string (LargeReal.toString (Time.toReal (Time.- (Time.now (), befor)))))];*) 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@447: L.EDVal (x, co, e) => 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: adamc@447: val (e', et, gs2) = elabExp (env, denv) e adamc@628: adamc@629: val () = checkCon env e' et c' adamc@629: adamc@467: val c' = normClassConstraint env c' adamc@447: val env' = E.pushERel env x c' adamc@447: in adamc@628: ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ 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@459: fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), 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@191: | L.SgiDatatype (x, xs, xcs) => adamc@157: let adamc@157: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: val (env, n) = E.pushCNamed env x k' NONE adamc@157: val t = (L'.CNamed n, loc) adamc@194: val nxs = length xs - 1 adamc@194: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@157: adamc@284: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@284: (E.pushCRel env' x k, adamc@284: D.enter denv')) (env, denv) xs adamc@284: adamc@157: val (xcs, (used, env, gs)) = adamc@157: ListUtil.foldlMap adamc@157: (fn ((x, to), (used, env, gs)) => adamc@157: let adamc@157: val (to, t, gs') = case to of adamc@157: NONE => (NONE, t, gs) adamc@157: | SOME t' => adamc@157: let adamc@284: val (t', tk, gs') = elabCon (env', denv') t' adamc@157: in adamc@284: checkKind env' t' tk k; adamc@157: (SOME t', (L'.TFun (t', t), loc), gs' @ gs) adamc@157: end adamc@191: val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@157: adamc@157: val (env, n') = E.pushENamed env x t adamc@157: in adamc@157: if SS.member (used, x) then adamc@157: strError env (DuplicateConstructor (x, loc)) adamc@157: else adamc@157: (); adamc@157: ((x, n', to), (SS.add (used, x), env, gs')) adamc@157: end) adamc@157: (SS.empty, env, []) xcs adamc@191: adamc@191: val env = E.pushDatatype env n xs xcs adamc@157: in adamc@191: ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) adamc@157: end adamc@156: adamc@158: | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" adamc@158: adamc@158: | L.SgiDatatypeImp (x, m1 :: ms, s) => adamc@158: (case E.lookupStr env m1 of adamc@158: NONE => (strError env (UnboundStr (loc, m1)); adamc@158: ([], (env, denv, gs))) adamc@158: | SOME (n, sgn) => adamc@158: let adamc@158: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@158: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@158: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@158: (strerror, sgnerror)) adamc@158: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@158: ((L'.StrVar n, loc), sgn) ms adamc@158: in adamc@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@76: val (env', n) = E.pushENamed env x c' adamc@467: val c' = normClassConstraint env c' adamc@76: in adamc@623: (unifyKinds env ck ktype adamc@76: handle KUnify ue => strError env (NotType (ck, ue))); adamc@31: adamc@467: ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiStr (x, sgn) => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: val (env', n) = E.pushStrNamed env x sgn' adamc@76: in adamc@88: ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiSgn (x, sgn) => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: val (env', n) = E.pushSgnNamed env x sgn' adamc@76: in adamc@88: ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@76: | L.SgiInclude sgn => adamc@76: let adamc@83: val (sgn', gs') = elabSgn (env, denv) sgn adamc@76: in adamc@76: case #1 (hnormSgn env sgn') of adamc@76: L'.SgnConst sgis => adamc@88: (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) adamc@76: | _ => (sgnError env (NotIncludable sgn'); adamc@88: ([], (env, denv, []))) adamc@88: end adamc@88: adamc@88: | L.SgiConstraint (c1, c2) => adamc@88: let adamc@88: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@88: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@88: adamc@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@563: val k' = (L'.KArrow (k, (L'.KType, loc)), loc) adamc@563: 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@563: val k' = (L'.KArrow (k, (L'.KType, loc)), loc) adamc@211: val (c', ck, gs) = elabCon (env, denv) c adamc@563: val (env, n) = E.pushCNamed env x k' (SOME c') adamc@211: val env = E.pushClass env n adamc@211: in adamc@563: 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@191: | L'.SgiDatatype (x, _, _, xncs) => adamc@156: let adamc@156: val vals = foldl (fn ((x, _, _), vals) => adamc@156: (if SS.member (vals, x) then adamc@156: sgnError env (DuplicateVal (loc, x)) adamc@156: else adamc@156: (); adamc@156: SS.add (vals, x))) adamc@156: vals xncs adamc@156: in adamc@156: if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => adamc@156: (if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiVal (x, _, _) => adamc@62: (if SS.member (vals, x) then adamc@62: sgnError env (DuplicateVal (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, SS.add (vals, x), sgns, strs)) adamc@62: | L'.SgiSgn (x, _, _) => adamc@62: (if SS.member (sgns, x) then adamc@62: sgnError env (DuplicateSgn (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, vals, SS.add (sgns, x), strs)) adamc@62: | L'.SgiStr (x, _, _) => adamc@62: (if SS.member (strs, x) then adamc@62: sgnError env (DuplicateStr (loc, x)) adamc@62: else adamc@62: (); adamc@88: (cons, vals, sgns, SS.add (strs, x))) adamc@203: | L'.SgiConstraint _ => (cons, vals, sgns, strs) adamc@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@66: fun selfify env {str, strs, sgn} = adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnError => sgn adamc@66: | L'.SgnVar _ => sgn adamc@66: adamc@66: | L'.SgnConst sgis => adamc@66: (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => adamc@66: (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | (L'.SgiDatatype (x, n, xs, xncs), loc) => adamc@191: (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@563: | (L'.SgiClassAbs (x, n, k), loc) => adamc@563: (L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@66: | (L'.SgiStr (x, n, sgn), loc) => adamc@66: (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) adamc@66: | x => x) sgis), #2 sgn) adamc@66: | L'.SgnFun _ => sgn adamc@66: | L'.SgnWhere _ => sgn adamc@66: | L'.SgnProj (m, ms, x) => adamc@66: case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar m, #2 sgn) ms, adamc@66: sgn = #2 (E.lookupStrNamed env m), adamc@66: field = x} of adamc@66: NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" adamc@66: | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} adamc@66: adamc@66: fun selfifyAt env {str, sgn} = adamc@66: let adamc@66: fun self (str, _) = adamc@66: case str of adamc@66: L'.StrVar x => SOME (x, []) adamc@66: | L'.StrProj (str, x) => adamc@66: (case self str of adamc@66: NONE => NONE adamc@66: | SOME (m, ms) => SOME (m, ms @ [x])) adamc@66: | _ => NONE adamc@66: in adamc@66: case self str of adamc@66: NONE => sgn adamc@66: | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} adamc@66: end adamc@66: adamc@628: fun 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@628: ListUtil.foldlMap (fn ((sgi, loc), env') => adamc@162: let adamc@162: val d = adamc@162: case sgi of adamc@162: L'.SgiConAbs (x, n, k) => adamc@162: let adamc@162: val c = (L'.CModProj (str, strs, x), loc) adamc@162: in adamc@162: (L'.DCon (x, n, k, c), loc) adamc@162: end adamc@162: | L'.SgiCon (x, n, k, c) => adamc@162: (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | L'.SgiDatatype (x, n, xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) adamc@162: | L'.SgiVal (x, n, t) => adamc@162: (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiStr (x, n, sgn) => adamc@162: (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) adamc@162: | L'.SgiSgn (x, n, sgn) => adamc@162: (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiConstraint (c1, c2) => adamc@162: (L'.DConstraint (c1, c2), loc) adamc@563: | L'.SgiClassAbs (x, n, k) => adamc@211: let adamc@563: val k' = (L'.KArrow (k, (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@563: (L'.DCon (x, n, k', c), loc) adamc@211: end adamc@563: | L'.SgiClass (x, n, k, _) => adamc@211: let adamc@563: val k' = (L'.KArrow (k, (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@563: (L'.DCon (x, n, k', c), loc) adamc@211: end adamc@162: in adamc@628: (d, E.declBinds env' d) adamc@162: end) adamc@628: env sgis adamc@66: | _ => (strError env (UnOpenable sgn); adamc@628: ([], env)) adamc@66: end adamc@66: adamc@31: fun sgiOfDecl (d, loc) = adamc@31: case d of adamc@123: L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] adamc@156: | L'.DDatatype x => [(L'.SgiDatatype x, loc)] adamc@156: | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] adamc@123: | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] adamc@123: | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis adamc@123: | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] adamc@123: | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] adamc@123: | L'.DExport _ => [] adamc@460: | L'.DTable (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (tableOf (), c), loc)), loc)] adamc@460: | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), 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@88: adamc@628: fun subSgn 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@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@31: fun seek p = adamc@31: let adamc@628: fun seek env ls = adamc@31: case ls of adamc@31: [] => (sgnError env (UnmatchedSgi sgi2All); adamc@628: 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@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@628: 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@191: | L'.SgiDatatype (x', n1, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', NONE) adamc@191: end adamc@191: | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) adamc@191: end adamc@563: | L'.SgiClassAbs (x', n1, k) => found (x', n1, adamc@563: (L'.KArrow (k, adamc@563: (L'.KType, loc)), loc), adamc@563: NONE) adamc@563: | L'.SgiClass (x', n1, k, c) => found (x', n1, adamc@563: (L'.KArrow (k, adamc@563: (L'.KType, loc)), loc), adamc@563: 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@327: fun good () = adamc@327: let adamc@327: val env = E.pushCNamedAs env x n2 k2 (SOME c2) adamc@327: val env = if n1 = n2 then adamc@327: env adamc@327: else adamc@327: E.pushCNamedAs env x n1 k1 (SOME c1) adamc@327: in adamc@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@563: | L'.SgiClass (x', n1, k1, c1) => adamc@563: found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: adamc@191: | L'.SgiDatatype (x, n2, xs2, xncs2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@160: let adamc@191: fun found (n1, xs1, xncs1) = adamc@160: let adamc@160: fun mismatched ue = adamc@160: (sgnError env (SgiMismatchedDatatypes (sgi1All, sgi2All, ue)); adamc@628: SOME env) adamc@156: adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 adamc@191: adamc@160: fun good () = adamc@160: let adamc@471: val env = E.sgiBinds env sgi1All adamc@160: val env = if n1 = n2 then adamc@160: env adamc@160: else adamc@471: E.pushCNamedAs env x n2 k' adamc@471: (SOME (L'.CNamed n1, loc)) adamc@160: in adamc@628: SOME env adamc@160: end adamc@156: adamc@397: val env = E.pushCNamedAs env x n1 k' NONE adamc@397: val env = if n1 = n2 then adamc@397: env adamc@397: else adamc@397: E.pushCNamedAs env x n2 k' (SOME (L'.CNamed n1, loc)) adamc@191: val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 adamc@160: fun xncBad ((x1, _, t1), (x2, _, t2)) = adamc@160: String.compare (x1, x2) <> EQUAL adamc@160: orelse case (t1, t2) of adamc@160: (NONE, NONE) => false adamc@160: | (SOME t1, SOME t2) => adamc@628: (unifyCons env t1 t2; false) adamc@160: | _ => true adamc@160: in adamc@191: (if xs1 <> xs2 adamc@191: orelse length xncs1 <> length xncs2 adamc@160: orelse ListPair.exists xncBad (xncs1, xncs2) then adamc@160: mismatched NONE adamc@160: else adamc@160: good ()) adamc@160: handle CUnify ue => mismatched (SOME ue) adamc@160: end adamc@160: in adamc@160: case sgi1 of adamc@191: L'.SgiDatatype (x', n1, xs, xncs1) => adamc@160: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@160: else adamc@160: NONE adamc@191: | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => adamc@162: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@162: else adamc@162: NONE adamc@160: | _ => NONE adamc@160: end) adamc@156: adamc@191: | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => adamc@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@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@628: (unifyCons env c1 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@628: val () = subSgn 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@628: val () = subSgn env sgn1 sgn2 adamc@628: val () = subSgn 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@65: 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@563: val k = (L'.KArrow (k1, (L'.KType, loc)), loc) adamc@211: val env = E.pushCNamedAs env x n1 k co adamc@211: in adamc@211: SOME (if n1 = n2 then adamc@211: env adamc@211: else adamc@628: E.pushCNamedAs env x n2 k (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: val k = (L'.KArrow (k2, (L'.KType, loc)), loc) adamc@563: 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@218: fun good () = adamc@218: let adamc@218: val env = E.pushCNamedAs env x n2 k (SOME c2) adamc@218: val env = if n1 = n2 then adamc@218: env adamc@218: else adamc@218: E.pushCNamedAs env x n1 k (SOME c1) adamc@218: in adamc@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@628: subSgn env dom2 dom1; adamc@628: subSgn (E.pushStrNamedAs env m1 n1 dom2) ran1 ran2 adamc@43: end adamc@41: adamc@469: | _ => sgnError env (SgnWrongForm (sgn1, sgn2))) adamc@41: adamc@61: adamc@312: fun positive self = adamc@312: let adamc@312: open L adamc@312: adamc@312: fun none (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => none c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso none c2 adamc@312: | TCFun (_, _, _, c) => none c adamc@312: | TRecord c => none c adamc@312: adamc@312: | CVar ([], x) => x <> self adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => none c1 andalso none c2 adamc@312: | CAbs _ => false adamc@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@325: fun wildifyStr env (str, sgn) = adamc@325: case #1 (hnormSgn env sgn) of adamc@325: L'.SgnConst sgis => adamc@325: (case #1 str of adamc@325: L.StrConst ds => adamc@325: let adamc@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@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@493: L'.SgiConAbs (x, _, k) => (SM.insert (neededC, x, k), 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@493: val ds'' = map (fn (x, k) => 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@493: val cwild = (L.CWild k, #2 str) adamc@493: in adamc@493: (L.DCon (x, NONE, cwild), #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@628: fun elabDecl (dAll as (d, loc), (env, denv, gs)) = adamc@255: let adamc@255: (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) 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@255: | L.DDatatype (x, xs, xcs) => adamc@255: let adamc@312: val positive = List.all (fn (_, to) => adamc@312: case to of adamc@312: NONE => true adamc@312: | SOME t => positive x t) xcs adamc@312: adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val (env, n) = E.pushCNamed env x k' NONE adamc@255: val t = (L'.CNamed n, loc) adamc@255: val nxs = length xs - 1 adamc@255: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@255: adamc@255: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@255: (E.pushCRel env' x k, adamc@255: D.enter denv')) (env, denv) xs adamc@255: adamc@255: val (xcs, (used, env, gs')) = adamc@255: ListUtil.foldlMap adamc@255: (fn ((x, to), (used, env, gs)) => adamc@255: let adamc@255: val (to, t, gs') = case to of adamc@255: NONE => (NONE, t, gs) adamc@255: | SOME t' => adamc@255: let adamc@255: val (t', tk, gs') = elabCon (env', denv') t' adamc@255: in adamc@255: checkKind env' t' tk k; adamc@255: (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) adamc@255: end adamc@255: val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@255: adamc@255: val (env, n') = E.pushENamed env x t adamc@255: in adamc@255: if SS.member (used, x) then adamc@255: strError env (DuplicateConstructor (x, loc)) adamc@255: else adamc@255: (); adamc@255: ((x, n', to), (SS.add (used, x), env, gs')) adamc@255: end) adamc@255: (SS.empty, env, []) xcs adamc@255: adamc@255: val env = E.pushDatatype env n xs xcs adamc@312: val d' = (L'.DDatatype (x, n, xs, xcs), loc) adamc@255: in adamc@601: (*if positive then adamc@312: () adamc@312: else adamc@601: declError env (Nonpositive d');*) adamc@312: adamc@312: ([d'], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" adamc@255: adamc@255: | L.DDatatypeImp (x, m1 :: ms, s) => adamc@255: (case E.lookupStr env m1 of adamc@255: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@255: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: in adamc@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@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@467: 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@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@255: in adamc@255: case #1 (hnormSgn env sgn') of adamc@255: L'.SgnFun _ => adamc@255: (case #1 str' of adamc@255: L'.StrFun _ => () adamc@255: | _ => strError env (FunctorRebind loc)) adamc@255: | _ => (); adamc@255: adamc@255: ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DFfiStr (x, sgn) => adamc@255: let adamc@255: val (sgn', gs') = elabSgn (env, denv) sgn adamc@255: adamc@255: val (env', n) = E.pushStrNamed env x sgn' adamc@255: in adamc@255: ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpen (m, ms) => adamc@255: (case E.lookupStr env m of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (_, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: adamc@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@628: (L'.CApp (tf, arg3), _)) => adamc@325: (case (basis = !basis_r, adamc@628: hnormCon env tf, hnormCon env arg3) of adamc@325: (true, adamc@628: (L'.CApp (tf, arg2), _), adamc@628: ((L'.CRecord (_, []), _))) => adamc@628: (case (hnormCon env tf) of adamc@628: (L'.CApp (tf, arg1), _) => adamc@628: (case (hnormCon env tf, adamc@628: hnormCon env arg1, adamc@628: hnormCon env arg2) of adamc@628: (tf, arg1, adamc@628: (L'.CRecord (_, []), _)) => adamc@325: let adamc@325: val t = (L'.CApp (tf, arg1), loc) adamc@325: val t = (L'.CApp (t, arg2), loc) adamc@325: val t = (L'.CApp (t, arg3), loc) adamc@325: val t = (L'.CApp ( adamc@325: (L'.CModProj adamc@325: (basis, [], "transaction"), loc), adamc@325: t), loc) adamc@325: in adamc@325: (L'.SgiVal (x, n, makeRes t), loc) adamc@325: end adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all adamc@325: in adamc@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@255: | L.DTable (x, c) => adamc@255: let adamc@255: val (c', k, gs') = elabCon (env, denv) c adamc@255: val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) adamc@255: in adamc@255: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@255: ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@255: end adamc@338: | L.DSequence x => adamc@338: let adamc@338: val (env, n) = E.pushENamed env x (sequenceOf ()) adamc@338: in adamc@338: ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) adamc@338: end adamc@255: adamc@563: | L.DClass (x, k, c) => adamc@255: let adamc@623: val k = elabKind env k adamc@563: val k' = (L'.KArrow (k, (L'.KType, loc)), loc) adamc@280: val (c', ck, gs') = elabCon (env, denv) c adamc@563: val (env, n) = E.pushCNamed env x k' (SOME c') adamc@255: val env = E.pushClass env n adamc@255: in adamc@563: 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@459: adamc@280: (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) adamc@255: in adamc@280: (*prefaces "elabDecl" [("e", SourcePrint.p_decl dAll), adamc@514: ("t", PD.string (LargeReal.toString (Time.toReal adamc@514: (Time.- (Time.now (), befor)))))];*) adamc@280: adamc@255: r adamc@255: end adamc@211: adamc@83: and elabStr (env, denv) (str, loc) = adamc@31: case str of adamc@31: L.StrConst ds => adamc@31: let adamc@88: val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds adamc@123: val sgis = ListUtil.mapConcat sgiOfDecl ds' adamc@63: adamc@63: val (sgis, _, _, _, _) = adamc@64: foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => adamc@63: case sgi of adamc@64: L'.SgiConAbs (x, n, k) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiCon (x, n, k, c) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@191: | L'.SgiDatatype (x, n, xs, xncs) => adamc@156: let adamc@156: val (cons, x) = adamc@156: if SS.member (cons, x) then adamc@156: (cons, "?" ^ x) adamc@156: else adamc@156: (SS.add (cons, x), x) adamc@156: adamc@156: val (xncs, vals) = adamc@156: ListUtil.foldlMap adamc@156: (fn ((x, n, t), vals) => adamc@156: if SS.member (vals, x) then adamc@156: (("?" ^ x, n, t), vals) adamc@156: else adamc@156: ((x, n, t), SS.add (vals, x))) adamc@156: vals xncs adamc@156: in adamc@191: ((L'.SgiDatatype (x, n, xs, xncs), loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@156: let adamc@156: val (cons, x) = adamc@156: if SS.member (cons, x) then adamc@156: (cons, "?" ^ x) adamc@156: else adamc@156: (SS.add (cons, x), x) adamc@156: in adamc@191: ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@64: | L'.SgiVal (x, n, c) => adamc@64: let adamc@64: val (vals, x) = adamc@64: if SS.member (vals, x) then adamc@64: (vals, "?" ^ x) adamc@64: else adamc@64: (SS.add (vals, x), x) adamc@64: in adamc@64: ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiSgn (x, n, sgn) => adamc@64: let adamc@64: val (sgns, x) = adamc@64: if SS.member (sgns, x) then adamc@64: (sgns, "?" ^ x) adamc@64: else adamc@64: (SS.add (sgns, x), x) adamc@64: in adamc@64: ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: adamc@64: | L'.SgiStr (x, n, sgn) => adamc@64: let adamc@64: val (strs, x) = adamc@64: if SS.member (strs, x) then adamc@64: (strs, "?" ^ x) adamc@64: else adamc@64: (SS.add (strs, x), x) adamc@64: in adamc@64: ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@88: end adamc@203: | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) adamc@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@83: val (str', actual, gs2) = elabStr (env', denv) str adamc@41: adamc@83: val (formal, gs3) = adamc@41: case ranO of adamc@83: NONE => (actual, []) adamc@41: | SOME ran => adamc@41: let adamc@83: val (ran', gs) = elabSgn (env', denv) ran adamc@41: in adamc@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@325: fun elabFile basis topStr topSgn env file = adamc@56: let adamc@83: val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) adamc@83: val () = case gs of adamc@83: [] => () adamc@207: | _ => (app (fn (_, env, _, c1, c2) => adamc@207: prefaces "Unresolved" adamc@207: [("c1", p_con env c1), adamc@207: ("c2", p_con env c2)]) gs; adamc@207: raise Fail "Unresolved disjointness constraints in Basis") adamc@83: adamc@56: val (env', basis_n) = E.pushStrNamed env "Basis" sgn adamc@210: val () = basis_r := basis_n adamc@56: adamc@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@203: val () = discoverC table "sql_table" adamc@56: adamc@325: val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@325: | _ => raise Fail "Unresolved disjointness constraints in top.urs" adamc@325: val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@329: | _ => app (fn Disjoint (loc, env, denv, c1, c2) => adamc@329: (case D.prove env denv (c1, c2, loc) of adamc@329: [] => () adamc@329: | _ => adamc@329: (prefaces "Unresolved constraint in top.ur" adamc@329: [("loc", PD.string (ErrorMsg.spanToString loc)), adamc@329: ("c1", p_con env c1), adamc@329: ("c2", p_con env c2)]; adamc@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@564: case E.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@628: val () = subSgn env' topSgn' topSgn adamc@325: 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@83: fun elabDecl' (d, (env, gs)) = adamc@76: let adamc@76: val () = resetKunif () adamc@76: val () = resetCunif () adamc@88: val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) adamc@76: in adamc@76: if ErrorMsg.anyErrors () then adamc@76: () adamc@76: else ( adamc@76: if List.exists kunifsInDecl ds then adamc@91: declError env (KunifsRemain ds) adamc@76: else adamc@76: (); adamc@76: adamc@76: case ListUtil.search cunifsInDecl ds of adamc@76: NONE => () adamc@76: | SOME loc => adamc@91: declError env (CunifsRemain ds) adamc@76: ); adamc@76: adamc@83: (ds, (env, gs)) adamc@76: end adamc@76: adamc@83: val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file adamc@56: in adamc@84: if ErrorMsg.anyErrors () then adamc@84: () adamc@84: else adamc@228: app (fn Disjoint (loc, env, denv, c1, c2) => adamc@228: (case D.prove env denv (c1, c2, loc) of adamc@228: [] => () adamc@228: | _ => adamc@228: (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; adamc@228: eprefaces' [("Con 1", p_con env c1), adamc@228: ("Con 2", p_con env c2), adamc@228: ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), adamc@228: ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) adamc@228: | TypeClass (env, c, r, loc) => adamc@349: let adamc@634: fun default () = expError env (Unresolvable (loc, c)) adamc@634: adamc@467: val c = normClassKey env c adamc@349: in adamc@349: case E.resolveClass env c of adamc@349: SOME e => r := SOME e adamc@634: | NONE => adamc@634: case #1 (hnormCon env c) of adamc@634: L'.CApp (f, x) => adamc@634: (case (#1 (hnormCon env f), #1 (hnormCon env x)) of adamc@634: (L'.CKApp (f, _), L'.CRecord (k, xcs)) => adamc@634: (case #1 (hnormCon env f) of adamc@634: L'.CModProj (top_n', [], "folder") => adamc@634: if top_n' = top_n then adamc@634: let adamc@634: val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) adamc@634: val e = (L'.EKApp (e, k), loc) adamc@634: adamc@634: val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => adamc@634: let adamc@634: val e = (L'.EModProj (top_n, ["Folder"], adamc@634: "cons"), loc) adamc@634: val e = (L'.EKApp (e, k), loc) adamc@634: val e = (L'.ECApp (e, adamc@634: (L'.CRecord (k, xcs), adamc@634: loc)), loc) adamc@634: val e = (L'.ECApp (e, x), loc) adamc@634: val e = (L'.ECApp (e, c), loc) adamc@634: val e = (L'.EApp (e, folder), loc) adamc@634: in adamc@634: (e, (x, c) :: xcs) adamc@634: end) adamc@634: (e, []) xcs adamc@634: in adamc@634: r := SOME folder adamc@634: end adamc@634: else adamc@634: default () adamc@634: | _ => default ()) adamc@634: | _ => default ()) adamc@634: | _ => default () adamc@349: end) gs; adamc@83: adamc@325: (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) adamc@325: :: ds adamc@325: @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) adamc@325: :: ds' @ file adamc@56: end adamc@2: adamc@2: end