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@510: fun ei2s ei = adamc@510: case ei of adamc@510: UnknownC => "UC" adamc@510: | KnownC _ => "KC" adamc@510: | UnknownE => "UE" adamc@510: | KnownE _ => "KE" adamc@510: | Lift (n1, n2) => "(" ^ Int.toString n1 ^ ", " ^ Int.toString n2 ^ ")" adamc@510: adamc@510: fun e2s env = String.concatWith " " (map ei2s env) adamc@510: adamc@510: val deKnown = List.filter (fn KnownC _ => false adamc@510: | KnownE _ => false adamc@510: | _ => true) adamc@510: adamc@508: fun conAndExp (namedC, namedE) = adamc@508: let adamc@508: fun con env (all as (c, loc)) = adamc@510: ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) 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@510: fun find (n', env, nudge, lift) = adamc@510: case env of adamc@510: [] => raise Fail "Reduce.con: CRel" adamc@510: | UnknownE :: rest => find (n', rest, nudge, lift) adamc@510: | KnownE _ :: rest => find (n', rest, nudge, lift) adamc@510: | Lift (lift', _) :: rest => find (n', rest, nudge + lift', lift + lift') adamc@510: | UnknownC :: rest => adamc@510: if n' = 0 then adamc@510: (CRel (n + nudge), loc) adamc@510: else adamc@510: find (n' - 1, rest, nudge, lift + 1) adamc@510: | KnownC c :: rest => adamc@510: if n' = 0 then adamc@510: con (Lift (lift, 0) :: rest) c adamc@510: else adamc@510: find (n' - 1, rest, nudge - 1, lift) adamc@508: in adamc@510: (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) adamc@510: find (n, env, 0, 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@510: con (KnownC c2 :: deKnown env) b adamc@215: adamc@511: | CApp ((CApp ((CFold _, _), f), _), i) => adamc@508: (case #1 c2 of adamc@508: CRecord (_, []) => i adamc@508: | CRecord (k, (x, c) :: rest) => adamc@510: con (deKnown env) adamc@510: (CApp ((CApp ((CApp (f, x), loc), c), loc), adamc@511: (CApp (c1, adamc@510: (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@510: end) adamc@22: adamc@509: fun patCon pc = adamc@509: case pc of adamc@509: PConVar _ => pc adamc@509: | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => adamc@509: PConFfi {mod = m, datatyp = datatyp, params = params, con = c, adamc@509: arg = Option.map (con (map (fn _ => UnknownC) params)) arg, adamc@509: kind = kind} adamc@509: adamc@509: adamc@509: val k = (KType, ErrorMsg.dummySpan) adamc@509: fun doPart e (this as (x, t), rest) = adamc@509: ((x, (EField (e, x, {field = t, rest = (CRecord (k, rest), #2 t)}), #2 t), t), adamc@509: this :: rest) adamc@509: adamc@509: fun exp env (all as (e, loc)) = adamc@510: ((*Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), adamc@510: ("env", Print.PD.string (e2s env))];*) adamc@509: case e of adamc@509: EPrim _ => all adamc@509: | ERel n => adamc@509: let adamc@510: fun find (n', env, nudge, liftC, liftE) = adamc@510: case env of adamc@510: [] => raise Fail "Reduce.exp: ERel" adamc@510: | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) adamc@510: | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) adamc@510: | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', adamc@510: liftC + liftC', liftE + liftE') adamc@510: | UnknownE :: rest => adamc@510: if n' = 0 then adamc@510: (ERel (n + nudge), loc) adamc@510: else adamc@510: find (n' - 1, rest, nudge, liftC, liftE + 1) adamc@510: | KnownE e :: rest => adamc@510: if n' = 0 then adamc@510: ((*print "SUBSTITUTING\n";*) adamc@510: exp (Lift (liftC, liftE) :: rest) e) adamc@510: else adamc@510: find (n' - 1, rest, nudge - 1, liftC, liftE) adamc@509: in adamc@510: (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) adamc@510: find (n, env, 0, 0, 0) adamc@509: end adamc@509: | ENamed n => adamc@509: (case IM.find (namedE, n) of adamc@509: NONE => all adamc@509: | SOME e => e) adamc@509: | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, adamc@509: map (con env) cs, Option.map (exp env) eo), loc) adamc@509: | EFfi _ => all adamc@509: | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) adamc@509: adamc@509: | EApp (e1, e2) => adamc@509: let adamc@509: val e1 = exp env e1 adamc@509: val e2 = exp env e2 adamc@509: in adamc@509: case #1 e1 of adamc@510: EAbs (_, _, _, b) => exp (KnownE e2 :: deKnown env) b adamc@509: | _ => (EApp (e1, e2), loc) adamc@509: end adamc@509: adamc@509: | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (UnknownE :: env) e), loc) adamc@509: adamc@509: | ECApp (e, c) => adamc@509: let adamc@509: val e = exp env e adamc@509: val c = con env c adamc@509: in adamc@509: case #1 e of adamc@510: ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b adamc@511: adamc@511: | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) => adamc@511: (case #1 c of adamc@511: CRecord (_, []) => i adamc@511: | CRecord (k, (nm, v) :: rest) => adamc@511: let adamc@511: val rest = (CRecord (k, rest), loc) adamc@511: in adamc@511: exp (deKnown env) adamc@511: (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc), adamc@511: (ECApp (e, rest), loc)), loc) adamc@511: end adamc@511: | _ => (ECApp (e, c), loc)) adamc@511: adamc@509: | _ => (ECApp (e, c), loc) adamc@509: end adamc@509: adamc@509: | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) adamc@509: adamc@509: | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) adamc@509: | EField (e, c, {field, rest}) => adamc@509: let adamc@509: val e = exp env e adamc@509: val c = con env c adamc@509: adamc@509: fun default () = (EField (e, c, {field = con env field, rest = con env rest}), loc) adamc@509: in adamc@509: case (#1 e, #1 c) of adamc@509: (ERecord xcs, CName x) => adamc@509: (case List.find (fn ((CName x', _), _, _) => x' = x | _ => false) xcs of adamc@509: NONE => default () adamc@509: | SOME (_, e, _) => e) adamc@509: | _ => default () adamc@509: end adamc@509: adamc@509: | EConcat (e1, c1, e2, c2) => adamc@509: let adamc@509: val e1 = exp env e1 adamc@509: val e2 = exp env e2 adamc@509: in adamc@509: case (#1 e1, #1 e2) of adamc@509: (ERecord xes1, ERecord xes2) => (ERecord (xes1 @ xes2), loc) adamc@509: | _ => adamc@509: let adamc@509: val c1 = con env c1 adamc@509: val c2 = con env c2 adamc@509: in adamc@509: case (#1 c1, #1 c2) of adamc@509: (CRecord (k, xcs1), CRecord (_, xcs2)) => adamc@509: let adamc@509: val (xes1, rest) = ListUtil.foldlMap (doPart e1) [] xcs1 adamc@509: val (xes2, _) = ListUtil.foldlMap (doPart e2) rest xcs2 adamc@509: in adamc@510: exp (deKnown env) (ERecord (xes1 @ xes2), loc) adamc@509: end adamc@509: | _ => (EConcat (e1, c1, e2, c2), loc) adamc@509: end adamc@509: end adamc@509: adamc@509: | ECut (e, c, {field, rest}) => adamc@509: let adamc@509: val e = exp env e adamc@509: val c = con env c adamc@509: adamc@509: fun default () = adamc@509: let adamc@509: val rest = con env rest adamc@509: in adamc@509: case #1 rest of adamc@509: CRecord (k, xcs) => adamc@509: let adamc@509: val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs adamc@509: in adamc@510: exp (deKnown env) (ERecord xes, loc) adamc@509: end adamc@509: | _ => (ECut (e, c, {field = con env field, rest = rest}), loc) adamc@509: end adamc@509: in adamc@509: case (#1 e, #1 c) of adamc@509: (ERecord xes, CName x) => adamc@509: if List.all (fn ((CName _, _), _, _) => true | _ => false) xes then adamc@509: (ERecord (List.filter (fn ((CName x', _), _, _) => x' <> x adamc@509: | _ => raise Fail "Reduce: ECut") xes), loc) adamc@509: else adamc@509: default () adamc@509: | _ => default () adamc@509: end adamc@509: adamc@509: | ECutMulti (e, c, {rest}) => adamc@509: let adamc@509: val e = exp env e adamc@509: val c = con env c adamc@509: adamc@509: fun default () = adamc@509: let adamc@509: val rest = con env rest adamc@509: in adamc@509: case #1 rest of adamc@509: CRecord (k, xcs) => adamc@509: let adamc@509: val (xes, _) = ListUtil.foldlMap (doPart e) [] xcs adamc@509: in adamc@510: exp (deKnown env) (ERecord xes, loc) adamc@509: end adamc@509: | _ => (ECutMulti (e, c, {rest = rest}), loc) adamc@509: end adamc@509: in adamc@509: case (#1 e, #1 c) of adamc@509: (ERecord xes, CRecord (_, xcs)) => adamc@509: if List.all (fn ((CName _, _), _, _) => true | _ => false) xes adamc@509: andalso List.all (fn ((CName _, _), _) => true | _ => false) xcs then adamc@509: (ERecord (List.filter (fn ((CName x', _), _, _) => adamc@509: List.all (fn ((CName x, _), _) => x' <> x adamc@509: | _ => raise Fail "Reduce: ECutMulti [1]") xcs adamc@509: | _ => raise Fail "Reduce: ECutMulti [2]") xes), loc) adamc@509: else adamc@509: default () adamc@509: | _ => default () adamc@509: end adamc@509: adamc@509: | EFold _ => all adamc@509: adamc@509: | ECase (e, pes, {disc, result}) => adamc@509: let adamc@509: fun patBinds (p, _) = adamc@509: case p of adamc@509: PWild => 0 adamc@509: | PVar _ => 1 adamc@509: | PPrim _ => 0 adamc@509: | PCon (_, _, _, NONE) => 0 adamc@509: | PCon (_, _, _, SOME p) => patBinds p adamc@509: | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts adamc@509: adamc@509: fun pat (all as (p, loc)) = adamc@509: case p of adamc@509: PWild => all adamc@509: | PVar (x, t) => (PVar (x, con env t), loc) adamc@509: | PPrim _ => all adamc@509: | PCon (dk, pc, cs, po) => adamc@509: (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) adamc@509: | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) adamc@509: in adamc@509: (ECase (exp env e, adamc@509: map (fn (p, e) => (pat p, adamc@509: exp (List.tabulate (patBinds p, fn _ => UnknownE) @ env) e)) adamc@509: pes, {disc = con env disc, result = con env result}), loc) adamc@509: end adamc@509: adamc@509: | EWrite e => (EWrite (exp env e), loc) adamc@509: | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) adamc@509: adamc@607: | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (UnknownE :: env) e2), loc) adamc@607: adamc@609: | EServerCall (n, es, e, t) => (EServerCall (n, map (exp env) es, exp env e, con env t), loc)) adamc@417: in adamc@508: {con = con, exp = exp} adamc@417: end adamc@21: adamc@509: fun con namedC env c = #con (conAndExp (namedC, IM.empty)) env c adamc@509: fun exp (namedC, namedE) env e = #exp (conAndExp (namedC, namedE)) env 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@509: 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@509: let adamc@509: val env = map (fn _ => UnknownC) ps adamc@509: in adamc@509: ((DDatatype (x, n, ps, map (fn (x, n, co) => (x, n, Option.map (con namedC env) co)) cs), loc), adamc@509: st) adamc@509: end adamc@508: | DVal (x, n, t, e, s) => adamc@508: let adamc@509: val t = con namedC [] t adamc@509: 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@509: ((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@509: | 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@509: | 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