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@516: fun liftConInCon by = adamc@516: U.Con.mapB {kind = 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) adamc@516: (*| CUnif _ => raise SynUnif*) adamc@516: | _ => c, adamc@516: bind = fn (bound, U.Con.Rel _) => bound + 1 adamc@516: | (bound, _) => bound} adamc@81: adamc@516: fun subConInCon' rep = adamc@81: U.Con.mapB {kind = 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) adamc@516: (*| CUnif _ => raise SynUnif*) adamc@516: | _ => c, adamc@516: bind = fn ((by, xn), U.Con.Rel _) => (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@81: adamc@81: fun hnormCon env (cAll as (c, loc)) = adamc@81: case c of adamc@81: CUnif (_, _, _, ref (SOME c)) => hnormCon env c 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@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@326: | c1' as CApp (c', i) => 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@326: CApp (c', f) => adamc@326: (case #1 (hnormCon env c') of adamc@326: CFold ks => adamc@326: (case #1 (hnormCon env c2) of adamc@326: CRecord (_, []) => hnormCon env i adamc@326: | CRecord (k, (x, c) :: rest) => adamc@326: hnormCon env adamc@326: (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@81: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@326: (CRecord (k, rest), loc)), loc)), loc) adamc@326: | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => adamc@326: let adamc@326: val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) adamc@81: adamc@326: (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@326: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@326: rest''), loc)), loc)*) adamc@326: in adamc@326: (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) adamc@326: hnormCon env adamc@326: (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@81: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@326: rest''), loc)), loc) adamc@326: end adamc@329: | _ => adamc@329: let adamc@329: fun cunif () = adamc@329: let adamc@329: val r = ref NONE adamc@329: in adamc@329: (r, (CUnif (loc, (KType, loc), "_", r), loc)) adamc@329: end adamc@329: adamc@329: val (nmR, nm) = cunif () adamc@329: val (vR, v) = cunif () adamc@329: val (rR, r) = cunif () adamc@329: adamc@329: val c = f adamc@329: val c = (CApp (c, nm), loc) adamc@329: val c = (CApp (c, v), loc) adamc@329: val c = (CApp (c, r), loc) adamc@329: fun unconstraint c = adamc@329: case hnormCon env c of adamc@345: (CDisjoint (_, _, _, c), _) => unconstraint c adamc@329: | c => c adamc@329: val c = unconstraint c adamc@339: adamc@494: fun tryDistributivity () = adamc@494: let adamc@494: fun distribute (c1, c2) = adamc@494: let adamc@494: val c = (CFold ks, loc) adamc@494: val c = (CApp (c, f), loc) adamc@494: val c = (CApp (c, i), loc) adamc@494: adamc@494: val c1 = (CApp (c, c1), loc) adamc@494: val c2 = (CApp (c, c2), loc) adamc@494: val c = (CConcat (c1, c2), loc) adamc@494: in adamc@494: hnormCon env c adamc@494: end adamc@494: in adamc@494: case (hnormCon env i, hnormCon env c2, hnormCon env c) of adamc@494: ((CRecord (_, []), _), adamc@494: (CConcat (arg1, arg2), _), adamc@494: (CConcat (c1, c2'), _)) => adamc@494: (case (hnormCon env c1, hnormCon env c2') of adamc@494: ((CRecord (_, [(nm', v')]), _), adamc@494: (CUnif (_, _, _, rR'), _)) => adamc@494: (case hnormCon env nm' of adamc@494: (CUnif (_, _, _, nmR'), _) => adamc@494: if nmR' = nmR andalso rR' = rR then adamc@494: distribute (arg1, arg2) adamc@494: else adamc@494: default () adamc@494: | _ => default ()) adamc@494: | _ => default ()) adamc@494: | _ => default () adamc@494: end adamc@494: adamc@339: fun tryFusion () = adamc@339: let adamc@339: fun fuse (dom, new_v, r') = adamc@339: let adamc@339: val ran = #2 ks adamc@339: adamc@339: val f = (CApp (f, (CRel 2, loc)), loc) adamc@339: val f = (CApp (f, new_v), loc) adamc@339: val f = (CApp (f, (CRel 0, loc)), loc) adamc@339: val f = (CAbs ("acc", ran, f), loc) adamc@339: val f = (CAbs ("v", dom, f), loc) adamc@339: val f = (CAbs ("nm", (KName, loc), f), loc) adamc@339: adamc@339: val c = (CFold (dom, ran), loc) adamc@339: val c = (CApp (c, f), loc) adamc@339: val c = (CApp (c, i), loc) adamc@339: val c = (CApp (c, r'), loc) adamc@339: in adamc@339: hnormCon env c adamc@339: end adamc@339: in adamc@339: case #1 (hnormCon env c2) of adamc@339: CApp (f, r') => adamc@339: (case #1 (hnormCon env f) of adamc@339: CApp (f, inner_i) => adamc@339: (case (#1 (hnormCon env f), #1 (hnormCon env inner_i)) of adamc@339: (CApp (f, inner_f), CRecord (_, [])) => adamc@339: (case #1 (hnormCon env f) of adamc@339: CFold (dom, _) => adamc@339: let adamc@339: val c = inner_f adamc@339: val c = (CApp (c, nm), loc) adamc@339: val c = (CApp (c, v), loc) adamc@339: val c = (CApp (c, r), loc) adamc@339: val c = unconstraint c adamc@339: adamc@339: (*val () = Print.prefaces "Onto something!" adamc@339: [("c", ElabPrint.p_con env cAll), adamc@339: ("c'", ElabPrint.p_con env c)]*) adamc@339: adamc@339: in adamc@339: case #1 (hnormCon env c) of adamc@339: CConcat (first, rest) => adamc@339: (case (#1 (hnormCon env first), adamc@339: #1 (hnormCon env rest)) of adamc@339: (CRecord (_, [(nm', v')]), adamc@339: CUnif (_, _, _, rR')) => adamc@339: (case #1 (hnormCon env nm') of adamc@339: CUnif (_, _, _, nmR') => adamc@339: if rR' = rR andalso nmR' = nmR then adamc@339: (nmR := SOME (CRel 2, loc); adamc@339: vR := SOME (CRel 1, loc); adamc@339: rR := SOME (CError, loc); adamc@339: fuse (dom, v', r')) adamc@339: else adamc@494: tryDistributivity () adamc@494: | _ => tryDistributivity ()) adamc@494: | _ => tryDistributivity ()) adamc@494: | _ => tryDistributivity () adamc@339: end adamc@494: | _ => tryDistributivity ()) adamc@494: | _ => tryDistributivity ()) adamc@494: | _ => tryDistributivity ()) adamc@494: | _ => tryDistributivity () adamc@339: end adamc@494: adamc@329: in adamc@329: (*Print.prefaces "Consider" [("c", ElabPrint.p_con env c)];*) adamc@329: case (hnormCon env i, unconstraint c) of adamc@329: ((CRecord (_, []), _), adamc@329: (CConcat (c1, c2'), _)) => adamc@329: (case (hnormCon env c1, hnormCon env c2') of adamc@329: ((CRecord (_, [(nm', v')]), _), adamc@329: (CUnif (_, _, _, rR'), _)) => adamc@329: (case (hnormCon env nm', hnormCon env v') of adamc@329: ((CUnif (_, _, _, nmR'), _), adamc@329: (CUnif (_, _, _, vR'), _)) => adamc@329: if nmR' = nmR andalso vR' = vR andalso rR' = rR then adamc@329: hnormCon env c2 adamc@329: else adamc@339: tryFusion () adamc@339: | _ => tryFusion ()) adamc@339: | _ => tryFusion ()) adamc@339: | _ => tryFusion () adamc@329: end) adamc@326: | _ => default ()) adamc@326: | _ => default () adamc@326: end adamc@326: | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) adamc@81: 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