adam@2044: (* Copyright (c) 2008-2014, 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: adam@1531: val dumpTypes = ref false adam@1745: val dumpTypesOnError = ref false adam@1723: val unifyMore = ref false adam@1733: val incremental = ref false adam@1744: val verbose = ref false adam@1531: adamc@819: structure IS = IntBinarySet adamc@403: structure IM = IntBinaryMap adamc@403: adamc@403: structure SK = struct adamc@403: type ord_key = string adamc@403: val compare = String.compare adamc@403: end adamc@403: adamc@403: structure SS = BinarySetFn(SK) adamc@403: structure SM = BinaryMapFn(SK) adamc@403: adamc@403: val basis_r = ref 0 adamc@633: val top_r = ref 0 adamc@403: adamc@403: fun elabExplicitness e = adamc@403: case e of adamc@403: L.Explicit => L'.Explicit adamc@403: | L.Implicit => L'.Implicit adamc@403: adamc@403: fun occursKind r = adamc@403: U.Kind.exists (fn L'.KUnif (_, _, r') => r = r' adamc@403: | _ => false) adamc@403: adam@1639: fun validateCon env c = adam@1639: (U.Con.appB {kind = fn env' => fn k => case k of adam@1639: L'.KRel n => ignore (E.lookupKRel env' n) adam@1639: | L'.KUnif (_, _, r as ref (L'.KUnknown f)) => adam@1639: r := L'.KUnknown (fn k => f k andalso validateKind env' k) adam@1639: | _ => (), adam@1639: con = fn env' => fn c => case c of adam@1639: L'.CRel n => ignore (E.lookupCRel env' n) adam@1639: | L'.CNamed n => ignore (E.lookupCNamed env' n) adam@1639: | L'.CModProj (n, _, _) => ignore (E.lookupStrNamed env' n) adam@1639: | L'.CUnif (_, _, _, _, r as ref (L'.Unknown f)) => adam@1639: r := L'.Unknown (fn c => f c andalso validateCon env' c) adam@1639: | _ => (), adam@1639: bind = fn (env', b) => case b of adam@1639: U.Con.RelK x => E.pushKRel env' x adam@1639: | U.Con.RelC (x, k) => E.pushCRel env' x k adam@1639: | U.Con.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co} adam@1639: env c; adam@1639: true) adam@1639: handle _ => false adam@1639: adam@1639: and validateKind env k = validateCon env (L'.CRecord (k, []), ErrorMsg.dummySpan) adam@1639: adam@1719: exception KUnify' of E.env * kunify_error adamc@403: adamc@623: fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = adamc@403: let adam@1719: fun err f = raise KUnify' (env, f (k1All, k2All)) adamc@403: in adamc@403: case (k1, k2) of adamc@403: (L'.KType, L'.KType) => () adamc@403: | (L'.KUnit, L'.KUnit) => () adamc@403: adamc@403: | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => adamc@623: (unifyKinds' env d1 d2; adamc@623: unifyKinds' env r1 r2) adamc@403: | (L'.KName, L'.KName) => () adamc@623: | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2 adamc@403: | (L'.KTuple ks1, L'.KTuple ks2) => adamc@623: ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2)) adamc@403: handle ListPair.UnequalLengths => err KIncompatible) adamc@403: adamc@623: | (L'.KRel n1, L'.KRel n2) => adamc@623: if n1 = n2 then adamc@623: () adamc@623: else adamc@623: err KIncompatible adamc@623: | (L'.KFun (x, k1), L'.KFun (_, k2)) => adamc@623: unifyKinds' (E.pushKRel env x) k1 k2 adamc@623: adamc@403: | (L'.KError, _) => () adamc@403: | (_, L'.KError) => () adamc@403: adam@1639: | (L'.KUnif (_, _, ref (L'.KKnown k1All)), _) => unifyKinds' env k1All k2All adam@1639: | (_, L'.KUnif (_, _, ref (L'.KKnown k2All))) => unifyKinds' env k1All k2All adam@1639: adam@1639: | (L'.KTupleUnif (_, _, ref (L'.KKnown k)), _) => unifyKinds' env k k2All adam@1639: | (_, L'.KTupleUnif (_, _, ref (L'.KKnown k))) => unifyKinds' env k1All k adam@1639: adam@1639: | (L'.KUnif (_, _, r1 as ref (L'.KUnknown f1)), L'.KUnif (_, _, r2 as ref (L'.KUnknown f2))) => adamc@403: if r1 = r2 then adamc@403: () adamc@403: else adam@1639: (r1 := L'.KKnown k2All; adam@1639: r2 := L'.KUnknown (fn x => f1 x andalso f2 x)) adam@1639: adam@1639: | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) => adamc@403: if occursKind r k2All then adamc@403: err KOccursCheckFailed adam@1639: else if not (f k2All) then adam@1639: err KScope adamc@403: else adam@1639: r := L'.KKnown k2All adam@1639: | (_, L'.KUnif (_, _, r as ref (L'.KUnknown f))) => adamc@403: if occursKind r k1All then adamc@403: err KOccursCheckFailed adam@1639: else if not (f k1All) then adam@1639: err KScope adamc@403: else adam@1639: r := L'.KKnown k1All adam@1639: adam@1639: | (L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f)), L'.KTuple ks) => adam@1639: if not (f k2All) then adam@1639: err KScope adam@1639: else adam@1639: ((app (fn (n, k) => unifyKinds' env k (List.nth (ks, n-1))) nks; adam@1639: r := L'.KKnown k2All) adam@1639: handle Subscript => err KIncompatible) adam@1639: | (L'.KTuple ks, L'.KTupleUnif (_, nks, r as ref (L'.KUnknown f))) => adam@1639: if not (f k2All) then adam@1639: err KScope adam@1639: else adam@1639: ((app (fn (n, k) => unifyKinds' env (List.nth (ks, n-1)) k) nks; adam@1639: r := L'.KKnown k1All) adam@1639: handle Subscript => err KIncompatible) adam@1639: | (L'.KTupleUnif (loc, nks1, r1 as ref (L'.KUnknown f1)), L'.KTupleUnif (_, nks2, r2 as ref (L'.KUnknown f2))) => adam@1302: let adam@1302: val nks = foldl (fn (p as (n, k1), nks) => adam@1302: case ListUtil.search (fn (n', k2) => adam@1302: if n' = n then adam@1302: SOME k2 adam@1302: else adam@1302: NONE) nks2 of adam@1302: NONE => p :: nks adam@1302: | SOME k2 => (unifyKinds' env k1 k2; adam@1302: nks)) nks2 nks1 adam@1302: adam@1639: val k = (L'.KTupleUnif (loc, nks, ref (L'.KUnknown (fn x => f1 x andalso f2 x))), loc) adam@1302: in adam@1639: r1 := L'.KKnown k; adam@1639: r2 := L'.KKnown k adam@1302: end adam@1302: adamc@403: | _ => err KIncompatible adamc@403: end adamc@403: adam@1719: exception KUnify of L'.kind * L'.kind * E.env * kunify_error adamc@403: adamc@623: fun unifyKinds env k1 k2 = adamc@623: unifyKinds' env k1 k2 adam@1719: handle KUnify' (env', err) => raise KUnify (k1, k2, env', err) adamc@403: adamc@403: fun checkKind env c k1 k2 = adamc@623: unifyKinds env k1 k2 adam@1719: handle KUnify (k1, k2, env', err) => adam@1719: conError env (WrongKind (c, k1, k2, env', err)) adamc@403: adamc@403: val dummy = ErrorMsg.dummySpan adamc@403: adamc@403: val ktype = (L'.KType, dummy) adamc@403: val kname = (L'.KName, dummy) adamc@403: val ktype_record = (L'.KRecord ktype, dummy) adamc@403: adamc@403: val cerror = (L'.CError, dummy) adamc@403: val kerror = (L'.KError, dummy) adamc@403: val eerror = (L'.EError, dummy) adamc@403: val sgnerror = (L'.SgnError, dummy) adamc@403: val strerror = (L'.StrError, dummy) adamc@403: adamc@403: val int = ref cerror adamc@403: val float = ref cerror adamc@403: val string = ref cerror adamc@821: val char = ref cerror adamc@403: val table = ref cerror adamc@403: adam@1639: adamc@403: local adamc@403: val count = ref 0 adamc@403: in adamc@403: adamc@403: fun resetKunif () = count := 0 adamc@403: adam@1639: fun kunif' f 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; adam@1639: (L'.KUnif (loc, s, ref (L'.KUnknown f)), loc) adamc@403: end adamc@403: adam@1639: fun kunif env = kunif' (validateKind env) adam@1639: 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: adam@1639: fun cunif' f (loc, k) = adamc@403: let adamc@403: val n = !count adamc@712: val s = if n < 26 then adamc@403: str (chr (ord #"A" + n)) adamc@403: else adamc@403: "U" ^ Int.toString (n - 26) adamc@403: in adamc@403: count := n + 1; adam@1639: (L'.CUnif (0, loc, k, s, ref (L'.Unknown f)), loc) adamc@403: end adamc@403: adam@1639: fun cunif env = cunif' (validateCon env) adam@1639: adamc@403: end adamc@403: adamc@623: fun elabKind env (k, loc) = adamc@403: case k of adamc@403: L.KType => (L'.KType, loc) adamc@623: | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc) adamc@403: | L.KName => (L'.KName, loc) adamc@623: | L.KRecord k => (L'.KRecord (elabKind env k), loc) adamc@403: | L.KUnit => (L'.KUnit, loc) adamc@623: | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) adam@1639: | L.KWild => kunif env loc adamc@403: adamc@623: | L.KVar s => (case E.lookupK env s of adamc@623: NONE => adamc@623: (kindError env (UnboundKind (loc, s)); adamc@623: kerror) adamc@623: | SOME n => (L'.KRel n, loc)) adamc@623: | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc) adamc@623: adamc@621: fun mapKind (dom, ran, loc)= adamc@621: (L'.KArrow ((L'.KArrow (dom, ran), loc), adamc@621: (L'.KArrow ((L'.KRecord dom, loc), adamc@621: (L'.KRecord ran, loc)), loc)), loc) adamc@403: adamc@403: fun hnormKind (kAll as (k, _)) = adamc@403: case k of adam@1639: L'.KUnif (_, _, ref (L'.KKnown k)) => hnormKind k adamc@403: | _ => kAll adamc@403: adamc@623: open ElabOps adamc@623: adam@1639: fun elabConHead env (c as (_, loc)) k = adamc@623: let adamc@623: fun unravel (k, c) = adamc@623: case hnormKind k of adamc@623: (L'.KFun (x, k'), _) => adamc@623: let adam@1639: val u = kunif env loc adamc@623: adamc@623: val k'' = subKindInKind (0, u) k' adamc@623: in adamc@623: unravel (k'', (L'.CKApp (c, u), loc)) adamc@623: end adamc@623: | _ => (c, k) adamc@623: in adamc@623: unravel (k, c) adamc@623: end adamc@623: adamc@403: fun elabCon (env, denv) (c, loc) = adamc@403: case c of adamc@403: L.CAnnot (c, k) => adamc@403: let adamc@623: val k' = elabKind env k adamc@403: val (c', ck, gs) = elabCon (env, denv) c adamc@403: in adamc@403: checkKind env c' ck k'; adamc@403: (c', k', gs) adamc@403: end adamc@403: adamc@403: | L.TFun (t1, t2) => adamc@403: let adamc@403: val (t1', k1, gs1) = elabCon (env, denv) t1 adamc@403: val (t2', k2, gs2) = elabCon (env, denv) t2 adamc@403: in adamc@403: checkKind env t1' k1 ktype; adamc@403: checkKind env t2' k2 ktype; adamc@403: ((L'.TFun (t1', t2'), loc), ktype, gs1 @ gs2) adamc@403: end adamc@403: | L.TCFun (e, x, k, t) => adamc@403: let adamc@403: val e' = elabExplicitness e adamc@623: val k' = elabKind env k adamc@403: val env' = E.pushCRel env x k' adamc@403: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@403: in adamc@403: checkKind env t' tk ktype; adamc@403: ((L'.TCFun (e', x, k', t'), loc), ktype, gs) adamc@403: end adamc@623: | L.TKFun (x, t) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (t', tk, gs) = elabCon (env', denv) t adamc@623: in adamc@623: checkKind env t' tk ktype; adamc@623: ((L'.TKFun (x, t'), loc), ktype, gs) adamc@623: end adamc@628: | L.TDisjoint (c1, c2, c) => adamc@403: let adamc@403: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@403: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@403: adam@1639: val ku1 = kunif env loc adam@1639: val ku2 = kunif env loc adamc@403: adamc@628: val denv' = D.assert env denv (c1', c2') adamc@403: val (c', k, gs4) = elabCon (env, denv') c adamc@403: in adamc@403: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@403: checkKind env c2' k2 (L'.KRecord ku2, loc); adam@1351: checkKind env c' k (L'.KType, loc); adamc@403: adamc@628: ((L'.TDisjoint (c1', c2', c'), loc), k, gs1 @ gs2 @ gs4) adamc@403: end adamc@403: | L.TRecord c => adamc@403: let adamc@403: val (c', ck, gs) = elabCon (env, denv) c adamc@403: val k = (L'.KRecord ktype, loc) adamc@403: in adamc@403: checkKind env c' ck k; adamc@403: ((L'.TRecord c', loc), ktype, gs) adamc@403: end adamc@403: adamc@403: | L.CVar ([], s) => adamc@403: (case E.lookupC env s of adamc@403: E.NotBound => adamc@403: (conError env (UnboundCon (loc, s)); adamc@403: (cerror, kerror, [])) adamc@403: | E.Rel (n, k) => adamc@623: let adam@1639: val (c, k) = elabConHead env (L'.CRel n, loc) k adamc@623: in adamc@623: (c, k, []) adamc@623: end adamc@403: | E.Named (n, k) => adamc@623: let adam@1639: val (c, k) = elabConHead env (L'.CNamed n, loc) k adamc@623: in adamc@623: (c, k, []) adamc@623: end) adamc@403: | L.CVar (m1 :: ms, s) => adamc@403: (case E.lookupStr env m1 of adamc@403: NONE => (conError env (UnboundStrInCon (loc, m1)); adamc@403: (cerror, kerror, [])) adamc@403: | SOME (n, sgn) => adamc@403: let adamc@403: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@403: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@403: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@403: (strerror, sgnerror)) adamc@403: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@403: ((L'.StrVar n, loc), sgn) ms adamc@403: adam@1717: val (c, k) = case E.projectCon env {sgn = sgn, str = str, field = s} of adam@1717: NONE => (conError env (UnboundCon (loc, s)); adam@1717: (cerror, kerror)) adam@1717: | SOME (k, _) => elabConHead env (L'.CModProj (n, ms, s), loc) k adamc@403: in adamc@987: (c, 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 adam@1639: val dom = kunif env loc adam@1639: val ran = kunif env 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 adam@1639: NONE => kunif env loc adamc@623: | SOME k => elabKind env k adamc@403: val env' = E.pushCRel env x k' adamc@403: val (t', tk, gs) = elabCon (env', D.enter denv) t adamc@403: in adamc@403: ((L'.CAbs (x, k', t'), loc), adamc@403: (L'.KArrow (k', tk), loc), adamc@403: gs) adamc@403: end adamc@623: | L.CKAbs (x, t) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (t', tk, gs) = elabCon (env', denv) t adamc@623: in adamc@623: ((L'.CKAbs (x, t'), loc), adamc@623: (L'.KFun (x, tk), loc), adamc@623: gs) adamc@623: end adamc@403: adamc@403: | L.CName s => adamc@403: ((L'.CName s, loc), kname, []) adamc@403: adamc@403: | L.CRecord xcs => adamc@403: let adam@1639: val k = kunif env 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 adam@1639: val ku = kunif env loc adamc@403: val k = (L'.KRecord ku, loc) adamc@403: in adamc@403: checkKind env c1' k1 k; adamc@403: checkKind env c2' k2 k; adamc@403: ((L'.CConcat (c1', c2'), loc), k, adamc@403: D.prove env denv (c1', c2', loc) @ gs1 @ gs2) adamc@403: end adamc@621: | L.CMap => adamc@403: let adam@1639: val dom = kunif env loc adam@1639: val ran = kunif env loc adamc@403: in adamc@621: ((L'.CMap (dom, ran), loc), adamc@621: mapKind (dom, ran, loc), adamc@403: []) adamc@403: end adamc@403: adamc@403: | L.CUnit => ((L'.CUnit, loc), (L'.KUnit, loc), []) adamc@403: adamc@403: | L.CTuple cs => adamc@403: let adamc@403: val (cs', ks, gs) = foldl (fn (c, (cs', ks, gs)) => adamc@403: let adamc@403: val (c', k, gs') = elabCon (env, denv) c adamc@403: in adamc@403: (c' :: cs', k :: ks, gs' @ gs) adamc@403: end) ([], [], []) cs adamc@403: in adamc@403: ((L'.CTuple (rev cs'), loc), (L'.KTuple (rev ks), loc), gs) adamc@403: end adamc@403: | L.CProj (c, n) => adamc@403: let adamc@403: val (c', k, gs) = elabCon (env, denv) c adam@1302: adam@1639: val k' = kunif env loc adamc@403: in adam@1302: if n <= 0 then adam@1302: (conError env (ProjBounds (c', n)); adam@1302: (cerror, kerror, [])) adam@1302: else adam@1639: (checkKind env c' k (L'.KTupleUnif (loc, [(n, k')], ref (L'.KUnknown (validateKind env))), loc); adam@1302: ((L'.CProj (c', n), loc), k', gs)) adamc@403: end adamc@403: adamc@403: | L.CWild k => adamc@403: let adamc@623: val k' = elabKind env k adamc@403: in adam@1639: (cunif env (loc, k'), k', []) adamc@403: end adamc@403: adamc@403: fun kunifsRemain k = adamc@403: case k of adam@1639: L'.KUnif (_, _, ref (L'.KUnknown _)) => true adam@1639: | L'.KTupleUnif (_, _, ref (L'.KUnknown _)) => true adamc@403: | _ => false adamc@403: fun cunifsRemain c = adamc@403: case c of adam@1639: L'.CUnif (_, loc, k, _, r as ref (L'.Unknown _)) => adam@1326: (case #1 (hnormKind k) of adam@1639: L'.KUnit => (r := L'.Known (L'.CUnit, loc); false) adam@1584: | _ => true) adam@1584: | _ => false 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: adam@1584: val cunifsInDecl = U.Decl.exists {kind = fn _ => false, adamc@403: con = cunifsRemain, adam@1584: exp = fn _ => false, adam@1584: sgn_item = fn _ => false, adam@1584: sgn = fn _ => false, adam@1584: str = fn _ => false, adam@1584: decl = fn _ => false} adamc@403: adamc@403: fun occursCon r = adamc@403: U.Con.exists {kind = fn _ => false, adam@1303: con = fn L'.CUnif (_, _, _, _, r') => r = r' adamc@403: | _ => false} adamc@403: adam@1719: exception CUnify' of E.env * cunify_error adamc@403: adamc@403: type record_summary = { adamc@403: fields : (L'.con * L'.con) list, adam@1639: unifs : (L'.con * L'.cunif ref) list, adamc@403: others : L'.con list adamc@403: } adamc@403: adamc@403: fun summaryToCon {fields, unifs, others} = adamc@403: let adam@1626: fun concat (c1, c2) = adam@1626: case #1 c1 of adam@1626: L'.CRecord (_, []) => c2 adam@1626: | _ => case #1 c2 of adam@1626: L'.CRecord (_, []) => c1 adam@1626: | _ => (L'.CConcat (c1, c2), dummy) adam@1626: adamc@403: val c = (L'.CRecord (ktype, []), dummy) adam@1626: val c = List.foldr concat c others adam@1626: val c = List.foldr (fn ((c', _), c) => concat (c', c)) c unifs adamc@403: in adam@1626: concat ((L'.CRecord (ktype, fields), dummy), c) adamc@403: end adamc@403: adamc@403: fun p_summary env s = p_con env (summaryToCon s) adamc@403: adam@1719: exception CUnify of L'.con * L'.con * E.env * cunify_error adamc@403: adamc@403: fun kindof env (c, loc) = adamc@403: case c of adamc@403: L'.TFun _ => ktype adamc@403: | L'.TCFun _ => ktype adamc@403: | L'.TRecord _ => ktype adamc@628: | L'.TDisjoint _ => ktype adamc@403: adamc@403: | L'.CRel xn => #2 (E.lookupCRel env xn) adamc@403: | L'.CNamed xn => #2 (E.lookupCNamed env xn) adamc@403: | L'.CModProj (n, ms, x) => adamc@403: let adamc@403: val (_, sgn) = E.lookupStrNamed env n adamc@403: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@403: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@403: NONE => raise Fail "kindof: Unknown substructure" adamc@403: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@403: ((L'.StrVar n, loc), sgn) ms adamc@403: in adamc@403: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@403: NONE => raise Fail "kindof: Unknown con in structure" adamc@403: | SOME (k, _) => k adamc@403: end adamc@403: adamc@403: | L'.CApp (c, _) => adamc@403: (case hnormKind (kindof env c) of adamc@403: (L'.KArrow (_, k), _) => k adamc@403: | (L'.KError, _) => kerror adam@1719: | k => raise CUnify' (env, CKindof (k, c, "arrow"))) adamc@403: | L'.CAbs (x, k, c) => (L'.KArrow (k, kindof (E.pushCRel env x k) c), loc) adamc@628: adamc@403: adamc@403: | L'.CName _ => kname adamc@403: adamc@403: | L'.CRecord (k, _) => (L'.KRecord k, loc) adamc@403: | L'.CConcat (c, _) => kindof env c adamc@621: | L'.CMap (dom, ran) => mapKind (dom, ran, loc) adamc@403: adamc@403: | L'.CUnit => (L'.KUnit, loc) adamc@403: adamc@403: | L'.CTuple cs => (L'.KTuple (map (kindof env) cs), loc) adamc@403: | L'.CProj (c, n) => adamc@403: (case hnormKind (kindof env c) of adamc@403: (L'.KTuple ks, _) => List.nth (ks, n - 1) adam@1311: | (L'.KUnif (_, _, r), _) => adam@1311: let adam@1639: val ku = kunif env loc adam@1639: val k = (L'.KTupleUnif (loc, [(n, ku)], r), loc) adam@1311: in adam@1639: r := L'.KKnown k; adam@1311: k adam@1311: end adam@1311: | (L'.KTupleUnif (_, nks, r), _) => adam@1311: (case ListUtil.search (fn (n', k) => if n' = n then SOME k else NONE) nks of adam@1311: SOME k => k adam@1311: | NONE => adam@1311: let adam@1639: val ku = kunif env loc adam@1639: val k = (L'.KTupleUnif (loc, ((n, ku) :: nks), r), loc) adam@1311: in adam@1639: r := L'.KKnown k; adam@1311: k adam@1311: end) adam@1719: | k => raise CUnify' (env, CKindof (k, c, "tuple"))) adamc@403: adamc@403: | L'.CError => kerror adam@1303: | L'.CUnif (_, _, k, _, _) => k adamc@403: adamc@623: | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) adamc@623: | L'.CKApp (c, k) => adamc@623: (case hnormKind (kindof env c) of adamc@623: (L'.KFun (_, k'), _) => subKindInKind (0, k) k' adam@1719: | k => raise CUnify' (env, CKindof (k, c, "kapp"))) adamc@623: | L'.TKFun _ => ktype adamc@403: adamc@621: exception GuessFailure adamc@403: adamc@513: fun isUnitCon env (c, loc) = adamc@513: case c of adamc@513: L'.TFun _ => false adamc@513: | L'.TCFun _ => false adamc@513: | L'.TRecord _ => false adamc@628: | L'.TDisjoint _ => false adamc@513: adam@1316: | L'.CRel xn => #1 (hnormKind (#2 (E.lookupCRel env xn))) = L'.KUnit adam@1316: | L'.CNamed xn => #1 (hnormKind (#2 (E.lookupCNamed env xn))) = L'.KUnit adamc@518: | L'.CModProj (n, ms, x) => false adamc@518: (*let adamc@513: val (_, sgn) = E.lookupStrNamed env n adamc@513: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@513: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@513: NONE => raise Fail "kindof: Unknown substructure" adamc@513: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@513: ((L'.StrVar n, loc), sgn) ms adamc@513: in adamc@513: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@513: NONE => raise Fail "kindof: Unknown con in structure" adamc@513: | SOME ((k, _), _) => k = L'.KUnit adamc@518: end*) adamc@518: adamc@518: | L'.CApp (c, _) => false adamc@518: (*(case hnormKind (kindof env c) of adamc@513: (L'.KArrow (_, k), _) => #1 k = L'.KUnit adamc@513: | (L'.KError, _) => false adamc@518: | k => raise CUnify' (CKindof (k, c, "arrow")))*) adamc@513: | L'.CAbs _ => false adamc@513: adamc@513: | L'.CName _ => false adamc@513: adamc@513: | L'.CRecord _ => false adamc@513: | L'.CConcat _ => false adamc@621: | L'.CMap _ => false adamc@513: adamc@513: | L'.CUnit => true adamc@513: adamc@513: | L'.CTuple _ => false adamc@518: | L'.CProj (c, n) => false adamc@518: (*(case hnormKind (kindof env c) of adamc@513: (L'.KTuple ks, _) => #1 (List.nth (ks, n - 1)) = L'.KUnit adamc@518: | k => raise CUnify' (CKindof (k, c, "tuple")))*) adamc@513: adamc@513: | L'.CError => false adam@1316: | L'.CUnif (_, _, k, _, _) => #1 (hnormKind k) = L'.KUnit adamc@513: adamc@623: | L'.CKAbs _ => false adamc@623: | L'.CKApp _ => false adamc@623: | L'.TKFun _ => false adamc@623: adamc@709: val recdCounter = ref 0 adamc@709: adamc@713: val mayDelay = ref false adamc@777: val delayedUnifs = ref ([] : (ErrorMsg.span * E.env * L'.kind * record_summary * record_summary) list) adamc@777: adamc@830: val delayedExhaustives = ref ([] : (E.env * L'.con * L'.pat list * ErrorMsg.span) list) adamc@830: adam@1304: exception CantSquish adam@1304: adam@1304: fun squish by = adam@1304: U.Con.mapB {kind = fn _ => fn k => k, adam@1304: con = fn bound => fn c => adam@1304: case c of adam@1304: L'.CRel xn => adam@1304: if xn < bound then adam@1304: c adam@1304: else if bound <= xn andalso xn < bound + by then adam@1304: raise CantSquish adam@1304: else adam@1304: L'.CRel (xn - by) adam@1304: | L'.CUnif _ => raise CantSquish adam@1304: | _ => c, adam@1304: bind = fn (bound, U.Con.RelC _) => bound + 1 adam@1304: | (bound, _) => bound} 0 adam@1304: adam@1582: val reducedSummaries = ref (NONE : (Print.PD.pp_desc * Print.PD.pp_desc) option) adam@1582: adamc@777: fun unifyRecordCons env (loc, c1, c2) = adamc@403: let adamc@403: fun rkindof c = adamc@403: case hnormKind (kindof env c) of adamc@403: (L'.KRecord k, _) => k adamc@403: | (L'.KError, _) => kerror adam@1639: | (L'.KUnif (_, _, r as ref (L'.KUnknown f)), _) => adamc@753: let adam@1639: val k = kunif' f (#2 c) adamc@753: in adam@1639: r := L'.KKnown (L'.KRecord k, #2 c); adamc@753: k adamc@753: end adam@1719: | k => raise CUnify' (env, CKindof (k, c, "record")) adamc@403: adamc@403: val k1 = rkindof c1 adamc@403: val k2 = rkindof c2 adamc@403: adamc@628: val r1 = recordSummary env c1 adamc@628: val r2 = recordSummary env c2 adamc@403: in adamc@623: unifyKinds env k1 k2; adamc@777: unifySummaries env (loc, k1, r1, r2) adamc@403: end adamc@403: adamc@777: and normalizeRecordSummary env (r : record_summary) = adamc@777: recordSummary env (summaryToCon r) adamc@777: adamc@628: and recordSummary env c = adamc@403: let adamc@628: val c = hnormCon env c adamc@628: adamc@628: val sum = adamc@403: case c of adamc@628: (L'.CRecord (_, xcs), _) => {fields = xcs, unifs = [], others = []} adamc@403: | (L'.CConcat (c1, c2), _) => adamc@403: let adamc@628: val s1 = recordSummary env c1 adamc@628: val s2 = recordSummary env c2 adamc@403: in adamc@628: {fields = #fields s1 @ #fields s2, adamc@628: unifs = #unifs s1 @ #unifs s2, adamc@628: others = #others s1 @ #others s2} adamc@403: end adam@1639: | (L'.CUnif (nl, _, _, _, ref (L'.Known c)), _) => recordSummary env (E.mliftConInCon nl c) adam@1303: | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} adamc@628: | c' => {fields = [], unifs = [], others = [c']} adamc@403: in adamc@628: sum adamc@403: end adamc@403: adamc@987: and consEq env loc (c1, c2) = adamc@777: let adamc@777: val mayDelay' = !mayDelay adamc@777: in adamc@777: (mayDelay := false; adamc@987: unifyCons env loc c1 c2; adamc@777: mayDelay := mayDelay'; adamc@777: true) adamc@777: handle CUnify _ => (mayDelay := mayDelay'; false) adamc@777: end adamc@403: adamc@403: and consNeq env (c1, c2) = adamc@628: case (#1 (hnormCon env c1), #1 (hnormCon env c2)) of adamc@403: (L'.CName x1, L'.CName x2) => x1 <> x2 adamc@1093: | (L'.CName _, L'.CRel _) => true adamc@1093: | (L'.CRel _, L'.CName _) => true adamc@1093: | (L'.CRel n1, L'.CRel n2) => n1 <> n2 adamc@1093: | (L'.CRel _, L'.CNamed _) => true adamc@1093: | (L'.CNamed _, L'.CRel _) => true adamc@1093: | (L'.CRel _, L'.CModProj _) => true adamc@1093: | (L'.CModProj _, L'.CRel _) => true adamc@1269: | (L'.CModProj (_, _, n1), L'.CModProj (_, _, n2)) => n1 <> n2 adam@1589: | (L'.CModProj _, L'.CName _) => true adam@1589: | (L'.CName _, L'.CModProj _) => true adam@1589: | (L'.CNamed _, L'.CName _) => true adam@1589: | (L'.CName _, L'.CNamed _) => true adamc@403: | _ => false adamc@403: adamc@777: and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = adamc@403: let adam@1583: val () = reducedSummaries := NONE adam@1583: adamc@848: (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), adam@1303: ("#1", p_summary env s1), adam@1303: ("#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@987: andalso consEq env loc (c1, c2) adamc@987: andalso consEq env loc (x1, x2)) adamc@403: (#fields s1, #fields s2) adamc@403: (*val () = eprefaces "Summaries2" [("#1", p_summary env {fields = fs1, unifs = #unifs s1, others = #others s1}), adamc@403: ("#2", p_summary env {fields = fs2, unifs = #unifs s2, others = #others s2})]*) adamc@646: adamc@403: val (unifs1, unifs2) = eatMatching (fn ((_, r1), (_, r2)) => r1 = r2) (#unifs s1, #unifs s2) adamc@646: adam@1660: val hasUnifs = U.Con.exists {kind = fn _ => false, adam@1660: con = fn L'.CUnif _ => true adam@1660: | _ => false} adam@1657: adam@1657: val (others1, others2) = eatMatching (fn (c1, c2) => adam@1964: c1 = c2 adam@1964: orelse (not (hasUnifs c1 andalso hasUnifs c2) adam@1964: andalso consEq env loc (c1, c2))) (#others s1, #others s2) adamc@403: (*val () = eprefaces "Summaries3" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@403: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@709: fun unsummarize {fields, unifs, others} = adamc@709: let adamc@709: val c = (L'.CRecord (k, fields), loc) adamc@709: adamc@709: val c = foldl (fn ((c1, _), c2) => (L'.CConcat (c1, c2), loc)) adamc@709: c unifs adamc@709: in adamc@709: foldl (fn (c1, c2) => (L'.CConcat (c1, c2), loc)) adamc@709: c others adamc@709: end adamc@709: adamc@710: val empties = ([], [], [], [], [], []) adamc@710: adamc@709: val (unifs1, fs1, others1, unifs2, fs2, others2) = adamc@709: case (unifs1, fs1, others1, unifs2, fs2, others2) of adam@1639: orig as ([(_, r as ref (L'.Unknown f))], [], [], _, _, _) => adamc@709: let adamc@709: val c = unsummarize {fields = fs2, others = others2, unifs = unifs2} adamc@709: in adam@1639: if occursCon r c orelse not (f c) then adamc@709: orig adamc@709: else adam@1639: (r := L'.Known c; adamc@710: empties) adamc@709: end adam@1639: | orig as (_, _, _, [(_, r as ref (L'.Unknown f))], [], []) => adamc@709: let adamc@709: val c = unsummarize {fields = fs1, others = others1, unifs = unifs1} adamc@709: in adam@1639: if occursCon r c orelse not (f c) then adamc@709: orig adamc@709: else adam@1639: (r := L'.Known c; adamc@710: empties) adamc@709: end adam@1639: | orig as ([(_, r1 as ref (L'.Unknown f1))], _, [], [(_, r2 as ref (L'.Unknown f2))], _, []) => adamc@710: if List.all (fn (x1, _) => List.all (fn (x2, _) => consNeq env (x1, x2)) fs2) fs1 then adamc@710: let adamc@838: val kr = (L'.KRecord k, loc) adam@1639: val u = cunif env (loc, kr) adam@1639: adam@1639: val c1 = (L'.CConcat ((L'.CRecord (k, fs2), loc), u), loc) adam@1639: val c2 = (L'.CConcat ((L'.CRecord (k, fs1), loc), u), loc) adamc@710: in adam@1639: if not (f1 c1) orelse not (f2 c2) then adam@1639: orig adam@1639: else adam@1639: (r1 := L'.Known c1; adam@1639: r2 := L'.Known c2; adam@1639: empties) adamc@710: end adamc@710: else adamc@710: orig adamc@709: | orig => orig adamc@709: adamc@403: (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@777: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@753: fun isGuessable (other, fs, unifs) = adamc@753: let adamc@753: val c = (L'.CRecord (k, fs), loc) adamc@753: val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs adamc@753: in adamc@987: (guessMap env loc (other, c, GuessFailure); adamc@753: true) adamc@753: handle GuessFailure => false adamc@753: end adamc@403: adamc@754: val (fs1, fs2, others1, others2, unifs1, unifs2) = adamc@753: case (fs1, fs2, others1, others2, unifs1, unifs2) of adamc@753: ([], _, [other1], [], [], _) => adamc@753: if isGuessable (other1, fs2, unifs2) then adamc@754: ([], [], [], [], [], []) adamc@403: else adamc@754: (fs1, fs2, others1, others2, unifs1, unifs2) adamc@753: | (_, [], [], [other2], _, []) => adamc@777: if isGuessable (other2, fs1, unifs1) then adamc@777: ([], [], [], [], [], []) adamc@777: else adamc@777: (fs1, fs2, others1, others2, unifs1, unifs2) adamc@754: | _ => (fs1, fs2, others1, others2, unifs1, unifs2) adamc@403: adam@1582: val () = if !mayDelay then adam@1582: () adam@1582: else adam@1626: let adam@1626: val c1 = summaryToCon {fields = fs1, unifs = unifs1, others = others1} adam@1626: val c2 = summaryToCon {fields = fs2, unifs = unifs2, others = others2} adam@1626: in adam@1626: case (c1, c2) of adam@1626: ((L'.CRecord (_, []), _), (L'.CRecord (_, []), _)) => reducedSummaries := NONE adam@1626: | _ => reducedSummaries := SOME (p_con env c1, p_con env c2) adam@1626: end adam@1582: adamc@403: (*val () = eprefaces "Summaries5" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), adamc@646: ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) adamc@403: adamc@838: val empty = (L'.CRecord (k, []), loc) adamc@1071: fun failure () = adamc@1071: let adamc@1071: val fs2 = #fields s2 adamc@1071: adamc@1071: fun findPointwise fs1 = adamc@1071: case fs1 of adamc@1071: [] => NONE adamc@1071: | (nm1, c1) :: fs1 => adamc@1071: case List.find (fn (nm2, _) => consEq env loc (nm1, nm2)) fs2 of adamc@1071: NONE => findPointwise fs1 adamc@1071: | SOME (_, c2) => adamc@1071: if consEq env loc (c1, c2) then adamc@1071: findPointwise fs1 adamc@1071: else adam@1588: SOME (nm1, c1, c2, (unifyCons env loc c1 c2; NONE) adam@1719: handle CUnify (_, _, env', err) => (reducedSummaries := NONE; adam@1719: SOME (env', err))) adamc@1071: in adam@1719: raise CUnify' (env, CRecordFailure (unsummarize s1, unsummarize s2, findPointwise (#fields s1))) adamc@1071: end adam@1341: adam@1341: fun default () = if !mayDelay then adam@1341: delayedUnifs := (loc, env, k, s1, s2) :: !delayedUnifs adam@1341: else adam@1341: failure () adamc@709: in adamc@777: (case (unifs1, fs1, others1, unifs2, fs2, others2) of adamc@777: (_, [], [], [], [], []) => adam@1639: app (fn (_, r) => r := L'.Known empty) unifs1 adamc@777: | ([], [], [], _, [], []) => adam@1639: app (fn (_, r) => r := L'.Known empty) unifs2 adam@1639: | (_, _, _, [], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)]) => adam@1341: let adam@1341: val c = summaryToCon {fields = fs1, unifs = unifs1, others = others1} adam@1341: in adam@1341: if occursCon r c then adam@1588: (reducedSummaries := NONE; adam@1719: raise CUnify' (env, COccursCheckFailed (cr, c))) adam@1341: else adam@1639: let adam@1639: val sq = squish nl c adam@1639: in adam@1639: if not (f sq) then adam@1639: default () adam@1639: else adam@1639: r := L'.Known sq adam@1639: end adam@1341: handle CantSquish => default () adam@1341: end adam@1639: | ([], [], [cr as (L'.CUnif (nl, _, _, _, r as ref (L'.Unknown f)), _)], _, _, _) => adam@1341: let adam@1341: val c = summaryToCon {fields = fs2, unifs = unifs2, others = others2} adam@1341: in adam@1341: if occursCon r c then adam@1588: (reducedSummaries := NONE; adam@1719: raise CUnify' (env, COccursCheckFailed (cr, c))) adam@1341: else adam@1639: let adam@1639: val sq = squish nl c adam@1639: in adam@1639: if not (f sq) then adam@1639: default () adam@1639: else adam@1639: r := L'.Known sq adam@1639: end adam@1341: handle CantSquish => default () adam@1341: end adam@1341: | _ => default ()) adam@1341: adamc@777: (*before eprefaces "Summaries'" [("#1", p_summary env (normalizeRecordSummary env s1)), adamc@777: ("#2", p_summary env (normalizeRecordSummary env s2))]*) adamc@403: end adamc@403: adamc@987: and guessMap env loc (c1, c2, ex) = adamc@403: let adamc@621: fun unfold (dom, ran, f, r, c) = adamc@403: let adamc@621: fun unfold (r, c) = adamc@754: case #1 (hnormCon env c) of adamc@987: L'.CRecord (_, []) => unifyCons env loc r (L'.CRecord (dom, []), loc) adamc@628: | L'.CRecord (_, [(x, v)]) => adamc@628: let adamc@628: val v' = case dom of adamc@628: (L'.KUnit, _) => (L'.CUnit, loc) adam@1639: | _ => cunif env (loc, dom) adamc@628: in adamc@987: unifyCons env loc v (L'.CApp (f, v'), loc); adamc@987: unifyCons env loc r (L'.CRecord (dom, [(x, v')]), loc) adamc@628: end adamc@628: | L'.CRecord (_, (x, v) :: rest) => adamc@628: let adam@1639: val r1 = cunif env (loc, (L'.KRecord dom, loc)) adam@1639: val r2 = cunif env (loc, (L'.KRecord dom, loc)) adamc@628: in adamc@628: unfold (r1, (L'.CRecord (ran, [(x, v)]), loc)); adamc@628: unfold (r2, (L'.CRecord (ran, rest), loc)); adamc@987: unifyCons env loc r (L'.CConcat (r1, r2), loc) adamc@628: end adamc@628: | L'.CConcat (c1', c2') => adamc@628: let adam@1639: val r1 = cunif env (loc, (L'.KRecord dom, loc)) adam@1639: val r2 = cunif env (loc, (L'.KRecord dom, loc)) adamc@628: in adamc@628: unfold (r1, c1'); adamc@628: unfold (r2, c2'); adamc@987: unifyCons env loc r (L'.CConcat (r1, r2), loc) adamc@628: end adam@1639: | L'.CUnif (0, _, _, _, ur as ref (L'.Unknown rf)) => adam@1639: let adam@1639: val c' = (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) adam@1639: in adam@1639: if not (rf c') then adam@1639: cunifyError env (CScope (c, c')) adam@1639: else adam@1639: ur := L'.Known c' adam@1639: end adamc@628: | _ => raise ex adamc@403: in adamc@621: unfold (r, c) adamc@403: end adamc@632: handle _ => raise ex adamc@403: in adamc@403: case (#1 c1, #1 c2) of adamc@621: (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r), _) => adamc@621: unfold (dom, ran, f, r, c2) adamc@621: | (_, L'.CApp ((L'.CApp ((L'.CMap (dom, ran), _), f), _), r)) => adamc@621: unfold (dom, ran, f, r, c1) adamc@403: | _ => raise ex adamc@403: end adamc@403: adamc@987: and unifyCons' env loc c1 c2 = adamc@628: if isUnitCon env c1 andalso isUnitCon env c2 then adamc@628: () adamc@628: else adamc@403: let adamc@628: (*val befor = Time.now () adamc@628: val old1 = c1 adamc@628: val old2 = c2*) adamc@628: val c1 = hnormCon env c1 adamc@628: val c2 = hnormCon env c2 adamc@403: in adamc@987: unifyCons'' env loc c1 c2 adamc@987: handle ex => guessMap env loc (c1, c2, ex) adamc@403: end adamc@628: adamc@987: and unifyCons'' env loc (c1All as (c1, _)) (c2All as (c2, _)) = adamc@403: let adam@1719: fun err f = raise CUnify' (env, f (c1All, c2All)) adamc@403: adamc@706: fun projSpecial1 (c1, n1, onFail) = adamc@403: let adamc@632: fun trySnd () = adamc@632: case #1 (hnormCon env c2All) of adamc@632: L'.CProj (c2, n2) => adamc@632: let adamc@632: fun tryNormal () = adamc@632: if n1 = n2 then adamc@987: unifyCons' env loc c1 c2 adamc@632: else adamc@706: onFail () adamc@632: in adamc@632: case #1 (hnormCon env c2) of adam@1639: L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) => adamc@632: (case #1 (hnormKind k) of adamc@632: L'.KTuple ks => adamc@632: let adamc@632: val loc = #2 c2 adam@1639: val us = map (fn k => cunif' f (loc, k)) ks adamc@632: in adam@1639: r := L'.Known (L'.CTuple us, loc); adamc@987: unifyCons' env loc c1All (List.nth (us, n2 - 1)) adamc@632: end adamc@632: | _ => tryNormal ()) adamc@632: | _ => tryNormal () adamc@632: end adamc@706: | _ => onFail () adamc@403: in adamc@632: case #1 (hnormCon env c1) of adam@1639: L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) => adamc@632: (case #1 (hnormKind k) of adamc@632: L'.KTuple ks => adamc@632: let adamc@632: val loc = #2 c1 adam@1639: val us = map (fn k => cunif' f (loc, k)) ks adamc@632: in adam@1639: r := L'.Known (L'.CTuple us, loc); adamc@987: unifyCons' env loc (List.nth (us, n1 - 1)) c2All adamc@632: end adamc@632: | _ => trySnd ()) adamc@632: | _ => trySnd () adamc@403: end adamc@632: adamc@706: fun projSpecial2 (c2, n2, onFail) = adamc@706: case #1 (hnormCon env c2) of adam@1639: L'.CUnif (0, _, k, _, r as ref (L'.Unknown f)) => adamc@706: (case #1 (hnormKind k) of adamc@706: L'.KTuple ks => adamc@706: let adamc@706: val loc = #2 c2 adam@1639: val us = map (fn k => cunif' f (loc, k)) ks adamc@706: in adam@1639: r := L'.Known (L'.CTuple us, loc); adamc@987: unifyCons' env loc c1All (List.nth (us, n2 - 1)) adamc@706: end adamc@706: | _ => onFail ()) adamc@706: | _ => onFail () adamc@706: adamc@777: fun isRecord' () = unifyRecordCons env (loc, c1All, c2All) adamc@706: adamc@706: fun isRecord () = adamc@706: case (c1, c2) of adamc@706: (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, isRecord') adamc@706: | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, isRecord') adamc@706: | _ => isRecord' () adam@2044: adam@2044: fun maybeIsRecord c = adam@2044: case c of adam@2044: L'.CRecord _ => isRecord () adam@2044: | L'.CConcat _ => isRecord () adam@2044: | _ => err COccursCheckFailed adamc@706: in adam@1668: (*eprefaces "unifyCons''" [("c1", p_con env c1All), adam@1668: ("c2", p_con env c2All)];*) adam@1668: adam@1668: (case (c1, c2) of adamc@706: (L'.CError, _) => () adamc@706: | (_, L'.CError) => () adamc@403: adam@1639: | (L'.CUnif (nl1, loc1, k1, _, r1 as ref (L'.Unknown f1)), L'.CUnif (nl2, loc2, k2, _, r2 as ref (L'.Unknown f2))) => adam@1668: if r1 = r2 then adam@1668: if nl1 = nl2 then adam@1668: () adam@1668: else adam@1668: err (fn _ => TooLifty (loc1, loc2)) adam@1303: else if nl1 = 0 then adamc@705: (unifyKinds env k1 k2; adam@1639: if f1 c2All then adam@1639: r1 := L'.Known c2All adam@1639: else adam@1639: err CScope) adam@1303: else if nl2 = 0 then adam@1303: (unifyKinds env k1 k2; adam@1639: if f2 c1All then adam@1639: r2 := L'.Known c1All adam@1639: else adam@1639: err CScope) adam@1303: else adam@1303: err (fn _ => TooLifty (loc1, loc2)) adam@1303: adam@2049: | (L'.CUnif (0, _, k1, _, r as ref (L'.Unknown f)), _) => adam@2049: (unifyKinds env k1 (kindof env c2All); adam@2049: if occursCon r c2All then adam@2049: maybeIsRecord c2 adam@2049: else if f c2All then adam@2049: r := L'.Known c2All adam@2049: else adam@2049: err CScope) adam@2049: | (_, L'.CUnif (0, _, k2, _, r as ref (L'.Unknown f))) => adam@2049: (unifyKinds env (kindof env c1All) k2; adam@2049: if occursCon r c1All then adam@2049: maybeIsRecord c1 adam@2049: else if f c1All then adam@2049: r := L'.Known c1All adam@2049: else adam@2049: err CScope) adam@2049: adam@2049: | (L'.CUnif (nl, _, k1, _, r as ref (L'.Unknown f)), _) => adamc@705: if occursCon r c2All then adam@2044: maybeIsRecord c2 adamc@705: else adam@2049: (unifyKinds env k1 (kindof env c2All); adam@2049: let adam@1639: val sq = squish nl c2All adam@1639: in adam@1639: if f sq then adam@1639: r := L'.Known sq adam@1639: else adam@1639: err CScope adam@1639: end adam@1639: handle CantSquish => err (fn _ => TooDeep)) adam@2049: | (_, L'.CUnif (nl, _, k2, _, r as ref (L'.Unknown f))) => adamc@705: if occursCon r c1All then adam@2044: maybeIsRecord c1 adamc@705: else adam@2049: (unifyKinds env (kindof env c1All) k2; adam@2049: let adam@1639: val sq = squish nl c1All adam@1639: in adam@1639: if f sq then adam@1639: r := L'.Known sq adam@1639: else adam@1639: err CScope adam@1639: end adam@1306: handle CantSquish => err (fn _ => TooDeep)) adam@1304: adam@2044: | (L'.CRecord _, _) => isRecord () adam@2044: | (_, L'.CRecord _) => isRecord () adam@2044: | (L'.CConcat _, _) => isRecord () adam@2044: | (_, L'.CConcat _) => isRecord () adam@2044: adam@1341: adamc@705: | (L'.CUnit, L'.CUnit) => () adamc@705: adamc@705: | (L'.TFun (d1, r1), L'.TFun (d2, r2)) => adamc@987: (unifyCons' env loc d1 d2; adam@1639: unifyCons' env loc r1 r2) adamc@705: | (L'.TCFun (expl1, x1, d1, r1), L'.TCFun (expl2, _, d2, r2)) => adamc@705: if expl1 <> expl2 then adamc@705: err CExplicitness adamc@705: else adamc@705: (unifyKinds env d1 d2; adamc@705: let adamc@705: (*val befor = Time.now ()*) adamc@705: val env' = E.pushCRel env x1 d1 adamc@705: in adamc@705: (*TextIO.print ("E.pushCRel: " adamc@705: ^ LargeReal.toString (Time.toReal (Time.- (Time.now (), befor))) adamc@705: ^ "\n");*) adamc@987: unifyCons' env' loc r1 r2 adamc@705: end) adamc@987: | (L'.TRecord r1, L'.TRecord r2) => unifyCons' env loc r1 r2 adamc@705: | (L'.TDisjoint (c1, d1, e1), L'.TDisjoint (c2, d2, e2)) => adamc@987: (unifyCons' env loc c1 c2; adamc@987: unifyCons' env loc d1 d2; adamc@987: unifyCons' env loc e1 e2) adamc@705: adamc@705: | (L'.CRel n1, L'.CRel n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: | (L'.CNamed n1, L'.CNamed n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CApp (d1, r1), L'.CApp (d2, r2)) => adamc@987: (unifyCons' env loc d1 d2; adamc@987: unifyCons' env loc r1 r2) adamc@705: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => adamc@705: (unifyKinds env k1 k2; adamc@987: unifyCons' (E.pushCRel env x1 k1) loc c1 c2) adamc@705: adamc@705: | (L'.CName n1, L'.CName n2) => adamc@705: if n1 = n2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CModProj (n1, ms1, x1), L'.CModProj (n2, ms2, x2)) => adamc@705: if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then adamc@705: () adamc@705: else adamc@705: err CIncompatible adamc@705: adamc@705: | (L'.CTuple cs1, L'.CTuple cs2) => adamc@987: ((ListPair.appEq (fn (c1, c2) => unifyCons' env loc c1 c2) (cs1, cs2)) adamc@705: handle ListPair.UnequalLengths => err CIncompatible) adamc@705: adamc@706: | (L'.CProj (c1, n1), _) => projSpecial1 (c1, n1, fn () => err CIncompatible) adamc@706: | (_, L'.CProj (c2, n2)) => projSpecial2 (c2, n2, fn () => err CIncompatible) adamc@706: adamc@623: | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => adamc@623: (unifyKinds env dom1 dom2; adamc@628: unifyKinds env ran1 ran2) adamc@623: adamc@623: | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => adamc@987: unifyCons' (E.pushKRel env x) loc c1 c2 adamc@623: | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => adamc@623: (unifyKinds env k1 k2; adamc@987: unifyCons' env loc c1 c2) adamc@623: | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => adamc@987: unifyCons' (E.pushKRel env x) loc c1 c2 adamc@628: adam@1668: | _ => err CIncompatible)(*; adam@1668: eprefaces "/unifyCons''" [("c1", p_con env c1All), adam@1668: ("c2", p_con env c2All)]*) adamc@403: end adamc@403: adamc@987: and unifyCons env loc c1 c2 = adamc@987: unifyCons' env loc c1 c2 adam@1719: handle CUnify' (env', err) => raise CUnify (c1, c2, env', err) adam@1719: | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg) adamc@403: adamc@628: fun checkCon env e c1 c2 = adamc@987: unifyCons env (#2 e) c1 c2 adam@1719: handle CUnify (c1, c2, env', err) => adam@1719: expError env (Unify (e, c1, c2, env', err)) adamc@628: adamc@628: fun checkPatCon env p c1 c2 = adamc@987: unifyCons env (#2 p) c1 c2 adam@1719: handle CUnify (c1, c2, env', err) => adam@1719: expError env (PatUnify (p, c1, c2, env', err)) adamc@71: adamc@403: fun primType env p = adamc@403: case p of adamc@403: P.Int _ => !int adamc@403: | P.Float _ => !float adamc@403: | P.String _ => !string adamc@821: | P.Char _ => !char adamc@623: adamc@403: datatype constraint = adamc@403: Disjoint of D.goal adamc@403: | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span adamc@403: adam@1591: fun relocConstraint loc c = adam@1591: case c of adam@1591: Disjoint (_, a, b, c, d) => Disjoint (loc, a, b, c, d) adam@1591: | TypeClass (a, b, c, _) => TypeClass (a, b, c, loc) adam@1591: adamc@403: val enD = map Disjoint adamc@403: adamc@634: fun isClassOrFolder env cl = adamc@634: E.isClass env cl adamc@634: orelse case hnormCon env cl of adamc@634: (L'.CKApp (cl, _), _) => adamc@634: (case hnormCon env cl of adamc@634: (L'.CModProj (top_n, [], "folder"), _) => top_n = !top_r adamc@634: | _ => false) adamc@634: | _ => false adamc@634: adam@1303: fun subConInCon env x y = adam@1303: ElabOps.subConInCon x y adam@1303: handle SubUnif => (cunifyError env (TooUnify (#2 x, y)); adam@1303: cerror) adam@1303: adamc@629: fun elabHead (env, denv) infer (e as (_, loc)) t = adamc@403: let adamc@898: fun unravelKind (t, e) = adamc@898: case hnormCon env t of adamc@898: (L'.TKFun (x, t'), _) => adamc@898: let adam@1639: val u = kunif env loc adamc@898: adamc@898: val t'' = subKindInCon (0, u) t' adamc@898: in adamc@898: unravelKind (t'', (L'.EKApp (e, u), loc)) adamc@898: end adamc@898: | t => (e, t, []) adamc@898: adamc@403: fun unravel (t, e) = adamc@628: case hnormCon env t of adamc@628: (L'.TKFun (x, t'), _) => adamc@628: let adam@1639: val u = kunif env loc adamc@628: adamc@628: val t'' = subKindInCon (0, u) t' adamc@628: in adamc@628: unravel (t'', (L'.EKApp (e, u), loc)) adamc@628: end adamc@628: | (L'.TCFun (L'.Implicit, x, k, t'), _) => adamc@628: let adam@1639: val u = cunif env (loc, k) adamc@628: adam@1303: val t'' = subConInCon env (0, u) t' adamc@628: in adamc@628: unravel (t'', (L'.ECApp (e, u), loc)) adamc@628: end adamc@633: | (L'.TFun (dom, ran), _) => adamc@628: let adamc@633: fun default () = (e, t, []) adamc@750: adamc@750: fun isInstance () = adamc@750: if infer <> L.TypesOnly then adamc@750: let adamc@750: val r = ref NONE adamc@750: val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) adamc@750: in adamc@750: (e, t, TypeClass (env, dom, r, loc) :: gs) adamc@750: end adamc@750: else adamc@750: default () adamc@750: adamc@750: fun hasInstance c = adamc@753: case hnormCon env c of adamc@753: (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false, adamc@753: con = fn c => adam@1767: isClassOrFolder env (hnormCon env (c, loc))} c adamc@753: | c => adamc@750: let adamc@753: fun findHead c = adamc@753: case #1 c of adamc@753: L'.CApp (f, _) => findHead f adamc@753: | _ => c adamc@753: adamc@753: val cl = hnormCon env (findHead c) adamc@750: in adamc@750: isClassOrFolder env cl adamc@750: end adamc@628: in adamc@750: if hasInstance dom then adamc@750: isInstance () adamc@750: else adamc@750: default () adamc@628: end adamc@629: | (L'.TDisjoint (r1, r2, t'), loc) => adamc@629: if infer <> L.TypesOnly then adamc@629: let adamc@792: val gs = D.prove env denv (r1, r2, #2 e) adamc@629: val (e, t, gs') = unravel (t', e) adamc@629: in adamc@629: (e, t, enD gs @ gs') adamc@629: end adamc@629: else adamc@629: (e, t, []) adamc@628: | t => (e, t, []) adam@1591: adam@1591: val (e, t, gs) = case infer of adam@1591: L.DontInfer => unravelKind (t, e) adam@1591: | _ => unravel (t, e) adamc@704: in adam@1591: ((#1 e, loc), (#1 t, loc), map (relocConstraint loc) gs) adamc@704: end adamc@15: adamc@628: fun elabPat (pAll as (p, loc), (env, bound)) = adamc@171: let adamc@171: val perror = (L'.PWild, loc) adamc@171: val terror = (L'.CError, loc) adamc@171: val pterror = (perror, terror) adamc@171: val rerror = (pterror, (env, bound)) adamc@171: adamc@191: fun pcon (pc, po, xs, to, dn, dk) = adamc@188: case (po, to) of adamc@188: (NONE, SOME _) => (expError env (PatHasNoArg loc); adamc@188: rerror) adamc@188: | (SOME _, NONE) => (expError env (PatHasArg loc); adamc@188: rerror) adamc@191: | (NONE, NONE) => adamc@191: let adamc@191: val k = (L'.KType, loc) adam@1639: val unifs = map (fn _ => cunif env (loc, k)) xs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@191: in adamc@191: (((L'.PCon (dk, pc, unifs, NONE), loc), dn), adamc@191: (env, bound)) adamc@191: end adamc@188: | (SOME p, SOME t) => adamc@188: let adamc@628: val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) adamc@191: adamc@191: val k = (L'.KType, loc) adam@1639: val unifs = map (fn _ => cunif env (loc, k)) xs adamc@194: val nxs = length unifs - 1 adam@1304: val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, adam@1304: E.mliftConInCon (nxs - i) u) t) t unifs adamc@191: val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs adamc@188: in adamc@628: ignore (checkPatCon env p' pt t); adamc@191: (((L'.PCon (dk, pc, unifs, SOME p'), loc), dn), adamc@188: (env, bound)) adamc@188: end adamc@171: in adamc@171: case p of adam@1639: L.PWild => (((L'.PWild, loc), cunif env (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 adam@1639: cunif env (loc, (L'.KType, loc)) adamc@171: in adamc@182: (((L'.PVar (x, t), loc), t), adamc@171: (E.pushERel env x t, SS.add (bound, x))) adamc@171: end adamc@173: | L.PPrim p => (((L'.PPrim p, loc), primType env p), adamc@173: (env, bound)) adamc@171: | L.PCon ([], x, po) => adamc@171: (case E.lookupConstructor env x of adamc@174: NONE => (expError env (UnboundConstructor (loc, [], x)); adamc@171: rerror) adamc@191: | SOME (dk, n, xs, to, dn) => pcon (L'.PConVar n, po, xs, to, (L'.CNamed dn, loc), dk)) adamc@174: | L.PCon (m1 :: ms, x, po) => adamc@174: (case E.lookupStr env m1 of adamc@174: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@174: rerror) adamc@174: | SOME (n, sgn) => adamc@174: let adamc@174: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@174: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@182: NONE => raise Fail "elabPat: Unknown substructure" adamc@174: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@174: ((L'.StrVar n, loc), sgn) ms adamc@174: in adamc@174: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@174: NONE => (expError env (UnboundConstructor (loc, m1 :: ms, x)); adamc@174: rerror) adamc@191: | SOME (dk, _, xs, to, dn) => pcon (L'.PConProj (n, ms, x), po, xs, to, dn, dk) adamc@174: end) adamc@174: adamc@175: | L.PRecord (xps, flex) => adamc@175: let adamc@175: val (xpts, (env, bound, _)) = adamc@175: ListUtil.foldlMap (fn ((x, p), (env, bound, fbound)) => adamc@175: let adamc@628: val ((p', t), (env, bound)) = elabPat (p, (env, bound)) adamc@175: in adamc@175: if SS.member (fbound, x) then adamc@175: expError env (DuplicatePatField (loc, x)) adamc@175: else adamc@175: (); adamc@175: ((x, p', t), (env, bound, SS.add (fbound, x))) adamc@175: end) adamc@175: (env, bound, SS.empty) xps adamc@175: adamc@175: val k = (L'.KType, loc) adamc@175: val c = (L'.CRecord (k, map (fn (x, _, t) => ((L'.CName x, loc), t)) xpts), loc) adamc@176: val c = adamc@175: if flex then adam@1639: (L'.CConcat (c, cunif env (loc, (L'.KRecord k, loc))), loc) adamc@175: else adamc@176: c adamc@175: in adamc@182: (((L'.PRecord xpts, loc), adamc@175: (L'.TRecord c, loc)), adamc@175: (env, bound)) adamc@175: end adamc@822: adamc@822: | L.PAnnot (p, t) => adamc@822: let adamc@822: val ((p', pt), (env, bound)) = elabPat (p, (env, bound)) adamc@822: val (t', k, _) = elabCon (env, D.empty) t adamc@822: in adamc@822: checkPatCon env p' pt t'; adamc@822: ((p', t'), (env, bound)) adamc@822: end adamc@171: end adamc@171: adamc@819: (* This exhaustiveness checking follows Luc Maranget's paper "Warnings for pattern matching." *) adamc@819: fun exhaustive (env, t, ps, loc) = adamc@819: let adamc@819: fun fail n = raise Fail ("Elaborate.exhaustive: Impossible " ^ Int.toString n) adamc@819: adamc@819: fun patConNum pc = adamc@819: case pc of adamc@819: L'.PConVar n => n adamc@819: | L'.PConProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectConstructor env {str = str, sgn = sgn, field = x} of adamc@819: NONE => raise Fail "exhaustive: Can't project datatype" adamc@819: | SOME (_, n, _, _, _) => n adamc@819: end adamc@819: adamc@819: fun nameOfNum (t, n) = adamc@819: case t of adamc@819: L'.CModProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@819: NONE => raise Fail "exhaustive: Can't project datatype" adamc@819: | SOME (_, cons) => adamc@819: case ListUtil.search (fn (name, n', _) => adamc@819: if n' = n then adamc@819: SOME name adamc@819: else adamc@819: NONE) cons of adamc@819: NONE => fail 9 adamc@819: | SOME name => L'.PConProj (m1, ms, name) adamc@819: end adamc@819: | _ => L'.PConVar n adamc@819: adamc@819: fun S (args, c, P) = adamc@819: List.mapPartial adamc@819: (fn [] => fail 1 adamc@819: | p1 :: ps => adamc@819: let adamc@819: val loc = #2 p1 adamc@819: adamc@819: fun wild () = adamc@819: SOME (map (fn _ => (L'.PWild, loc)) args @ ps) adamc@819: in adamc@819: case #1 p1 of adamc@819: L'.PPrim _ => NONE adamc@819: | L'.PCon (_, c', _, NONE) => adamc@819: if patConNum c' = c then adamc@819: SOME ps adamc@819: else adamc@819: NONE adamc@819: | L'.PCon (_, c', _, SOME p) => adamc@819: if patConNum c' = c then adamc@819: SOME (p :: ps) adamc@819: else adamc@819: NONE adamc@819: | L'.PRecord xpts => adamc@819: SOME (map (fn x => adamc@819: case ListUtil.search (fn (x', p, _) => adamc@819: if x = x' then adamc@819: SOME p adamc@819: else adamc@819: NONE) xpts of adamc@819: NONE => (L'.PWild, loc) adamc@819: | SOME p => p) args @ ps) adamc@819: | L'.PWild => wild () adamc@819: | L'.PVar _ => wild () adamc@819: end) adamc@819: P adamc@819: adamc@819: fun D P = adamc@819: List.mapPartial adamc@819: (fn [] => fail 2 adamc@819: | (p1, _) :: ps => adamc@819: case p1 of adamc@819: L'.PWild => SOME ps adamc@819: | L'.PVar _ => SOME ps adamc@819: | L'.PPrim _ => NONE adamc@819: | L'.PCon _ => NONE adamc@819: | L'.PRecord _ => NONE) adamc@819: P adamc@819: adamc@819: fun I (P, q) = adamc@819: (*(prefaces "I" [("P", p_list (fn P' => box [PD.string "[", p_list (p_pat env) P', PD.string "]"]) P), adamc@819: ("q", p_list (p_con env) q)];*) adamc@819: case q of adamc@819: [] => (case P of adamc@819: [] => SOME [] adamc@819: | _ => NONE) adamc@819: | q1 :: qs => adamc@819: let adamc@819: val loc = #2 q1 adamc@819: adamc@819: fun unapp (t, acc) = adamc@830: case #1 t of adamc@830: L'.CApp (t, arg) => unapp (t, arg :: acc) adamc@819: | _ => (t, rev acc) adamc@819: adamc@830: val (t1, args) = unapp (hnormCon env q1, []) adamc@830: val t1 = hnormCon env t1 adam@1303: fun doSub t = foldl (fn (arg, t) => subConInCon env (0, arg) t) t args adamc@819: adamc@819: fun dtype (dtO, names) = adamc@819: let adamc@819: val nameSet = IS.addList (IS.empty, names) adamc@819: val nameSet = foldl (fn (ps, nameSet) => adamc@819: case ps of adamc@819: [] => fail 4 adamc@819: | (L'.PCon (_, pc, _, _), _) :: _ => adamc@819: (IS.delete (nameSet, patConNum pc) adamc@819: handle NotFound => nameSet) adamc@819: | _ => nameSet) adamc@819: nameSet P adamc@819: in adamc@819: nameSet adamc@819: end adamc@819: adamc@819: fun default () = (NONE, IS.singleton 0, []) adamc@819: adamc@819: val (dtO, unused, cons) = adamc@830: case #1 t1 of adamc@819: L'.CNamed n => adamc@819: let adamc@819: val dt = E.lookupDatatype env n adamc@819: val cons = E.constructors dt adamc@819: in adamc@819: (SOME dt, adamc@819: dtype (SOME dt, map #2 cons), adamc@819: map (fn (_, n, co) => adamc@819: (n, adamc@819: case co of adamc@819: NONE => [] adamc@819: | SOME t => [("", doSub t)])) cons) adamc@819: end adamc@819: | L'.CModProj (m1, ms, x) => adamc@819: let adamc@819: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@819: in adamc@819: case E.projectDatatype env {str = str, sgn = sgn, field = x} of adamc@819: NONE => default () adamc@819: | SOME (_, cons) => adamc@819: (NONE, adamc@819: dtype (NONE, map #2 cons), adamc@819: map (fn (s, _, co) => adamc@819: (patConNum (L'.PConProj (m1, ms, s)), adamc@819: case co of adamc@819: NONE => [] adamc@819: | SOME t => [("", doSub t)])) cons) adamc@819: end adamc@830: | L'.TRecord t => adamc@830: (case #1 (hnormCon env t) of adamc@830: L'.CRecord (_, xts) => adamc@830: let adamc@830: val xts = map (fn ((L'.CName x, _), co) => SOME (x, co) adamc@830: | _ => NONE) xts adamc@830: in adamc@830: if List.all Option.isSome xts then adamc@830: let adamc@830: val xts = List.mapPartial (fn x => x) xts adamc@830: val xts = ListMergeSort.sort (fn ((x1, _), (x2, _)) => adamc@830: String.compare (x1, x2) = GREATER) xts adamc@830: in adamc@830: (NONE, IS.empty, [(0, xts)]) adamc@830: end adamc@830: else adamc@830: default () adamc@830: end adamc@830: | _ => default ()) adamc@819: | _ => default () adamc@819: in adamc@819: if IS.isEmpty unused then adamc@819: let adamc@819: fun recurse cons = adamc@819: case cons of adamc@819: [] => NONE adamc@819: | (name, args) :: cons => adamc@819: case I (S (map #1 args, name, P), adamc@819: map #2 args @ qs) of adamc@819: NONE => recurse cons adamc@819: | SOME ps => adamc@819: let adamc@819: val nargs = length args adamc@819: val argPs = List.take (ps, nargs) adamc@819: val restPs = List.drop (ps, nargs) adamc@819: adamc@819: val p = case name of adamc@819: 0 => L'.PRecord (ListPair.map adamc@819: (fn ((name, t), p) => (name, p, t)) adamc@819: (args, argPs)) adamc@830: | _ => L'.PCon (L'.Default, nameOfNum (#1 t1, name), [], adamc@819: case argPs of adamc@819: [] => NONE adamc@819: | [p] => SOME p adamc@819: | _ => fail 3) adamc@819: in adamc@819: SOME ((p, loc) :: restPs) adamc@819: end adamc@819: in adamc@819: recurse cons adamc@819: end adamc@819: else adamc@819: case I (D P, qs) of adamc@819: NONE => NONE adamc@819: | SOME ps => adamc@819: let adamc@819: val p = case cons of adamc@819: [] => L'.PWild adamc@819: | (0, _) :: _ => L'.PWild adamc@819: | _ => adamc@819: case IS.find (fn _ => true) unused of adamc@819: NONE => fail 6 adamc@819: | SOME name => adamc@819: case ListUtil.search (fn (name', args) => adamc@819: if name = name' then adamc@819: SOME (name', args) adamc@819: else adamc@819: NONE) cons of adamc@819: SOME (n, []) => adamc@830: L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], NONE) adamc@819: | SOME (n, [_]) => adamc@830: L'.PCon (L'.Default, nameOfNum (#1 t1, n), [], SOME (L'.PWild, loc)) adamc@819: | _ => fail 7 adamc@819: in adamc@819: SOME ((p, loc) :: ps) adamc@819: end adamc@819: end adamc@819: in adamc@819: case I (map (fn x => [x]) ps, [t]) of adamc@819: NONE => NONE adamc@819: | SOME [p] => SOME p adamc@819: | _ => fail 7 adamc@819: end adamc@819: adamc@217: fun unmodCon env (c, loc) = adamc@217: case c of adamc@217: L'.CNamed n => adamc@217: (case E.lookupCNamed env n of adamc@217: (_, _, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc)) adamc@217: | L'.CModProj (m1, ms, x) => adamc@217: let adamc@217: val (str, sgn) = E.chaseMpath env (m1, ms) adamc@217: in adamc@217: case E.projectCon env {str = str, sgn = sgn, field = x} of adamc@217: NONE => raise Fail "unmodCon: Can't projectCon" adamc@217: | SOME (_, SOME (c as (L'.CModProj _, _))) => unmodCon env c adamc@217: | _ => (c, loc) adamc@217: end adamc@217: | _ => (c, loc) adamc@217: adamc@721: fun normClassKey env c = adamc@467: let adamc@721: val c = hnormCon env c adamc@467: in adamc@467: case #1 c of adamc@467: L'.CApp (c1, c2) => adamc@467: let adamc@721: val c1 = normClassKey env c1 adamc@721: val c2 = normClassKey env c2 adamc@467: in adamc@467: (L'.CApp (c1, c2), #2 c) adamc@467: end adamc@721: | L'.CRecord (k, xcs) => (L'.CRecord (k, map (fn (x, c) => (normClassKey env x, adamc@721: normClassKey env c)) xcs), #2 c) adamc@721: | _ => unmodCon env c adamc@467: end adamc@467: adamc@467: fun normClassConstraint env (c, loc) = adamc@217: case c of adamc@217: L'.CApp (f, x) => adamc@217: let adamc@721: val f = normClassKey env f adamc@467: val x = normClassKey env x adamc@217: in adamc@467: (L'.CApp (f, x), loc) adamc@217: end adamc@674: | L'.TFun (c1, c2) => adamc@674: let adamc@674: val c1 = normClassConstraint env c1 adamc@674: val c2 = normClassConstraint env c2 adamc@674: in adamc@674: (L'.TFun (c1, c2), loc) adamc@674: end adamc@674: | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) adam@1639: | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => normClassConstraint env (E.mliftConInCon nl c) adamc@721: | _ => unmodCon env (c, loc) adamc@216: adamc@1093: fun findHead e e' = adamc@1093: let adamc@1093: fun findHead (e, _) = adamc@1093: case e of adamc@1093: L.EVar (_, _, infer) => adamc@1093: let adamc@1093: fun findHead' (e, _) = adamc@1093: case e of adamc@1093: L'.ENamed _ => true adamc@1093: | L'.EModProj _ => true adam@1472: | L'.ERel _ => true adamc@1093: | L'.EApp (e, _) => findHead' e adamc@1093: | L'.ECApp (e, _) => findHead' e adamc@1093: | L'.EKApp (e, _) => findHead' e adamc@1093: | _ => false adamc@1093: in adamc@1093: if findHead' e' then adamc@1093: SOME infer adamc@1093: else adamc@1093: NONE adamc@1093: end adamc@1093: | L.EApp (e, _) => findHead e adamc@1093: | L.ECApp (e, _) => findHead e adamc@1093: | L.EDisjointApp e => findHead e adamc@1093: | _ => NONE adamc@1093: in adamc@1093: findHead e adamc@1093: end adamc@1093: adam@1640: datatype needed = Needed of {Cons : (L'.kind * int) SM.map, adam@1640: NextCon : int, adamc@1264: Constraints : (E.env * (L'.con * L'.con) * ErrorMsg.span) list, adamc@1264: Vals : SS.set, adamc@1270: Mods : (E.env * needed) SM.map} adamc@1264: adam@1640: fun ncons (Needed r) = map (fn (k, (v, _)) => (k, v)) adam@1640: (ListMergeSort.sort (fn ((_, (_, n1)), (_, (_, n2))) => n1 > n2) adam@1640: (SM.listItemsi (#Cons r))) adamc@1264: fun nconstraints (Needed r) = #Constraints r adamc@1264: fun nvals (Needed r) = #Vals r adamc@1264: fun nmods (Needed r) = #Mods r adamc@1264: adamc@1264: val nempty = Needed {Cons = SM.empty, adam@1640: NextCon = 0, adamc@1264: Constraints = nil, adamc@1264: Vals = SS.empty, adamc@1264: Mods = SM.empty} adamc@1264: adamc@1264: fun naddCon (r : needed, k, v) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adam@1640: Needed {Cons = SM.insert (#Cons r, k, (v, #NextCon r)), adam@1640: NextCon = #NextCon r + 1, adamc@1264: Constraints = #Constraints r, adamc@1264: Vals = #Vals r, adamc@1264: Mods = #Mods r} adamc@1264: end adamc@1264: adamc@1264: fun naddConstraint (r : needed, v) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adamc@1264: Needed {Cons = #Cons r, adam@1640: NextCon = #NextCon r, adamc@1264: Constraints = v :: #Constraints r, adamc@1264: Vals = #Vals r, adamc@1264: Mods = #Mods r} adamc@1264: end adamc@1264: adamc@1264: fun naddVal (r : needed, k) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adamc@1264: Needed {Cons = #Cons r, adam@1640: NextCon = #NextCon r, adamc@1264: Constraints = #Constraints r, adamc@1264: Vals = SS.add (#Vals r, k), adamc@1264: Mods = #Mods r} adamc@1264: end adamc@1264: adamc@1264: fun naddMod (r : needed, k, v) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adamc@1264: Needed {Cons = #Cons r, adam@1640: NextCon = #NextCon r, adamc@1264: Constraints = #Constraints r, adamc@1264: Vals = #Vals r, adamc@1264: Mods = SM.insert (#Mods r, k, v)} adamc@1264: end adamc@1264: adamc@1264: fun ndelCon (r : needed, k) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adamc@1264: Needed {Cons = #1 (SM.remove (#Cons r, k)) handle NotFound => #Cons r, adam@1640: NextCon = #NextCon r, adamc@1264: Constraints = #Constraints r, adamc@1264: Vals = #Vals r, adamc@1264: Mods = #Mods r} adamc@1264: end adamc@1264: adamc@1264: fun ndelVal (r : needed, k) = adamc@1264: let adamc@1264: val Needed r = r adamc@1264: in adamc@1264: Needed {Cons = #Cons r, adam@1640: NextCon = #NextCon r, adamc@1264: Constraints = #Constraints r, adamc@1264: Vals = SS.delete (#Vals r, k) handle NotFound => #Vals r, adamc@1264: Mods = #Mods r} adamc@1264: end adamc@1264: adam@1591: fun chaseUnifs c = adam@1591: case #1 c of adam@1639: L'.CUnif (_, _, _, _, ref (L'.Known c)) => chaseUnifs c adam@1591: | _ => c adam@1591: adam@2092: val consEqSimple = adam@2092: let adam@2092: fun ces env (c1 : L'.con, c2 : L'.con) = adam@2092: let adam@2092: val c1 = hnormCon env c1 adam@2092: val c2 = hnormCon env c2 adam@2092: in adam@2092: case (#1 c1, #1 c2) of adam@2092: (L'.CRel n1, L'.CRel n2) => n1 = n2 adam@2092: | (L'.CNamed n1, L'.CNamed n2) => adam@2092: n1 = n2 orelse adam@2092: (case #3 (E.lookupCNamed env n1) of adam@2092: SOME (L'.CNamed n2', _) => n2' = n1 adam@2092: | _ => false) adam@2092: | (L'.CModProj n1, L'.CModProj n2) => n1 = n2 adam@2092: | (L'.CApp (f1, x1), L'.CApp (f2, x2)) => ces env (f1, f2) andalso ces env (x1, x2) adam@2092: | (L'.CAbs (x1, k1, c1), L'.CAbs (_, _, c2)) => ces (E.pushCRel env x1 k1) (c1, c2) adam@2092: | (L'.CName x1, L'.CName x2) => x1 = x2 adam@2092: | (L'.CRecord (_, xts1), L'.CRecord (_, xts2)) => adam@2092: ListPair.all (fn ((x1, t1), (x2, t2)) => adam@2092: ces env (x1, x2) andalso ces env (t2, t2)) (xts1, xts2) adam@2092: | (L'.CConcat (x1, y1), L'.CConcat (x2, y2)) => adam@2092: ces env (x1, x2) andalso ces env (y1, y2) adam@2092: | (L'.CMap _, L'.CMap _) => true adam@2092: | (L'.CUnit, L'.CUnit) => true adam@2092: | (L'.CTuple cs1, L'.CTuple cs2) => ListPair.all (ces env) (cs1, cs2) adam@2092: | (L'.CProj (c1, n1), L'.CProj (c2, n2)) => ces env (c1, c2) andalso n1 = n2 adam@2092: | (L'.CUnif (_, _, _, _, r1), L'.CUnif (_, _, _, _, r2)) => r1 = r2 adam@2092: | _ => false adam@2092: end adam@2092: in adam@2092: ces adam@2092: end adam@2092: adam@2092: adamc@92: fun elabExp (env, denv) (eAll as (e, loc)) = adamc@91: let adamc@848: (*val () = eprefaces "elabExp" [("eAll", SourcePrint.p_exp eAll)]*) adamc@514: (*val befor = Time.now ()*) adamc@280: adamc@280: val r = case e of adamc@91: L.EAnnot (e, t) => adamc@91: let adamc@91: val (e', et, gs1) = elabExp (env, denv) e adamc@91: val (t', _, gs2) = elabCon (env, denv) t adamc@91: in adamc@628: checkCon env e' et t'; adamc@628: (e', t', gs1 @ enD gs2) adamc@91: end adamc@34: adamc@91: | L.EPrim p => ((L'.EPrim p, loc), primType env p, []) adamc@403: | L.EVar ([], s, infer) => adamc@91: (case E.lookupE env s of adamc@91: E.NotBound => adamc@91: (expError env (UnboundExp (loc, s)); adamc@91: (eerror, cerror, [])) adamc@629: | E.Rel (n, t) => elabHead (env, denv) infer (L'.ERel n, loc) t adamc@629: | E.Named (n, t) => elabHead (env, denv) infer (L'.ENamed n, loc) t) adamc@403: | L.EVar (m1 :: ms, s, infer) => adamc@91: (case E.lookupStr env m1 of adamc@91: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@91: (eerror, cerror, [])) adamc@91: | SOME (n, sgn) => adamc@91: let adamc@91: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@91: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@91: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@91: (strerror, sgnerror)) adamc@91: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@91: ((L'.StrVar n, loc), sgn) ms adamc@10: adamc@91: val t = case E.projectVal env {sgn = sgn, str = str, field = s} of adamc@91: NONE => (expError env (UnboundExp (loc, s)); adamc@91: cerror) adamc@91: | SOME t => t adamc@91: in adamc@629: elabHead (env, denv) infer (L'.EModProj (n, ms, s), loc) t adamc@91: end) adamc@86: adamc@349: | L.EWild => adamc@210: let adamc@349: val r = ref NONE adam@1639: val c = cunif env (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@1093: adamc@403: val (e2', t2, gs2) = elabExp (env, denv) e2 adamc@71: adam@1639: val dom = cunif env (loc, ktype) adam@1639: val ran = cunif env (loc, ktype) adamc@838: val t = (L'.TFun (dom, ran), loc) adamc@1093: adamc@1093: val () = checkCon env e1' t1 t adamc@1093: val () = checkCon env e2' t2 dom adamc@1093: adamc@1093: val ef = (L'.EApp (e1', e2'), loc) adamc@1093: val (ef, et, gs3) = adamc@1093: case findHead e1 e1' of adam@1591: NONE => (ef, (#1 (chaseUnifs ran), loc), []) adamc@1093: | SOME infer => elabHead (env, denv) infer ef ran adamc@91: in adamc@1093: (ef, et, gs1 @ gs2 @ gs3) adamc@91: end adamc@91: | L.EAbs (x, to, e) => adamc@91: let adamc@91: val (t', gs1) = case to of adam@1639: NONE => (cunif env (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@1093: adamc@328: val oldEt = et adamc@403: val (c', ck, gs2) = elabCon (env, denv) c adamc@628: val (et', _) = hnormCon env et adamc@91: in adamc@91: case et' of adamc@91: L'.CError => (eerror, cerror, []) adamc@328: | L'.TCFun (_, x, k, eb) => adamc@91: let adamc@91: val () = checkKind env c' ck k adam@1303: val eb' = subConInCon env (0, c') eb adamc@1093: adamc@1093: val ef = (L'.ECApp (e', c'), loc) adamc@1093: val (ef, eb', gs3) = adamc@1093: case findHead e e' of adamc@1093: NONE => (ef, eb', []) adamc@1093: | SOME infer => elabHead (env, denv) infer ef eb' 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')];*) adam@1591: (ef, (#1 eb', loc), gs1 @ enD gs2 @ 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@623: val k' = elabKind env k adamc@328: adamc@328: val env' = E.pushCRel env x k' adamc@328: val (e', et, gs) = elabExp (env', D.enter denv) e adamc@91: in adamc@91: ((L'.ECAbs (expl', x, k', e'), loc), adamc@91: (L'.TCFun (expl', x, k', et), loc), adamc@91: gs) adamc@91: end adamc@623: | L.EKAbs (x, e) => adamc@623: let adamc@623: val env' = E.pushKRel env x adamc@623: val (e', et, gs) = elabExp (env', denv) e adamc@623: in adamc@623: ((L'.EKAbs (x, e'), loc), adamc@623: (L'.TKFun (x, et), loc), adamc@623: gs) adamc@623: end adamc@91: adamc@91: | L.EDisjoint (c1, c2, e) => adamc@91: let adamc@91: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@91: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@91: adam@1639: val ku1 = kunif env loc adam@1639: val ku2 = kunif env loc adamc@91: adamc@628: val denv' = D.assert env denv (c1', c2') adamc@628: val (e', t, gs3) = elabExp (env, denv') e adamc@91: in adamc@91: checkKind env c1' k1 (L'.KRecord ku1, loc); adamc@91: checkKind env c2' k2 (L'.KRecord ku2, loc); adamc@91: adamc@628: (e', (L'.TDisjoint (c1', c2', t), loc), enD gs1 @ enD gs2 @ gs3) adamc@91: end adamc@629: | L.EDisjointApp e => adamc@629: let adamc@629: val (e', t, gs1) = elabExp (env, denv) e adamc@629: adam@1639: val k1 = kunif env loc adam@1639: val c1 = cunif env (loc, (L'.KRecord k1, loc)) adam@1639: val k2 = kunif env loc adam@1639: val c2 = cunif env (loc, (L'.KRecord k2, loc)) adam@1639: val t' = cunif env (loc, ktype) adamc@629: val () = checkCon env e' t (L'.TDisjoint (c1, c2, t'), loc) adamc@629: val gs2 = D.prove env denv (c1, c2, loc) adamc@629: in adam@1591: (e', (#1 (chaseUnifs t'), loc), enD gs2 @ gs1) adamc@629: end adamc@91: adam@2009: | L.ERecord (xes, flex) => adamc@91: let adam@2009: val () = if flex then adam@2009: expError env (IllegalFlex eAll) adam@2009: else adam@2009: () adam@2009: 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: adam@1639: val ft = cunif env (loc, ktype) adam@1639: val rest = cunif env (loc, ktype_record) adamc@91: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (first, rest), loc), loc); adamc@628: val gs3 = D.prove env denv (first, rest, loc) adamc@91: in adamc@628: ((L'.EField (e', c', {field = ft, rest = rest}), loc), ft, gs1 @ enD gs2 @ enD gs3) adamc@91: end adamc@91: adamc@445: | L.EConcat (e1, e2) => adamc@339: let adamc@339: val (e1', e1t, gs1) = elabExp (env, denv) e1 adamc@445: val (e2', e2t, gs2) = elabExp (env, denv) e2 adamc@445: adam@1639: val r1 = cunif env (loc, ktype_record) adam@1639: val r2 = cunif env (loc, ktype_record) adamc@445: adamc@629: val () = checkCon env e1' e1t (L'.TRecord r1, loc) adamc@629: val () = checkCon env e2' e2t (L'.TRecord r2, loc) adamc@629: adamc@628: val gs3 = D.prove env denv (r1, r2, loc) adamc@339: in adamc@445: ((L'.EConcat (e1', r1, e2', r2), loc), adamc@445: (L'.TRecord ((L'.CConcat (r1, r2), loc)), loc), adamc@628: gs1 @ gs2 @ enD gs3) adamc@339: end adamc@149: | L.ECut (e, c) => adamc@149: let adamc@149: val (e', et, gs1) = elabExp (env, denv) e adamc@149: val (c', ck, gs2) = elabCon (env, denv) c adamc@149: adam@1639: val ft = cunif env (loc, ktype) adam@1639: val rest = cunif env (loc, ktype_record) adamc@149: val first = (L'.CRecord (ktype, [(c', ft)]), loc) adamc@629: adamc@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (first, rest), loc), loc) adamc@149: adamc@628: val gs3 = D.prove env denv (first, rest, loc) adamc@149: in adam@1299: checkKind env c' ck kname; adamc@228: ((L'.ECut (e', c', {field = ft, rest = rest}), loc), (L'.TRecord rest, loc), adamc@628: gs1 @ enD gs2 @ enD gs3) adamc@149: end adamc@493: | L.ECutMulti (e, c) => adamc@493: let adamc@493: val (e', et, gs1) = elabExp (env, denv) e adamc@493: val (c', ck, gs2) = elabCon (env, denv) c adamc@493: adam@1639: val rest = cunif env (loc, ktype_record) adamc@629: adamc@629: val () = checkCon env e' et adamc@629: (L'.TRecord (L'.CConcat (c', rest), loc), loc) adamc@493: adamc@628: val gs3 = D.prove env denv (c', rest, loc) adamc@493: in adam@1299: checkKind env c' ck (L'.KRecord ktype, loc); adamc@493: ((L'.ECutMulti (e', c', {rest = rest}), loc), (L'.TRecord rest, loc), adamc@628: gs1 @ enD gs2 @ enD gs3) adamc@493: end adamc@149: adamc@171: | L.ECase (e, pes) => adamc@171: let adamc@171: val (e', et, gs1) = elabExp (env, denv) e adam@1639: val result = cunif env (loc, (L'.KType, loc)) adamc@171: val (pes', gs) = ListUtil.foldlMap adamc@171: (fn ((p, e), gs) => adamc@171: let adamc@628: val ((p', pt), (env, _)) = elabPat (p, (env, SS.empty)) adamc@628: adamc@629: val (e', et', gs1) = elabExp (env, denv) e adamc@171: in adamc@628: checkPatCon env p' pt et; adamc@629: checkCon env e' et' result; adamc@628: ((p', e'), gs1 @ gs) adamc@171: end) adamc@171: gs1 pes adamc@171: in adamc@819: case exhaustive (env, et, map #1 pes', loc) of adamc@819: NONE => () adamc@830: | SOME p => if !mayDelay then adamc@830: delayedExhaustives := (env, et, map #1 pes', loc) :: !delayedExhaustives adamc@830: else adamc@830: expError env (Inexhaustive (loc, p)); adamc@172: adamc@628: ((L'.ECase (e', pes', {disc = et, result = result}), loc), result, gs) adamc@171: end adamc@447: adamc@447: | L.ELet (eds, e) => adamc@447: let adamc@447: val (eds, (env, gs1)) = ListUtil.foldlMap (elabEdecl denv) (env, []) eds adamc@447: val (e, t, gs2) = elabExp (env, denv) e adamc@447: in adamc@825: ((L'.ELet (eds, e, t), loc), t, gs1 @ gs2) adamc@447: end adamc@280: in adamc@819: (*prefaces "/elabExp" [("e", SourcePrint.p_exp eAll)];*) adamc@280: r adamc@91: end adamc@31: adamc@628: and elabEdecl denv (dAll as (d, loc), (env, gs)) = adamc@447: let adamc@447: val r = adamc@447: case d of adamc@825: L.EDVal (p, e) => adamc@447: let adamc@825: val ((p', pt), (env', _)) = elabPat (p, (env, SS.empty)) adamc@825: val (e', et, gs1) = elabExp (env, denv) e adamc@825: adamc@825: val () = checkCon env e' et pt adamc@825: adam@1554: val env' = E.patBinds env p' adam@1554: (* Redo to get proper detection of type class witnesses *) adam@1554: adamc@825: val pt = normClassConstraint env pt adamc@447: in adamc@830: case exhaustive (env, et, [p'], loc) of adamc@830: NONE => () adamc@830: | SOME p => if !mayDelay then adamc@830: delayedExhaustives := (env, et, [p'], loc) :: !delayedExhaustives adamc@830: else adamc@830: expError env (Inexhaustive (loc, p)); adamc@830: adamc@825: ((L'.EDVal (p', pt, e'), loc), (env', gs1 @ gs)) adamc@447: end adamc@447: | L.EDValRec vis => adamc@447: let adamc@447: fun allowable (e, _) = adamc@447: case e of adamc@447: L.EAbs _ => true adamc@447: | L.ECAbs (_, _, _, e) => allowable e adamc@623: | L.EKAbs (_, e) => allowable e adamc@447: | L.EDisjoint (_, _, e) => allowable e adamc@447: | _ => false adamc@447: adamc@447: val (vis, gs) = ListUtil.foldlMap adamc@447: (fn ((x, co, e), gs) => adamc@447: let adamc@447: val (c', _, gs1) = case co of adam@1639: NONE => (cunif env (loc, ktype), ktype, []) adamc@447: | SOME c => elabCon (env, denv) c adamc@447: in adamc@447: ((x, c', e), enD gs1 @ gs) adamc@447: end) gs vis adamc@447: adamc@447: val env = foldl (fn ((x, c', _), env) => E.pushERel env x c') env vis adamc@447: adamc@447: val (vis, gs) = ListUtil.foldlMap (fn ((x, c', e), gs) => adamc@447: let adamc@447: val (e', et, gs1) = elabExp (env, denv) e adamc@447: in adamc@628: checkCon env e' et c'; adamc@447: if allowable e then adamc@447: () adamc@447: else adamc@447: expError env (IllegalRec (x, e')); adamc@628: ((x, c', e'), gs1 @ gs) adamc@447: end) gs vis adamc@447: in adamc@447: ((L'.EDValRec vis, loc), (env, gs)) adamc@447: end adamc@447: in adamc@447: r adamc@447: end adamc@447: adamc@42: val hnormSgn = E.hnormSgn adamc@31: adamc@210: fun tableOf () = (L'.CModProj (!basis_r, [], "sql_table"), ErrorMsg.dummySpan) adamc@338: fun sequenceOf () = (L'.CModProj (!basis_r, [], "sql_sequence"), ErrorMsg.dummySpan) adamc@754: fun viewOf () = (L'.CModProj (!basis_r, [], "sql_view"), ErrorMsg.dummySpan) adamc@754: fun queryOf () = (L'.CModProj (!basis_r, [], "sql_query"), ErrorMsg.dummySpan) adamc@459: fun cookieOf () = (L'.CModProj (!basis_r, [], "http_cookie"), ErrorMsg.dummySpan) adamc@718: fun styleOf () = (L'.CModProj (!basis_r, [], "css_class"), ErrorMsg.dummySpan) adamc@205: adamc@469: fun dopenConstraints (loc, env, denv) {str, strs} = adamc@469: case E.lookupStr env str of adamc@469: NONE => (strError env (UnboundStr (loc, str)); adamc@469: denv) adamc@469: | SOME (n, sgn) => adamc@469: let adamc@469: val (st, sgn) = foldl (fn (m, (str, sgn)) => adamc@469: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@469: NONE => (strError env (UnboundStr (loc, m)); adamc@469: (strerror, sgnerror)) adamc@469: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@469: ((L'.StrVar n, loc), sgn) strs adamc@1030: adamc@1030: fun collect first (st, sgn) = adamc@1030: case E.projectConstraints env {sgn = sgn, str = st} of adamc@1182: NONE => [] adamc@1030: | SOME cs => adamc@1030: case #1 (hnormSgn env sgn) of adamc@1030: L'.SgnConst sgis => adamc@1030: foldl (fn (sgi, cs) => adamc@1030: case #1 sgi of adamc@1030: L'.SgiStr (x, _, _) => adamc@1030: (case E.projectStr env {sgn = sgn, str = st, field = x} of adamc@1030: NONE => raise Fail "Elaborate: projectStr in collect" adamc@1030: | SOME sgn' => adamc@1030: List.revAppend (collect false ((L'.StrProj (st, x), loc), sgn'), adamc@1030: cs)) adamc@1030: | _ => cs) cs sgis adamc@1030: | _ => cs adamc@469: in adamc@1030: foldl (fn ((c1, c2), denv) => adamc@1030: D.assert env denv (c1, c2)) denv (collect true (st, sgn)) adamc@469: end adamc@469: adamc@88: fun elabSgn_item ((sgi, loc), (env, denv, gs)) = adamc@1270: ((*Print.preface ("elabSgi", SourcePrint.p_sgn_item (sgi, loc));*) adamc@1270: case sgi of adamc@1270: L.SgiConAbs (x, k) => adamc@1270: let adamc@1270: val k' = elabKind env k adamc@1270: adamc@1270: val (env', n) = E.pushCNamed env x k' NONE adamc@1270: in adamc@1270: ([(L'.SgiConAbs (x, n, k'), loc)], (env', denv, gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiCon (x, ko, c) => adamc@1270: let adamc@1270: val k' = case ko of adam@1639: NONE => kunif env loc adamc@1270: | SOME k => elabKind env k adamc@1270: adamc@1270: val (c', ck, gs') = elabCon (env, denv) c adamc@1270: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@1270: in adamc@1270: checkKind env c' ck k'; adamc@1270: adamc@1270: ([(L'.SgiCon (x, n, k', c'), loc)], (env', denv, gs' @ gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiDatatype dts => adamc@1270: let adamc@1270: val k = (L'.KType, loc) adamc@1270: adamc@1270: val (dts, env) = ListUtil.foldlMap (fn ((x, xs, xcs), env) => adamc@1270: let adamc@1270: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@1270: val (env, n) = E.pushCNamed env x k' NONE adamc@1270: in adamc@1270: ((x, n, xs, xcs), env) adamc@1270: end) adamc@1270: env dts adamc@1270: adamc@1270: val (dts, env) = ListUtil.foldlMap adamc@1270: (fn ((x, n, xs, xcs), env) => adamc@1270: let adamc@1270: val t = (L'.CNamed n, loc) adamc@1270: val nxs = length xs - 1 adamc@1270: val t = ListUtil.foldli (fn (i, _, t) => adamc@1270: (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@1270: adamc@1270: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@1270: (E.pushCRel env' x k, adamc@1270: D.enter denv')) (env, denv) xs adamc@1270: adamc@1270: val (xcs, (used, env, gs)) = adamc@1270: ListUtil.foldlMap adamc@1270: (fn ((x, to), (used, env, gs)) => adamc@1270: let adamc@1270: val (to, t, gs') = case to of adamc@1270: NONE => (NONE, t, gs) adamc@1270: | SOME t' => adamc@1270: let adamc@1270: val (t', tk, gs') = adamc@1270: elabCon (env', denv') t' adamc@1270: in adamc@1270: checkKind env' t' tk k; adamc@1270: (SOME t', adamc@1270: (L'.TFun (t', t), loc), adamc@1270: gs' @ gs) adamc@1270: end adamc@1270: val t = foldl (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@1270: t xs adamc@1270: adamc@1270: val (env, n') = E.pushENamed env x t adamc@1270: in adamc@1270: if SS.member (used, x) then adamc@1270: strError env (DuplicateConstructor (x, loc)) adamc@1270: else adamc@1270: (); adamc@1270: ((x, n', to), (SS.add (used, x), env, gs')) adamc@1270: end) adamc@1270: (SS.empty, env, []) xcs adamc@1270: in adamc@1270: ((x, n, xs, xcs), E.pushDatatype env n xs xcs) adamc@1270: end) adamc@1270: env dts adamc@1270: in adamc@1270: ([(L'.SgiDatatype dts, loc)], (env, denv, gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiDatatypeImp (_, [], _) => raise Fail "Empty SgiDatatypeImp" adamc@1270: adamc@1270: | L.SgiDatatypeImp (x, m1 :: ms, s) => adamc@1270: (case E.lookupStr env m1 of adamc@1270: NONE => (strError env (UnboundStr (loc, m1)); adamc@1270: ([], (env, denv, gs))) adamc@1270: | SOME (n, sgn) => adamc@1270: let adamc@1270: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@1270: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@1270: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@1270: (strerror, sgnerror)) adamc@1270: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@1270: ((L'.StrVar n, loc), sgn) ms adamc@1270: in adamc@1270: case hnormCon env (L'.CModProj (n, ms, s), loc) of adamc@1270: (L'.CModProj (n, ms, s), _) => adamc@1270: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@1270: NONE => (conError env (UnboundDatatype (loc, s)); adamc@1270: ([], (env, denv, []))) adamc@1270: | SOME (xs, xncs) => adamc@1270: let adamc@1270: val k = (L'.KType, loc) adamc@1270: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@1270: adamc@1270: val t = (L'.CModProj (n, ms, s), loc) adamc@1270: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@1270: val env = E.pushDatatype env n' xs xncs adamc@1270: adamc@1270: val t = (L'.CNamed n', loc) adamc@1270: val env = foldl (fn ((x, n, to), env) => adamc@805: let adamc@1270: val t = case to of adamc@1270: NONE => t adamc@1270: | SOME t' => (L'.TFun (t', t), loc) adamc@1270: adamc@1270: val t = foldr (fn (x, t) => adamc@1270: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@1270: t xs adamc@805: in adamc@1270: E.pushENamedAs env x n t adamc@1270: end) env xncs adamc@1270: in adamc@1270: ([(L'.SgiDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, [])) adamc@1270: end) adamc@1270: | _ => (strError env (NotDatatype loc); adamc@1270: ([], (env, denv, []))) adamc@1270: end) adamc@1270: adamc@1270: | L.SgiVal (x, c) => adamc@1270: let adamc@1270: val (c', ck, gs') = elabCon (env, denv) c adamc@1270: adamc@1270: val old = c' adamc@1270: val c' = normClassConstraint env c' adamc@1270: val (env', n) = E.pushENamed env x c' adamc@1270: in adamc@1270: (unifyKinds env ck ktype adam@1719: handle KUnify arg => strError env (NotType (loc, ck, arg))); adamc@1270: adamc@1270: ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiTable (x, c, pe, ce) => adamc@1270: let adamc@1270: val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) adamc@1270: adamc@1270: val (c', ck, gs') = elabCon (env, denv) c adam@1639: val pkey = cunif env (loc, cstK) adam@1639: val visible = cunif env (loc, cstK) adam@1886: adam@1886: val x' = x ^ "_hidden_constraints" adam@1886: val (env', hidden_n) = E.pushCNamed env x' cstK NONE adam@1886: val hidden = (L'.CNamed hidden_n, loc) adam@1886: adam@1886: val uniques = (L'.CConcat (visible, hidden), loc) adamc@1270: adamc@1270: val ct = tableOf () adamc@1270: val ct = (L'.CApp (ct, c'), loc) adamc@1270: val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) adamc@1270: adamc@1270: val (pe', pet, gs'') = elabExp (env', denv) pe adamc@1270: val gs'' = List.mapPartial (fn Disjoint x => SOME x adamc@707: | _ => NONE) gs'' adamc@707: adamc@1270: val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) adamc@1270: val pst = (L'.CApp (pst, c'), loc) adamc@1270: val pst = (L'.CApp (pst, pkey), loc) adamc@1270: adamc@1270: val (ce', cet, gs''') = elabExp (env', denv) ce adamc@1270: val gs''' = List.mapPartial (fn Disjoint x => SOME x adamc@1270: | _ => NONE) gs''' adamc@1270: adamc@1270: val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) adamc@1270: val cst = (L'.CApp (cst, c'), loc) adamc@1270: val cst = (L'.CApp (cst, visible), loc) adam@1886: adam@1886: val (env', n) = E.pushENamed env' x ct adamc@1270: in adamc@1270: checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); adamc@1270: checkCon env' pe' pet pst; adamc@1270: checkCon env' ce' cet cst; adamc@1270: adam@1886: ([(L'.SgiConAbs (x', hidden_n, cstK), loc), adam@1912: (L'.SgiConstraint ((L'.CConcat (pkey, visible), loc), hidden), loc), adam@1886: (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiStr (x, sgn) => adamc@1270: let adamc@1270: val (sgn', gs') = elabSgn (env, denv) sgn adamc@1270: val (env', n) = E.pushStrNamed env x sgn' adam@1864: val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} adamc@1270: in adam@1864: ([(L'.SgiStr (x, n, sgn'), loc)], (env', denv', gs' @ gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiSgn (x, sgn) => adamc@1270: let adamc@1270: val (sgn', gs') = elabSgn (env, denv) sgn adamc@1270: val (env', n) = E.pushSgnNamed env x sgn' adamc@1270: in adamc@1270: ([(L'.SgiSgn (x, n, sgn'), loc)], (env', denv, gs' @ gs)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiInclude sgn => adamc@1270: let adamc@1270: val (sgn', gs') = elabSgn (env, denv) sgn adamc@1270: in adamc@1270: case #1 (hnormSgn env sgn') of adamc@1270: L'.SgnConst sgis => adamc@1270: (sgis, (foldl (fn (sgi, env) => E.sgiBinds env sgi) env sgis, denv, gs' @ gs)) adamc@1270: | _ => (sgnError env (NotIncludable sgn'); adamc@1270: ([], (env, denv, []))) adamc@1270: end adamc@1270: adamc@1270: | L.SgiConstraint (c1, c2) => adamc@1270: let adamc@1270: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@1270: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@1270: adamc@1270: val denv = D.assert env denv (c1', c2') adamc@1270: in adam@1639: checkKind env c1' k1 (L'.KRecord (kunif env loc), loc); adam@1639: checkKind env c2' k2 (L'.KRecord (kunif env loc), loc); adamc@1270: adamc@1270: ([(L'.SgiConstraint (c1', c2'), loc)], (env, denv, gs1 @ gs2)) adamc@1270: end adamc@1270: adamc@1270: | L.SgiClassAbs (x, k) => adamc@1270: let adamc@1270: val k = elabKind env k adamc@1270: val (env, n) = E.pushCNamed env x k NONE adamc@1270: val env = E.pushClass env n adamc@1270: in adamc@1270: ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) adamc@1270: end adamc@1270: adamc@1270: | L.SgiClass (x, k, c) => adamc@1270: let adamc@1270: val k = elabKind env k adamc@1270: val (c', ck, gs) = elabCon (env, denv) c adamc@1270: val (env, n) = E.pushCNamed env x k (SOME c') adamc@1270: val env = E.pushClass env n adamc@1270: in adamc@1270: checkKind env c' ck k; adamc@1270: ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) adamc@1270: end) adamc@211: adamc@83: and elabSgn (env, denv) (sgn, loc) = adamc@31: case sgn of adamc@31: L.SgnConst sgis => adamc@31: let adamc@88: val (sgis', (_, _, gs)) = ListUtil.foldlMapConcat elabSgn_item (env, denv, []) sgis adamc@62: adamc@62: val _ = foldl (fn ((sgi, loc), (cons, vals, sgns, strs)) => adamc@62: case sgi of adamc@62: L'.SgiConAbs (x, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiCon (x, _, _, _) => adamc@62: (if SS.member (cons, x) then adamc@62: sgnError env (DuplicateCon (loc, x)) adamc@62: else adamc@62: (); adamc@62: (SS.add (cons, x), vals, sgns, strs)) adamc@805: | L'.SgiDatatype dts => adamc@156: let adamc@805: val (cons, vals) = adamc@805: let adamc@805: fun doOne ((x, _, _, xncs), (cons, vals)) = adamc@805: let adamc@805: val vals = foldl (fn ((x, _, _), vals) => adamc@805: (if SS.member (vals, x) then adamc@805: sgnError env (DuplicateVal (loc, x)) adamc@805: else adamc@805: (); adamc@805: SS.add (vals, x))) adamc@805: vals xncs adamc@805: in adamc@805: if SS.member (cons, x) then adamc@805: sgnError env (DuplicateCon (loc, x)) adamc@805: else adamc@805: (); adamc@805: (SS.add (cons, x), vals) adamc@805: end adamc@805: in adamc@805: foldl doOne (cons, vals) dts adamc@805: end adamc@156: in adamc@805: (cons, vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, _, _, _, _, _, _) => adamc@156: (if SS.member (cons, x) then adamc@156: sgnError env (DuplicateCon (loc, x)) adamc@156: else adamc@156: (); adamc@156: (SS.add (cons, x), vals, sgns, strs)) adamc@62: | L'.SgiVal (x, _, _) => adamc@62: (if SS.member (vals, x) then adamc@62: sgnError env (DuplicateVal (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, SS.add (vals, x), sgns, strs)) adamc@62: | L'.SgiSgn (x, _, _) => adamc@62: (if SS.member (sgns, x) then adamc@62: sgnError env (DuplicateSgn (loc, x)) adamc@62: else adamc@62: (); adamc@62: (cons, vals, SS.add (sgns, x), strs)) adamc@62: | L'.SgiStr (x, _, _) => adamc@62: (if SS.member (strs, x) then adamc@62: sgnError env (DuplicateStr (loc, x)) adamc@62: else adamc@62: (); adamc@88: (cons, vals, sgns, SS.add (strs, x))) adamc@203: | L'.SgiConstraint _ => (cons, vals, sgns, strs) adamc@563: | L'.SgiClassAbs (x, _, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@211: (SS.add (cons, x), vals, sgns, strs)) adamc@563: | L'.SgiClass (x, _, _, _) => adamc@211: (if SS.member (cons, x) then adamc@211: sgnError env (DuplicateCon (loc, x)) adamc@211: else adamc@211: (); adamc@460: (SS.add (cons, x), vals, sgns, strs))) adamc@62: (SS.empty, SS.empty, SS.empty, SS.empty) sgis' adamc@31: in adamc@83: ((L'.SgnConst sgis', loc), gs) adamc@31: end adamc@31: | L.SgnVar x => adamc@31: (case E.lookupSgn env x of adamc@31: NONE => adamc@31: (sgnError env (UnboundSgn (loc, x)); adamc@83: ((L'.SgnError, loc), [])) adamc@83: | SOME (n, sgis) => ((L'.SgnVar n, loc), [])) adamc@41: | L.SgnFun (m, dom, ran) => adamc@41: let adamc@83: val (dom', gs1) = elabSgn (env, denv) dom adamc@41: val (env', n) = E.pushStrNamed env m dom' adamc@469: val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []} adamc@469: val (ran', gs2) = elabSgn (env', denv') ran adamc@41: in adamc@83: ((L'.SgnFun (m, n, dom', ran'), loc), gs1 @ gs2) adamc@41: end adam@1864: | L.SgnWhere (sgn, ms, x, c) => adamc@42: let adamc@83: val (sgn', ds1) = elabSgn (env, denv) sgn adamc@83: val (c', ck, ds2) = elabCon (env, denv) c adam@1864: adam@1864: fun checkPath (ms, sgn') = adam@1864: case #1 (hnormSgn env sgn') of adam@1864: L'.SgnConst sgis => adam@1864: List.exists (fn (L'.SgiConAbs (x', _, k), _) => adam@1864: List.null ms andalso x' = x andalso adam@1864: (unifyKinds env k ck adam@1864: handle KUnify x => sgnError env (WhereWrongKind x); adam@1864: true) adam@1864: | (L'.SgiStr (x', _, sgn''), _) => adam@1864: (case ms of adam@1864: [] => false adam@1864: | m :: ms' => adam@1864: m = x' andalso adam@1864: checkPath (ms', sgn'')) adam@1864: | _ => false) sgis adam@1864: | _ => false adam@1864: in adam@1864: if checkPath (ms, sgn') then adam@1864: ((L'.SgnWhere (sgn', ms, x, c'), loc), ds1 @ ds2) adam@1864: else adam@1864: (sgnError env (UnWhereable (sgn', x)); adam@1864: (sgnerror, [])) adamc@42: end adamc@59: | L.SgnProj (m, ms, x) => adamc@59: (case E.lookupStr env m of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@83: (sgnerror, [])) adamc@59: | SOME (n, sgn) => adamc@59: let adamc@59: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@59: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@59: NONE => (strError env (UnboundStr (loc, m)); adamc@59: (strerror, sgnerror)) adamc@59: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@59: ((L'.StrVar n, loc), sgn) ms adamc@59: in adamc@59: case E.projectSgn env {sgn = sgn, str = str, field = x} of adamc@59: NONE => (sgnError env (UnboundSgn (loc, x)); adamc@83: (sgnerror, [])) adamc@83: | SOME _ => ((L'.SgnProj (n, ms, x), loc), []) adamc@59: end) adamc@59: adamc@31: adamc@706: and selfify env {str, strs, sgn} = adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnError => sgn adamc@66: | L'.SgnVar _ => sgn adamc@66: adamc@66: | L'.SgnConst sgis => adam@1387: (L'.SgnConst (#1 (ListUtil.foldlMapConcat adam@1387: (fn (sgi, env) => adam@1387: (case sgi of (L'.SgiConAbs (x, n, k), loc) => adam@1387: [(L'.SgiCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adam@1387: | (L'.SgiDatatype dts, loc) => adam@1387: map (fn (x, n, xs, xncs) => (L'.SgiDatatypeImp (x, n, str, strs, x, xs, xncs), loc)) dts adam@1387: | (L'.SgiClassAbs (x, n, k), loc) => adam@1387: [(L'.SgiClass (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adam@1387: | (L'.SgiStr (x, n, sgn), loc) => adam@1387: [(L'.SgiStr (x, n, selfify env {str = str, strs = strs @ [x], sgn = sgn}), loc)] adam@1387: | x => [x], adam@1387: E.sgiBinds env sgi)) env sgis)), #2 sgn) adamc@66: | L'.SgnFun _ => sgn adamc@66: | L'.SgnWhere _ => sgn adamc@66: | L'.SgnProj (m, ms, x) => adamc@66: case E.projectSgn env {str = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar m, #2 sgn) ms, adamc@66: sgn = #2 (E.lookupStrNamed env m), adamc@66: field = x} of adamc@66: NONE => raise Fail "Elaborate.selfify: projectSgn returns NONE" adamc@66: | SOME sgn => selfify env {str = str, strs = strs, sgn = sgn} adamc@66: adamc@706: and selfifyAt env {str, sgn} = adamc@66: let adamc@66: fun self (str, _) = adamc@66: case str of adamc@66: L'.StrVar x => SOME (x, []) adamc@66: | L'.StrProj (str, x) => adamc@66: (case self str of adamc@66: NONE => NONE adamc@66: | SOME (m, ms) => SOME (m, ms @ [x])) adamc@66: | _ => NONE adamc@66: in adamc@66: case self str of adamc@66: NONE => sgn adamc@66: | SOME (str, strs) => selfify env {sgn = sgn, str = str, strs = strs} adamc@66: end adamc@66: adamc@706: and dopen env {str, strs, sgn} = adamc@66: let adam@1527: fun isVisible x = x <> "" andalso String.sub (x, 0) <> #"?" adam@1527: adamc@66: val m = foldl (fn (m, str) => (L'.StrProj (str, m), #2 sgn)) adamc@66: (L'.StrVar str, #2 sgn) strs adamc@66: in adamc@66: case #1 (hnormSgn env sgn) of adamc@66: L'.SgnConst sgis => adamc@805: ListUtil.foldlMapConcat adamc@805: (fn ((sgi, loc), env') => adamc@805: let adamc@805: val d = adamc@805: case sgi of adamc@805: L'.SgiConAbs (x, n, k) => adam@1527: if isVisible x then adam@1527: let adam@1527: val c = (L'.CModProj (str, strs, x), loc) adam@1527: in adam@1527: [(L'.DCon (x, n, k, c), loc)] adam@1527: end adam@1527: else adam@1527: [] adamc@805: | L'.SgiCon (x, n, k, c) => adam@1527: if isVisible x then adam@1527: [(L'.DCon (x, n, k, (L'.CModProj (str, strs, x), loc)), loc)] adam@1527: else adam@1527: [] adamc@805: | L'.SgiDatatype dts => adam@1527: List.mapPartial (fn (x, n, xs, xncs) => if isVisible x then adam@1527: SOME (L'.DDatatypeImp (x, n, str, strs, x, xs, xncs), loc) adam@1527: else adam@1527: NONE) dts adamc@805: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adam@1527: if isVisible x then adam@1527: [(L'.DDatatypeImp (x, n, m1, ms, x', xs, xncs), loc)] adam@1527: else adam@1527: [] adamc@805: | L'.SgiVal (x, n, t) => adam@1527: if isVisible x then adam@1527: [(L'.DVal (x, n, t, (L'.EModProj (str, strs, x), loc)), loc)] adam@1527: else adam@1527: [] adamc@805: | L'.SgiStr (x, n, sgn) => adam@1527: if isVisible x then adam@1527: [(L'.DStr (x, n, sgn, (L'.StrProj (m, x), loc)), loc)] adam@1527: else adam@1527: [] adamc@805: | L'.SgiSgn (x, n, sgn) => adam@1527: if isVisible x then adam@1527: [(L'.DSgn (x, n, (L'.SgnProj (str, strs, x), loc)), loc)] adam@1527: else adam@1527: [] adamc@805: | L'.SgiConstraint (c1, c2) => adamc@805: [(L'.DConstraint (c1, c2), loc)] adamc@805: | L'.SgiClassAbs (x, n, k) => adam@1527: if isVisible x then adam@1527: let adam@1527: val c = (L'.CModProj (str, strs, x), loc) adam@1527: in adam@1527: [(L'.DCon (x, n, k, c), loc)] adam@1527: end adam@1527: else adam@1527: [] adamc@805: | L'.SgiClass (x, n, k, _) => adam@1527: if isVisible x then adam@1527: let adam@1527: val c = (L'.CModProj (str, strs, x), loc) adam@1527: in adam@1527: [(L'.DCon (x, n, k, c), loc)] adam@1527: end adam@1527: else adam@1527: [] adamc@805: in adamc@805: (d, foldl (fn (d, env') => E.declBinds env' d) env' d) adamc@805: end) adamc@805: env sgis adamc@66: | _ => (strError env (UnOpenable sgn); adamc@628: ([], env)) adamc@66: end adamc@66: adamc@706: and sgiOfDecl (d, loc) = adamc@31: case d of adamc@123: L'.DCon (x, n, k, c) => [(L'.SgiCon (x, n, k, c), loc)] adamc@156: | L'.DDatatype x => [(L'.SgiDatatype x, loc)] adamc@156: | L'.DDatatypeImp x => [(L'.SgiDatatypeImp x, loc)] adamc@123: | L'.DVal (x, n, t, _) => [(L'.SgiVal (x, n, t), loc)] adamc@123: | L'.DValRec vis => map (fn (x, n, t, _) => (L'.SgiVal (x, n, t), loc)) vis adamc@123: | L'.DSgn (x, n, sgn) => [(L'.SgiSgn (x, n, sgn), loc)] adamc@123: | L'.DStr (x, n, sgn, _) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DFfiStr (x, n, sgn) => [(L'.SgiStr (x, n, sgn), loc)] adamc@123: | L'.DConstraint cs => [(L'.SgiConstraint cs, loc)] adamc@123: | L'.DExport _ => [] adamc@707: | L'.DTable (tn, x, n, c, _, pc, _, cc) => adamc@707: [(L'.SgiVal (x, n, (L'.CApp ((L'.CApp (tableOf (), c), loc), adamc@707: (L'.CConcat (pc, cc), loc)), loc)), loc)] adamc@460: | L'.DSequence (tn, x, n) => [(L'.SgiVal (x, n, sequenceOf ()), loc)] adamc@754: | L'.DView (tn, x, n, _, c) => adamc@754: [(L'.SgiVal (x, n, (L'.CApp (viewOf (), c), loc)), loc)] adamc@271: | L'.DDatabase _ => [] adamc@460: | L'.DCookie (tn, x, n, c) => [(L'.SgiVal (x, n, (L'.CApp (cookieOf (), c), loc)), loc)] adamc@720: | L'.DStyle (tn, x, n) => [(L'.SgiVal (x, n, styleOf ()), loc)] adamc@1075: | L'.DTask _ => [] adamc@1199: | L'.DPolicy _ => [] adam@1294: | L'.DOnError _ => [] adam@2010: | L'.DFfi (x, n, _, t) => [(L'.SgiVal (x, n, t), loc)] adamc@88: adamc@1000: and subSgn' counterparts env strLoc 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 adam@2092: (*val () = prefaces "subSgn" [("sgn1", p_sgn env sgn1), adamc@362: ("sgn2", p_sgn env sgn2), adamc@362: ("sgis1", p_sgn env (L'.SgnConst sgis1, loc2)), adamc@362: ("sgis2", p_sgn env (L'.SgnConst sgis2, loc2))]*) adamc@362: adamc@838: fun cpart n = IM.find (!counterparts, n) adamc@838: fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1) adamc@838: adamc@838: val sub2 = U.Con.map {kind = fn k => k, adamc@838: con = fn c => adamc@838: case c of adamc@838: L'.CNamed n2 => adamc@838: (case cpart n2 of adamc@838: NONE => c adamc@838: | SOME n1 => L'.CNamed n1) adamc@838: | _ => c} adamc@838: adamc@628: fun folder (sgi2All as (sgi, loc), env) = adamc@31: let adam@1668: (*val () = prefaces "folder" [("sgi2", p_sgn_item env sgi2All)]*) adamc@362: adamc@805: fun seek' f p = adamc@31: let adamc@628: fun seek env ls = adamc@31: case ls of adamc@805: [] => f env adamc@31: | h :: t => adamc@469: case p (env, h) of adamc@469: NONE => adamc@469: let adamc@469: val env = case #1 h of adamc@469: L'.SgiCon (x, n, k, c) => adamc@471: if E.checkENamed env n then adamc@471: env adamc@471: else adamc@471: E.pushCNamedAs env x n k (SOME c) adamc@469: | L'.SgiConAbs (x, n, k) => adamc@471: if E.checkENamed env n then adamc@471: env adamc@471: else adamc@471: E.pushCNamedAs env x n k NONE adamc@469: | _ => env adamc@469: in adamc@628: seek (E.sgiBinds env h) t adamc@469: end adamc@88: | SOME envs => envs adamc@31: in adamc@628: seek env sgis1 adamc@31: end adamc@805: adamc@1000: val seek = seek' (fn env => (sgnError env (UnmatchedSgi (strLoc, sgi2All)); adamc@805: env)) adamc@31: in adamc@31: case sgi of adamc@31: L'.SgiConAbs (x, n2, k2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@31: let adamc@41: fun found (x', n1, k1, co1) = adamc@41: if x = x' then adamc@41: let adamc@623: val () = unifyKinds env k1 k2 adam@1719: handle KUnify (k1, k2, env', err) => adam@1591: sgnError env (SgiWrongKind (loc, sgi1All, k1, adam@1719: sgi2All, k2, env', err)) adamc@41: val env = E.pushCNamedAs env x n1 k1 co1 adamc@41: in adamc@41: SOME (if n1 = n2 then adamc@41: env adamc@41: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x n2 k2 (SOME (L'.CNamed n1, loc2)))) adamc@41: end adamc@41: else adamc@41: NONE adamc@31: in adamc@31: case sgi1 of adamc@41: L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) adamc@41: | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, SOME c1) adamc@805: | L'.SgiDatatype dts => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@805: adamc@805: fun search dts = adamc@805: case dts of adamc@805: [] => NONE adamc@805: | (x', n1, xs, _) :: dts => adamc@805: let adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@805: in adamc@805: case found (x', n1, k', NONE) of adamc@805: NONE => search dts adamc@805: | x => x adamc@805: end adamc@191: in adamc@805: search dts adamc@191: end adamc@191: | L'.SgiDatatypeImp (x', n1, m1, ms, s, xs, _) => adamc@191: let adamc@191: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@191: in adamc@191: found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) adamc@191: end adamc@711: | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE) adamc@711: | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c) adamc@31: | _ => NONE adamc@31: end) adamc@31: adamc@31: | L'.SgiCon (x, n2, k2, c2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@211: let adamc@211: fun found (x', n1, k1, c1) = adamc@211: if x = x' then adamc@211: let adamc@838: val c2 = sub2 c2 adamc@838: adamc@327: fun good () = adamc@327: let adamc@327: val env = E.pushCNamedAs env x n2 k2 (SOME c2) adamc@327: val env = if n1 = n2 then adamc@327: env adamc@327: else adamc@839: (cparts (n2, n1); adamc@839: E.pushCNamedAs env x n1 k1 (SOME c1)) adamc@327: in adamc@628: SOME env adamc@327: end adamc@211: in adamc@987: (unifyCons env loc c1 c2; adamc@628: good ()) adam@1719: handle CUnify (c1, c2, env', err) => adam@1591: (sgnError env (SgiWrongCon (loc, sgi1All, c1, adam@1719: sgi2All, c2, env', err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@211: L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@711: | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: adamc@805: | L'.SgiDatatype dts2 => adamc@805: let adam@1591: fun found' (sgi1All as (_, loc), (x1, n1, xs1, xncs1), (x2, n2, xs2, xncs2), env) = adamc@805: if x1 <> x2 then adamc@805: NONE adamc@805: else adamc@805: let adamc@805: fun mismatched ue = adam@1591: (sgnError env (SgiMismatchedDatatypes (loc, sgi1All, sgi2All, ue)); adamc@805: SOME env) adamc@805: adamc@805: val k = (L'.KType, loc) adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs1 adamc@805: adamc@805: fun good () = adamc@805: let adamc@805: val env = E.sgiBinds env sgi1All adamc@805: val env = if n1 = n2 then adamc@805: env adamc@805: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x1 n2 k' adamc@838: (SOME (L'.CNamed n1, loc))) adamc@805: in adamc@805: SOME env adamc@805: end adamc@805: adamc@805: val env = E.pushCNamedAs env x1 n1 k' NONE adamc@805: val env = if n1 = n2 then adamc@805: env adamc@805: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x1 n2 k' (SOME (L'.CNamed n1, loc))) adamc@805: val env = foldl (fn (x, env) => E.pushCRel env x k) env xs1 adamc@805: fun xncBad ((x1, _, t1), (x2, _, t2)) = adamc@805: String.compare (x1, x2) <> EQUAL adamc@805: orelse case (t1, t2) of adamc@805: (NONE, NONE) => false adamc@805: | (SOME t1, SOME t2) => adamc@987: (unifyCons env loc t1 (sub2 t2); false) adamc@805: | _ => true adamc@805: in adamc@805: (if xs1 <> xs2 adamc@805: orelse length xncs1 <> length xncs2 adamc@805: orelse ListPair.exists xncBad (xncs1, xncs2) then adamc@805: mismatched NONE adamc@160: else adamc@805: good ()) adamc@805: handle CUnify ue => mismatched (SOME ue) adamc@805: end adamc@805: in adamc@805: seek' adamc@805: (fn _ => adamc@805: let adamc@805: fun seekOne (dt2, env) = adamc@805: seek (fn (env, sgi1All as (sgi1, _)) => adamc@805: case sgi1 of adamc@805: L'.SgiDatatypeImp (x', n1, _, _, _, xs, xncs1) => adamc@805: found' (sgi1All, (x', n1, xs, xncs1), dt2, env) adamc@805: | _ => NONE) adamc@805: adamc@805: fun seekAll (dts, env) = adamc@805: case dts of adamc@805: [] => env adamc@805: | dt :: dts => seekAll (dts, seekOne (dt, env)) adamc@805: in adamc@805: seekAll (dts2, env) adamc@805: end) adamc@805: (fn (env, sgi1All as (sgi1, _)) => adamc@805: let adamc@805: fun found dts1 = adamc@805: let adamc@805: fun iter (dts1, dts2, env) = adamc@805: case (dts1, dts2) of adamc@805: ([], []) => SOME env adamc@805: | (dt1 :: dts1, dt2 :: dts2) => adamc@805: (case found' (sgi1All, dt1, dt2, env) of adamc@805: NONE => NONE adamc@805: | SOME env => iter (dts1, dts2, env)) adamc@805: | _ => NONE adamc@805: in adamc@805: iter (dts1, dts2, env) adamc@805: end adamc@805: in adamc@805: case sgi1 of adamc@805: L'.SgiDatatype dts1 => found dts1 adamc@805: | _ => NONE adamc@805: end) adamc@805: end adamc@156: adamc@191: | L'.SgiDatatypeImp (x, n2, m12, ms2, s2, xs, _) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@158: case sgi1 of adamc@191: L'.SgiDatatypeImp (x', n1, m11, ms1, s1, _, _) => adamc@158: if x = x' then adamc@158: let adamc@158: val k = (L'.KType, loc) adamc@191: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@158: val t1 = (L'.CModProj (m11, ms1, s1), loc) adamc@158: val t2 = (L'.CModProj (m12, ms2, s2), loc) adamc@158: adamc@158: fun good () = adamc@158: let adamc@191: val env = E.pushCNamedAs env x n1 k' (SOME t1) adamc@191: val env = E.pushCNamedAs env x n2 k' (SOME t2) adamc@158: in adamc@838: cparts (n2, n1); adamc@628: SOME env adamc@158: end adamc@158: in adamc@987: (unifyCons env loc t1 t2; adamc@628: good ()) adam@1719: handle CUnify (c1, c2, env', err) => adam@1719: (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', 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) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@32: case sgi1 of adamc@41: L'.SgiVal (x', n1, c1) => adamc@41: if x = x' then adamc@838: ((*prefaces "val" [("x", PD.string x), adamc@838: ("n1", PD.string (Int.toString n1)), adamc@838: ("c1", p_con env c1), adamc@838: ("c2", p_con env c2), adamc@838: ("c2'", p_con env (sub2 c2))];*) adamc@987: unifyCons env loc c1 (sub2 c2); adamc@628: SOME env) adam@1719: handle CUnify (c1, c2, env', err) => adam@1719: (sgnError env (SgiWrongCon (loc, sgi1All, c1, sgi2All, c2, env', err)); adamc@628: SOME env) adamc@41: else adamc@41: NONE adamc@32: | _ => NONE) adamc@32: adamc@33: | L'.SgiStr (x, n2, sgn2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@33: case sgi1 of adamc@41: L'.SgiStr (x', n1, sgn1) => adamc@41: if x = x' then adamc@66: let adam@1591: val () = subSgn' counterparts env loc sgn1 sgn2 adamc@66: val env = E.pushStrNamedAs env x n1 sgn1 adamc@66: val env = if n1 = n2 then adamc@66: env adamc@66: else adamc@66: E.pushStrNamedAs env x n2 adamc@66: (selfifyAt env {str = (L'.StrVar n1, #2 sgn2), adamc@66: sgn = sgn2}) adamc@66: in adamc@628: SOME env adamc@66: end adamc@41: else adamc@41: NONE adamc@33: | _ => NONE) adamc@59: adamc@59: | L'.SgiSgn (x, n2, sgn2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@59: case sgi1 of adamc@59: L'.SgiSgn (x', n1, sgn1) => adamc@59: if x = x' then adamc@65: let adam@1591: val () = subSgn' counterparts env loc sgn1 sgn2 adam@1591: val () = subSgn' counterparts env loc sgn2 sgn1 adamc@65: adamc@65: val env = E.pushSgnNamedAs env x n2 sgn2 adamc@65: val env = if n1 = n2 then adamc@65: env adamc@65: else adamc@838: (cparts (n2, n1); adamc@838: E.pushSgnNamedAs env x n1 sgn2) adamc@65: in adamc@628: SOME env adamc@65: end adamc@59: else adamc@59: NONE adamc@59: | _ => NONE) adamc@88: adamc@88: | L'.SgiConstraint (c2, d2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@88: case sgi1 of adamc@88: L'.SgiConstraint (c1, d1) => adam@2092: (* It's important to do only simple equality checking here, adam@2092: * with no unification, because constraints are unnamed. adam@2092: * It's too easy to pick the wrong pair to unify! *) adam@2092: if consEqSimple env (c1, c2) adam@2092: andalso consEqSimple env (d1, d2) then adamc@628: SOME env adamc@88: else adamc@88: NONE adamc@88: | _ => NONE) adamc@203: adamc@563: | L'.SgiClassAbs (x, n2, k2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@211: let adamc@563: fun found (x', n1, k1, co) = adamc@211: if x = x' then adamc@211: let adamc@623: val () = unifyKinds env k1 k2 adam@1719: handle KUnify (k1, k2, env', err) => adam@1591: sgnError env (SgiWrongKind (loc, sgi1All, k1, adam@1719: sgi2All, k2, env', err)) adamc@563: adamc@711: val env = E.pushCNamedAs env x n1 k1 co adamc@211: in adamc@211: SOME (if n1 = n2 then adamc@211: env adamc@211: else adamc@838: (cparts (n2, n1); adamc@838: E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2)))) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@563: L'.SgiClassAbs (x', n1, k1) => found (x', n1, k1, NONE) adamc@563: | L'.SgiClass (x', n1, k1, c) => found (x', n1, k1, SOME c) adam@1797: | L'.SgiConAbs (x', n1, k1) => found (x', n1, k1, NONE) adam@1797: | L'.SgiCon (x', n1, k1, c) => found (x', n1, k1, SOME c) adamc@211: | _ => NONE adamc@211: end) adamc@563: | L'.SgiClass (x, n2, k2, c2) => adam@1591: seek (fn (env, sgi1All as (sgi1, loc)) => adamc@211: let adamc@563: fun found (x', n1, k1, c1) = adamc@211: if x = x' then adamc@211: let adamc@623: val () = unifyKinds env k1 k2 adam@1719: handle KUnify (k1, k2, env', err) => adam@1591: sgnError env (SgiWrongKind (loc, sgi1All, k1, adam@1719: sgi2All, k2, env', err)) adamc@563: adamc@838: val c2 = sub2 c2 adamc@838: adamc@218: fun good () = adamc@218: let adamc@711: val env = E.pushCNamedAs env x n2 k2 (SOME c2) adamc@218: val env = if n1 = n2 then adamc@218: env adamc@218: else adamc@839: (cparts (n2, n1); adamc@839: E.pushCNamedAs env x n1 k2 (SOME c1)) adamc@218: in adamc@628: SOME env adamc@218: end adamc@211: in adamc@987: (unifyCons env loc c1 c2; adamc@628: good ()) adam@1719: handle CUnify (c1, c2, env', err) => adam@1591: (sgnError env (SgiWrongCon (loc, sgi1All, c1, adam@1719: sgi2All, c2, env', err)); adamc@211: good ()) adamc@211: end adamc@211: else adamc@211: NONE adamc@211: in adamc@211: case sgi1 of adamc@563: L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) adam@1797: | L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) adamc@211: | _ => NONE adamc@211: end) adamc@31: end adamc@31: in adamc@628: ignore (foldl folder env sgis2) adamc@31: end adamc@31: adamc@41: | (L'.SgnFun (m1, n1, dom1, ran1), L'.SgnFun (m2, n2, dom2, ran2)) => adamc@43: let adamc@480: val ran2 = adamc@43: if n1 = n2 then adamc@480: ran2 adamc@43: else adamc@480: subStrInSgn (n2, n1) ran2 adamc@43: in adamc@1000: subSgn' counterparts env strLoc dom2 dom1; adamc@1000: subSgn' counterparts (E.pushStrNamedAs env m1 n1 dom2) strLoc ran1 ran2 adamc@43: end adamc@41: adamc@1000: | _ => sgnError env (SgnWrongForm (strLoc, sgn1, sgn2))) adamc@41: adam@1580: and subSgn env x y z = subSgn' (ref IM.empty) env x y z adam@1580: handle e as E.UnboundNamed _ => if ErrorMsg.anyErrors () then () else raise e adamc@61: adamc@706: and positive self = adamc@312: let adamc@312: open L adamc@312: adamc@312: fun none (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => none c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso none c2 adamc@312: | TCFun (_, _, _, c) => none c adamc@312: | TRecord c => none c adamc@312: adamc@312: | CVar ([], x) => x <> self adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => none c1 andalso none c2 adamc@312: | CAbs _ => false adamc@628: | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@623: | CKAbs _ => false adamc@623: | TKFun _ => false adamc@623: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs adamc@312: | CConcat (c1, c2) => none c1 andalso none c2 adamc@621: | CMap => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all none cs adamc@312: | CProj (c, _) => none c adamc@312: adamc@312: | CWild _ => false adamc@312: adamc@312: fun pos (c, _) = adamc@312: case c of adamc@312: CAnnot (c, _) => pos c adamc@312: adamc@312: | TFun (c1, c2) => none c1 andalso pos c2 adamc@312: | TCFun (_, _, _, c) => pos c adamc@312: | TRecord c => pos c adamc@312: adamc@312: | CVar _ => true adamc@312: | CApp (c1, c2) => pos c1 andalso none c2 adamc@312: | CAbs _ => false adamc@628: | TDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 adamc@312: adamc@623: | CKAbs _ => false adamc@623: | TKFun _ => false adamc@623: adamc@312: | CName _ => true adamc@312: adamc@312: | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs adamc@312: | CConcat (c1, c2) => pos c1 andalso pos c2 adamc@621: | CMap => true adamc@312: adamc@312: | CUnit => true adamc@312: adamc@312: | CTuple cs => List.all pos cs adamc@312: | CProj (c, _) => pos c adamc@312: adamc@312: | CWild _ => false adamc@312: in adamc@312: pos adamc@312: end adamc@312: adamc@706: and wildifyStr env (str, sgn) = adamc@325: case #1 (hnormSgn env sgn) of adamc@325: L'.SgnConst sgis => adamc@325: (case #1 str of adamc@325: L.StrConst ds => adamc@325: let adamc@1270: fun cname d = adamc@1270: case d of adamc@1270: L'.SgiCon (x, _, _, _) => SOME x adamc@1270: | L'.SgiConAbs (x, _, _) => SOME x adamc@1270: | L'.SgiClass (x, _, _, _) => SOME x adamc@1270: | L'.SgiClassAbs (x, _, _) => SOME x adamc@1270: | _ => NONE adamc@1270: adamc@1270: fun dname (d, _) = adamc@1270: case d of adamc@1270: L.DCon (x, _, _) => SOME x adamc@1270: | _ => NONE adamc@1270: 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 adam@1639: | L'.KUnif (_, _, ref (L'.KKnown k)) => decompileKind k adamc@493: | L'.KUnif _ => NONE adam@1639: | L'.KTupleUnif (_, _, ref (L'.KKnown k)) => decompileKind k adam@1302: | L'.KTupleUnif _ => NONE adamc@493: adamc@623: | L'.KRel _ => NONE adamc@623: | L'.KFun _ => NONE adamc@623: adam@1529: fun maybeHnorm env c = adam@1865: hnormCon env c adam@1865: handle E.UnboundNamed _ => c adam@1865: adam@1865: fun decompileCon env c = adam@1865: case decompileCon' env c of adam@1865: SOME v => SOME v adam@1865: | NONE => decompileCon' env (maybeHnorm env c) adam@1865: adam@1865: and decompileCon' env (c as (_, loc)) = adam@1865: case #1 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) adam@1886: | L'.CRecord (k, 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 adam@1886: adam@1886: val c' = Option.map (fn xcs => (L.CRecord xcs, loc)) adam@1886: (fields xcs) adamc@325: in adam@1886: Option.map (fn c' => adam@1886: case decompileKind k of adam@1886: NONE => c' adam@1886: | SOME k' => (L.CAnnot (c', (L.KRecord k', loc)), loc)) c' 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) adam@1639: | L'.CUnif (nl, _, _, _, ref (L'.Known c)) => decompileCon env (E.mliftConInCon nl c) adamc@325: adam@1585: | L'.CApp (f, x) => adam@1585: (case (decompileCon env f, decompileCon env x) of adam@1585: (SOME f, SOME x) => SOME (L.CApp (f, x), loc) adam@1585: | _ => NONE) adam@1585: adam@1864: | L'.CTuple cs => adam@1864: let adam@1864: val cs' = foldr (fn (c, cs') => adam@1864: case cs' of adam@1864: NONE => NONE adam@1864: | SOME cs' => adam@1864: case decompileCon env c of adam@1864: NONE => NONE adam@1864: | SOME c' => SOME (c' :: cs')) adam@1864: (SOME []) cs adam@1864: in adam@1864: case cs' of adam@1864: NONE => NONE adam@1864: | SOME cs' => SOME (L.CTuple cs', loc) adam@1864: end adam@1864: adam@1864: | L'.CMap _ => SOME (L.CMap, loc) adam@1865: | L'.TRecord c => adam@1865: (case decompileCon env c of adam@1865: NONE => NONE adam@1865: | SOME c' => SOME (L.TRecord c', loc)) adam@1864: adam@1912: | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) adamc@325: adamc@1264: fun buildNeeded env sgis = adamc@1275: #1 (foldl (fn ((sgi, loc), (nd, env')) => adamc@1264: (case sgi of adam@1570: L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) adam@1570: | L'.SgiConAbs (x, _, k) => naddCon (nd, x, k) adamc@1264: | L'.SgiConstraint cs => naddConstraint (nd, (env', cs, loc)) adamc@1264: | L'.SgiVal (x, _, t) => adamc@1264: let adamc@1277: fun should t = adamc@1277: let adamc@1277: val t = normClassConstraint env' t adam@2094: adam@2094: fun shouldR c = adam@2094: case hnormCon env' c of adam@2094: (L'.CApp (f, _), _) => adam@2094: (case hnormCon env' f of adam@2094: (L'.CApp (f, cl), loc) => adam@2094: (case hnormCon env' f of adam@2094: (L'.CMap _, _) => isClassOrFolder env' cl adam@2094: | _ => false) adam@2094: | _ => false) adam@2094: | (L'.CConcat (c1, c2), _) => adam@2094: shouldR c1 orelse shouldR c2 adam@2094: | c => false adamc@1277: in adamc@1277: case #1 t of adamc@1277: L'.CApp (f, _) => isClassOrFolder env' f adam@2094: | L'.TRecord t => shouldR t adamc@1277: | _ => false adamc@1277: end adamc@1270: in adamc@1277: if should t then adamc@1277: naddVal (nd, x) adamc@1277: else adamc@1277: nd adamc@1264: end adamc@1264: | L'.SgiStr (x, _, s) => adamc@1270: (case #1 (hnormSgn env' s) of adamc@1270: L'.SgnConst sgis' => naddMod (nd, x, (env', buildNeeded env' sgis')) adamc@1264: | _ => nd) adamc@1264: | _ => nd, adamc@1275: E.sgiBinds env' (sgi, loc))) adamc@1275: (nempty, env) sgis) adamc@1264: adamc@1264: val nd = buildNeeded env sgis adamc@1264: adamc@1264: fun removeUsed (nd, ds) = adamc@1264: foldl (fn ((d, _), nd) => adamc@634: case d of adamc@1264: L.DCon (x, _, _) => ndelCon (nd, x) adamc@1264: | L.DVal (x, _, _) => ndelVal (nd, x) adamc@1264: | L.DOpen _ => nempty adam@1868: | L.DStr (x, _, _, (L.StrConst ds', _), _) => adamc@1264: (case SM.find (nmods nd, x) of adamc@1264: NONE => nd adamc@1270: | SOME (env, nd') => naddMod (nd, x, (env, removeUsed (nd', ds')))) adamc@1264: | _ => nd) adamc@1264: nd ds adamc@1264: adamc@1264: val nd = removeUsed (nd, ds) adamc@1264: adam@1662: (* Among the declarations present explicitly in the program, find the last constructor or constraint declaration. adam@1662: * The new constructor/constraint declarations that we add may safely be put after that point. *) adam@1662: fun findLast (ds, acc) = adam@1662: case ds of adam@1662: [] => ([], acc) adam@1662: | (d : L.decl) :: ds' => adam@1662: let adam@1662: val isCony = case #1 d of adam@1662: L.DCon _ => true adam@1662: | L.DDatatype _ => true adam@1662: | L.DDatatypeImp _ => true adam@1662: | L.DStr _ => true adam@1662: | L.DConstraint _ => true adam@1662: | _ => false adam@1662: in adam@1662: if isCony then adam@1662: (ds, acc) adam@1662: else adam@1662: findLast (ds', d :: acc) adam@1662: end adam@1662: adam@1662: val (dPrefix, dSuffix) = findLast (rev ds, []) adam@1662: adamc@1270: fun extend (env, nd, ds) = adamc@1264: let adamc@1264: val ds' = List.mapPartial (fn (env', (c1, c2), loc) => adamc@1264: case (decompileCon env' c1, decompileCon env' c2) of adamc@1264: (SOME c1, SOME c2) => adamc@1264: SOME (L.DConstraint (c1, c2), loc) adam@1586: | _ => NONE) (nconstraints nd) adamc@1264: adamc@1264: val ds' = adamc@1264: case SS.listItems (nvals nd) of adamc@1264: [] => ds' adamc@1264: | xs => adamc@1264: let adamc@1264: val ewild = (L.EWild, #2 str) adamc@1264: val ds'' = map (fn x => (L.DVal (x, NONE, ewild), #2 str)) xs adamc@1264: in adamc@1264: ds'' @ ds' adamc@1264: end adamc@1264: adamc@1275: val ds' = adam@1640: case ncons nd of adamc@1275: [] => ds' adamc@1264: | xs => adam@1570: map (fn (x, k) => adamc@1270: let adamc@1270: val k = adamc@1270: case decompileKind k of adamc@1270: NONE => (L.KWild, #2 str) adamc@1270: | SOME k => k adamc@1275: adamc@1270: val cwild = (L.CWild k, #2 str) adamc@1270: in adam@1570: (L.DCon (x, NONE, cwild), #2 str) adamc@1275: end) xs @ ds' adamc@1275: adamc@1275: val ds = ds @ ds' adamc@1264: in adam@1868: map (fn d as (L.DStr (x, s, tm, (L.StrConst ds', loc'), r), loc) => adamc@1270: (case SM.find (nmods nd, x) of adamc@1270: NONE => d adamc@1270: | SOME (env, nd') => adam@1868: (L.DStr (x, s, tm, (L.StrConst (extend (env, nd', ds')), loc'), r), loc)) adamc@1270: | d => d) ds adamc@1264: end adamc@325: in adam@1662: (L.StrConst (extend (env, nd, rev dPrefix) @ dSuffix), #2 str) adamc@325: end adamc@325: | _ => str) adamc@325: | _ => str adamc@325: adamc@706: and elabDecl (dAll as (d, loc), (env, denv, gs)) = adamc@255: let adamc@904: (*val () = preface ("elabDecl", SourcePrint.p_decl dAll)*) adamc@514: (*val befor = Time.now ()*) adamc@255: adamc@255: val r = adamc@255: case d of adamc@255: L.DCon (x, ko, c) => adamc@255: let adamc@255: val k' = case ko of adam@1639: NONE => kunif env loc adamc@623: | SOME k => elabKind env k adamc@255: adamc@255: val (c', ck, gs') = elabCon (env, denv) c adamc@255: val (env', n) = E.pushCNamed env x k' (SOME c') adamc@255: in adamc@255: checkKind env c' ck k'; adamc@255: adamc@255: ([(L'.DCon (x, n, k', c'), loc)], (env', denv, enD gs' @ gs)) adamc@255: end adamc@805: | L.DDatatype dts => adamc@255: let adamc@255: val k = (L'.KType, loc) adamc@805: adamc@805: val (dts, env) = ListUtil.foldlMap adamc@805: (fn ((x, xs, xcs), env) => adamc@805: let adamc@805: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@805: val (env, n) = E.pushCNamed env x k' NONE adamc@805: in adamc@805: ((x, n, xs, xcs), env) adamc@805: end) adamc@805: env dts adamc@805: adamc@805: val (dts, (env, gs')) = ListUtil.foldlMap adamc@805: (fn ((x, n, xs, xcs), (env, gs')) => adamc@805: let adamc@805: val t = (L'.CNamed n, loc) adamc@805: val nxs = length xs - 1 adamc@805: val t = ListUtil.foldli adamc@805: (fn (i, _, t) => adamc@805: (L'.CApp (t, (L'.CRel (nxs - i), loc)), loc)) t xs adamc@805: adamc@805: val (env', denv') = foldl (fn (x, (env', denv')) => adamc@805: (E.pushCRel env' x k, adamc@805: D.enter denv')) (env, denv) xs adamc@805: adamc@805: val (xcs, (used, env, gs')) = adamc@805: ListUtil.foldlMap adamc@805: (fn ((x, to), (used, env, gs)) => adamc@805: let adamc@805: val (to, t, gs') = case to of adamc@805: NONE => (NONE, t, gs) adamc@805: | SOME t' => adamc@805: let adamc@805: val (t', tk, gs') = elabCon (env', denv') t' adamc@805: in adamc@805: checkKind env' t' tk k; adamc@805: (SOME t', (L'.TFun (t', t), loc), enD gs' @ gs) adamc@805: end adamc@805: val t = foldr (fn (x, t) => (L'.TCFun (L'.Implicit, x, k, t), loc)) t xs adamc@805: adamc@805: val (env, n') = E.pushENamed env x t adamc@805: in adamc@805: if SS.member (used, x) then adamc@805: strError env (DuplicateConstructor (x, loc)) adamc@805: else adamc@805: (); adamc@805: ((x, n', to), (SS.add (used, x), env, gs')) adamc@805: end) adamc@805: (SS.empty, env, gs') xcs adamc@805: in adamc@805: ((x, n, xs, xcs), (E.pushDatatype env n xs xcs, gs')) adamc@805: end) adamc@805: (env, []) dts adamc@255: in adamc@805: ([(L'.DDatatype dts, loc)], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@255: | L.DDatatypeImp (_, [], _) => raise Fail "Empty DDatatypeImp" adamc@255: adamc@255: | L.DDatatypeImp (x, m1 :: ms, s) => adamc@255: (case E.lookupStr env m1 of adamc@255: NONE => (expError env (UnboundStrInExp (loc, m1)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (n, sgn) => adamc@255: let adamc@255: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@255: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@255: NONE => (conError env (UnboundStrInCon (loc, m)); adamc@255: (strerror, sgnerror)) adamc@255: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@255: ((L'.StrVar n, loc), sgn) ms adamc@255: in adamc@628: case hnormCon env (L'.CModProj (n, ms, s), loc) of adamc@628: (L'.CModProj (n, ms, s), _) => adamc@255: (case E.projectDatatype env {sgn = sgn, str = str, field = s} of adamc@255: NONE => (conError env (UnboundDatatype (loc, s)); adamc@255: ([], (env, denv, gs))) adamc@255: | SOME (xs, xncs) => adamc@255: let adamc@255: val k = (L'.KType, loc) adamc@255: val k' = foldl (fn (_, k') => (L'.KArrow (k, k'), loc)) k xs adamc@255: val t = (L'.CModProj (n, ms, s), loc) adamc@255: val (env, n') = E.pushCNamed env x k' (SOME t) adamc@255: val env = E.pushDatatype env n' xs xncs adamc@255: adamc@255: val t = (L'.CNamed n', loc) adamc@844: val nxs = length xs adamc@844: val t = ListUtil.foldli (fn (i, _, t) => adamc@844: (L'.CApp (t, (L'.CRel (nxs - 1 - i), loc)), loc)) adamc@844: t xs adamc@255: val env = foldl (fn ((x, n, to), env) => adamc@255: let adamc@255: val t = case to of adamc@255: NONE => t adamc@255: | SOME t' => (L'.TFun (t', t), loc) adamc@255: adamc@255: val t = foldr (fn (x, t) => adamc@255: (L'.TCFun (L'.Implicit, x, k, t), loc)) adamc@255: t xs adamc@255: in adamc@255: E.pushENamedAs env x n t adamc@255: end) env xncs adamc@255: in adamc@628: ([(L'.DDatatypeImp (x, n', n, ms, s, xs, xncs), loc)], (env, denv, gs)) adamc@255: end) adamc@255: | _ => (strError env (NotDatatype loc); adamc@255: ([], (env, denv, []))) adamc@255: end) adamc@255: adamc@255: | L.DVal (x, co, e) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adam@1639: NONE => (cunif env (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@255: adamc@255: val (e', et, gs2) = elabExp (env, denv) e adamc@629: adamc@629: val () = checkCon env e' et c' adamc@629: adamc@674: val c' = normClassConstraint env c' adamc@255: val (env', n) = E.pushENamed env x c' adamc@255: in adamc@255: (*prefaces "DVal" [("x", Print.PD.string x), adamc@362: ("c'", p_con env c')];*) adamc@628: ([(L'.DVal (x, n, c', e'), loc)], (env', denv, enD gs1 @ gs2 @ gs)) adamc@255: end adamc@255: | L.DValRec vis => adamc@255: let adamc@255: fun allowable (e, _) = adamc@255: case e of adamc@255: L.EAbs _ => true adamc@255: | L.ECAbs (_, _, _, e) => allowable e adamc@623: | L.EKAbs (_, e) => allowable e adamc@255: | L.EDisjoint (_, _, e) => allowable e adamc@255: | _ => false adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap adamc@255: (fn ((x, co, e), gs) => adamc@255: let adamc@255: val (c', _, gs1) = case co of adam@1639: NONE => (cunif env (loc, ktype), ktype, []) adamc@255: | SOME c => elabCon (env, denv) c adamc@674: val c' = normClassConstraint env c' adamc@255: in adamc@255: ((x, c', e), enD gs1 @ gs) adamc@280: end) gs vis adamc@255: adamc@255: val (vis, env) = ListUtil.foldlMap (fn ((x, c', e), env) => adamc@255: let adamc@255: val (env, n) = E.pushENamed env x c' adamc@255: in adamc@255: ((x, n, c', e), env) adamc@255: end) env vis adamc@255: adamc@255: val (vis, gs) = ListUtil.foldlMap (fn ((x, n, c', e), gs) => adamc@255: let adamc@255: val (e', et, gs1) = elabExp (env, denv) e adamc@255: in adamc@628: checkCon env e' et c'; adamc@255: if allowable e then adamc@255: () adamc@255: else adamc@255: expError env (IllegalRec (x, e')); adamc@628: ((x, n, c', e'), gs1 @ gs) adamc@255: end) gs vis adam@1736: adam@1736: val vis = map (fn (x, n, t, e) => (x, n, normClassConstraint env t, e)) vis adam@1736: val d = (L'.DValRec vis, loc) adamc@255: in adam@1736: ([d], (E.declBinds env d, 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: adam@1868: | L.DStr (x, sgno, tmo, str, _) => adam@1732: (case ModDb.lookup dAll of adam@1732: SOME d => adam@1732: let adam@1744: val () = if !verbose then TextIO.print ("REUSE: " ^ x ^ "\n") else () adam@1732: val env' = E.declBinds env d adam@1732: val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} adam@1732: in adam@1738: ([d], (env', denv', gs)) adam@1732: end adam@1732: | NONE => adam@1732: let adam@1744: val () = if !verbose then TextIO.print ("CHECK: " ^ x ^ "\n") else () adam@1744: adam@1732: val () = if x = "Basis" then adam@1732: raise Fail "Not allowed to redefine structure 'Basis'" adam@1732: else adam@1732: () adam@1732: adam@1732: val formal = Option.map (elabSgn (env, denv)) sgno adam@1732: adam@1732: val (str', sgn', gs') = adam@1732: case formal of adam@1732: NONE => adam@1732: let adam@1732: val (str', actual, gs') = elabStr (env, denv) str adam@1732: in adam@1732: (str', selfifyAt env {str = str', sgn = actual}, gs') adam@1732: end adam@1732: | SOME (formal, gs1) => adam@1732: let adam@1732: val str = wildifyStr env (str, formal) adam@1732: val (str', actual, gs2) = elabStr (env, denv) str adam@1732: in adam@1732: subSgn env loc (selfifyAt env {str = str', sgn = actual}) formal; adam@1732: (str', formal, enD gs1 @ gs2) adam@1732: end adam@1732: adam@1732: val (env', n) = E.pushStrNamed env x sgn' adam@1883: adam@1732: val denv' = adam@1732: case #1 str' of adam@1732: L'.StrConst _ => dopenConstraints (loc, env', denv) {str = x, strs = []} adam@1732: | L'.StrApp _ => dopenConstraints (loc, env', denv) {str = x, strs = []} adam@1732: | _ => denv adam@1732: adam@1732: val dNew = (L'.DStr (x, n, sgn', str'), loc) adam@1732: in adam@1732: case #1 (hnormSgn env sgn') of adam@1732: L'.SgnFun _ => adam@1732: (case #1 str' of adam@1732: L'.StrFun _ => () adam@1732: | _ => strError env (FunctorRebind loc)) adam@1732: | _ => (); adam@1732: Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; adam@1732: ([dNew], (env', denv', gs' @ gs)) adam@1732: end) adam@1732: adam@1733: | L.DFfiStr (x, sgn, tmo) => adam@1732: (case ModDb.lookup dAll of adam@1732: SOME d => adam@1732: let adam@1732: val env' = E.declBinds env d adam@1732: val denv' = dopenConstraints (loc, env', denv) {str = x, strs = []} adam@1732: in adam@1732: ([d], (env', denv', [])) adam@1732: end adam@1732: | NONE => adam@1732: let adam@1732: val (sgn', gs') = elabSgn (env, denv) sgn adam@1732: adam@1732: val (env', n) = E.pushStrNamed env x sgn' adam@1732: adam@1732: val dNew = (L'.DFfiStr (x, n, sgn'), loc) adam@1732: in adam@1733: Option.map (fn tm => ModDb.insert (dNew, tm)) tmo; adam@1732: ([dNew], (env', denv, enD gs' @ gs)) adam@1732: 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@1030: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@1030: case E.projectStr env {str = str, sgn = sgn, field = m} of adamc@1030: NONE => (strError env (UnboundStr (loc, m)); adamc@1030: (strerror, sgnerror)) adamc@1030: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adamc@1030: ((L'.StrVar n, loc), sgn) ms adamc@1030: adamc@1030: val sgn = selfifyAt env {str = str, sgn = sgn} adamc@255: adamc@628: val (ds, env') = dopen env {str = n, strs = ms, sgn = sgn} adamc@628: val denv' = dopenConstraints (loc, env', denv) {str = m, strs = ms} adamc@255: in adamc@255: (ds, (env', denv', gs)) adamc@255: end) adamc@255: adamc@255: | L.DConstraint (c1, c2) => adamc@255: let adamc@255: val (c1', k1, gs1) = elabCon (env, denv) c1 adamc@255: val (c2', k2, gs2) = elabCon (env, denv) c2 adamc@255: val gs3 = D.prove env denv (c1', c2', loc) adamc@255: adamc@628: val denv' = D.assert env denv (c1', c2') adamc@255: in adam@1639: checkKind env c1' k1 (L'.KRecord (kunif env loc), loc); adam@1639: checkKind env c2' k2 (L'.KRecord (kunif env loc), loc); adamc@255: adamc@628: ([(L'.DConstraint (c1', c2'), loc)], (env, denv', enD gs1 @ enD gs2 @ enD gs3 @ gs)) adamc@255: end adamc@255: adamc@255: | L.DOpenConstraints (m, ms) => adamc@255: let adamc@255: val denv = dopenConstraints (loc, env, denv) {str = m, strs = ms} adamc@255: in adamc@255: ([], (env, denv, gs)) adamc@255: end adamc@255: adamc@255: | L.DExport str => adamc@255: let adamc@255: val (str', sgn, gs') = elabStr (env, denv) str adamc@255: adamc@255: val sgn = adamc@255: case #1 (hnormSgn env sgn) of adamc@255: L'.SgnConst sgis => adamc@255: let adamc@255: fun doOne (all as (sgi, _), env) = adamc@255: (case sgi of adamc@255: L'.SgiVal (x, n, t) => adamc@325: let adamc@325: fun doPage (makeRes, ran) = adamc@628: case hnormCon env ran of adamc@628: (L'.CApp (tf, arg), _) => adamc@628: (case (hnormCon env tf, hnormCon env arg) of adamc@628: ((L'.CModProj (basis, [], "transaction"), _), adamc@720: (L'.CApp (tf, arg3), _)) => adamc@325: (case (basis = !basis_r, adamc@720: hnormCon env tf, hnormCon env arg3) of adamc@325: (true, adamc@720: (L'.CApp (tf, arg2), _), adamc@628: ((L'.CRecord (_, []), _))) => adamc@720: (case (hnormCon env tf) of adamc@720: (L'.CApp (tf, arg1), _) => adamc@720: (case (hnormCon env tf, adamc@720: hnormCon env arg1, adamc@720: hnormCon env arg2) of adamc@720: (tf, arg1, adamc@720: (L'.CRecord (_, []), _)) => adamc@720: let adamc@720: val t = (L'.CApp (tf, arg1), loc) adamc@720: val t = (L'.CApp (t, arg2), loc) adamc@720: val t = (L'.CApp (t, arg3), loc) adamc@720: val t = (L'.CApp ( adamc@720: (L'.CModProj adamc@720: (basis, [], "transaction"), loc), adamc@325: t), loc) adam@1347: adam@1347: fun normArgs t = adam@1347: case hnormCon env t of adam@1347: (L'.TFun (dom, ran), loc) => adam@1347: (L'.TFun (hnormCon env dom, normArgs ran), loc) adam@1347: | t' => t' adamc@720: in adam@1347: (L'.SgiVal (x, n, normArgs (makeRes t)), loc) adamc@720: end adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all) adamc@325: | _ => all adamc@325: in adamc@628: case hnormCon env t of adamc@628: (L'.TFun (dom, ran), _) => adamc@628: (case hnormCon env dom of adamc@628: (L'.TRecord domR, _) => adamc@325: doPage (fn t => (L'.TFun ((L'.TRecord domR, adamc@325: loc), adamc@325: t), loc), ran) adamc@325: | _ => all) adamc@325: | _ => doPage (fn t => t, t) adamc@325: end adamc@255: | _ => all, adamc@255: E.sgiBinds env all) adamc@255: in adamc@255: (L'.SgnConst (#1 (ListUtil.foldlMap doOne env sgis)), loc) adamc@255: end adamc@255: | _ => sgn adamc@255: in adamc@255: ([(L'.DExport (E.newNamed (), sgn, str'), loc)], (env, denv, gs' @ gs)) adamc@255: end adamc@255: adamc@707: | L.DTable (x, c, pe, ce) => adamc@255: let adamc@707: val cstK = (L'.KRecord (L'.KRecord (L'.KUnit, loc), loc), loc) adamc@707: adamc@255: val (c', k, gs') = elabCon (env, denv) c adam@1639: val pkey = cunif env (loc, cstK) adam@1639: val uniques = cunif env (loc, cstK) adamc@705: adamc@705: val ct = tableOf () adamc@705: val ct = (L'.CApp (ct, c'), loc) adamc@707: val ct = (L'.CApp (ct, (L'.CConcat (pkey, uniques), loc)), loc) adamc@705: adamc@705: val (env, n) = E.pushENamed env x ct adamc@707: val (pe', pet, gs'') = elabExp (env, denv) pe adamc@707: val (ce', cet, gs''') = elabExp (env, denv) ce adamc@707: adamc@707: val pst = (L'.CModProj (!basis_r, [], "primary_key"), loc) adamc@707: val pst = (L'.CApp (pst, c'), loc) adamc@707: val pst = (L'.CApp (pst, pkey), loc) adamc@704: adamc@704: val cst = (L'.CModProj (!basis_r, [], "sql_constraints"), loc) adamc@704: val cst = (L'.CApp (cst, c'), loc) adamc@705: val cst = (L'.CApp (cst, uniques), loc) adamc@255: in adamc@255: checkKind env c' k (L'.KRecord (L'.KType, loc), loc); adamc@707: checkCon env pe' pet pst; adamc@707: checkCon env ce' cet cst; adamc@707: ([(L'.DTable (!basis_r, x, n, c', pe', pkey, ce', uniques), loc)], adamc@707: (env, denv, gs''' @ gs'' @ enD gs' @ gs)) adamc@255: end adamc@338: | L.DSequence x => adamc@338: let adamc@338: val (env, n) = E.pushENamed env x (sequenceOf ()) adamc@338: in adamc@338: ([(L'.DSequence (!basis_r, x, n), loc)], (env, denv, gs)) adamc@338: end adamc@754: | L.DView (x, e) => adamc@754: let adamc@754: val (e', t, gs') = elabExp (env, denv) e adamc@754: adamc@754: val k = (L'.KRecord (L'.KType, loc), loc) adam@1639: val fs = cunif env (loc, k) adam@1639: val ts = cunif env (loc, (L'.KRecord k, loc)) adamc@754: val tf = (L'.CApp ((L'.CMap (k, k), loc), adamc@754: (L'.CAbs ("_", k, (L'.CRecord ((L'.KType, loc), []), loc)), loc)), loc) adamc@754: val ts = (L'.CApp (tf, ts), loc) adamc@754: adamc@754: val cv = viewOf () adamc@754: val cv = (L'.CApp (cv, fs), loc) adamc@754: val (env', n) = E.pushENamed env x cv adamc@754: adamc@754: val ct = queryOf () adamc@1191: val ct = (L'.CApp (ct, (L'.CRecord ((L'.KRecord (L'.KType, loc), loc), []), loc)), loc) adam@1395: val ct = (L'.CApp (ct, (L'.CRecord ((L'.KRecord (L'.KType, loc), loc), []), loc)), loc) adamc@754: val ct = (L'.CApp (ct, ts), loc) adamc@754: val ct = (L'.CApp (ct, fs), loc) adamc@754: in adamc@754: checkCon env e' t ct; adamc@754: ([(L'.DView (!basis_r, x, n, e', fs), loc)], adamc@754: (env', denv, gs' @ gs)) adamc@754: end adamc@255: adamc@280: | L.DDatabase s => ([(L'.DDatabase s, loc)], (env, denv, gs)) adamc@280: adamc@459: | L.DCookie (x, c) => adamc@459: let adamc@459: val (c', k, gs') = elabCon (env, denv) c adamc@459: val (env, n) = E.pushENamed env x (L'.CApp (cookieOf (), c'), loc) adamc@459: in adamc@459: checkKind env c' k (L'.KType, loc); adamc@459: ([(L'.DCookie (!basis_r, x, n, c'), loc)], (env, denv, enD gs' @ gs)) adamc@459: end adamc@720: | L.DStyle x => adamc@718: let adamc@720: val (env, n) = E.pushENamed env x (styleOf ()) adamc@718: in adamc@720: ([(L'.DStyle (!basis_r, x, n), loc)], (env, denv, gs)) adamc@718: end adamc@1075: | L.DTask (e1, e2) => adamc@1073: let adamc@1075: val (e1', t1, gs1) = elabExp (env, denv) e1 adamc@1075: val (e2', t2, gs2) = elabExp (env, denv) e2 adamc@1075: adam@1639: val targ = cunif env (loc, (L'.KType, loc)) adam@1348: adamc@1075: val t1' = (L'.CModProj (!basis_r, [], "task_kind"), loc) adam@1348: val t1' = (L'.CApp (t1', targ), loc) adam@1348: adamc@1075: val t2' = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), adamc@1075: (L'.TRecord (L'.CRecord ((L'.KType, loc), []), loc), loc)), loc) adam@1348: val t2' = (L'.TFun (targ, t2'), loc) adamc@1073: in adamc@1075: checkCon env e1' t1 t1'; adamc@1075: checkCon env e2' t2 t2'; adamc@1075: ([(L'.DTask (e1', e2'), loc)], (env, denv, gs2 @ gs1 @ gs)) adamc@1073: end adamc@1199: | L.DPolicy e1 => adamc@1199: let adamc@1199: val (e1', t1, gs1) = elabExp (env, denv) e1 adamc@1199: adamc@1199: val t1' = (L'.CModProj (!basis_r, [], "sql_policy"), loc) adamc@1199: in adamc@1199: checkCon env e1' t1 t1'; adamc@1199: ([(L'.DPolicy e1', loc)], (env, denv, gs1 @ gs)) adamc@1199: end adamc@459: adam@1294: | L.DOnError (m1, ms, s) => adam@1294: (case E.lookupStr env m1 of adam@1294: NONE => (expError env (UnboundStrInExp (loc, m1)); adam@1294: ([], (env, denv, []))) adam@1294: | SOME (n, sgn) => adam@1294: let adam@1294: val (str, sgn) = foldl (fn (m, (str, sgn)) => adam@1294: case E.projectStr env {sgn = sgn, str = str, field = m} of adam@1294: NONE => (conError env (UnboundStrInCon (loc, m)); adam@1294: (strerror, sgnerror)) adam@1294: | SOME sgn => ((L'.StrProj (str, m), loc), sgn)) adam@1294: ((L'.StrVar n, loc), sgn) ms adam@1294: adam@1294: val t = case E.projectVal env {sgn = sgn, str = str, field = s} of adam@1294: NONE => (expError env (UnboundExp (loc, s)); adam@1294: cerror) adam@1294: | SOME t => t adam@1294: adam@1294: val page = (L'.CModProj (!basis_r, [], "page"), loc) adam@1294: val xpage = (L'.CApp ((L'.CModProj (!basis_r, [], "transaction"), loc), page), loc) adam@1294: val func = (L'.TFun ((L'.CModProj (!basis_r, [], "xbody"), loc), xpage), loc) adam@1294: in adam@1407: (unifyCons env loc t func adam@1407: handle CUnify _ => ErrorMsg.error "onError handler has wrong type."); adam@1294: ([(L'.DOnError (n, ms, s), loc)], (env, denv, gs)) adam@1294: end) adam@1294: adam@2010: | L.DFfi (x, modes, t) => adam@2010: let adam@2010: val () = if Settings.getLessSafeFfi () then adam@2010: () adam@2010: else adam@2010: ErrorMsg.errorAt loc "To enable 'ffi' declarations, the .urp directive 'lessSafeFfi' is mandatory." adam@2010: adam@2010: val (t', _, gs1) = elabCon (env, denv) t adam@2010: val t' = normClassConstraint env t' adam@2010: val (env', n) = E.pushENamed env x t' adam@2010: in adam@2010: ([(L'.DFfi (x, n, modes, t'), loc)], (env', denv, enD gs1 @ gs)) adam@2010: end adam@2010: adamc@280: (*val tcs = List.filter (fn TypeClass _ => true | _ => false) (#3 (#2 r))*) adamc@255: in adam@1989: (*prefaces "/elabDecl" [("d", SourcePrint.p_decl dAll), adam@1989: ("d'", p_list_sep PD.newline (ElabPrint.p_decl env) (#1 r))];*) adamc@255: r adamc@255: end adamc@211: adamc@83: and elabStr (env, denv) (str, loc) = adamc@31: case str of adamc@31: L.StrConst ds => adamc@31: let adamc@88: val (ds', (_, _, gs)) = ListUtil.foldlMapConcat elabDecl (env, denv, []) ds adamc@123: val sgis = ListUtil.mapConcat sgiOfDecl ds' adamc@63: adamc@63: val (sgis, _, _, _, _) = adamc@64: foldr (fn ((sgi, loc), (sgis, cons, vals, sgns, strs)) => adamc@63: case sgi of adamc@64: L'.SgiConAbs (x, n, k) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiConAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiCon (x, n, k, c) => adamc@64: let adamc@64: val (cons, x) = adamc@64: if SS.member (cons, x) then adamc@64: (cons, "?" ^ x) adamc@64: else adamc@64: (SS.add (cons, x), x) adamc@64: in adamc@64: ((L'.SgiCon (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@805: | L'.SgiDatatype dts => adamc@156: let adamc@805: fun doOne ((x, n, xs, xncs), (cons, vals)) = adamc@805: let adamc@805: val (cons, x) = adamc@805: if SS.member (cons, x) then adamc@805: (cons, "?" ^ x) adamc@156: else adamc@805: (SS.add (cons, x), x) adamc@805: adamc@805: val (xncs, vals) = adamc@805: ListUtil.foldlMap adamc@805: (fn ((x, n, t), vals) => adamc@805: if SS.member (vals, x) then adamc@805: (("?" ^ x, n, t), vals) adamc@805: else adamc@805: ((x, n, t), SS.add (vals, x))) adamc@805: vals xncs adamc@805: in adamc@805: ((x, n, xs, xncs), (cons, vals)) adamc@805: end adamc@805: adamc@805: val (dts, (cons, vals)) = ListUtil.foldlMap doOne (cons, vals) dts adamc@156: in adamc@805: ((L'.SgiDatatype dts, loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@191: | L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs) => adamc@156: let adamc@156: val (cons, x) = adamc@156: if SS.member (cons, x) then adamc@156: (cons, "?" ^ x) adamc@156: else adamc@156: (SS.add (cons, x), x) adamc@156: in adamc@191: ((L'.SgiDatatypeImp (x, n, m1, ms, x', xs, xncs), loc) :: sgis, cons, vals, sgns, strs) adamc@156: end adamc@64: | L'.SgiVal (x, n, c) => adamc@64: let adamc@64: val (vals, x) = adamc@64: if SS.member (vals, x) then adamc@64: (vals, "?" ^ x) adamc@64: else adamc@64: (SS.add (vals, x), x) adamc@64: in adamc@64: ((L'.SgiVal (x, n, c), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: | L'.SgiSgn (x, n, sgn) => adamc@64: let adamc@64: val (sgns, x) = adamc@64: if SS.member (sgns, x) then adamc@64: (sgns, "?" ^ x) adamc@64: else adamc@64: (SS.add (sgns, x), x) adamc@64: in adamc@64: ((L'.SgiSgn (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@64: end adamc@64: adamc@64: | L'.SgiStr (x, n, sgn) => adamc@64: let adamc@64: val (strs, x) = adamc@64: if SS.member (strs, x) then adamc@64: (strs, "?" ^ x) adamc@64: else adamc@64: (SS.add (strs, x), x) adamc@64: in adamc@64: ((L'.SgiStr (x, n, sgn), loc) :: sgis, cons, vals, sgns, strs) adamc@88: end adamc@203: | L'.SgiConstraint _ => ((sgi, loc) :: sgis, cons, vals, sgns, strs) adamc@563: | L'.SgiClassAbs (x, n, k) => adamc@211: let adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@563: ((L'.SgiClassAbs (x, n, k), loc) :: sgis, cons, vals, sgns, strs) adamc@211: end adamc@563: | L'.SgiClass (x, n, k, c) => adamc@211: let adamc@211: val (cons, x) = adamc@211: if SS.member (cons, x) then adamc@211: (cons, "?" ^ x) adamc@211: else adamc@211: (SS.add (cons, x), x) adamc@211: in adamc@563: ((L'.SgiClass (x, n, k, c), loc) :: sgis, cons, vals, sgns, strs) adamc@203: end) adamc@64: adamc@63: ([], SS.empty, SS.empty, SS.empty, SS.empty) sgis adamc@31: in adamc@83: ((L'.StrConst ds', loc), (L'.SgnConst sgis, loc), gs) adamc@31: end adamc@31: | L.StrVar x => adamc@31: (case E.lookupStr env x of adamc@31: NONE => adamc@31: (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME (n, sgn) => ((L'.StrVar n, loc), sgn, [])) adamc@34: | L.StrProj (str, x) => adamc@34: let adamc@83: val (str', sgn, gs) = elabStr (env, denv) str adamc@34: in adamc@34: case E.projectStr env {str = str', sgn = sgn, field = x} of adamc@34: NONE => (strError env (UnboundStr (loc, x)); adamc@83: (strerror, sgnerror, [])) adamc@83: | SOME sgn => ((L'.StrProj (str', x), loc), sgn, gs) adamc@34: end adamc@41: | L.StrFun (m, dom, ranO, str) => adamc@41: let adamc@83: val (dom', gs1) = elabSgn (env, denv) dom adamc@41: val (env', n) = E.pushStrNamed env m dom' adamc@834: val denv' = dopenConstraints (loc, env', denv) {str = m, strs = []} adamc@834: val (str', actual, gs2) = elabStr (env', denv') str adamc@41: adamc@83: val (formal, gs3) = adamc@41: case ranO of adamc@83: NONE => (actual, []) adamc@41: | SOME ran => adamc@41: let adamc@834: val (ran', gs) = elabSgn (env', denv') ran adamc@41: in adamc@1000: subSgn env' loc 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@1275: let adamc@1275: val s = wildifyStr env (str2, dom) adamc@1275: in adamc@1275: (*Print.preface ("Wild", SourcePrint.p_str s);*) adamc@1275: s adamc@1275: end adamc@325: | _ => str2 adamc@83: val (str2', sgn2, gs2) = elabStr (env, denv) str2 adamc@1270: in adamc@44: case #1 (hnormSgn env sgn1) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnFun (m, n, dom, ran) => adamc@1000: (subSgn env loc sgn2 dom; adamc@44: case #1 (hnormSgn env ran) of adamc@83: L'.SgnError => (strerror, sgnerror, []) adamc@44: | L'.SgnConst sgis => adam@1968: let adam@1968: (* This code handles a tricky case that led to a very nasty bug. adam@1968: * An invariant about signatures of elaborated modules is that no adam@1968: * identifier that could appear directly in a program is defined adam@1968: * twice. We add "?" in front of identifiers where necessary to adam@1968: * maintain the invariant, but the code below, to extend a functor adam@1968: * body with a binding for the functor argument, wasn't written adam@1968: * with the invariant in mind. Luckily for us, references to adam@1968: * an identifier later within a signature work by globally adam@1968: * unique index, so we just need to change the string name in the adam@1989: * new declaration. adam@1989: * adam@1989: * ~~~ A few days later.... ~~~ adam@1989: * This is trickier than I thought! We might need to add adam@1989: * arbitarily many question marks before the module name to adam@1989: * avoid a clash, since some other code might depend on adam@1989: * question-mark identifiers generated previously by this adam@1989: * very code fragment. *) adam@1989: fun mungeName m = adam@1968: if List.exists (fn (L'.SgiStr (x, _, _), _) => x = m adam@1968: | _ => false) sgis then adam@1989: mungeName ("?" ^ m) adam@1968: else adam@1968: m adam@1989: adam@1989: val m = mungeName m adam@1968: in adam@1968: ((L'.StrApp (str1', str2'), loc), adam@1968: (L'.SgnConst ((L'.SgiStr (m, n, selfifyAt env {str = str2', sgn = sgn2}), loc) :: sgis), loc), adam@1968: gs1 @ gs2) adam@1968: end 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@987: fun resolveClass env = E.resolveClass (hnormCon env) (consEq env dummy) env adamc@833: adam@1732: fun elabFile basis basis_tm topStr topSgn top_tm env file = adamc@56: let adam@1737: val () = ModDb.snapshot () adam@1737: adamc@713: val () = mayDelay := true adamc@713: val () = delayedUnifs := [] adamc@830: val () = delayedExhaustives := [] adamc@713: adam@1733: val d = (L.DFfiStr ("Basis", (L.SgnConst basis, ErrorMsg.dummySpan), SOME basis_tm), ErrorMsg.dummySpan) adam@1732: val (basis_n, env', sgn) = adam@1733: case (if !incremental then ModDb.lookup d else NONE) of adam@1732: NONE => adam@1732: let adam@1732: val (sgn, gs) = elabSgn (env, D.empty) (L.SgnConst basis, ErrorMsg.dummySpan) adam@1732: val () = case gs of adam@1732: [] => () adam@1732: | _ => (app (fn (_, env, _, c1, c2) => adam@1732: prefaces "Unresolved" adam@1732: [("c1", p_con env c1), adam@1732: ("c2", p_con env c2)]) gs; adam@1732: raise Fail "Unresolved disjointness constraints in Basis") adam@1732: adam@1732: val (env', basis_n) = E.pushStrNamed env "Basis" sgn adam@1732: in adam@1732: ModDb.insert ((L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan), basis_tm); adam@1732: (basis_n, env', sgn) adam@1732: end adam@1732: | SOME (d' as (L'.DFfiStr (_, basis_n, sgn), _)) => adam@1732: (basis_n, E.pushStrNamedAs env "Basis" basis_n sgn, sgn) adam@1732: | _ => raise Fail "Elaborate: Basis impossible" adam@1732: adamc@210: val () = basis_r := basis_n adamc@628: val (ds, env') = dopen env' {str = basis_n, strs = [], sgn = sgn} adamc@56: adamc@56: fun discoverC r x = adamc@56: case E.lookupC env' x of adamc@56: E.NotBound => raise Fail ("Constructor " ^ x ^ " unbound in Basis") adamc@56: | E.Rel _ => raise Fail ("Constructor " ^ x ^ " bound relatively in Basis") adamc@56: | E.Named (n, (_, loc)) => r := (L'.CNamed n, loc) adamc@56: adamc@56: val () = discoverC int "int" adamc@56: val () = discoverC float "float" adamc@56: val () = discoverC string "string" adamc@821: val () = discoverC char "char" adamc@203: val () = discoverC table "sql_table" adamc@56: adam@1732: val d = (L.DStr ("Top", SOME (L.SgnConst topSgn, ErrorMsg.dummySpan), adam@1732: SOME (if Time.< (top_tm, basis_tm) then basis_tm else top_tm), adam@1868: (L.StrConst topStr, ErrorMsg.dummySpan), false), ErrorMsg.dummySpan) adam@1732: val (top_n, env', topSgn, topStr) = adam@1733: case (if !incremental then ModDb.lookup d else NONE) of adam@1732: NONE => adam@1732: let adam@1732: val (topSgn, gs) = elabSgn (env', D.empty) (L.SgnConst topSgn, ErrorMsg.dummySpan) adam@1732: val () = case gs of adam@1732: [] => () adam@1732: | _ => raise Fail "Unresolved disjointness constraints in top.urs" adam@1732: val (topStr, topSgn', gs) = elabStr (env', D.empty) (L.StrConst topStr, ErrorMsg.dummySpan) adam@1732: adam@1732: val () = case gs of adam@1732: [] => () adam@1732: | _ => app (fn Disjoint (loc, env, denv, c1, c2) => adam@1732: (case D.prove env denv (c1, c2, loc) of adam@1732: [] => () adam@1732: | _ => adam@1732: (prefaces "Unresolved constraint in top.ur" adam@1732: [("loc", PD.string (ErrorMsg.spanToString loc)), adam@1732: ("c1", p_con env c1), adam@1732: ("c2", p_con env c2)]; adam@1732: raise Fail "Unresolved constraint in top.ur")) adam@1732: | TypeClass (env, c, r, loc) => adam@1732: let adam@1732: val c = normClassKey env c adam@1732: in adam@1732: case resolveClass env c of adam@1732: SOME e => r := SOME e adam@1732: | NONE => expError env (Unresolvable (loc, c)) adam@1732: end) gs adam@1732: adam@1732: val () = subSgn env' ErrorMsg.dummySpan topSgn' topSgn adam@1732: adam@1732: val (env', top_n) = E.pushStrNamed env' "Top" topSgn adam@1732: in adam@1732: ModDb.insert ((L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan), top_tm); adam@1732: (top_n, env', topSgn, topStr) adam@1732: end adam@1732: | SOME (d' as (L'.DStr (_, top_n, topSgn, topStr), _)) => adam@1732: (top_n, E.declBinds env' d', topSgn, topStr) adam@1732: | _ => raise Fail "Elaborate: Top impossible" adam@1732: adamc@633: val () = top_r := top_n adamc@325: adamc@628: val (ds', env') = dopen env' {str = top_n, strs = [], sgn = topSgn} adamc@325: adam@1883: fun elabDecl' x = adam@1883: (resetKunif (); adam@1883: resetCunif (); adam@1883: elabDecl x) adam@1883: adam@1883: val (file, (env'', _, gs)) = ListUtil.foldlMapConcat elabDecl' (env', D.empty, []) file adamc@753: adamc@777: fun oneSummaryRound () = adamc@777: if ErrorMsg.anyErrors () then adamc@777: () adamc@777: else adamc@777: let adamc@777: val delayed = !delayedUnifs adamc@777: in adamc@777: delayedUnifs := []; adamc@777: app (fn (loc, env, k, s1, s2) => adamc@777: unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) adamc@777: delayed adamc@777: end adam@1576: adam@1576: val checkConstraintErrors = ref (fn () => ()) adam@1723: fun stopHere () = not (!unifyMore) andalso ErrorMsg.anyErrors () adamc@56: in adamc@777: oneSummaryRound (); adamc@753: adam@1723: if stopHere () then adamc@753: () adamc@753: else adamc@753: let adam@1767: fun solver (gs : constraint list) = adamc@753: let adamc@753: val (gs, solved) = adamc@753: ListUtil.foldlMapPartial adam@1767: (fn (g : constraint, solved) => adamc@753: case g of adamc@753: Disjoint (loc, env, denv, c1, c2) => adamc@753: (case D.prove env denv (c1, c2, loc) of adamc@753: [] => (NONE, true) adamc@753: | _ => (SOME g, solved)) adamc@753: | TypeClass (env, c, r, loc) => adamc@753: let adamc@753: fun default () = (SOME g, solved) adam@1767: adam@1767: fun resolver r c = adam@1767: let adam@1767: val c = normClassKey env c adam@1767: in adam@1767: case resolveClass env c of adam@1767: SOME e => (r := SOME e; adam@1767: (NONE, true)) adam@1767: | NONE => adam@1767: case #1 (hnormCon env c) of adam@1767: L'.CApp (f, x) => adam@1767: (case (#1 (hnormCon env f), #1 (hnormCon env x)) of adam@1767: (L'.CKApp (f, _), L'.CRecord (k, xcs)) => adam@1767: (case #1 (hnormCon env f) of adam@1767: L'.CModProj (top_n', [], "folder") => adam@1767: if top_n' = top_n then adam@1767: let adam@1767: val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) adam@1767: val e = (L'.EKApp (e, k), loc) adam@1767: adam@1767: val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => adam@1767: let adam@1767: val e = (L'.EModProj (top_n, ["Folder"], adam@1767: "cons"), loc) adam@1767: val e = (L'.EKApp (e, k), loc) adam@1767: val e = (L'.ECApp (e, adam@1767: (L'.CRecord (k, xcs), adam@1767: loc)), loc) adam@1767: val e = (L'.ECApp (e, x), loc) adam@1767: val e = (L'.ECApp (e, c), loc) adam@1767: val e = (L'.EApp (e, folder), loc) adam@1767: in adam@1767: (e, (x, c) :: xcs) adam@1767: end) adam@1767: (e, []) xcs adam@1767: in adam@1767: (r := SOME folder; adam@1767: (NONE, true)) adam@1767: end adam@1767: else adam@1767: default () adam@1767: | _ => default ()) adam@1767: | _ => default ()) adam@1767: adam@1767: | L'.TRecord c' => adam@1767: (case #1 (hnormCon env c') of adam@1767: L'.CRecord (_, xts) => adam@1767: let adam@1767: val witnesses = map (fn (x, t) => adam@1767: let adam@1767: val r = ref NONE adam@1767: val (opt, _) = resolver r t adam@1767: in adam@1767: case opt of adam@1767: SOME _ => NONE adam@1767: | NONE => adam@1767: case !r of adam@1767: NONE => NONE adam@1767: | SOME e => adam@1767: SOME (x, e, t) adam@1767: end) xts adam@1767: in adam@1767: if List.all Option.isSome witnesses then adam@1767: (r := SOME (L'.ERecord (map valOf witnesses), loc); adam@1767: (NONE, true)) adam@1767: else adam@1767: (SOME g, solved) adam@1767: end adam@1767: | _ => (SOME g, solved)) adam@1767: adam@1767: | _ => default () adam@1767: end adamc@753: in adam@1767: resolver r c adamc@753: end) adamc@753: false gs adamc@753: in adamc@753: case (gs, solved) of adamc@753: ([], _) => () adamc@777: | (_, true) => (oneSummaryRound (); solver gs) adamc@753: | _ => adam@1576: checkConstraintErrors := adam@1576: (fn () => app (fn Disjoint (loc, env, denv, c1, c2) => adam@1576: let adam@1576: val c1' = ElabOps.hnormCon env c1 adam@1576: val c2' = ElabOps.hnormCon env c2 adam@1576: adam@1576: fun isUnif (c, _) = adam@1576: case c of adam@1576: L'.CUnif _ => true adam@1576: | _ => false adam@1576: adam@1576: fun maybeAttr (c, _) = adam@1576: case c of adam@1576: L'.CRecord ((L'.KType, _), xts) => true adam@1576: | _ => false adam@1576: in adam@1576: ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; adam@1576: eprefaces' [("Con 1", p_con env c1), adam@1576: ("Con 2", p_con env c2), adam@1576: ("Hnormed 1", p_con env c1'), adam@1576: ("Hnormed 2", p_con env c2')] adam@1576: adam@1576: (*app (fn (loc, env, k, s1, s2) => adam@1576: eprefaces' [("s1", p_summary env (normalizeRecordSummary env s1)), adam@1576: ("s2", p_summary env (normalizeRecordSummary env s2))]) adam@1576: (!delayedUnifs);*) adam@1576: end adam@1576: | TypeClass (env, c, r, loc) => adam@1742: let adam@1742: val c = normClassKey env c adam@1742: in adam@1742: case resolveClass env c of adam@1767: SOME e => r := SOME e adam@1742: | NONE => expError env (Unresolvable (loc, c)) adam@1742: end) adam@1576: gs) adamc@753: end adamc@753: in adamc@753: solver gs adamc@753: end; adamc@753: adamc@713: mayDelay := false; adamc@713: adam@1723: if stopHere () then adamc@777: () adamc@777: else adamc@777: (app (fn (loc, env, k, s1, s2) => adamc@777: unifySummaries env (loc, k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) adam@1719: handle CUnify' (env', err) => (ErrorMsg.errorAt loc "Error in final record unification"; adam@1719: cunifyError env' err; adam@1719: case !reducedSummaries of adam@1719: NONE => () adam@1719: | SOME (s1, s2) => adam@1719: (ErrorMsg.errorAt loc "Stuck unifying these records after canceling matching pieces:"; adam@1719: eprefaces' [("Have", s1), adam@1719: ("Need", s2)]))) adamc@777: (!delayedUnifs); adamc@777: delayedUnifs := []); adamc@713: adam@1723: if stopHere () then adam@1346: () adam@1346: else adam@1584: if List.exists kunifsInDecl file then adam@1584: case U.File.findDecl kunifsInDecl file of adam@1584: NONE => () adam@1584: | SOME d => declError env'' (KunifsRemain [d]) adam@1584: else adam@1584: (); adam@1345: adam@1723: if stopHere () then adam@1346: () adam@1346: else adam@1584: if List.exists cunifsInDecl file then adam@1584: case U.File.findDecl cunifsInDecl file of adam@1584: NONE => () adam@1584: | SOME d => declError env'' (CunifsRemain [d]) adam@1584: else adam@1584: (); adamc@750: adam@1723: if stopHere () then adamc@830: () adamc@830: else adamc@837: app (fn all as (env, _, _, loc) => adamc@830: case exhaustive all of adamc@830: NONE => () adamc@830: | SOME p => expError env (Inexhaustive (loc, p))) adamc@830: (!delayedExhaustives); adamc@830: adam@1723: if stopHere () then adam@1576: () adam@1576: else adam@1576: !checkConstraintErrors (); adam@1576: adamc@799: (*preface ("file", p_file env' file);*) adam@1531: adam@1745: if !dumpTypes orelse (!dumpTypesOnError andalso ErrorMsg.anyErrors ()) then adam@1531: let adam@1531: open L' adam@1531: open Print.PD adam@1531: open Print adam@1531: adam@1715: fun p_con env c = ElabPrint.p_con env (ElabOps.reduceCon env c) adam@1715: adam@1531: fun dumpDecl (d, env) = adam@1531: case #1 d of adam@1531: DCon (x, _, k, _) => (print (box [string x, adam@1531: space, adam@1531: string "::", adam@1531: space, adam@1531: p_kind env k, adam@1531: newline, adam@1531: newline]); adam@1531: E.declBinds env d) adam@1531: | DVal (x, _, t, _) => (print (box [string x, adam@1531: space, adam@1531: string ":", adam@1531: space, adam@1531: p_con env t, adam@1531: newline, adam@1531: newline]); adam@1531: E.declBinds env d) adam@1531: | DValRec vis => (app (fn (x, _, t, _) => print (box [string x, adam@1531: space, adam@1531: string ":", adam@1531: space, adam@1531: p_con env t, adam@1531: newline, adam@1531: newline])) vis; adam@1531: E.declBinds env d) adam@1531: | DStr (x, _, _, str) => (print (box [string ("<" ^ x ^ ">"), adam@1531: newline, adam@1531: newline]); adam@1531: dumpStr (str, env); adam@1531: print (box [string (""), adam@1531: newline, adam@1531: newline]); adam@1531: E.declBinds env d) adam@1531: | _ => E.declBinds env d adam@1531: adam@1531: and dumpStr (str, env) = adam@1531: case #1 str of adam@1531: StrConst ds => ignore (foldl dumpDecl env ds) adam@1531: | _ => () adam@1531: in adam@1531: ignore (foldl dumpDecl env' file) adam@1531: end adam@1531: else adam@1531: (); adam@1737: adam@1737: if ErrorMsg.anyErrors () then adam@1737: ModDb.revert () adam@1737: else adam@1737: (); adam@1912: adam@1912: (*Print.preface("File", ElabPrint.p_file env file);*) adam@1345: 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