adamc@81: (* Copyright (c) 2008, Adam Chlipala adamc@81: * All rights reserved. adamc@81: * adamc@81: * Redistribution and use in source and binary forms, with or without adamc@81: * modification, are permitted provided that the following conditions are met: adamc@81: * adamc@81: * - Redistributions of source code must retain the above copyright notice, adamc@81: * this list of conditions and the following disclaimer. adamc@81: * - Redistributions in binary form must reproduce the above copyright notice, adamc@81: * this list of conditions and the following disclaimer in the documentation adamc@81: * and/or other materials provided with the distribution. adamc@81: * - The names of contributors may not be used to endorse or promote products adamc@81: * derived from this software without specific prior written permission. adamc@81: * adamc@81: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@81: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@81: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@81: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@81: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@81: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@81: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@81: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@81: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@81: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@81: * POSSIBILITY OF SUCH DAMAGE. adamc@81: *) adamc@81: adamc@81: structure ElabOps :> ELAB_OPS = struct adamc@81: adamc@81: open Elab adamc@81: adamc@81: structure E = ElabEnv adamc@81: structure U = ElabUtil adamc@81: adamc@623: fun liftKindInKind' by = adamc@623: U.Kind.mapB {kind = fn bound => fn k => adamc@623: case k of adamc@623: KRel xn => adamc@623: if xn < bound then adamc@623: k adamc@623: else adamc@623: KRel (xn + by) adamc@623: | _ => k, adamc@623: bind = fn (bound, _) => bound + 1} adamc@623: adamc@623: fun subKindInKind' rep = adamc@623: U.Kind.mapB {kind = fn (by, xn) => fn k => adamc@623: case k of adamc@623: KRel xn' => adamc@623: (case Int.compare (xn', xn) of adamc@623: EQUAL => #1 (liftKindInKind' by 0 rep) adamc@623: | GREATER => KRel (xn' - 1) adamc@623: | LESS => k) adamc@623: | _ => k, adamc@623: bind = fn ((by, xn), _) => (by+1, xn+1)} adamc@623: adamc@623: val liftKindInKind = liftKindInKind' 1 adamc@623: adamc@623: fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn) adamc@623: adamc@623: fun liftKindInCon by = adamc@623: U.Con.mapB {kind = fn bound => fn k => adamc@623: case k of adamc@623: KRel xn => adamc@623: if xn < bound then adamc@623: k adamc@623: else adamc@623: KRel (xn + by) adamc@623: | _ => k, adamc@623: con = fn _ => fn c => c, adamc@623: bind = fn (bound, U.Con.RelK _) => bound + 1 adamc@623: | (bound, _) => bound} adamc@623: adamc@623: fun subKindInCon' rep = adamc@623: U.Con.mapB {kind = fn (by, xn) => fn k => adamc@623: case k of adamc@623: KRel xn' => adamc@623: (case Int.compare (xn', xn) of adamc@623: EQUAL => #1 (liftKindInKind' by 0 rep) adamc@623: | GREATER => KRel (xn' - 1) adamc@623: | LESS => k) adamc@623: | _ => k, adamc@623: con = fn _ => fn c => c, adamc@623: bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1) adamc@623: | (st, _) => st} adamc@623: adamc@623: val liftKindInCon = liftKindInCon 1 adamc@623: adamc@623: fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn) adamc@623: adamc@516: fun liftConInCon by = adamc@623: U.Con.mapB {kind = fn _ => fn k => k, adamc@516: con = fn bound => fn c => adamc@516: case c of adamc@516: CRel xn => adamc@516: if xn < bound then adamc@516: c adamc@516: else adamc@516: CRel (xn + by) adam@1303: | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r) adamc@516: | _ => c, adamc@623: bind = fn (bound, U.Con.RelC _) => bound + 1 adamc@516: | (bound, _) => bound} adamc@81: adam@1303: exception SubUnif adam@1303: adamc@516: fun subConInCon' rep = adamc@623: U.Con.mapB {kind = fn _ => fn k => k, adamc@516: con = fn (by, xn) => fn c => adamc@516: case c of adamc@516: CRel xn' => adamc@516: (case Int.compare (xn', xn) of adamc@516: EQUAL => #1 (liftConInCon by 0 rep) adamc@516: | GREATER => CRel (xn' - 1) adamc@516: | LESS => c) adam@1303: | CUnif (0, _, _, _, _) => raise SubUnif adam@1303: | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r) adamc@516: | _ => c, adamc@623: bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) adamc@81: | (ctx, _) => ctx} adamc@81: adamc@516: val liftConInCon = liftConInCon 1 adamc@516: adamc@516: fun subConInCon (xn, rep) = subConInCon' rep (0, xn) adamc@516: adamc@81: fun subStrInSgn (m1, m2) = adamc@81: U.Sgn.map {kind = fn k => k, adamc@81: con = fn c as CModProj (m1', ms, x) => adamc@81: if m1 = m1' then adamc@81: CModProj (m2, ms, x) adamc@81: else adamc@81: c adamc@81: | c => c, adamc@81: sgn_item = fn sgi => sgi, adamc@81: sgn = fn sgn => sgn} adamc@81: adamc@905: val occurs = adamc@905: U.Con.existsB {kind = fn _ => false, adamc@905: con = fn (n, c) => adamc@905: case c of adamc@905: CRel n' => n' = n adamc@905: | _ => false, adamc@905: bind = fn (n, b) => adamc@905: case b of adamc@905: U.Con.RelC _ => n + 1 adamc@905: | _ => n} adamc@905: 0 adamc@905: adamc@1034: val identity = ref 0 adamc@1034: val distribute = ref 0 adamc@1034: val fuse = ref 0 adamc@1034: adamc@1034: fun reset () = (identity := 0; adamc@1034: distribute := 0; adamc@1034: fuse := 0) adamc@81: adamc@81: fun hnormCon env (cAll as (c, loc)) = adamc@81: case c of adam@1591: CUnif (nl, _, _, _, ref (SOME c)) => (#1 (hnormCon env (E.mliftConInCon nl c)), loc) adamc@81: adamc@81: | CNamed xn => adamc@81: (case E.lookupCNamed env xn of adamc@81: (_, _, SOME c') => hnormCon env c' adamc@81: | _ => cAll) adamc@81: adamc@81: | CModProj (n, ms, x) => adamc@81: let adamc@81: val (_, sgn) = E.lookupStrNamed env n adamc@81: val (str, sgn) = foldl (fn (m, (str, sgn)) => adamc@81: case E.projectStr env {sgn = sgn, str = str, field = m} of adamc@81: NONE => raise Fail "hnormCon: Unknown substructure" adamc@81: | SOME sgn => ((StrProj (str, m), loc), sgn)) adamc@81: ((StrVar n, loc), sgn) ms adamc@81: in adamc@81: case E.projectCon env {sgn = sgn, str = str, field = x} of adamc@81: NONE => raise Fail "kindof: Unknown con in structure" adamc@81: | SOME (_, NONE) => cAll adamc@81: | SOME (_, SOME c) => hnormCon env c adamc@81: end adamc@81: adamc@905: (* Eta reduction *) adamc@905: | CAbs (x, k, b) => adamc@905: (case #1 (hnormCon (E.pushCRel env x k) b) of adamc@905: CApp (f, (CRel 0, _)) => adamc@905: if occurs f then adamc@905: cAll adamc@905: else adamc@905: hnormCon env (subConInCon (0, (CUnit, loc)) f) adamc@905: | _ => cAll) adamc@905: adamc@81: | CApp (c1, c2) => adamc@81: (case #1 (hnormCon env c1) of adamc@81: CAbs (x, k, cb) => adamc@81: let adamc@81: val sc = (hnormCon env (subConInCon (0, c2) cb)) adamc@81: handle SynUnif => cAll adamc@81: (*val env' = E.pushCRel env x k*) adamc@81: in adamc@328: (*Print.eprefaces "Subst" [("x", Print.PD.string x), adamc@328: ("cb", ElabPrint.p_con env' cb), adamc@328: ("c2", ElabPrint.p_con env c2), adamc@328: ("sc", ElabPrint.p_con env sc)];*) adamc@81: sc adamc@81: end adamc@621: | c1' as CApp (c', f) => adamc@326: let adamc@326: fun default () = (CApp ((c1', loc), hnormCon env c2), loc) adamc@326: in adamc@326: case #1 (hnormCon env c') of adamc@621: CMap (ks as (k1, k2)) => adamc@621: (case #1 (hnormCon env c2) of adamc@621: CRecord (_, []) => (CRecord (k2, []), loc) adamc@621: | CRecord (_, (x, c) :: rest) => adamc@621: hnormCon env adamc@621: (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), adamc@621: (CApp (c1, (CRecord (k2, rest), loc)), loc)), loc) adamc@621: | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => adamc@621: let adamc@621: val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) adamc@621: in adamc@621: hnormCon env adamc@621: (CConcat ((CRecord (k2, [(x, (CApp (f, c), loc))]), loc), adamc@621: (CApp (c1, rest''), loc)), loc) adamc@621: end adamc@621: | _ => adamc@621: let adamc@621: fun unconstraint c = adamc@621: case hnormCon env c of adamc@628: (TDisjoint (_, _, c), _) => unconstraint c adamc@621: | c => c adamc@81: adamc@1034: fun inc r = r := !r + 1 adamc@1034: adamc@621: fun tryDistributivity () = adamc@621: case hnormCon env c2 of adamc@621: (CConcat (c1, c2'), _) => adamc@621: let adamc@621: val c = (CMap ks, loc) adamc@621: val c = (CApp (c, f), loc) adamc@621: adamc@621: val c1 = (CApp (c, c1), loc) adamc@621: val c2 = (CApp (c, c2'), loc) adamc@621: val c = (CConcat (c1, c2), loc) adamc@621: in adamc@1034: inc distribute; adamc@621: hnormCon env c adamc@621: end adamc@621: | _ => default () adamc@329: adamc@621: fun tryFusion () = adamc@621: case #1 (hnormCon env c2) of adamc@621: CApp (f', r') => adamc@621: (case #1 (hnormCon env f') of adamc@621: CApp (f', inner_f) => adamc@621: (case #1 (hnormCon env f') of adamc@621: CMap (dom, _) => adamc@621: let adamc@990: val inner_f = liftConInCon 0 inner_f adamc@990: val f = liftConInCon 0 f adamc@990: adamc@621: val f' = (CApp (inner_f, (CRel 0, loc)), loc) adamc@621: val f' = (CApp (f, f'), loc) adamc@621: val f' = (CAbs ("v", dom, f'), loc) adamc@329: adamc@621: val c = (CMap (dom, k2), loc) adamc@621: val c = (CApp (c, f'), loc) adamc@621: val c = (CApp (c, r'), loc) adamc@621: in adamc@1034: inc fuse; adamc@621: hnormCon env c adamc@621: end adamc@621: | _ => tryDistributivity ()) adamc@621: | _ => tryDistributivity ()) adamc@621: | _ => tryDistributivity () adamc@339: adamc@621: fun tryIdentity () = adamc@621: let adamc@621: fun cunif () = adamc@621: let adamc@621: val r = ref NONE adamc@621: in adam@1303: (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) adamc@621: end adamc@621: adamc@621: val (vR, v) = cunif () adamc@494: adamc@621: val c = (CApp (f, v), loc) adamc@621: in adamc@621: case unconstraint c of adam@1303: (CUnif (_, _, _, _, vR'), _) => adamc@621: if vR' = vR then adamc@1034: (inc identity; adamc@1034: hnormCon env c2) adamc@621: else adamc@621: tryFusion () adamc@621: | _ => tryFusion () adamc@621: end adamc@621: in adamc@621: tryIdentity () adamc@621: end) adamc@326: | _ => default () adamc@326: end adamc@326: | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) adamc@623: adamc@623: | CKApp (c1, k) => adamc@623: (case hnormCon env c1 of adamc@623: (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body) adamc@623: | _ => cAll) adamc@621: adamc@81: | CConcat (c1, c2) => adamc@81: (case (hnormCon env c1, hnormCon env c2) of adamc@81: ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => adamc@81: (CRecord (k, xcs1 @ xcs2), loc) adamc@81: | ((CRecord (_, []), _), c2') => c2' adamc@81: | ((CConcat (c11, c12), loc), c2') => adamc@81: hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc) adamc@209: | (c1', (CRecord (_, []), _)) => c1' adamc@329: | (c1', c2') => (CConcat (c1', c2'), loc)) adamc@81: adamc@207: | CProj (c, n) => adamc@207: (case hnormCon env c of adamc@207: (CTuple cs, _) => hnormCon env (List.nth (cs, n - 1)) adamc@207: | _ => cAll) adamc@207: adamc@81: | _ => cAll adamc@81: adamc@81: end