adamc@482: (* Copyright (c) 2008, Adam Chlipala adamc@482: * All rights reserved. adamc@482: * adamc@482: * Redistribution and use in source and binary forms, with or without adamc@482: * modification, are permitted provided that the following conditions are met: adamc@482: * adamc@482: * - Redistributions of source code must retain the above copyright notice, adamc@482: * this list of conditions and the following disclaimer. adamc@482: * - Redistributions in binary form must reproduce the above copyright notice, adamc@482: * this list of conditions and the following disclaimer in the documentation adamc@482: * and/or other materials provided with the distribution. adamc@482: * - The names of contributors may not be used to endorse or promote products adamc@482: * derived from this software without specific prior written permission. adamc@482: * adamc@482: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@482: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@482: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@482: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@482: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@482: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@482: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@482: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@482: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@482: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@482: * POSSIBILITY OF SUCH DAMAGE. adamc@482: *) adamc@482: adamc@482: (* Simplify a Core program algebraically, without unfolding definitions *) adamc@482: adamc@482: structure ReduceLocal :> REDUCE_LOCAL = struct adamc@482: adamc@482: open Core adamc@482: adamc@512: structure IM = IntBinaryMap adamc@482: adamc@512: datatype env_item = adamc@512: Unknown adamc@512: | Known of exp adamc@482: adamc@512: | Lift of int adamc@482: adamc@512: type env = env_item list adamc@512: adamc@512: val deKnown = List.filter (fn Known _ => false adamc@512: | _ => true) adamc@512: adamc@512: fun exp env (all as (e, loc)) = adamc@512: case e of adamc@512: EPrim _ => all adamc@512: | ERel n => adamc@512: let adamc@512: fun find (n', env, nudge, lift) = adamc@512: case env of adamc@512: [] => raise Fail "ReduceLocal.exp: ERel" adamc@512: | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift') adamc@512: | Unknown :: rest => adamc@512: if n' = 0 then adamc@512: (ERel (n + nudge), loc) adamc@512: else adamc@512: find (n' - 1, rest, nudge, lift + 1) adamc@512: | Known e :: rest => adamc@512: if n' = 0 then adamc@512: ((*print "SUBSTITUTING\n";*) adamc@512: exp (Lift lift :: rest) e) adamc@512: else adamc@512: find (n' - 1, rest, nudge - 1, lift) adamc@512: in adamc@512: find (n, env, 0, 0) adamc@512: end adamc@512: | ENamed _ => all adamc@512: | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc) adamc@512: | EFfi _ => all adamc@512: | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) adamc@512: adamc@512: | EApp (e1, e2) => adamc@512: let adamc@512: val e1 = exp env e1 adamc@512: val e2 = exp env e2 adamc@512: in adamc@512: case #1 e1 of adamc@512: EAbs (_, _, _, b) => exp (Known e2 :: deKnown env) b adamc@512: | _ => (EApp (e1, e2), loc) adamc@512: end adamc@512: adamc@512: | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) adamc@512: adamc@512: | ECApp (e, c) => (ECApp (exp env e, c), loc) adamc@512: adamc@512: | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) adamc@512: adamc@512: | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc) adamc@512: | EField (e, c, others) => adamc@512: let adamc@512: val e = exp env e adamc@512: adamc@512: fun default () = (EField (e, c, others), loc) adamc@512: in adamc@512: case (#1 e, #1 c) of adamc@512: (ERecord xcs, CName x) => adamc@512: (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of adamc@512: NONE => default () adamc@512: | SOME (_, e, _) => e) adamc@512: | _ => default () adamc@512: end adamc@512: adamc@512: | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc) adamc@512: | ECut (e, c, others) => (ECut (exp env e, c, others), loc) adamc@512: | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) adamc@512: adamc@512: | EFold _ => all adamc@512: adamc@512: | ECase (e, pes, others) => adamc@512: let adamc@512: fun patBinds (p, _) = adamc@512: case p of adamc@512: PWild => 0 adamc@512: | PVar _ => 1 adamc@512: | PPrim _ => 0 adamc@512: | PCon (_, _, _, NONE) => 0 adamc@512: | PCon (_, _, _, SOME p) => patBinds p adamc@512: | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts adamc@512: in adamc@512: (ECase (exp env e, adamc@512: map (fn (p, e) => (p, adamc@512: exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e)) adamc@512: pes, others), loc) adamc@512: end adamc@512: adamc@512: | EWrite e => (EWrite (exp env e), loc) adamc@512: | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) adamc@512: adamc@512: | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) adamc@512: adamc@512: fun reduce file = adamc@482: let adamc@512: fun doDecl (d as (_, loc)) = adamc@512: case #1 d of adamc@512: DCon _ => d adamc@512: | DDatatype _ => d adamc@512: | DVal (x, n, t, e, s) => adamc@512: let adamc@512: val e = exp [] e adamc@512: in adamc@512: (DVal (x, n, t, e, s), loc) adamc@512: end adamc@512: | DValRec vis => adamc@512: (DValRec (map (fn (x, n, t, e, s) => (x, n, t, exp [] e, s)) vis), loc) adamc@512: | DExport _ => d adamc@512: | DTable _ => d adamc@512: | DSequence _ => d adamc@512: | DDatabase _ => d adamc@512: | DCookie _ => d adamc@482: in adamc@512: map doDecl file adamc@482: end adamc@482: adamc@482: end