adamc@1272: (* Copyright (c) 2008-2010, 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@1062: fun multiLiftExpInExp n e = adamc@1062: if n = 0 then adamc@1062: e adamc@1062: else adamc@1062: multiLiftExpInExp (n - 1) (CoreEnv.liftExpInExp 0 e) adamc@1062: adamc@512: datatype env_item = adamc@512: Unknown adamc@512: | Known of exp adamc@482: adamc@1272: | UnknownC adamc@1272: | KnownC of con adamc@1272: adamc@1272: | Lift of int * int adamc@482: adamc@512: type env = env_item list adamc@512: adamc@512: val deKnown = List.filter (fn Known _ => false adamc@1272: | KnownC _ => false adamc@512: | _ => true) adamc@512: adamc@1062: datatype result = Yes of env | No | Maybe adamc@1062: adamc@1062: fun match (env, p : pat, e : exp) = adamc@1062: let adamc@1062: val baseline = length env adamc@1062: adamc@1062: fun match (env, p, e) = adamc@1062: case (#1 p, #1 e) of adamc@1062: (PWild, _) => Yes env adamc@1062: | (PVar (x, t), _) => Yes (Known (multiLiftExpInExp (length env - baseline) e) :: env) adamc@1062: adamc@1062: | (PPrim p, EPrim p') => adamc@1062: if Prim.equal (p, p') then adamc@1062: Yes env adamc@1062: else adamc@1062: No adamc@1062: adamc@1062: | (PCon (_, PConVar n1, _, NONE), ECon (_, PConVar n2, _, NONE)) => adamc@1062: if n1 = n2 then adamc@1062: Yes env adamc@1062: else adamc@1062: No adamc@1062: adamc@1062: | (PCon (_, PConVar n1, _, SOME p), ECon (_, PConVar n2, _, SOME e)) => adamc@1062: if n1 = n2 then adamc@1062: match (env, p, e) adamc@1062: else adamc@1062: No adamc@1062: adamc@1062: | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, NONE), adamc@1062: ECon (_, PConFfi {mod = m2, con = con2, ...}, _, NONE)) => adamc@1062: if m1 = m2 andalso con1 = con2 then adamc@1062: Yes env adamc@1062: else adamc@1062: No adamc@1062: adamc@1062: | (PCon (_, PConFfi {mod = m1, con = con1, ...}, _, SOME ep), adamc@1062: ECon (_, PConFfi {mod = m2, con = con2, ...}, _, SOME e)) => adamc@1062: if m1 = m2 andalso con1 = con2 then adamc@1062: match (env, p, e) adamc@1062: else adamc@1062: No adamc@1062: adamc@1062: | (PRecord xps, ERecord xes) => adamc@1062: if List.exists (fn ((CName _, _), _, _) => false adamc@1062: | _ => true) xes then adamc@1062: Maybe adamc@1062: else adamc@1062: let adamc@1062: fun consider (xps, env) = adamc@1062: case xps of adamc@1062: [] => Yes env adamc@1062: | (x, p, _) :: rest => adamc@1062: case List.find (fn ((CName x', _), _, _) => x' = x adamc@1062: | _ => false) xes of adamc@1062: NONE => No adamc@1062: | SOME (_, e, _) => adamc@1062: case match (env, p, e) of adamc@1062: No => No adamc@1062: | Maybe => Maybe adamc@1062: | Yes env => consider (rest, env) adamc@1062: in adamc@1062: consider (xps, env) adamc@1062: end adamc@1062: adamc@1062: | _ => Maybe adamc@1062: in adamc@1062: match (env, p, e) adamc@1062: end adamc@1062: adamc@1272: fun con env (all as (c, loc)) = adamc@1272: ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) adamc@1272: case c of adamc@1272: TFun (c1, c2) => (TFun (con env c1, con env c2), loc) adamc@1272: | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) adamc@1272: | TKFun (x, c2) => (TKFun (x, con env c2), loc) adamc@1272: | TRecord c => (TRecord (con env c), loc) adamc@1272: adamc@1272: | CRel n => adamc@1272: let adamc@1272: fun find (n', env, nudge, liftC) = adamc@1272: case env of adamc@1272: [] => raise Fail "Reduce.con: CRel" adamc@1272: | Unknown :: rest => find (n', rest, nudge, liftC) adamc@1272: | Known _ :: rest => find (n', rest, nudge, liftC) adamc@1272: | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC', adamc@1272: liftC + liftC') adamc@1272: | UnknownC :: rest => adamc@1272: if n' = 0 then adamc@1272: (CRel (n + nudge), loc) adamc@1272: else adamc@1272: find (n' - 1, rest, nudge, liftC + 1) adamc@1272: | KnownC c :: rest => adamc@1272: if n' = 0 then adamc@1272: con (Lift (liftC, 0) :: rest) c adamc@1272: else adamc@1272: find (n' - 1, rest, nudge - 1, liftC) adamc@1272: in adamc@1272: (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) adamc@1272: find (n, env, 0, 0) adamc@1272: end adamc@1272: | CNamed _ => all adamc@1272: | CFfi _ => all adamc@1272: | CApp (c1, c2) => adamc@1272: let adamc@1272: val c1 = con env c1 adamc@1272: val c2 = con env c2 adamc@1272: in adamc@1272: case #1 c1 of adamc@1272: CAbs (_, _, b) => adamc@1272: con (KnownC c2 :: deKnown env) b adamc@1272: adamc@1272: | CApp ((CMap (dom, ran), _), f) => adamc@1272: (case #1 c2 of adamc@1272: CRecord (_, []) => (CRecord (ran, []), loc) adamc@1272: | CRecord (_, (x, c) :: rest) => adamc@1272: con (deKnown env) adamc@1272: (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), adamc@1272: (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc) adamc@1272: | _ => (CApp (c1, c2), loc)) adamc@1272: adamc@1272: | _ => (CApp (c1, c2), loc) adamc@1272: end adamc@1272: | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) adamc@1272: adamc@1272: | CKApp (c1, k) => adamc@1272: let adamc@1272: val c1 = con env c1 adamc@1272: in adamc@1272: case #1 c1 of adamc@1272: CKAbs (_, b) => adamc@1272: con (deKnown env) b adamc@1272: adamc@1272: | _ => (CKApp (c1, k), loc) adamc@1272: end adamc@1272: | CKAbs (x, b) => (CKAbs (x, con env b), loc) adamc@1272: adamc@1272: | CName _ => all adamc@1272: adamc@1272: | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) adamc@1272: | CConcat (c1, c2) => adamc@1272: let adamc@1272: val c1 = con env c1 adamc@1272: val c2 = con env c2 adamc@1272: in adamc@1272: case (#1 c1, #1 c2) of adamc@1272: (CRecord (k, xcs1), CRecord (_, xcs2)) => adamc@1272: (CRecord (k, xcs1 @ xcs2), loc) adamc@1272: | (CRecord (_, []), _) => c2 adamc@1272: | (_, CRecord (_, [])) => c1 adamc@1272: | _ => (CConcat (c1, c2), loc) adamc@1272: end adamc@1272: | CMap _ => all adamc@1272: adamc@1272: | CUnit => all adamc@1272: adamc@1272: | CTuple cs => (CTuple (map (con env) cs), loc) adamc@1272: | CProj (c, n) => adamc@1272: let adamc@1272: val c = con env c adamc@1272: in adamc@1272: case #1 c of adamc@1272: CTuple cs => List.nth (cs, n - 1) adamc@1272: | _ => (CProj (c, n), loc) adamc@1272: end) adamc@1272: adamc@1272: fun patCon pc = adamc@1272: case pc of adamc@1272: PConVar _ => pc adamc@1272: | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => adamc@1272: PConFfi {mod = m, datatyp = datatyp, params = params, con = c, adamc@1272: arg = Option.map (con (map (fn _ => UnknownC) params)) arg, adamc@1272: kind = kind} adamc@1272: 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@1272: fun find (n', env, nudge, liftC, liftE) = adamc@512: case env of adamc@642: [] => (ERel (n + nudge), loc) adamc@1272: | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE') adamc@1272: | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) adamc@1272: | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) adamc@512: | Unknown :: rest => adamc@512: if n' = 0 then adamc@512: (ERel (n + nudge), loc) adamc@512: else adamc@1272: find (n' - 1, rest, nudge, liftC, liftE + 1) adamc@512: | Known e :: rest => adamc@512: if n' = 0 then adamc@512: ((*print "SUBSTITUTING\n";*) adamc@1272: exp (Lift (liftC, liftE) :: rest) e) adamc@512: else adamc@1272: find (n' - 1, rest, nudge - 1, liftC, liftE) adamc@512: in adamc@1272: find (n, env, 0, 0, 0) adamc@512: end adamc@512: | ENamed _ => all adamc@1272: | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) 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@1272: | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc) adamc@512: adamc@1272: | ECApp (e, c) => adamc@1272: let adamc@1272: val e = exp env e adamc@1272: val c = con env c adamc@1272: in adamc@1272: case #1 e of adamc@1272: ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b adamc@1272: | _ => (ECApp (e, c), loc) adamc@1272: end adamc@721: adamc@1272: | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) adamc@512: adamc@626: | EKApp (e, k) => (EKApp (exp env e, k), loc) adamc@626: | EKAbs (x, e) => (EKAbs (x, exp env e), loc) adamc@512: adamc@1272: | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) adamc@512: | EField (e, c, others) => adamc@512: let adamc@512: val e = exp env e adamc@1272: val c = con env c 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@1272: | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc) adamc@1272: | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e, adamc@1272: con env c, adamc@1272: {field = con env f, rest = con env r}), loc) adamc@1272: | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc) adamc@512: adamc@1272: | ECase (e, pes, {disc = d, result = r}) => adamc@512: let adamc@1272: val others = {disc = con env d, result = con env r} adamc@1272: 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@1062: adamc@1272: fun pat (all as (p, loc)) = adamc@1272: case p of adamc@1272: PWild => all adamc@1272: | PVar (x, t) => (PVar (x, con env t), loc) adamc@1272: | PPrim _ => all adamc@1272: | PCon (dk, pc, cs, po) => adamc@1272: (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) adamc@1272: | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) adamc@1272: adamc@1062: fun push () = adamc@1062: (ECase (exp env e, adamc@1272: map (fn (p, e) => (pat p, adamc@1062: exp (List.tabulate (patBinds p, adamc@1062: fn _ => Unknown) @ env) e)) adamc@1062: pes, others), loc) adamc@1062: adamc@1062: fun search pes = adamc@1062: case pes of adamc@1062: [] => push () adamc@1062: | (p, body) :: pes => adamc@1062: case match (env, p, e) of adamc@1062: No => search pes adamc@1062: | Maybe => push () adamc@1062: | Yes env' => exp env' body adamc@512: in adamc@1062: search pes 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@1272: | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc) adamc@512: adamc@1272: | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc) adamc@607: 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@754: | DView _ => d adamc@512: | DDatabase _ => d adamc@512: | DCookie _ => d adamc@718: | DStyle _ => d adamc@1075: | DTask (e1, e2) => (DTask (exp [] e1, exp [] e2), loc) adamc@1199: | DPolicy e1 => (DPolicy (exp [] e1), loc) adamc@482: in adamc@512: map doDecl file adamc@482: end adamc@482: adamc@642: val reduceExp = exp [] adamc@1276: val reduceCon = con [] adamc@642: adamc@482: end