# HG changeset patch # User Adam Chlipala # Date 1214918989 14400 # Node ID 60d97de1bbe82e554a66be34e6b2d484d7585d94 # Parent 321cb9805c8ecdd0eabb6b227f320d65db22452b Factor some operations into ElabOps diff -r 321cb9805c8e -r 60d97de1bbe8 src/elab_ops.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/elab_ops.sig Tue Jul 01 09:29:49 2008 -0400 @@ -0,0 +1,36 @@ +(* 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. + *) + +signature ELAB_OPS = sig + + val liftConInCon : int -> Elab.con -> Elab.con + val subConInCon : int * Elab.con -> Elab.con -> Elab.con + val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn + + val hnormCon : ElabEnv.env -> Elab.con -> Elab.con + +end diff -r 321cb9805c8e -r 60d97de1bbe8 src/elab_ops.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/elab_ops.sml Tue Jul 01 09:29:49 2008 -0400 @@ -0,0 +1,143 @@ +(* 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 ElabOps :> ELAB_OPS = struct + +open Elab + +structure E = ElabEnv +structure U = ElabUtil + +val liftConInCon = E.liftConInCon + +val subConInCon = + U.Con.mapB {kind = fn k => k, + con = fn (xn, rep) => fn c => + case c of + CRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER => CRel (xn' - 1) + | LESS => c) + (*| CUnif _ => raise SynUnif*) + | _ => c, + bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + | (ctx, _) => ctx} + +fun subStrInSgn (m1, m2) = + U.Sgn.map {kind = fn k => k, + con = fn c as CModProj (m1', ms, x) => + if m1 = m1' then + CModProj (m2, ms, x) + else + c + | c => c, + sgn_item = fn sgi => sgi, + sgn = fn sgn => sgn} + + +fun hnormCon env (cAll as (c, loc)) = + case c of + CUnif (_, _, _, ref (SOME c)) => hnormCon env c + + | CNamed xn => + (case E.lookupCNamed env xn of + (_, _, SOME c') => hnormCon env c' + | _ => cAll) + + | 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 "hnormCon: Unknown substructure" + | SOME sgn => ((StrProj (str, m), loc), sgn)) + ((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 (_, NONE) => cAll + | SOME (_, SOME c) => hnormCon env c + end + + | CApp (c1, c2) => + (case #1 (hnormCon env c1) of + CAbs (x, k, cb) => + let + val sc = (hnormCon env (subConInCon (0, c2) cb)) + handle SynUnif => cAll + (*val env' = E.pushCRel env x k*) + in + (*eprefaces "Subst" [("x", Print.PD.string x), + ("cb", p_con env' cb), + ("c2", p_con env c2), + ("sc", p_con env sc)];*) + sc + end + | CApp (c', i) => + (case #1 (hnormCon env c') of + CApp (c', f) => + (case #1 (hnormCon env c') of + CFold ks => + (case #1 (hnormCon env c2) of + CRecord (_, []) => hnormCon env i + | CRecord (k, (x, c) :: rest) => + hnormCon env + (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), + (CRecord (k, rest), loc)), loc)), loc) + | CConcat ((CRecord (k, (x, c) :: rest), _), rest') => + let + val rest'' = (CConcat ((CRecord (k, rest), loc), rest'), loc) + + (*val ccc = (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), + rest''), loc)), loc)*) + in + (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) + hnormCon env + (CApp ((CApp ((CApp (f, x), loc), c), loc), + (CApp ((CApp ((CApp ((CFold ks, loc), f), loc), i), loc), + rest''), loc)), loc) + end + | _ => cAll) + | _ => cAll) + | _ => cAll) + | _ => cAll) + + | CConcat (c1, c2) => + (case (hnormCon env c1, hnormCon env c2) of + ((CRecord (k, xcs1), loc), (CRecord (_, xcs2), _)) => + (CRecord (k, xcs1 @ xcs2), loc) + | ((CRecord (_, []), _), c2') => c2' + | ((CConcat (c11, c12), loc), c2') => + hnormCon env (CConcat (c11, (CConcat (c12, c2'), loc)), loc) + | _ => cAll) + + | _ => cAll + +end diff -r 321cb9805c8e -r 60d97de1bbe8 src/elaborate.sml --- a/src/elaborate.sml Sun Jun 29 11:23:22 2008 -0400 +++ b/src/elaborate.sml Tue Jul 01 09:29:49 2008 -0400 @@ -416,32 +416,8 @@ eprefaces "Can't unify record constructors" [] exception SynUnif = E.SynUnif -val liftConInCon = E.liftConInCon -val subConInCon = - U.Con.mapB {kind = fn k => k, - con = fn (xn, rep) => fn c => - case c of - L'.CRel xn' => - (case Int.compare (xn', xn) of - EQUAL => #1 rep - | GREATER => L'.CRel (xn' - 1) - | LESS => c) - (*| L'.CUnif _ => raise SynUnif*) - | _ => c, - bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) - | (ctx, _) => ctx} - -fun subStrInSgn (m1, m2) = - U.Sgn.map {kind = fn k => k, - con = fn c as L'.CModProj (m1', ms, x) => - if m1 = m1' then - L'.CModProj (m2, ms, x) - else - c - | c => c, - sgn_item = fn sgi => sgi, - sgn = fn sgn => sgn} +open ElabOps type record_summary = { fields : (L'.con * L'.con) list, @@ -631,85 +607,6 @@ pairOffUnifs (unifs1, unifs2) end -and hnormCon env (cAll as (c, loc)) = - case c of - L'.CUnif (_, _, _, ref (SOME c)) => hnormCon env c - - | L'.CNamed xn => - (case E.lookupCNamed env xn of - (_, _, SOME c') => hnormCon env c' - | _ => cAll) - - | 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 "hnormCon: 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 (_, NONE) => cAll - | SOME (_, SOME c) => hnormCon env c - end - - | L'.CApp (c1, c2) => - (case #1 (hnormCon env c1) of - L'.CAbs (x, k, cb) => - let - val sc = (hnormCon env (subConInCon (0, c2) cb)) - handle SynUnif => cAll - (*val env' = E.pushCRel env x k*) - in - (*eprefaces "Subst" [("x", Print.PD.string x), - ("cb", p_con env' cb), - ("c2", p_con env c2), - ("sc", p_con env sc)];*) - sc - end - | L'.CApp (c', i) => - (case #1 (hnormCon env c') of - L'.CApp (c', f) => - (case #1 (hnormCon env c') of - L'.CFold ks => - (case #1 (hnormCon env c2) of - L'.CRecord (_, []) => hnormCon env i - | L'.CRecord (k, (x, c) :: rest) => - hnormCon env - (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), - (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), - (L'.CRecord (k, rest), loc)), loc)), loc) - | L'.CConcat ((L'.CRecord (k, (x, c) :: rest), _), rest') => - let - val rest'' = (L'.CConcat ((L'.CRecord (k, rest), loc), rest'), loc) - - (*val ccc = (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), - (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc)*) - in - (*eprefaces "Red to" [("ccc", p_con env ccc), ("ccc'", p_con env (hnormCon env ccc))];*) - hnormCon env - (L'.CApp ((L'.CApp ((L'.CApp (f, x), loc), c), loc), - (L'.CApp ((L'.CApp ((L'.CApp ((L'.CFold ks, loc), f), loc), i), loc), - rest''), loc)), loc) - end - | _ => cAll) - | _ => cAll) - | _ => cAll) - | _ => cAll) - - | L'.CConcat (c1, c2) => - (case (hnormCon env c1, hnormCon env c2) of - ((L'.CRecord (k, xcs1), loc), (L'.CRecord (_, xcs2), _)) => - (L'.CRecord (k, xcs1 @ xcs2), loc) - | ((L'.CRecord (_, []), _), c2') => c2' - | ((L'.CConcat (c11, c12), loc), c2') => - hnormCon env (L'.CConcat (c11, (L'.CConcat (c12, c2'), loc)), loc) - | _ => cAll) - - | _ => cAll and unifyCons' env c1 c2 = unifyCons'' env (hnormCon env c1) (hnormCon env c2) diff -r 321cb9805c8e -r 60d97de1bbe8 src/sources --- a/src/sources Sun Jun 29 11:23:22 2008 -0400 +++ b/src/sources Tue Jul 01 09:29:49 2008 -0400 @@ -32,6 +32,9 @@ elab_print.sig elab_print.sml +elab_ops.sig +elab_ops.sml + elaborate.sig elaborate.sml