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@81: val liftConInCon = E.liftConInCon adamc@81: adamc@81: val subConInCon = adamc@81: U.Con.mapB {kind = fn k => k, adamc@81: con = fn (xn, rep) => fn c => adamc@81: case c of adamc@81: CRel xn' => adamc@81: (case Int.compare (xn', xn) of adamc@81: EQUAL => #1 rep adamc@81: | GREATER => CRel (xn' - 1) adamc@81: | LESS => c) adamc@81: (*| CUnif _ => raise SynUnif*) adamc@81: | _ => c, adamc@81: bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) adamc@81: | (ctx, _) => ctx} adamc@81: 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@81: (*eprefaces "Subst" [("x", Print.PD.string x), adamc@81: ("cb", p_con env' cb), adamc@81: ("c2", p_con env c2), adamc@81: ("sc", p_con env sc)];*) adamc@81: sc adamc@81: end adamc@81: | CApp (c', i) => adamc@81: (case #1 (hnormCon env c') of adamc@81: CApp (c', f) => adamc@81: (case #1 (hnormCon env c') of adamc@81: CFold ks => adamc@81: (case #1 (hnormCon env c2) of adamc@81: CRecord (_, []) => hnormCon env i adamc@81: | CRecord (k, (x, c) :: rest) => adamc@81: hnormCon env adamc@81: (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@81: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@81: (CRecord (k, rest), loc)), loc)), loc) adamc@81: | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => adamc@81: let adamc@81: val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) adamc@81: adamc@81: (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@81: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@81: rest''), loc)), loc)*) adamc@81: in adamc@81: (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) adamc@81: hnormCon env adamc@81: (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@81: (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), adamc@81: rest''), loc)), loc) adamc@81: end adamc@81: | _ => cAll) adamc@81: | _ => cAll) adamc@81: | _ => cAll) adamc@81: | _ => cAll) 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@81: | _ => cAll) adamc@81: adamc@81: | _ => cAll adamc@81: adamc@81: end