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