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@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@403: fun unifyKinds' (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@403: (unifyKinds' d1 d2; adamc@403: unifyKinds' r1 r2) adamc@403: | (L'.KName, L'.KName) => () adamc@403: | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 adamc@403: | (L'.KTuple ks1, L'.KTuple ks2) => adamc@403: ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) adamc@403: handle ListPair.UnequalLengths => err KIncompatible) adamc@403: adamc@403: | (L'.KError, _) => () adamc@403: | (_, L'.KError) => () adamc@403: adamc@403: | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All adamc@403: | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' 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@403: fun unifyKinds k1 k2 = adamc@403: unifyKinds' k1 k2 adamc@403: handle KUnify' err => raise KUnify (k1, k2, err) adamc@403: adamc@403: fun checkKind env c k1 k2 = adamc@403: unifyKinds 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@403: fun elabKind (k, loc) = adamc@403: case k of adamc@403: L.KType => (L'.KType, loc) adamc@403: | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) adamc@403: | L.KName => (L'.KName, loc) adamc@403: | L.KRecord k => (L'.KRecord (elabKind k), loc) adamc@403: | L.KUnit => (L'.KUnit, loc) adamc@403: | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) adamc@403: | L.KWild => kunif loc adamc@403: adamc@403: fun foldKind (dom, ran, loc)= adamc@403: (L'.KArrow ((L'.KArrow ((L'.KName, loc), adamc@403: (L'.KArrow (dom, adamc@403: (L'.KArrow (ran, ran), loc)), loc)), loc), adamc@403: (L'.KArrow (ran, adamc@403: (L'.KArrow ((L'.KRecord dom, loc), adamc@403: 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@403: fun elabCon (env, denv) (c, loc) = adamc@403: case c of adamc@403: L.CAnnot (c, k) => adamc@403: let adamc@403: val k' = elabKind 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@403: val k' = elabKind 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@403: | L.CDisjoint (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@403: val (denv', gs3) = 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@403: ((L'.CDisjoint (L'.Instantiate, c1', c2', c'), loc), k, gs1 @ gs2 @ gs3 @ 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@403: ((L'.CRel n, loc), k, []) adamc@403: | E.Named (n, k) => adamc@403: ((L'.CNamed n, loc), k, [])) 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@403: | SOME k => elabKind 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@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@403: | L.CFold => adamc@403: let adamc@403: val dom = kunif loc adamc@403: val ran = kunif loc adamc@403: in adamc@403: ((L'.CFold (dom, ran), loc), adamc@403: foldKind (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@403: val k' = elabKind 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: open ElabOps 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@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@403: | L'.CDisjoint (_, _, _, c) => kindof env c 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@403: | L'.CFold (dom, ran) => foldKind (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@403: val hnormCon = D.hnormCon adamc@403: adamc@403: datatype con_summary = adamc@403: Nil adamc@403: | Cons adamc@403: | Unknown adamc@403: adamc@403: fun compatible cs = adamc@403: case cs of adamc@403: (Unknown, _) => false adamc@403: | (_, Unknown) => false adamc@403: | (s1, s2) => s1 = s2 adamc@403: adamc@403: fun summarizeCon (env, denv) c = adamc@403: let adamc@403: val (c, gs) = hnormCon (env, denv) c adamc@403: in adamc@403: case #1 c of adamc@403: L'.CRecord (_, []) => (Nil, gs) adamc@403: | L'.CRecord (_, _ :: _) => (Cons, gs) adamc@403: | L'.CConcat ((L'.CRecord (_, _ :: _), _), _) => (Cons, gs) adamc@403: | L'.CDisjoint (_, _, _, c) => adamc@34: let adamc@403: val (s, gs') = summarizeCon (env, denv) c adamc@34: in adamc@403: (s, gs @ gs') adamc@403: end adamc@403: | _ => (Unknown, gs) adamc@403: end adamc@403: adamc@403: fun p_con_summary s = adamc@403: Print.PD.string (case s of adamc@403: Nil => "Nil" adamc@403: | Cons => "Cons" adamc@403: | Unknown => "Unknown") adamc@403: adamc@403: exception SummaryFailure 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@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@518: | L'.CDisjoint (_, _, _, c) => false(*isUnitCon env c*) adamc@513: adamc@513: | L'.CName _ => false adamc@513: adamc@513: | L'.CRecord _ => false adamc@513: | L'.CConcat _ => false adamc@513: | L'.CFold _ => 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@403: fun unifyRecordCons (env, denv) (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@403: val (r1, gs1) = recordSummary (env, denv) c1 adamc@403: val (r2, gs2) = recordSummary (env, denv) c2 adamc@403: in adamc@403: unifyKinds k1 k2; adamc@403: unifySummaries (env, denv) (k1, r1, r2); adamc@403: gs1 @ gs2 adamc@403: end adamc@403: adamc@403: and recordSummary (env, denv) c = adamc@403: let adamc@403: val (c, gs) = hnormCon (env, denv) c adamc@403: adamc@403: val (sum, gs') = adamc@403: case c of adamc@403: (L'.CRecord (_, xcs), _) => ({fields = xcs, unifs = [], others = []}, []) adamc@403: | (L'.CConcat (c1, c2), _) => adamc@403: let adamc@403: val (s1, gs1) = recordSummary (env, denv) c1 adamc@403: val (s2, gs2) = recordSummary (env, denv) c2 adamc@403: in adamc@403: ({fields = #fields s1 @ #fields s2, adamc@403: unifs = #unifs s1 @ #unifs s2, adamc@403: others = #others s1 @ #others s2}, adamc@403: gs1 @ gs2) adamc@403: end adamc@403: | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary (env, denv) c adamc@403: | c' as (L'.CUnif (_, _, _, r), _) => ({fields = [], unifs = [(c', r)], others = []}, []) adamc@403: | c' => ({fields = [], unifs = [], others = [c']}, []) adamc@403: in adamc@403: (sum, gs @ gs') adamc@403: end adamc@403: adamc@403: and consEq (env, denv) (c1, c2) = adamc@403: let adamc@403: val gs = unifyCons (env, denv) c1 c2 adamc@403: in adamc@403: List.all (fn (loc, env, denv, c1, c2) => adamc@403: case D.prove env denv (c1, c2, loc) of adamc@403: [] => true adamc@403: | _ => false) gs adamc@403: end adamc@403: handle CUnify _ => false adamc@403: adamc@403: and consNeq env (c1, c2) = adamc@403: case (#1 (ElabOps.hnormCon env c1), #1 (ElabOps.hnormCon env c2)) of adamc@403: (L'.CName x1, L'.CName x2) => x1 <> x2 adamc@403: | _ => false adamc@403: adamc@403: and unifySummaries (env, denv) (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@403: andalso consEq (env, denv) (c1, c2) adamc@403: andalso consEq (env, denv) (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@403: val (others1, others2) = eatMatching (consEq (env, denv)) (#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@403: let adamc@403: val gs = guessFold (env, denv) (other, (L'.CRecord (k, fs), loc), [], SummaryFailure) adamc@403: in adamc@403: List.all (fn (loc, env, denv, c1, c2) => adamc@403: case D.prove env denv (c1, c2, loc) of adamc@403: [] => true adamc@403: | _ => false) gs adamc@403: end adamc@403: handle SummaryFailure => 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@403: and guessFold (env, denv) (c1, c2, gs, ex) = adamc@403: let adamc@403: val loc = #2 c1 adamc@403: adamc@403: fun unfold (dom, ran, f, i, r, c) = adamc@403: let adamc@403: val nm = cunif (loc, (L'.KName, loc)) adamc@412: val v = adamc@412: case dom of adamc@412: (L'.KUnit, _) => (L'.CUnit, loc) adamc@412: | _ => cunif (loc, dom) adamc@403: val rest = cunif (loc, (L'.KRecord dom, loc)) adamc@403: val acc = (L'.CFold (dom, ran), loc) adamc@403: val acc = (L'.CApp (acc, f), loc) adamc@403: val acc = (L'.CApp (acc, i), loc) adamc@403: val acc = (L'.CApp (acc, rest), loc) adamc@403: adamc@403: val (iS, gs3) = summarizeCon (env, denv) i adamc@403: adamc@403: val app = (L'.CApp (f, nm), loc) adamc@403: val app = (L'.CApp (app, v), loc) adamc@403: val app = (L'.CApp (app, acc), loc) adamc@403: val (appS, gs4) = summarizeCon (env, denv) app adamc@403: adamc@403: val (cS, gs5) = summarizeCon (env, denv) c adamc@403: in adamc@403: (*prefaces "Summaries" [("iS", p_con_summary iS), adamc@403: ("appS", p_con_summary appS), adamc@403: ("cS", p_con_summary cS)];*) adamc@403: adamc@403: if compatible (iS, appS) then adamc@403: raise ex adamc@403: else if compatible (cS, iS) then adamc@403: let adamc@403: (*val () = prefaces "Same?" [("i", p_con env i), adamc@403: ("c", p_con env c)]*) adamc@403: val gs6 = unifyCons (env, denv) i c adamc@403: (*val () = TextIO.print "Yes!\n"*) adamc@403: adamc@403: val gs7 = unifyCons (env, denv) r (L'.CRecord (dom, []), loc) adamc@403: in adamc@403: gs @ gs3 @ gs5 @ gs6 @ gs7 adamc@403: end adamc@403: else if compatible (cS, appS) then adamc@403: let adamc@403: (*val () = prefaces "Same?" [("app", p_con env app), adamc@403: ("c", p_con env c), adamc@403: ("app'", p_con env (#1 (hnormCon (env, denv) app)))]*) adamc@403: val gs6 = unifyCons (env, denv) app c adamc@403: (*val () = TextIO.print "Yes!\n"*) adamc@403: adamc@403: val singleton = (L'.CRecord (dom, [(nm, v)]), loc) adamc@403: val concat = (L'.CConcat (singleton, rest), loc) adamc@403: (*val () = prefaces "Pre-crew" [("r", p_con env r), adamc@403: ("concat", p_con env concat)]*) adamc@403: val gs7 = unifyCons (env, denv) r concat adamc@403: in adamc@403: (*prefaces "The crew" [("nm", p_con env nm), adamc@403: ("v", p_con env v), adamc@403: ("rest", p_con env rest)];*) adamc@403: adamc@403: gs @ gs3 @ gs4 @ gs5 @ gs6 @ gs7 adamc@403: end adamc@403: else adamc@403: raise ex adamc@403: end adamc@403: handle _ => raise ex adamc@403: in adamc@403: case (#1 c1, #1 c2) of adamc@403: (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r), _) => adamc@403: unfold (dom, ran, f, i, r, c2) adamc@403: | (_, L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold (dom, ran), _), f), _), i), _), r)) => adamc@403: unfold (dom, ran, f, i, r, c1) adamc@403: | _ => raise ex adamc@403: end adamc@403: adamc@403: and unifyCons' (env, denv) c1 c2 = adamc@403: case (#1 c1, #1 c2) of adamc@403: (L'.CDisjoint (_, x1, y1, t1), L'.CDisjoint (_, x2, y2, t2)) => adamc@403: let adamc@403: val gs1 = unifyCons' (env, denv) x1 x2 adamc@403: val gs2 = unifyCons' (env, denv) y1 y2 adamc@403: val (denv', gs3) = D.assert env denv (x1, y1) adamc@403: val gs4 = unifyCons' (env, denv') t1 t2 adamc@403: in adamc@403: gs1 @ gs2 @ gs3 @ gs4 adamc@403: end adamc@403: | _ => adamc@513: if isUnitCon env c1 andalso isUnitCon env c2 then adamc@513: [] adamc@513: else adamc@403: let adamc@514: (*val befor = Time.now () adamc@514: val old1 = c1 adamc@514: val old2 = c2*) adamc@411: val (c1, gs1) = hnormCon (env, denv) c1 adamc@411: val (c2, gs2) = hnormCon (env, denv) c2 adamc@403: in adamc@411: let adamc@411: val gs3 = unifyCons'' (env, denv) c1 c2 adamc@411: in adamc@514: (*prefaces "unifyCons'" [("c1", p_con env old1), adamc@514: ("c2", p_con env old2), adamc@514: ("t", PD.string (LargeReal.toString (Time.toReal adamc@514: (Time.- (Time.now (), befor)))))];*) adamc@411: gs1 @ gs2 @ gs3 adamc@411: end adamc@411: handle ex => guessFold (env, denv) (c1, c2, gs1 @ gs2, ex) adamc@403: end adamc@403: adamc@403: and unifyCons'' (env, denv) (c1All as (c1, loc)) (c2All as (c2, _)) = adamc@403: let adamc@403: fun err f = raise CUnify' (f (c1All, c2All)) adamc@403: adamc@403: fun isRecord () = unifyRecordCons (env, denv) (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@403: (L'.CUnit, L'.CUnit) => [] adamc@403: adamc@403: | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => adamc@403: unifyCons' (env, denv) d1 d2 adamc@403: @ unifyCons' (env, denv) 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@403: (unifyKinds d1 d2; adamc@514: let adamc@514: val denv' = D.enter denv 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@514: unifyCons' (env', denv') r1 r2 adamc@514: end) adamc@403: | (L'.TRecord r1, L'.TRecord r2) => unifyCons' (env, denv) r1 r2 adamc@403: adamc@403: | (L'.CRel n1, L'.CRel n2) => adamc@403: if n1 = n2 then adamc@403: [] adamc@403: else adamc@403: err CIncompatible adamc@403: | (L'.CNamed n1, L'.CNamed n2) => adamc@403: if n1 = n2 then adamc@403: [] adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => adamc@403: (unifyCons' (env, denv) d1 d2; adamc@403: unifyCons' (env, denv) r1 r2) adamc@403: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => adamc@403: (unifyKinds k1 k2; adamc@403: unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) adamc@403: adamc@403: | (L'.CName n1, L'.CName n2) => adamc@403: if n1 = n2 then adamc@403: [] 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@403: [] adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CTuple cs1, L'.CTuple cs2) => adamc@403: ((ListPair.foldlEq (fn (c1, c2, gs) => adamc@403: let adamc@403: val gs' = unifyCons' (env, denv) c1 c2 adamc@403: in adamc@403: gs' @ gs adamc@403: end) [] (cs1, cs2)) adamc@403: handle ListPair.UnequalLengths => err CIncompatible) adamc@403: adamc@403: | (L'.CProj ((L'.CUnif (_, _, _, ref (SOME c1)), loc), n1), _) => adamc@403: unifyCons' (env, denv) (L'.CProj (c1, n1), loc) c2All adamc@403: | (_, L'.CProj ((L'.CUnif (_, _, _, ref (SOME c2)), loc), n2)) => adamc@403: unifyCons' (env, denv) c1All (L'.CProj (c2, n2), loc) adamc@403: | (L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n), _) => adamc@403: let adamc@403: val us = map (fn k => cunif (loc, k)) ks adamc@403: in adamc@403: r := SOME (L'.CTuple us, loc); adamc@403: unifyCons' (env, denv) (List.nth (us, n - 1)) c2All adamc@403: end adamc@403: | (_, L'.CProj ((L'.CUnif (_, (L'.KTuple ks, _), _, r), loc), n)) => adamc@403: let adamc@403: val us = map (fn k => cunif (loc, k)) ks adamc@403: in adamc@403: r := SOME (L'.CTuple us, loc); adamc@403: unifyCons' (env, denv) c1All (List.nth (us, n - 1)) adamc@403: end adamc@403: | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => adamc@403: if n1 = n2 then adamc@403: unifyCons' (env, denv) c1 c2 adamc@403: else adamc@403: err CIncompatible adamc@403: adamc@403: | (L'.CError, _) => [] adamc@403: | (_, L'.CError) => [] adamc@403: adamc@403: | (L'.CRecord _, _) => isRecord () adamc@403: | (_, L'.CRecord _) => isRecord () adamc@403: | (L'.CConcat _, _) => isRecord () adamc@403: | (_, L'.CConcat _) => isRecord () adamc@403: adamc@403: | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => adamc@403: if r1 = r2 then adamc@403: [] adamc@403: else adamc@403: (unifyKinds k1 k2; adamc@403: r1 := SOME c2All; adamc@403: []) adamc@403: adamc@403: | (L'.CUnif (_, _, _, r), _) => adamc@403: if occursCon r c2All then adamc@403: err COccursCheckFailed adamc@403: else adamc@403: (r := SOME c2All; adamc@403: []) adamc@403: | (_, L'.CUnif (_, _, _, r)) => adamc@403: if occursCon r c1All then adamc@403: err COccursCheckFailed adamc@403: else adamc@403: (r := SOME c1All; adamc@403: []) adamc@403: adamc@403: | (L'.CFold (dom1, ran1), L'.CFold (dom2, ran2)) => adamc@403: (unifyKinds dom1 dom2; adamc@403: unifyKinds ran1 ran2; adamc@403: []) adamc@403: adamc@403: | _ => err CIncompatible adamc@403: end adamc@403: adamc@403: and unifyCons (env, denv) c1 c2 = adamc@403: unifyCons' (env, denv) 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@403: fun checkCon (env, denv) e c1 c2 = adamc@403: unifyCons (env, denv) c1 c2 adamc@403: handle CUnify (c1, c2, err) => adamc@403: (expError env (Unify (e, c1, c2, err)); adamc@83: []) adamc@403: adamc@403: fun checkPatCon (env, denv) p c1 c2 = adamc@403: unifyCons (env, denv) c1 c2 adamc@403: handle CUnify (c1, c2, err) => adamc@403: (expError env (PatUnify (p, c1, c2, err)); adamc@86: []) 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@403: adamc@403: fun recCons (k, nm, v, rest, loc) = adamc@403: (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc), adamc@403: rest), loc) adamc@403: adamc@403: fun foldType (dom, loc) = adamc@403: (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), adamc@403: (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), adamc@403: (L'.TCFun (L'.Explicit, "v", dom, adamc@403: (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), adamc@403: (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), adamc@403: (L'.CDisjoint (L'.Instantiate, adamc@403: (L'.CRecord adamc@403: ((L'.KUnit, loc), adamc@403: [((L'.CRel 2, loc), adamc@403: (L'.CUnit, loc))]), loc), adamc@403: (L'.CRel 0, loc), adamc@403: (L'.CApp ((L'.CRel 3, loc), adamc@403: recCons (dom, adamc@403: (L'.CRel 2, loc), adamc@403: (L'.CRel 1, loc), adamc@403: (L'.CRel 0, loc), adamc@403: loc)), loc)), adamc@403: loc)), loc)), adamc@403: loc)), loc)), loc), adamc@403: (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), adamc@403: (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), adamc@403: (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), adamc@403: loc)), loc)), loc) adamc@403: 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@403: fun elabHead (env, denv) infer (e as (_, loc)) t = adamc@403: let adamc@403: fun unravel (t, e) = adamc@403: let adamc@403: val (t, gs) = hnormCon (env, denv) t adamc@403: in adamc@403: case t of adamc@403: (L'.TCFun (L'.Implicit, x, k, t'), _) => adamc@403: let adamc@403: val u = cunif (loc, k) adamc@403: adamc@403: val t'' = subConInCon (0, u) t' adamc@403: val (e, t, gs') = unravel (t'', (L'.ECApp (e, u), loc)) adamc@403: in adamc@403: (*prefaces "Unravel" [("t'", p_con env t'), adamc@403: ("t''", p_con env t'')];*) adamc@403: (e, t, enD gs @ gs') adamc@403: end adamc@403: | (L'.TFun (dom as (L'.CApp (cl, _), _), ran), _) => adamc@403: let adamc@403: val cl = #1 (hnormCon (env, denv) cl) adamc@403: in adamc@403: if infer <> L.TypesOnly andalso E.isClass env cl then adamc@403: let adamc@403: val r = ref NONE adamc@403: val (e, t, gs') = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) adamc@403: in adamc@403: (e, t, TypeClass (env, dom, r, loc) :: enD gs @ gs') adamc@403: end adamc@403: else adamc@403: (e, t, enD gs) adamc@403: end adamc@228: | _ => (e, t, enD gs) adamc@86: end 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@174: fun elabPat (pAll as (p, loc), (env, denv, bound)) = adamc@171: let adamc@171: val perror = (L'.PWild, loc) adamc@171: val terror = (L'.CError, loc) adamc@171: val pterror = (perror, terror) adamc@171: val rerror = (pterror, (env, bound)) adamc@171: adamc@191: fun pcon (pc, po, xs, to, dn, dk) = adamc@188: case (po, to) of adamc@188: (NONE, SOME _) => (expError env (PatHasNoArg loc); adamc@188: rerror) adamc@188: | (SOME _, NONE) => (expError env (PatHasArg loc); adamc@188: rerror) adamc@191: | (NONE, NONE) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val unifs = map (fn _ => cunif (loc, k)) xs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@191: in adamc@191: (((L'.PCon (dk, pc, unifs, NONE), loc), dn), adamc@191: (env, bound)) adamc@191: end adamc@188: | (SOME p, SOME t) => adamc@188: let adamc@188: val ((p', pt), (env, bound)) = elabPat (p, (env, denv, bound)) adamc@191: adamc@191: val k = (L'.KType, loc) adamc@191: val unifs = map (fn _ => cunif (loc, k)) xs adamc@194: val nxs = length unifs - 1 adamc@194: val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@188: in adamc@191: ignore (checkPatCon (env, denv) p' pt t); adamc@191: (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), adamc@188: (env, bound)) adamc@188: end adamc@171: in adamc@171: case p of adamc@171: L.PWild => (((L'.PWild, loc), cunif (loc, (L'.KType, loc))), adamc@171: (env, bound)) adamc@171: | L.PVar x => adamc@171: let adamc@171: val t = if SS.member (bound, x) then adamc@171: (expError env (DuplicatePatternVariable (loc, x)); adamc@171: terror) adamc@171: else adamc@171: cunif (loc, (L'.KType, loc)) adamc@171: in adamc@182: (((L'.PVar (x, t), loc), t), adamc@171: (E.pushERel env x t, SS.add (bound, x))) adamc@171: end adamc@173: | L.PPrim p => (((L'.PPrim p, loc), primType env p), adamc@173: (env, bound)) adamc@171: | L.PCon ([], x, po) => adamc@171: (case E.lookupConstructor env x of adamc@174: NONE => (expError env (UnboundConstructor (loc, [], x)); adamc@171: rerror) adamc@191: | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk)) adamc@174: | L.PCon (m1 :: ms, x, po) => adamc@174: (case E.lookupStr env m1 of adamc@174: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@174: rerror) adamc@174: | SOME (n, sgn) => adamc@174: let adamc@174: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@174: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@182: NONE => raise Fail "elabPat: Unknown substructure" adamc@174: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@174: ((L'.StrVar n, loc), sgn) ms adamc@174: in adamc@174: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@174: NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); adamc@174: rerror) adamc@191: | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk) adamc@174: end) adamc@174: adamc@175: | L.PRecord (xps, flex) => adamc@175: let adamc@175: val (xpts, (env, bound, _)) = adamc@175: ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) => adamc@175: let adamc@175: val ((p', t), (env, bound)) = elabPat (p, (env, denv, bound)) adamc@175: in adamc@175: if SS.member (fbound, x) then adamc@175: expError env (DuplicatePatField (loc, x)) adamc@175: else adamc@175: (); adamc@175: ((x, p', t), (env, bound, SS.add (fbound, x))) adamc@175: end) adamc@175: (env, bound, SS.empty) xps adamc@175: adamc@175: val k = (L'.KType, loc) adamc@175: val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc) adamc@176: val c = adamc@175: if flex then adamc@176: (L'.CConcat (c, cunif (loc, (L'.KRecord k, loc))), loc) adamc@175: else adamc@176: c adamc@175: in adamc@182: (((L'.PRecord xpts, loc), adamc@175: (L'.TRecord c, loc)), adamc@175: (env, bound)) adamc@175: end adamc@175: adamc@171: end adamc@171: adamc@172: datatype coverage = adamc@172: Wild adamc@173: | None adamc@172: | Datatype of coverage IM.map adamc@175: | Record of coverage SM.map list adamc@172: adamc@243: fun c2s c = adamc@243: case c of adamc@243: Wild => "Wild" adamc@243: | None => "None" adamc@243: | Datatype _ => "Datatype" adamc@243: | Record _ => "Record" adamc@243: adamc@172: fun exhaustive (env, denv, t, ps) = adamc@172: let adamc@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@402: case #1 (#1 (hnormCon (env, denv) 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@402: (case #1 (#1 (hnormCon (env, denv) c)) of adamc@402: L'.CRecord (_, xts) => adamc@402: let adamc@402: val xts = map (fn (x, t) => (#1 (hnormCon (env, denv) 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@173: None => (false, []) adamc@173: | Wild => (true, []) adamc@172: | Datatype cm => adamc@172: let adamc@172: val ((t, _), gs) = hnormCon (env, denv) t adamc@174: adamc@174: fun dtype cons = adamc@174: foldl (fn ((_, n, to), (total, gs)) => adamc@174: case IM.find (cm, n) of adamc@174: NONE => (false, gs) adamc@174: | SOME c' => adamc@174: case to of adamc@174: NONE => (total, gs) adamc@174: | SOME t' => adamc@174: let adamc@174: val (total, gs') = isTotal (c', t') adamc@174: in adamc@174: (total, gs' @ gs) adamc@174: end) adamc@174: (true, gs) cons adamc@191: adamc@191: fun unapp t = adamc@191: case t of adamc@191: L'.CApp ((t, _), _) => unapp t adamc@191: | _ => t adamc@172: in adamc@191: case unapp t of adamc@172: L'.CNamed n => adamc@172: let adamc@172: val dt = E.lookupDatatype env n adamc@172: val cons = E.constructors dt adamc@172: in adamc@174: dtype cons adamc@174: end adamc@174: | L'.CModProj (m1, ms, x) => adamc@174: let adamc@174: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@174: in adamc@174: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@174: NONE => raise Fail "isTotal: Can't project datatype" adamc@191: | SOME (_, cons) => dtype cons adamc@172: end adamc@172: | L'.CError => (true, gs) adamc@341: | c => adamc@341: (prefaces "Not a datatype" [("c", p_con env (c, ErrorMsg.dummySpan))]; adamc@341: raise Fail "isTotal: Not a datatype") adamc@172: end adamc@402: | 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@467: val c = ElabOps.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@447: adamc@447: val makeInstantiable = adamc@447: let adamc@447: fun kind k = k adamc@447: fun con c = adamc@447: case c of adamc@447: L'.CDisjoint (L'.LeaveAlone, c1, c2, c) => L'.CDisjoint (L'.Instantiate, c1, c2, c) adamc@447: | _ => c adamc@447: in adamc@447: U.Con.map {kind = kind, con = con} adamc@447: end adamc@447: 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: val gs3 = checkCon (env, denv) e' et t' adamc@91: in adamc@228: (e', t', gs1 @ enD gs2 @ enD gs3) adamc@91: end adamc@34: adamc@91: | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) adamc@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@403: | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t adamc@403: | 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@403: 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: adamc@403: val gs3 = checkCon (env, denv) e1' t1 t adamc@403: val gs4 = checkCon (env, denv) e2' t2 dom adamc@403: adamc@403: val gs = gs1 @ gs2 @ enD gs3 @ enD gs4 adamc@91: in adamc@205: ((L'.EApp (e1', e2'), loc), ran, gs) adamc@91: end adamc@91: | L.EAbs (x, to, e) => adamc@91: let adamc@91: val (t', gs1) = case to of adamc@91: NONE => (cunif (loc, ktype), []) adamc@91: | SOME t => adamc@91: let adamc@91: val (t', tk, gs) = elabCon (env, denv) t adamc@91: in adamc@91: checkKind env t' tk ktype; adamc@91: (t', gs) adamc@91: end adamc@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@403: val ((et', _), gs3) = hnormCon (env, denv) et adamc@91: in adamc@91: case et' of adamc@91: L'.CError => (eerror, cerror, []) adamc@328: | L'.TCFun (_, x, k, eb) => adamc@91: let adamc@91: val () = checkKind env c' ck k adamc@91: val eb' = subConInCon (0, c') eb adamc@339: handle SynUnif => (expError env (Unif ("substitution", loc, eb)); adamc@91: cerror) adamc@91: in adamc@328: (*prefaces "Elab ECApp" [("e", SourcePrint.p_exp eAll), adamc@328: ("et", p_con env oldEt), adamc@328: ("x", PD.string x), adamc@328: ("eb", p_con (E.pushCRel env x k) eb), adamc@328: ("c", p_con env c'), adamc@328: ("eb'", p_con env eb')];*) adamc@403: ((L'.ECApp (e', c'), loc), eb', gs1 @ enD gs2 @ enD gs3) adamc@91: end adamc@91: adamc@91: | _ => adamc@91: (expError env (WrongForm ("constructor function", e', et)); adamc@91: (eerror, cerror, [])) adamc@91: end adamc@91: | L.ECAbs (expl, x, k, e) => adamc@91: let adamc@91: val expl' = elabExplicitness expl adamc@91: val k' = elabKind k adamc@328: adamc@328: val env' = E.pushCRel env x k' adamc@328: val (e', et, gs) = elabExp (env', D.enter denv) e adamc@91: in adamc@91: ((L'.ECAbs (expl', x, k', e'), loc), adamc@91: (L'.TCFun (expl', x, k', et), loc), adamc@91: gs) adamc@91: end adamc@91: adamc@91: | L.EDisjoint (c1, c2, e) => adamc@91: let adamc@91: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@91: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@91: adamc@91: val ku1 = kunif loc adamc@91: val ku2 = kunif loc adamc@91: adamc@91: val (denv', gs3) = D.assert env denv (c1', c2') adamc@91: val (e', t, gs4) = elabExp (env, denv') e adamc@91: in adamc@91: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@91: checkKind env c2' k2 (L'.KRecord ku2, loc); adamc@91: adamc@345: (e', (L'.CDisjoint (L'.LeaveAlone, c1', c2', t), loc), enD gs1 @ enD gs2 @ enD gs3 @ gs4) adamc@91: end adamc@91: adamc@91: | L.ERecord xes => adamc@91: let adamc@91: val (xes', gs) = ListUtil.foldlMap (fn ((x, e), gs) => adamc@91: let adamc@91: val (x', xk, gs1) = elabCon (env, denv) x adamc@91: val (e', et, gs2) = elabExp (env, denv) e adamc@91: in adamc@91: checkKind env x' xk kname; adamc@228: ((x', e', et), enD gs1 @ gs2 @ gs) adamc@91: end) adamc@91: [] xes adamc@91: adamc@91: val k = (L'.KType, loc) adamc@91: adamc@91: fun prove (xets, gs) = adamc@91: case xets of adamc@91: [] => gs adamc@91: | (x, _, t) :: rest => adamc@91: let adamc@91: val xc = (x, t) adamc@91: val r1 = (L'.CRecord (k, [xc]), loc) adamc@91: val gs = foldl (fn ((x', _, t'), gs) => adamc@91: let adamc@91: val xc' = (x', t') adamc@91: val r2 = (L'.CRecord (k, [xc']), loc) adamc@91: in adamc@91: D.prove env denv (r1, r2, loc) @ gs adamc@91: end) adamc@91: gs rest adamc@91: in adamc@91: prove (rest, gs) adamc@91: end adamc@228: adamc@228: val gsD = List.mapPartial (fn Disjoint d => SOME d | _ => NONE) gs adamc@228: val gsO = List.filter (fn Disjoint _ => false | _ => true) gs adamc@91: in adamc@255: (*TextIO.print ("|gsO| = " ^ Int.toString (length gsO) ^ "\n");*) adamc@91: ((L'.ERecord xes', loc), adamc@91: (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc), adamc@228: enD (prove (xes', gsD)) @ gsO) adamc@91: end adamc@91: adamc@91: | L.EField (e, c) => adamc@91: let adamc@91: val (e', et, gs1) = elabExp (env, denv) e adamc@91: val (c', ck, gs2) = elabCon (env, denv) c adamc@91: adamc@91: val ft = cunif (loc, ktype) adamc@91: val rest = cunif (loc, ktype_record) adamc@91: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@91: adamc@91: val gs3 = adamc@91: checkCon (env, denv) e' et adamc@91: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@91: val gs4 = D.prove env denv (first, rest, loc) adamc@91: in adamc@228: ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3 @ enD gs4) adamc@91: end adamc@91: adamc@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@445: val gs3 = checkCon (env, denv) e1' e1t (L'.TRecord r1, loc) adamc@445: val gs4 = checkCon (env, denv) e2' e2t (L'.TRecord r2, loc) adamc@445: val gs5 = 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@445: gs1 @ gs2 @ enD gs3 @ enD gs4 @ enD gs5) adamc@339: end adamc@149: | L.ECut (e, c) => adamc@149: let adamc@149: val (e', et, gs1) = elabExp (env, denv) e adamc@149: val (c', ck, gs2) = elabCon (env, denv) c adamc@149: adamc@149: val ft = cunif (loc, ktype) adamc@149: val rest = cunif (loc, ktype_record) adamc@149: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@149: adamc@149: val gs3 = adamc@149: checkCon (env, denv) e' et adamc@149: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@149: val gs4 = D.prove env denv (first, rest, loc) adamc@149: in adamc@228: ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), adamc@228: gs1 @ enD gs2 @ enD gs3 @ enD gs4) adamc@149: end adamc@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@493: adamc@493: val gs3 = adamc@493: checkCon (env, denv) e' et adamc@493: (L'.TRecord (L'.CConcat (c', rest), loc), loc) adamc@493: val gs4 = D.prove env denv (c', rest, loc) adamc@493: in adamc@493: ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), adamc@493: gs1 @ enD gs2 @ enD gs3 @ enD gs4) adamc@493: end adamc@149: adamc@91: | L.EFold => adamc@91: let adamc@91: val dom = kunif loc adamc@91: in adamc@91: ((L'.EFold dom, loc), foldType (dom, loc), []) adamc@91: end adamc@170: adamc@171: | L.ECase (e, pes) => adamc@171: let adamc@171: val (e', et, gs1) = elabExp (env, denv) e adamc@171: val result = cunif (loc, (L'.KType, loc)) adamc@171: val (pes', gs) = ListUtil.foldlMap adamc@171: (fn ((p, e), gs) => adamc@171: let adamc@174: val ((p', pt), (env, _)) = elabPat (p, (env, denv, SS.empty)) adamc@171: adamc@171: val gs1 = checkPatCon (env, denv) p' pt et adamc@171: val (e', et, gs2) = elabExp (env, denv) e adamc@171: val gs3 = checkCon (env, denv) e' et result adamc@171: in adamc@228: ((p', e'), enD gs1 @ gs2 @ enD gs3 @ gs) adamc@171: end) adamc@171: gs1 pes adamc@172: adamc@172: val (total, gs') = exhaustive (env, denv, et, map #1 pes') adamc@171: in adamc@172: if total then adamc@172: () adamc@172: else adamc@172: expError env (Inexhaustive loc); adamc@172: adamc@228: ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, enD gs' @ gs) adamc@171: end adamc@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@447: and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = 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@447: val gs3 = checkCon (env, denv) e' et c' adamc@467: val c' = normClassConstraint env c' adamc@447: val env' = E.pushERel env x c' adamc@447: val c' = makeInstantiable c' adamc@447: in adamc@467: ((L'.EDVal (x, c', e'), loc), (env', enD gs1 @ gs2 @ enD gs3 @ 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@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: adamc@447: val gs2 = checkCon (env, denv) e' et c' adamc@447: adamc@447: val c' = makeInstantiable c' adamc@447: in adamc@447: if allowable e then adamc@447: () adamc@447: else adamc@447: expError env (IllegalRec (x, e')); adamc@447: ((x, c', e'), gs1 @ enD gs2 @ 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: adamc@469: val denv = case cso of adamc@469: NONE => (strError env (UnboundStr (loc, str)); adamc@469: denv) adamc@469: | SOME cs => foldl (fn ((c1, c2), denv) => adamc@469: let adamc@469: val (denv, gs) = D.assert env denv (c1, c2) adamc@469: in adamc@469: case gs of adamc@469: [] => () adamc@469: | _ => raise Fail "dopenConstraints: Sub-constraints remain"; adamc@469: adamc@469: denv adamc@469: end) denv cs adamc@469: in adamc@469: denv 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@76: val k' = elabKind k adamc@31: adamc@76: val (env', n) = E.pushCNamed env x k' NONE adamc@76: in adamc@88: ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) adamc@76: end adamc@31: adamc@76: | L.SgiCon (x, ko, c) => adamc@76: let adamc@76: val k' = case ko of adamc@76: NONE => kunif loc adamc@76: | SOME k => elabKind k adamc@31: adamc@83: val (c', ck, gs') = elabCon (env, denv) c adamc@76: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@76: in adamc@76: checkKind env c' ck k'; adamc@31: adamc@88: ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) adamc@76: end adamc@31: adamc@191: | L.SgiDatatype (x, xs, xcs) => adamc@157: let adamc@157: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: val (env, n) = E.pushCNamed env x k' NONE adamc@157: val t = (L'.CNamed n, loc) adamc@194: val nxs = length xs - 1 adamc@194: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@157: adamc@284: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@284: (E.pushCRel env' x k, adamc@284: D.enter denv')) (env, denv) xs adamc@284: adamc@157: val (xcs, (used, env, gs)) = adamc@157: ListUtil.foldlMap adamc@157: (fn ((x, to), (used, env, gs)) => adamc@157: let adamc@157: val (to, t, gs') = case to of adamc@157: NONE => (NONE, t, gs) adamc@157: | SOME t' => adamc@157: let adamc@284: val (t', tk, gs') = elabCon (env', denv') t' adamc@157: in adamc@284: checkKind env' t' tk k; adamc@157: (SOME t', (L'.TFun (t', t), loc), gs' @ gs) adamc@157: end adamc@191: val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@157: adamc@157: val (env, n') = E.pushENamed env x t adamc@157: in adamc@157: if SS.member (used, x) then adamc@157: strError env (DuplicateConstructor (x, loc)) adamc@157: else adamc@157: (); adamc@157: ((x, n', to), (SS.add (used, x), env, gs')) adamc@157: end) adamc@157: (SS.empty, env, []) xcs adamc@191: adamc@191: val env = E.pushDatatype env n xs xcs adamc@157: in adamc@191: ([(L'.SgiDatatype (x, n, xs, xcs), loc)], (env, denv, gs)) adamc@157: end adamc@156: adamc@158: | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" adamc@158: adamc@158: | L.SgiDatatypeImp (x, m1 :: ms, s) => adamc@158: (case E.lookupStr env m1 of adamc@158: NONE => (strError env (UnboundStr (loc, m1)); adamc@158: ([], (env, denv, gs))) adamc@158: | SOME (n, sgn) => adamc@158: let adamc@158: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@158: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@158: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@158: (strerror, sgnerror)) adamc@158: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@158: ((L'.StrVar n, loc), sgn) ms adamc@158: in adamc@161: case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of adamc@161: ((L'.CModProj (n, ms, s), _), gs) => adamc@161: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@161: NONE => (conError env (UnboundDatatype (loc, s)); adamc@161: ([], (env, denv, gs))) adamc@191: | SOME (xs, xncs) => adamc@161: let adamc@161: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: adamc@161: val t = (L'.CModProj (n, ms, s), loc) adamc@191: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@191: val env = E.pushDatatype env n' xs xncs adamc@158: adamc@161: val t = (L'.CNamed n', loc) adamc@161: val env = foldl (fn ((x, n, to), env) => adamc@161: let adamc@161: val t = case to of adamc@161: NONE => t adamc@161: | SOME t' => (L'.TFun (t', t), loc) adamc@191: adamc@191: val t = foldr (fn (x, t) => adamc@191: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@191: t xs adamc@161: in adamc@161: E.pushENamedAs env x n t adamc@161: end) env xncs adamc@161: in adamc@191: ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) adamc@161: end) adamc@161: | _ => (strError env (NotDatatype loc); adamc@161: ([], (env, denv, []))) adamc@158: end) adamc@156: adamc@76: | L.SgiVal (x, c) => adamc@76: let adamc@83: val (c', ck, gs') = elabCon (env, denv) c adamc@31: adamc@76: val (env', n) = E.pushENamed env x c' adamc@467: val c' = normClassConstraint env c' adamc@76: in adamc@76: (unifyKinds 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@90: val (denv, gs3) = D.assert env denv (c1', c2') adamc@88: in adamc@88: checkKind env c1' k1 (L'.KRecord (kunif loc), loc); adamc@88: checkKind env c2' k2 (L'.KRecord (kunif loc), loc); adamc@88: adamc@90: ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2 @ gs3)) adamc@76: end adamc@31: adamc@211: | L.SgiClassAbs x => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val (env, n) = E.pushCNamed env x k NONE adamc@211: val env = E.pushClass env n adamc@211: in adamc@211: ([(L'.SgiClassAbs (x, n), loc)], (env, denv, [])) adamc@211: end adamc@211: adamc@211: | L.SgiClass (x, c) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val (c', ck, gs) = elabCon (env, denv) c adamc@211: val (env, n) = E.pushCNamed env x k (SOME c') adamc@211: val env = E.pushClass env n adamc@211: in adamc@211: checkKind env c' ck k; adamc@211: ([(L'.SgiClass (x, n, c'), loc)], (env, denv, [])) adamc@211: end adamc@211: adamc@83: and elabSgn (env, denv) (sgn, loc) = adamc@31: case sgn of adamc@31: L.SgnConst sgis => adamc@31: let adamc@88: val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis adamc@62: adamc@62: val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => adamc@62: case sgi of adamc@62: L'.SgiConAbs (x, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiCon (x, _, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@191: | L'.SgiDatatype (x, _, _, xncs) => adamc@156: let adamc@156: val vals = foldl (fn ((x, _, _), vals) => adamc@156: (if SS.member (vals, x) then adamc@156: sgnError env (DuplicateVal (loc, x)) adamc@156: else adamc@156: (); adamc@156: SS.add (vals, x))) adamc@156: vals xncs adamc@156: in adamc@156: if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => adamc@156: (if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiVal (x, _, _) => adamc@62: (if SS.member (vals, x) then adamc@62: sgnError env (DuplicateVal (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, SS.add (vals, x), sgns, strs)) adamc@62: | L'.SgiSgn (x, _, _) => adamc@62: (if SS.member (sgns, x) then adamc@62: sgnError env (DuplicateSgn (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, vals, SS.add (sgns, x), strs)) adamc@62: | L'.SgiStr (x, _, _) => adamc@62: (if SS.member (strs, x) then adamc@62: sgnError env (DuplicateStr (loc, x)) adamc@62: else adamc@62: (); adamc@88: (cons, vals, sgns, SS.add (strs, x))) adamc@203: | L'.SgiConstraint _ => (cons, vals, sgns, strs) adamc@211: | L'.SgiClassAbs (x, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@211: (SS.add (cons, x), vals, sgns, strs)) adamc@211: | L'.SgiClass (x, _, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@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@75: (unifyKinds k ck adamc@75: handle KUnify x => sgnError env (WhereWrongKind x); adamc@42: true) adamc@42: | _ => false) sgis then adamc@83: ((L'.SgnWhere (sgn', x, c'), loc), ds1 @ ds2) adamc@42: else adamc@42: (sgnError env (UnWhereable (sgn', x)); adamc@83: (sgnerror, [])) adamc@42: | _ => (sgnError env (UnWhereable (sgn', x)); adamc@83: (sgnerror, [])) adamc@42: end adamc@59: | L.SgnProj (m, ms, x) => adamc@59: (case E.lookupStr env m of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@83: (sgnerror, [])) adamc@59: | SOME (n, sgn) => adamc@59: let adamc@59: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@59: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@59: (strerror, sgnerror)) adamc@59: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@59: ((L'.StrVar n, loc), sgn) ms adamc@59: in adamc@59: case E.projectSgn env {sgn = sgn, str = str, field = x} of adamc@59: NONE => (sgnError env (UnboundSgn (loc, x)); adamc@83: (sgnerror, [])) adamc@83: | SOME _ => ((L'.SgnProj (n, ms, x), loc), []) adamc@59: end) adamc@59: adamc@31: adamc@66: fun selfify env {str, strs, sgn} = adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnError => sgn adamc@66: | L'.SgnVar _ => sgn adamc@66: adamc@66: | L'.SgnConst sgis => adamc@66: (L'.SgnConst (map (fn (L'.SgiConAbs (x, n, k), loc) => adamc@66: (L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | (L'.SgiDatatype (x, n, xs, xncs), loc) => adamc@191: (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@218: | (L'.SgiClassAbs (x, n), loc) => adamc@218: (L'.SgiClass (x, n, (L'.CModProj (str, strs, x), loc)), loc) adamc@66: | (L'.SgiStr (x, n, sgn), loc) => adamc@66: (L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc) adamc@66: | x => x) sgis), #2 sgn) adamc@66: | L'.SgnFun _ => sgn adamc@66: | L'.SgnWhere _ => sgn adamc@66: | L'.SgnProj (m, ms, x) => adamc@66: case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar m, #2 sgn) ms, adamc@66: sgn = #2 (E.lookupStrNamed env m), adamc@66: field = x} of adamc@66: NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" adamc@66: | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} adamc@66: adamc@66: fun selfifyAt env {str, sgn} = adamc@66: let adamc@66: fun self (str, _) = adamc@66: case str of adamc@66: L'.StrVar x => SOME (x, []) adamc@66: | L'.StrProj (str, x) => adamc@66: (case self str of adamc@66: NONE => NONE adamc@66: | SOME (m, ms) => SOME (m, ms @ [x])) adamc@66: | _ => NONE adamc@66: in adamc@66: case self str of adamc@66: NONE => sgn adamc@66: | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} adamc@66: end adamc@66: adamc@88: fun dopen (env, denv) {str, strs, sgn} = adamc@66: let adamc@66: val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar str, #2 sgn) strs adamc@66: in adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnConst sgis => adamc@88: ListUtil.foldlMap (fn ((sgi, loc), (env', denv')) => adamc@162: let adamc@162: val d = adamc@162: case sgi of adamc@162: L'.SgiConAbs (x, n, k) => adamc@162: let adamc@162: val c = (L'.CModProj (str, strs, x), loc) adamc@162: in adamc@162: (L'.DCon (x, n, k, c), loc) adamc@162: end adamc@162: | L'.SgiCon (x, n, k, c) => adamc@162: (L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc) adamc@191: | L'.SgiDatatype (x, n, xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@191: (L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) adamc@162: | L'.SgiVal (x, n, t) => adamc@162: (L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiStr (x, n, sgn) => adamc@162: (L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc) adamc@162: | L'.SgiSgn (x, n, sgn) => adamc@162: (L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc) adamc@162: | L'.SgiConstraint (c1, c2) => adamc@162: (L'.DConstraint (c1, c2), loc) adamc@211: | L'.SgiClassAbs (x, n) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@211: (L'.DCon (x, n, k, c), loc) adamc@211: end adamc@211: | L'.SgiClass (x, n, _) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val c = (L'.CModProj (str, strs, x), loc) adamc@211: in adamc@211: (L'.DCon (x, n, k, c), loc) adamc@211: end adamc@162: in adamc@162: (d, (E.declBinds env' d, denv')) adamc@162: end) adamc@88: (env, denv) sgis adamc@66: | _ => (strError env (UnOpenable sgn); adamc@88: ([], (env, denv))) adamc@66: end adamc@66: adamc@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@213: | L'.DClass (x, n, c) => [(L'.SgiClass (x, n, 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@88: fun sgiBindsD (env, denv) (sgi, _) = adamc@88: case sgi of adamc@90: L'.SgiConstraint (c1, c2) => adamc@90: (case D.assert env denv (c1, c2) of adamc@90: (denv, []) => denv adamc@90: | _ => raise Fail "sgiBindsD: Sub-constraints remain") adamc@88: | _ => denv adamc@31: adamc@86: fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = adamc@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@156: fun folder (sgi2All as (sgi, loc), (env, denv)) = 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@88: fun seek (env, denv) ls = adamc@31: case ls of adamc@31: [] => (sgnError env (UnmatchedSgi sgi2All); adamc@88: (env, denv)) adamc@31: | h :: t => adamc@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@469: seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t adamc@469: end adamc@88: | SOME envs => envs adamc@31: in adamc@88: seek (env, denv) sgis1 adamc@31: end adamc@31: in adamc@31: case sgi of adamc@31: L'.SgiConAbs (x, n2, k2) => adamc@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@41: val () = unifyKinds k1 k2 adamc@41: handle KUnify (k1, k2, err) => adamc@41: sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) adamc@41: val env = E.pushCNamedAs env x n1 k1 co1 adamc@41: in adamc@41: SOME (if n1 = n2 then adamc@41: env adamc@41: else adamc@88: E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)), adamc@88: denv) adamc@41: end adamc@41: else adamc@41: NONE adamc@31: in adamc@31: case sgi1 of adamc@41: L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) adamc@41: | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) adamc@191: | L'.SgiDatatype (x', n1, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', NONE) adamc@191: end adamc@191: | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) adamc@191: end adamc@211: | L'.SgiClassAbs (x', n1) => found (x', n1, adamc@218: (L'.KArrow ((L'.KType, loc), adamc@218: (L'.KType, loc)), loc), adamc@218: NONE) adamc@211: | L'.SgiClass (x', n1, c) => found (x', n1, adamc@211: (L'.KArrow ((L'.KType, loc), adamc@211: (L'.KType, loc)), loc), adamc@211: SOME c) adamc@31: | _ => NONE adamc@31: end) adamc@31: adamc@31: | L'.SgiCon (x, n2, k2, c2) => adamc@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@327: SOME (env, denv) adamc@327: end adamc@211: in adamc@211: (case unifyCons (env, denv) c1 c2 of adamc@211: [] => good () adamc@211: | _ => NONE) adamc@211: handle CUnify (c1, c2, err) => adamc@211: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | L'.SgiClass (x', n1, c1) => adamc@211: found (x', n1, (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc), c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: adamc@191: | L'.SgiDatatype (x, n2, xs2, xncs2) => adamc@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@160: SOME (env, denv)) adamc@156: adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 adamc@191: adamc@160: fun good () = adamc@160: let adamc@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@160: SOME (env, denv) 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@160: not (List.null (unifyCons (env, denv) t1 t2)) adamc@160: | _ => true adamc@160: in adamc@191: (if xs1 <> xs2 adamc@191: orelse length xncs1 <> length xncs2 adamc@160: orelse ListPair.exists xncBad (xncs1, xncs2) then adamc@160: mismatched NONE adamc@160: else adamc@160: good ()) adamc@160: handle CUnify ue => mismatched (SOME ue) adamc@160: end adamc@160: in adamc@160: case sgi1 of adamc@191: L'.SgiDatatype (x', n1, xs, xncs1) => adamc@160: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@160: else adamc@160: NONE adamc@191: | L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => adamc@162: if x' = x then adamc@191: found (n1, xs, xncs1) adamc@162: else adamc@162: NONE adamc@160: | _ => NONE adamc@160: end) adamc@156: adamc@191: | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => adamc@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@158: SOME (env, denv) adamc@158: end adamc@158: in adamc@158: (case unifyCons (env, denv) t1 t2 of adamc@158: [] => good () adamc@158: | _ => NONE) adamc@158: handle CUnify (c1, c2, err) => adamc@158: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@158: good ()) adamc@158: end adamc@158: else adamc@158: NONE adamc@158: adamc@158: | _ => NONE) adamc@156: adamc@32: | L'.SgiVal (x, n2, c2) => adamc@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@362: ((*prefaces "Pre" [("c1", p_con env c1), adamc@362: ("c2", p_con env c2)];*) adamc@362: case unifyCons (env, denv) c1 c2 of adamc@88: [] => SOME (env, denv) adamc@86: | _ => NONE) adamc@86: handle CUnify (c1, c2, err) => adamc@86: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@88: SOME (env, denv)) adamc@41: else adamc@41: NONE adamc@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@86: val () = subSgn (env, denv) sgn1 sgn2 adamc@66: val env = E.pushStrNamedAs env x n1 sgn1 adamc@66: val env = if n1 = n2 then adamc@66: env adamc@66: else adamc@66: E.pushStrNamedAs env x n2 adamc@66: (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), adamc@66: sgn = sgn2}) adamc@66: in adamc@88: SOME (env, denv) adamc@66: end adamc@41: else adamc@41: NONE adamc@33: | _ => NONE) adamc@59: adamc@59: | L'.SgiSgn (x, n2, sgn2) => adamc@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@86: val () = subSgn (env, denv) sgn1 sgn2 adamc@86: val () = subSgn (env, denv) sgn2 sgn1 adamc@65: adamc@65: val env = E.pushSgnNamedAs env x n2 sgn2 adamc@65: val env = if n1 = n2 then adamc@65: env adamc@65: else adamc@65: E.pushSgnNamedAs env x n1 sgn2 adamc@65: in adamc@88: SOME (env, denv) adamc@65: end adamc@59: else adamc@59: NONE adamc@59: | _ => NONE) adamc@88: adamc@88: | L'.SgiConstraint (c2, d2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@88: case sgi1 of adamc@88: L'.SgiConstraint (c1, d1) => adamc@88: if consEq (env, denv) (c1, c2) andalso consEq (env, denv) (d1, d2) then adamc@90: let adamc@90: val (denv, gs) = D.assert env denv (c2, d2) adamc@90: in adamc@90: case gs of adamc@90: [] => () adamc@90: | _ => raise Fail "subSgn: Sub-constraints remain"; adamc@90: adamc@90: SOME (env, denv) adamc@90: end adamc@88: else adamc@88: NONE adamc@88: | _ => NONE) adamc@203: adamc@211: | L'.SgiClassAbs (x, n2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@211: let adamc@211: fun found (x', n1, co) = adamc@211: if x = x' then adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: val env = E.pushCNamedAs env x n1 k co adamc@211: in adamc@211: SOME (if n1 = n2 then adamc@211: env adamc@211: else adamc@211: E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2)), adamc@211: denv) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiClassAbs (x', n1) => found (x', n1, NONE) adamc@211: | L'.SgiClass (x', n1, c) => found (x', n1, SOME c) adamc@211: | _ => NONE adamc@211: end) adamc@211: | L'.SgiClass (x, n2, c2) => adamc@469: seek (fn (env, sgi1All as (sgi1, _)) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: fun found (x', n1, c1) = adamc@211: if x = x' then adamc@211: let adamc@218: fun good () = adamc@218: let adamc@218: val env = E.pushCNamedAs env x n2 k (SOME c2) adamc@218: val env = if n1 = n2 then adamc@218: env adamc@218: else adamc@218: E.pushCNamedAs env x n1 k (SOME c1) adamc@218: in adamc@218: SOME (env, denv) adamc@218: end adamc@211: in adamc@211: (case unifyCons (env, denv) c1 c2 of adamc@211: [] => good () adamc@211: | _ => NONE) adamc@211: handle CUnify (c1, c2, err) => adamc@211: (sgnError env (SgiWrongCon (sgi1All, c1, sgi2All, c2, err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiClass (x', n1, c1) => found (x', n1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: end adamc@31: in adamc@88: ignore (foldl folder (env, denv) sgis2) adamc@31: end adamc@31: adamc@41: | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => adamc@43: let adamc@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@86: subSgn (env, denv) dom2 dom1; adamc@480: subSgn (E.pushStrNamedAs env m1 n1 dom2, denv) 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@312: | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs adamc@312: | CConcat (c1, c2) => none c1 andalso none c2 adamc@312: | CFold => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all none cs adamc@312: | CProj (c, _) => none c adamc@312: adamc@312: | CWild _ => false adamc@312: adamc@312: fun pos (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => pos c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso pos c2 adamc@312: | TCFun (_, _, _, c) => pos c adamc@312: | TRecord c => pos c adamc@312: adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => pos c1 andalso none c2 adamc@312: | CAbs _ => false adamc@312: | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs adamc@312: | CConcat (c1, c2) => pos c1 andalso pos c2 adamc@312: | CFold => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all pos cs adamc@312: | CProj (c, _) => pos c adamc@312: adamc@312: | CWild _ => false adamc@312: in adamc@312: pos adamc@312: end adamc@312: adamc@325: fun wildifyStr env (str, sgn) = adamc@325: case #1 (hnormSgn env sgn) of adamc@325: L'.SgnConst sgis => adamc@325: (case #1 str of adamc@325: L.StrConst ds => adamc@325: let adamc@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@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@469: if E.isClass env' f then adamc@469: (neededC, constraints, SS.add (neededV, x)) adamc@469: else adamc@469: default () adamc@469: 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@469: val (neededC, neededV) = foldl (fn ((d, _), needed as (neededC, neededV)) => adamc@469: case d of adamc@493: L.DCon (x, _, _) => ((#1 (SM.remove (neededC, x)), neededV) adamc@469: handle NotFound => adamc@469: needed) adamc@493: | L.DClass (x, _) => ((#1 (SM.remove (neededC, x)), neededV) adamc@469: handle NotFound => needed) adamc@469: | L.DVal (x, _, _) => ((neededC, SS.delete (neededV, x)) adamc@469: handle NotFound => needed) adamc@493: | L.DOpen _ => (SM.empty, SS.empty) adamc@469: | _ => needed) adamc@469: (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@280: fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = adamc@255: let adamc@255: (*val () = preface ("elabDecl", SourcePrint.p_decl (d, loc))*) adamc@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@255: | SOME k => elabKind k adamc@255: adamc@255: val (c', ck, gs') = elabCon (env, denv) c adamc@255: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@255: in adamc@255: checkKind env c' ck k'; adamc@255: adamc@255: ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: | L.DDatatype (x, xs, xcs) => adamc@255: let adamc@312: val positive = List.all (fn (_, to) => adamc@312: case to of adamc@312: NONE => true adamc@312: | SOME t => positive x t) xcs adamc@312: adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val (env, n) = E.pushCNamed env x k' NONE adamc@255: val t = (L'.CNamed n, loc) adamc@255: val nxs = length xs - 1 adamc@255: val t = ListUtil.foldli (fn (i, _, t) => (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@255: adamc@255: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@255: (E.pushCRel env' x k, adamc@255: D.enter denv')) (env, denv) xs adamc@255: adamc@255: val (xcs, (used, env, gs')) = adamc@255: ListUtil.foldlMap adamc@255: (fn ((x, to), (used, env, gs)) => adamc@255: let adamc@255: val (to, t, gs') = case to of adamc@255: NONE => (NONE, t, gs) adamc@255: | SOME t' => adamc@255: let adamc@255: val (t', tk, gs') = elabCon (env', denv') t' adamc@255: in adamc@255: checkKind env' t' tk k; adamc@255: (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) adamc@255: end adamc@255: val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@255: adamc@255: val (env, n') = E.pushENamed env x t adamc@255: in adamc@255: if SS.member (used, x) then adamc@255: strError env (DuplicateConstructor (x, loc)) adamc@255: else adamc@255: (); adamc@255: ((x, n', to), (SS.add (used, x), env, gs')) adamc@255: end) adamc@255: (SS.empty, env, []) xcs adamc@255: adamc@255: val env = E.pushDatatype env n xs xcs adamc@312: val d' = (L'.DDatatype (x, n, xs, xcs), loc) adamc@255: in adamc@312: if positive then adamc@312: () adamc@312: else adamc@312: declError env (Nonpositive d'); adamc@312: adamc@312: ([d'], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" adamc@255: adamc@255: | L.DDatatypeImp (x, m1 :: ms, s) => adamc@255: (case E.lookupStr env m1 of adamc@255: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@255: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: in adamc@255: case hnormCon (env, denv) (L'.CModProj (n, ms, s), loc) of adamc@255: ((L'.CModProj (n, ms, s), _), gs') => adamc@255: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@255: NONE => (conError env (UnboundDatatype (loc, s)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (xs, xncs) => adamc@255: let adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val t = (L'.CModProj (n, ms, s), loc) adamc@255: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@255: val env = E.pushDatatype env n' xs xncs adamc@255: adamc@255: val t = (L'.CNamed n', loc) adamc@255: val env = foldl (fn ((x, n, to), env) => adamc@255: let adamc@255: val t = case to of adamc@255: NONE => t adamc@255: | SOME t' => (L'.TFun (t', t), loc) adamc@255: adamc@255: val t = foldr (fn (x, t) => adamc@255: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@255: t xs adamc@255: in adamc@255: E.pushENamedAs env x n t adamc@255: end) env xncs adamc@255: in adamc@255: ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, enD gs' @ gs)) adamc@255: end) adamc@255: | _ => (strError env (NotDatatype loc); adamc@255: ([], (env, denv, []))) adamc@255: end) adamc@255: adamc@255: | L.DVal (x, co, e) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adamc@255: NONE => (cunif (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@255: adamc@255: val (e', et, gs2) = elabExp (env, denv) e adamc@255: val gs3 = checkCon (env, denv) e' et c' adamc@467: val c = normClassConstraint env c' adamc@255: val (env', n) = E.pushENamed env x c' adamc@334: val c' = makeInstantiable c' adamc@255: in adamc@255: (*prefaces "DVal" [("x", Print.PD.string x), adamc@362: ("c'", p_con env c')];*) adamc@467: ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ enD gs3 @ gs)) adamc@255: end adamc@255: | L.DValRec vis => adamc@255: let adamc@255: fun allowable (e, _) = adamc@255: case e of adamc@255: L.EAbs _ => true adamc@255: | L.ECAbs (_, _, _, e) => allowable e adamc@255: | L.EDisjoint (_, _, e) => allowable e adamc@255: | _ => false adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap adamc@255: (fn ((x, co, e), gs) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adamc@255: NONE => (cunif (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@255: in adamc@255: ((x, c', e), enD gs1 @ gs) adamc@280: end) gs vis adamc@255: adamc@255: val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => adamc@255: let adamc@255: val (env, n) = E.pushENamed env x c' adamc@255: in adamc@255: ((x, n, c', e), env) adamc@255: end) env vis adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => adamc@255: let adamc@255: val (e', et, gs1) = elabExp (env, denv) e adamc@255: adamc@255: val gs2 = checkCon (env, denv) e' et c' adamc@334: adamc@334: val c' = makeInstantiable c' adamc@255: in adamc@255: if allowable e then adamc@255: () adamc@255: else adamc@255: expError env (IllegalRec (x, e')); adamc@255: ((x, n, c', e'), gs1 @ enD gs2 @ gs) adamc@255: end) gs vis adamc@255: in adamc@255: ([(L'.DValRec vis, loc)], (env, denv, gs)) adamc@255: end adamc@255: adamc@255: | L.DSgn (x, sgn) => adamc@255: let adamc@255: val (sgn', gs') = elabSgn (env, denv) sgn adamc@255: val (env', n) = E.pushSgnNamed env x sgn' adamc@255: in adamc@255: ([(L'.DSgn (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DStr (x, sgno, str) => adamc@255: let adamc@255: val () = if x = "Basis" then adamc@255: raise Fail "Not allowed to redefine structure 'Basis'" adamc@255: else adamc@255: () adamc@255: adamc@255: val formal = Option.map (elabSgn (env, denv)) sgno adamc@255: adamc@255: val (str', sgn', gs') = adamc@255: case formal of adamc@255: NONE => adamc@255: let adamc@255: val (str', actual, gs') = elabStr (env, denv) str adamc@255: in adamc@255: (str', selfifyAt env {str = str', sgn = actual}, gs') adamc@255: end adamc@255: | SOME (formal, gs1) => adamc@255: let adamc@325: val str = wildifyStr env (str, formal) adamc@255: val (str', actual, gs2) = elabStr (env, denv) str adamc@255: in adamc@255: subSgn (env, denv) (selfifyAt env {str = str', sgn = actual}) formal; adamc@255: (str', formal, enD gs1 @ gs2) adamc@255: end adamc@255: adamc@255: val (env', n) = E.pushStrNamed env x sgn' adamc@255: in adamc@255: case #1 (hnormSgn env sgn') of adamc@255: L'.SgnFun _ => adamc@255: (case #1 str' of adamc@255: L'.StrFun _ => () adamc@255: | _ => strError env (FunctorRebind loc)) adamc@255: | _ => (); adamc@255: adamc@255: ([(L'.DStr (x, n, sgn', str'), loc)], (env', denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DFfiStr (x, sgn) => adamc@255: let adamc@255: val (sgn', gs') = elabSgn (env, denv) sgn adamc@255: adamc@255: val (env', n) = E.pushStrNamed env x sgn' adamc@255: in adamc@255: ([(L'.DFfiStr (x, n, sgn'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpen (m, ms) => adamc@255: (case E.lookupStr env m of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (_, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@255: NONE => (strError env (UnboundStr (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: adamc@255: val (ds, (env', denv')) = dopen (env, denv) {str = n, strs = ms, sgn = sgn} adamc@255: val denv' = dopenConstraints (loc, env', denv') {str = m, strs = ms} adamc@255: in adamc@255: (ds, (env', denv', gs)) adamc@255: end) adamc@255: adamc@255: | L.DConstraint (c1, c2) => adamc@255: let adamc@255: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@255: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@255: val gs3 = D.prove env denv (c1', c2', loc) adamc@255: adamc@255: val (denv', gs4) = D.assert env denv (c1', c2') adamc@255: in adamc@255: checkKind env c1' k1 (L'.KRecord (kunif loc), loc); adamc@255: checkKind env c2' k2 (L'.KRecord (kunif loc), loc); adamc@255: adamc@255: ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ enD gs4 @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpenConstraints (m, ms) => adamc@255: let adamc@255: val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} adamc@255: in adamc@255: ([], (env, denv, gs)) adamc@255: end adamc@255: adamc@255: | L.DExport str => adamc@255: let adamc@255: val (str', sgn, gs') = elabStr (env, denv) str adamc@255: adamc@255: val sgn = adamc@255: case #1 (hnormSgn env sgn) of adamc@255: L'.SgnConst sgis => adamc@255: let adamc@255: fun doOne (all as (sgi, _), env) = adamc@255: (case sgi of adamc@255: L'.SgiVal (x, n, t) => adamc@325: let adamc@325: fun doPage (makeRes, ran) = adamc@325: case hnormCon (env, denv) ran of adamc@325: ((L'.CApp (tf, arg), _), []) => adamc@325: (case (hnormCon (env, denv) tf, hnormCon (env, denv) arg) of adamc@325: (((L'.CModProj (basis, [], "transaction"), _), []), adamc@325: ((L'.CApp (tf, arg3), _), [])) => adamc@325: (case (basis = !basis_r, adamc@325: hnormCon (env, denv) tf, hnormCon (env, denv) arg3) of adamc@325: (true, adamc@325: ((L'.CApp (tf, arg2), _), []), adamc@325: (((L'.CRecord (_, []), _), []))) => adamc@325: (case (hnormCon (env, denv) tf) of adamc@325: ((L'.CApp (tf, arg1), _), []) => adamc@325: (case (hnormCon (env, denv) tf, adamc@325: hnormCon (env, denv) arg1, adamc@325: hnormCon (env, denv) arg2) of adamc@325: ((tf, []), (arg1, []), adamc@325: ((L'.CRecord (_, []), _), [])) => adamc@325: let adamc@325: val t = (L'.CApp (tf, arg1), loc) adamc@325: val t = (L'.CApp (t, arg2), loc) adamc@325: val t = (L'.CApp (t, arg3), loc) adamc@325: val t = (L'.CApp ( adamc@325: (L'.CModProj adamc@325: (basis, [], "transaction"), loc), adamc@325: t), loc) adamc@325: in adamc@325: (L'.SgiVal (x, n, makeRes t), loc) adamc@325: end adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all adamc@325: in adamc@325: case hnormCon (env, denv) t of adamc@325: ((L'.TFun (dom, ran), _), []) => adamc@325: (case hnormCon (env, denv) dom of adamc@325: ((L'.TRecord domR, _), []) => adamc@325: doPage (fn t => (L'.TFun ((L'.TRecord domR, adamc@325: loc), adamc@325: t), loc), ran) adamc@325: | _ => all) adamc@325: | _ => doPage (fn t => t, t) adamc@325: end adamc@255: | _ => all, adamc@255: E.sgiBinds env all) adamc@255: in adamc@255: (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) adamc@255: end adamc@255: | _ => sgn adamc@255: in adamc@255: ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DTable (x, c) => adamc@255: let adamc@255: val (c', k, gs') = elabCon (env, denv) c adamc@255: val (env, n) = E.pushENamed env x (L'.CApp (tableOf (), c'), loc) adamc@255: in adamc@255: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@255: ([(L'.DTable (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@255: end adamc@338: | L.DSequence x => adamc@338: let adamc@338: val (env, n) = E.pushENamed env x (sequenceOf ()) adamc@338: in adamc@338: ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) adamc@338: end adamc@255: adamc@255: | L.DClass (x, c) => adamc@255: let adamc@255: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@280: val (c', ck, gs') = elabCon (env, denv) c adamc@255: val (env, n) = E.pushCNamed env x k (SOME c') adamc@255: val env = E.pushClass env n adamc@255: in adamc@255: checkKind env c' ck k; adamc@280: ([(L'.DClass (x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@255: end adamc@271: adamc@280: | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) adamc@280: adamc@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@211: | L'.SgiClassAbs (x, n) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@211: ((L'.SgiClassAbs (x, n), loc) :: sgis, cons, vals, sgns, strs) adamc@211: end adamc@211: | L'.SgiClass (x, n, c) => adamc@211: let adamc@211: val k = (L'.KArrow ((L'.KType, loc), (L'.KType, loc)), loc) adamc@211: adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@211: ((L'.SgiClass (x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@203: end) adamc@64: adamc@63: ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis adamc@31: in adamc@83: ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) adamc@31: end adamc@31: | L.StrVar x => adamc@31: (case E.lookupStr env x of adamc@31: NONE => adamc@31: (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, [])) adamc@34: | L.StrProj (str, x) => adamc@34: let adamc@83: val (str', sgn, gs) = elabStr (env, denv) str adamc@34: in adamc@34: case E.projectStr env {str = str', sgn = sgn, field = x} of adamc@34: NONE => (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs) adamc@34: end adamc@41: | L.StrFun (m, dom, ranO, str) => adamc@41: let adamc@83: val (dom', gs1) = elabSgn (env, denv) dom adamc@41: val (env', n) = E.pushStrNamed env m dom' adamc@83: val (str', actual, gs2) = elabStr (env', denv) str adamc@41: adamc@83: val (formal, gs3) = adamc@41: case ranO of adamc@83: NONE => (actual, []) adamc@41: | SOME ran => adamc@41: let adamc@83: val (ran', gs) = elabSgn (env', denv) ran adamc@41: in adamc@86: subSgn (env', denv) actual ran'; adamc@83: (ran', gs) adamc@41: end adamc@41: in adamc@41: ((L'.StrFun (m, n, dom', formal, str'), loc), adamc@83: (L'.SgnFun (m, n, dom', formal), loc), adamc@228: enD gs1 @ gs2 @ enD gs3) adamc@41: end adamc@44: | L.StrApp (str1, str2) => adamc@44: let adamc@83: val (str1', sgn1, gs1) = elabStr (env, denv) str1 adamc@325: val str2 = adamc@325: case sgn1 of adamc@325: (L'.SgnFun (_, _, dom, _), _) => adamc@325: wildifyStr env (str2, dom) adamc@325: | _ => str2 adamc@83: val (str2', sgn2, gs2) = elabStr (env, denv) str2 adamc@44: in adamc@44: case #1 (hnormSgn env sgn1) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnFun (m, n, dom, ran) => adamc@86: (subSgn (env, denv) sgn2 dom; adamc@44: case #1 (hnormSgn env ran) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnConst sgis => adamc@44: ((L'.StrApp (str1', str2'), loc), adamc@83: (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), adamc@83: gs1 @ gs2) adamc@44: | _ => raise Fail "Unable to hnormSgn in functor application") adamc@44: | _ => (strError env (NotFunctor sgn1); adamc@83: (strerror, sgnerror, [])) adamc@44: end adamc@31: adamc@325: fun elabFile basis topStr topSgn env file = adamc@56: let adamc@83: val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) adamc@83: val () = case gs of adamc@83: [] => () adamc@207: | _ => (app (fn (_, env, _, c1, c2) => adamc@207: prefaces "Unresolved" adamc@207: [("c1", p_con env c1), adamc@207: ("c2", p_con env c2)]) gs; adamc@207: raise Fail "Unresolved disjointness constraints in Basis") adamc@83: adamc@56: val (env', basis_n) = E.pushStrNamed env "Basis" sgn adamc@210: val () = basis_r := basis_n adamc@56: adamc@88: val (ds, (env', _)) = dopen (env', D.empty) {str = basis_n, strs = [], sgn = sgn} adamc@56: adamc@56: fun discoverC r x = adamc@56: case E.lookupC env' x of adamc@56: E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") adamc@56: | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis") adamc@56: | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc) adamc@56: adamc@56: val () = discoverC int "int" adamc@56: val () = discoverC float "float" adamc@56: val () = discoverC string "string" adamc@203: val () = discoverC table "sql_table" adamc@56: adamc@325: val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@325: | _ => raise Fail "Unresolved disjointness constraints in top.urs" adamc@325: val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) adamc@325: val () = case gs of adamc@325: [] => () adamc@329: | _ => app (fn Disjoint (loc, env, denv, c1, c2) => adamc@329: (case D.prove env denv (c1, c2, loc) of adamc@329: [] => () adamc@329: | _ => adamc@329: (prefaces "Unresolved constraint in top.ur" adamc@329: [("loc", PD.string (ErrorMsg.spanToString loc)), adamc@329: ("c1", p_con env c1), adamc@329: ("c2", p_con env c2)]; adamc@478: raise Fail "Unresolved constraint in top.ur")) adamc@329: | TypeClass _ => raise Fail "Unresolved type class constraint in top.ur") gs adamc@325: val () = subSgn (env', D.empty) topSgn' topSgn adamc@325: adamc@325: val (env', top_n) = E.pushStrNamed env' "Top" topSgn adamc@325: adamc@325: val (ds', (env', _)) = dopen (env', D.empty) {str = top_n, strs = [], sgn = topSgn} adamc@325: adamc@83: fun elabDecl' (d, (env, gs)) = adamc@76: let adamc@76: val () = resetKunif () adamc@76: val () = resetCunif () adamc@88: val (ds, (env, _, gs)) = elabDecl (d, (env, D.empty, gs)) adamc@76: in adamc@76: if ErrorMsg.anyErrors () then adamc@76: () adamc@76: else ( adamc@76: if List.exists kunifsInDecl ds then adamc@91: declError env (KunifsRemain ds) adamc@76: else adamc@76: (); adamc@76: adamc@76: case ListUtil.search cunifsInDecl ds of adamc@76: NONE => () adamc@76: | SOME loc => adamc@91: declError env (CunifsRemain ds) adamc@76: ); adamc@76: adamc@83: (ds, (env, gs)) adamc@76: end adamc@76: adamc@83: val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file adamc@56: in adamc@84: if ErrorMsg.anyErrors () then adamc@84: () adamc@84: else adamc@228: app (fn Disjoint (loc, env, denv, c1, c2) => adamc@228: (case D.prove env denv (c1, c2, loc) of adamc@228: [] => () adamc@228: | _ => adamc@228: (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; adamc@228: eprefaces' [("Con 1", p_con env c1), adamc@228: ("Con 2", p_con env c2), adamc@228: ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), adamc@228: ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) adamc@228: | TypeClass (env, c, r, loc) => adamc@349: let adamc@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@349: | NONE => expError env (Unresolvable (loc, c)) adamc@349: end) gs; adamc@83: adamc@325: (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) adamc@325: :: ds adamc@325: @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) adamc@325: :: ds' @ file adamc@56: end adamc@2: adamc@2: end