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