adamc@20: (* Copyright (c) 2008, Adam Chlipala adamc@20: * All rights reserved. adamc@20: * adamc@20: * Redistribution and use in source and binary forms, with or without adamc@20: * modification, are permitted provided that the following conditions are met: adamc@20: * adamc@20: * - Redistributions of source code must retain the above copyright notice, adamc@20: * this list of conditions and the following disclaimer. adamc@20: * - Redistributions in binary form must reproduce the above copyright notice, adamc@20: * this list of conditions and the following disclaimer in the documentation adamc@20: * and/or other materials provided with the distribution. adamc@20: * - The names of contributors may not be used to endorse or promote products adamc@20: * derived from this software without specific prior written permission. adamc@20: * adamc@20: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@20: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@20: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@20: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@20: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@20: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@20: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@20: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@20: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@20: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@20: * POSSIBILITY OF SUCH DAMAGE. adamc@20: *) adamc@20: adamc@20: (* Simplify a Core program algebraically *) adamc@20: adamc@20: structure Reduce :> REDUCE = struct adamc@20: adamc@20: open Core adamc@20: adamc@508: structure IM = IntBinaryMap adamc@20: adamc@508: datatype env_item = adamc@508: UnknownC adamc@508: | KnownC of con adamc@21: adamc@508: | UnknownE adamc@508: | KnownE of exp adamc@20: adamc@508: | Lift of int * int adamc@20: adamc@508: type env = env_item list adamc@20: adamc@508: fun conAndExp (namedC, namedE) = adamc@508: let adamc@508: fun con env (all as (c, loc)) = adamc@508: case c of adamc@508: TFun (c1, c2) => (TFun (con env c1, con env c2), loc) adamc@508: | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) adamc@508: | TRecord c => (TRecord (con env c), loc) adamc@215: adamc@508: | CRel n => adamc@508: let adamc@508: fun find (n', env, lift) = adamc@508: if n' = 0 then adamc@508: case env of adamc@508: UnknownC :: _ => (CRel (n + lift), loc) adamc@508: | KnownC c :: _ => con (Lift (lift, 0) :: env) c adamc@508: | _ => raise Fail "Reduce.con: CRel [1]" adamc@508: else adamc@508: case env of adamc@508: UnknownC :: rest => find (n' - 1, rest, lift + 1) adamc@508: | KnownC _ :: rest => find (n' - 1, rest, lift) adamc@508: | UnknownE :: rest => find (n' - 1, rest, lift) adamc@508: | KnownE _ :: rest => find (n' - 1, rest, lift) adamc@508: | Lift (lift', _) :: rest => find (n' - 1, rest, lift + lift') adamc@508: | [] => raise Fail "Reduce.con: CRel [2]" adamc@508: in adamc@508: find (n, env, 0) adamc@508: end adamc@508: | CNamed n => adamc@508: (case IM.find (namedC, n) of adamc@508: NONE => all adamc@508: | SOME c => c) adamc@508: | CFfi _ => all adamc@508: | CApp (c1, c2) => adamc@508: let adamc@508: val c1 = con env c1 adamc@508: val c2 = con env c2 adamc@508: in adamc@508: case #1 c1 of adamc@508: CAbs (_, _, b) => adamc@508: con (KnownC c2 :: env) b adamc@215: adamc@508: | CApp ((CApp (fold as (CFold _, _), f), _), i) => adamc@508: (case #1 c2 of adamc@508: CRecord (_, []) => i adamc@508: | CRecord (k, (x, c) :: rest) => adamc@508: con env (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@508: (CApp ((CApp ((CApp (fold, f), loc), i), loc), adamc@508: (CRecord (k, rest), loc)), loc)), loc) adamc@508: | _ => (CApp (c1, c2), loc)) adamc@20: adamc@508: | _ => (CApp (c1, c2), loc) adamc@508: end adamc@508: | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) adamc@20: adamc@508: | CName _ => all adamc@21: adamc@508: | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) adamc@508: | CConcat (c1, c2) => adamc@508: let adamc@508: val c1 = con env c1 adamc@508: val c2 = con env c2 adamc@508: in adamc@508: case (#1 c1, #1 c2) of adamc@508: (CRecord (k, xcs1), CRecord (_, xcs2)) => adamc@508: (CRecord (k, xcs1 @ xcs2), loc) adamc@508: | _ => (CConcat (c1, c2), loc) adamc@508: end adamc@508: | CFold _ => all adamc@74: adamc@508: | CUnit => all adamc@21: adamc@508: | CTuple cs => (CTuple (map (con env) cs), loc) adamc@508: | CProj (c, n) => adamc@508: let adamc@508: val c = con env c adamc@508: in adamc@508: case #1 c of adamc@508: CTuple cs => List.nth (cs, n - 1) adamc@508: | _ => (CProj (c, n), loc) adamc@508: end adamc@22: adamc@508: fun exp env e = e adamc@417: in adamc@508: {con = con, exp = exp} adamc@417: end adamc@21: adamc@508: fun con namedC c = #con (conAndExp (namedC, IM.empty)) [] c adamc@508: fun exp (namedC, namedE) e = #exp (conAndExp (namedC, namedE)) [] e adamc@20: adamc@508: fun reduce file = adamc@508: let adamc@508: fun doDecl (d as (_, loc), st as (namedC, namedE)) = adamc@508: case #1 d of adamc@508: DCon (x, n, k, c) => adamc@508: let adamc@508: val c = con namedC c adamc@508: in adamc@508: ((DCon (x, n, k, c), loc), adamc@508: (IM.insert (namedC, n, c), namedE)) adamc@508: end adamc@508: | DDatatype (x, n, ps, cs) => adamc@508: ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC) co)) cs), loc), adamc@508: st) adamc@508: | DVal (x, n, t, e, s) => adamc@508: let adamc@508: val t = con namedC t adamc@508: val e = exp (namedC, namedE) e adamc@508: in adamc@508: ((DVal (x, n, t, e, s), loc), adamc@508: (namedC, IM.insert (namedE, n, e))) adamc@508: end adamc@508: | DValRec vis => adamc@508: ((DValRec (map (fn (x, n, t, e, s) => (x, n, con namedC t, exp (namedC, namedE) e, s)) vis), loc), adamc@508: st) adamc@508: | DExport _ => (d, st) adamc@508: | DTable (s, n, c, s') => ((DTable (s, n, con namedC c, s'), loc), st) adamc@508: | DSequence _ => (d, st) adamc@508: | DDatabase _ => (d, st) adamc@508: | DCookie (s, n, c, s') => ((DCookie (s, n, con namedC c, s'), loc), st) adamc@20: adamc@508: val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file adamc@508: in adamc@508: file adamc@508: end adamc@20: adamc@20: end