adamc@133: (* Copyright (c) 2008, Adam Chlipala
adamc@133:  * All rights reserved.
adamc@133:  *
adamc@133:  * Redistribution and use in source and binary forms, with or without
adamc@133:  * modification, are permitted provided that the following conditions are met:
adamc@133:  *
adamc@133:  * - Redistributions of source code must retain the above copyright notice,
adamc@133:  *   this list of conditions and the following disclaimer.
adamc@133:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@133:  *   this list of conditions and the following disclaimer in the documentation
adamc@133:  *   and/or other materials provided with the distribution.
adamc@133:  * - The names of contributors may not be used to endorse or promote products
adamc@133:  *   derived from this software without specific prior written permission.
adamc@133:  *
adamc@133:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@133:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@133:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@133:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@133:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@133:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@133:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@133:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@133:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@133:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@133:  * POSSIBILITY OF SUCH DAMAGE.
adamc@133:  *)
adamc@133: 
adamc@133: (* Simplify a Mono program algebraically *)
adamc@133: 
adamc@133: structure MonoReduce :> MONO_REDUCE = struct
adamc@133: 
adamc@133: open Mono
adamc@133: 
adamc@133: structure E = MonoEnv
adamc@133: structure U = MonoUtil
adamc@133: 
adamc@133: 
adamc@252: fun impure (e, _) =
adamc@252:     case e of
adamc@252:         EWrite _ => true
adamc@252:       | EQuery _ => true
adamc@307:       | EDml _ => true
adamc@252:       | EAbs _ => false
adamc@252: 
adamc@252:       | EPrim _ => false
adamc@252:       | ERel _ => false
adamc@252:       | ENamed _ => false
adamc@252:       | ECon (_, _, eo) => (case eo of NONE => false | SOME e => impure e)
adamc@297:       | ENone _ => false
adamc@290:       | ESome (_, e) => impure e
adamc@252:       | EFfi _ => false
adamc@252:       | EFfiApp _ => false
adamc@252:       | EApp ((EFfi _, _), _) => false
adamc@252:       | EApp _ => true
adamc@252: 
adamc@252:       | ERecord xes => List.exists (fn (_, e, _) => impure e) xes
adamc@252:       | EField (e, _) => impure e
adamc@252: 
adamc@252:       | ECase (e, pes, _) => impure e orelse List.exists (fn (_, e) => impure e) pes
adamc@252: 
adamc@283:       | EError (e, _) => impure e
adamc@283: 
adamc@252:       | EStrcat (e1, e2) => impure e1 orelse impure e2
adamc@252: 
adamc@252:       | ESeq (e1, e2) => impure e1 orelse impure e2
adamc@252:       | ELet (_, _, e1, e2) => impure e1 orelse impure e2
adamc@252: 
adamc@252:       | EClosure (_, es) => List.exists impure es
adamc@252: 
adamc@252: 
adamc@252: val liftExpInExp = Monoize.liftExpInExp
adamc@252: 
adamc@252: val subExpInExp' =
adamc@133:     U.Exp.mapB {typ = fn t => t,
adamc@133:                 exp = fn (xn, rep) => fn e =>
adamc@133:                                   case e of
adamc@133:                                       ERel xn' =>
adamc@133:                                       (case Int.compare (xn', xn) of
adamc@133:                                            EQUAL => #1 rep
adamc@133:                                          | GREATER=> ERel (xn' - 1)
adamc@133:                                          | LESS => e)
adamc@133:                                     | _ => e,
adamc@133:                 bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep)
adamc@133:                         | (ctx, _) => ctx}
adamc@133: 
adamc@252: fun subExpInExp (n, e1) e2 =
adamc@252:     let
adamc@252:         val r = subExpInExp' (n, e1) e2
adamc@252:     in
adamc@252:         (*Print.prefaces "subExpInExp" [("e1", MonoPrint.p_exp MonoEnv.empty e1),
adamc@252:                                       ("e2", MonoPrint.p_exp MonoEnv.empty e2),
adamc@252:                                       ("r", MonoPrint.p_exp MonoEnv.empty r)];*)
adamc@252:         r
adamc@252:     end
adamc@133: 
adamc@133: fun typ c = c
adamc@133: 
adamc@316: val swapExpVars =
adamc@316:     U.Exp.mapB {typ = fn t => t,
adamc@316:                 exp = fn lower => fn e =>
adamc@316:                                      case e of
adamc@316:                                          ERel xn =>
adamc@316:                                          if xn = lower then
adamc@316:                                              ERel (lower + 1)
adamc@316:                                          else if xn = lower + 1 then
adamc@316:                                              ERel lower
adamc@316:                                          else
adamc@316:                                              e
adamc@316:                                        | _ => e,
adamc@316:                 bind = fn (lower, U.Exp.RelE _) => lower+1
adamc@316:                         | (lower, _) => lower}
adamc@316: 
adamc@258: datatype result = Yes of E.env | No | Maybe
adamc@258: 
adamc@183: fun match (env, p : pat, e : exp) =
adamc@183:     case (#1 p, #1 e) of
adamc@258:         (PWild, _) => Yes env
adamc@258:       | (PVar (x, t), _) => Yes (E.pushERel env x t (SOME e))
adamc@183: 
adamc@280:       | (PPrim (Prim.String s), EStrcat ((EPrim (Prim.String s'), _), _)) =>
adamc@280:         if String.isPrefix s' s then
adamc@280:             Maybe
adamc@280:         else
adamc@280:             No
adamc@280: 
adamc@183:       | (PPrim p, EPrim p') =>
adamc@183:         if Prim.equal (p, p') then
adamc@258:             Yes env
adamc@183:         else
adamc@258:             No
adamc@183: 
adamc@188:       | (PCon (_, PConVar n1, NONE), ECon (_, PConVar n2, NONE)) =>
adamc@183:         if n1 = n2 then
adamc@258:             Yes env
adamc@183:         else
adamc@258:             No
adamc@183: 
adamc@188:       | (PCon (_, PConVar n1, SOME p), ECon (_, PConVar n2, SOME e)) =>
adamc@183:         if n1 = n2 then
adamc@183:             match (env, p, e)
adamc@183:         else
adamc@258:             No
adamc@183: 
adamc@188:       | (PCon (_, PConFfi {mod = m1, con = con1, ...}, NONE), ECon (_, PConFfi {mod = m2, con = con2, ...}, NONE)) =>
adamc@185:         if m1 = m2 andalso con1 = con2 then
adamc@258:             Yes env
adamc@185:         else
adamc@258:             No
adamc@185: 
adamc@188:       | (PCon (_, PConFfi {mod = m1, con = con1, ...}, SOME ep), ECon (_, PConFfi {mod = m2, con = con2, ...}, SOME e)) =>
adamc@185:         if m1 = m2 andalso con1 = con2 then
adamc@185:             match (env, p, e)
adamc@185:         else
adamc@258:             No
adamc@185: 
adamc@183:       | (PRecord xps, ERecord xes) =>
adamc@183:         let
adamc@183:             fun consider (xps, env) =
adamc@183:                 case xps of
adamc@258:                     [] => Yes env
adamc@183:                   | (x, p, _) :: rest =>
adamc@183:                     case List.find (fn (x', _, _) => x' = x) xes of
adamc@258:                         NONE => No
adamc@183:                       | SOME (_, e, _) =>
adamc@183:                         case match (env, p, e) of
adamc@258:                             No => No
adamc@258:                           | Maybe => Maybe
adamc@258:                           | Yes env => consider (rest, env)
adamc@183:         in
adamc@183:             consider (xps, env)
adamc@183:         end
adamc@183: 
adamc@258:       | _ => Maybe
adamc@183: 
adamc@318: datatype event =
adamc@318:          WritePage
adamc@318:        | ReadDb
adamc@318:        | WriteDb
adamc@318:        | UseRel of int
adamc@318:        | Unsure
adamc@318: 
adamc@318: fun p_event e =
adamc@318:     let
adamc@318:         open Print.PD
adamc@318:     in
adamc@318:         case e of
adamc@318:             WritePage => string "WritePage"
adamc@318:           | ReadDb => string "ReadDb"
adamc@318:           | WriteDb => string "WriteDb"
adamc@318:           | UseRel n => string ("UseRel" ^ Int.toString n)
adamc@318:           | Unsure => string "Unsure"
adamc@318:     end
adamc@318: 
adamc@318: fun patBinds (p, _) =
adamc@318:     case p of
adamc@318:         PWild => 0
adamc@318:       | PVar _ => 1
adamc@318:       | PPrim _ => 0
adamc@318:       | PCon (_, _, NONE) => 0
adamc@318:       | PCon (_, _, SOME p) => patBinds p
adamc@318:       | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts
adamc@318:       | PNone _ => 0
adamc@318:       | PSome (_, p) => patBinds p
adamc@318: 
adamc@318: fun summarize d (e, _) =
adamc@318:     case e of
adamc@318:         EPrim _ => []
adamc@318:       | ERel n => if n >= d then [UseRel (n - d)] else []
adamc@318:       | ENamed _ => []
adamc@318:       | ECon (_, _, NONE) => []
adamc@318:       | ECon (_, _, SOME e) => summarize d e
adamc@318:       | ENone _ => []
adamc@318:       | ESome (_, e) => summarize d e
adamc@318:       | EFfi _ => []
adamc@318:       | EFfiApp (_, _, es) => List.concat (map (summarize d) es)
adamc@319:       | EApp ((EFfi _, _), e) => summarize d e
adamc@318:       | EApp _ => [Unsure]
adamc@318:       | EAbs _ => []
adamc@318: 
adamc@318:       | ERecord xets => List.concat (map (summarize d o #2) xets)
adamc@318:       | EField (e, _) => summarize d e
adamc@318: 
adamc@318:       | ECase (e, pes, _) =>
adamc@318:         let
adamc@318:             val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
adamc@318:         in
adamc@318:             case lss of
adamc@318:                 [] => raise Fail "Empty pattern match"
adamc@318:               | ls :: lss =>
adamc@318:                 if List.all (fn ls' => ls' = ls) lss then
adamc@318:                     summarize d e @ ls
adamc@318:                 else
adamc@318:                     [Unsure]
adamc@318:         end
adamc@318:       | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
adamc@318: 
adamc@318:       | EError (e, _) => summarize d e @ [Unsure]
adamc@318: 
adamc@318:       | EWrite e => summarize d e @ [WritePage]
adamc@318:         
adamc@318:       | ESeq (e1, e2) => summarize d e1 @ summarize d e2
adamc@318:       | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
adamc@318: 
adamc@318:       | EClosure (_, es) => List.concat (map (summarize d) es)
adamc@318: 
adamc@318:       | EQuery {query, body, initial, ...} =>
adamc@318:         List.concat [summarize d query,
adamc@319:                      summarize (d + 2) body,
adamc@318:                      summarize d initial,
adamc@318:                      [ReadDb]]
adamc@318: 
adamc@318:       | EDml e => summarize d e @ [WriteDb]
adamc@318: 
adamc@133: fun exp env e =
adamc@133:     case e of
adamc@183:         ERel n =>
adamc@183:         (case E.lookupERel env n of
adamc@183:              (_, _, SOME e') => #1 e'
adamc@183:            | _ => e)
adamc@183:       | ENamed n =>
adamc@133:         (case E.lookupENamed env n of
adamc@133:              (_, _, SOME e', _) => #1 e'
adamc@133:            | _ => e)
adamc@133: 
adamc@252:       | EApp ((EAbs (x, t, _, e1), loc), e2) =>
adamc@252:         ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp env e1),
adamc@252:                                        ("e2", MonoPrint.p_exp env e2)];*)
adamc@252:         if impure e2 then
adamc@252:             #1 (reduceExp env (ELet (x, t, e2, e1), loc))
adamc@252:         else
adamc@252:             #1 (reduceExp env (subExpInExp (0, e2) e1)))
adamc@133: 
adamc@184:       | ECase (disc, pes, _) =>
adamc@258:         let
adamc@258:             fun search pes =
adamc@258:                 case pes of
adamc@258:                     [] => e
adamc@258:                   | (p, body) :: pes =>
adamc@258:                     case match (env, p, disc) of
adamc@258:                         No => search pes
adamc@258:                       | Maybe => e
adamc@258:                       | Yes env => #1 (reduceExp env body)
adamc@258:         in
adamc@258:             search pes
adamc@258:         end
adamc@183: 
adamc@252:       | EField ((ERecord xes, _), x) =>
adamc@252:         (case List.find (fn (x', _, _) => x' = x) xes of
adamc@252:              SOME (_, e, _) => #1 e
adamc@252:            | NONE => e)
adamc@252: 
adamc@252:       | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) =>
adamc@252:         let
adamc@252:             val e' = (ELet (x2, t2, e1,
adamc@252:                             (ELet (x1, t1, b1,
adamc@252:                                    liftExpInExp 1 b2), loc)), loc)
adamc@252:         in
adamc@253:             (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)),
adamc@253:                                            ("e'", MonoPrint.p_exp env e')];*)
adamc@252:             #1 (reduceExp env e')
adamc@252:         end
adamc@252:       | EApp ((ELet (x, t, e, b), loc), e') =>
adamc@252:         #1 (reduceExp env (ELet (x, t, e,
adamc@252:                                  (EApp (b, liftExpInExp 0 e'), loc)), loc))
adamc@316: 
adamc@316:       | ELet (x, t, e, (EAbs (x', t' as (TRecord [], _), ran, e'), loc)) =>
adamc@316:         EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e, swapExpVars 0 e'), loc))
adamc@316: 
adamc@252:       | ELet (x, t, e', b) =>
adamc@252:         if impure e' then
adamc@318:             let
adamc@318:                 val effs_e' = summarize 0 e'
adamc@318:                 val effs_b = summarize 0 b
adamc@318: 
adamc@318:                 fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
adamc@318:                 val writesPage = does WritePage
adamc@318:                 val readsDb = does ReadDb
adamc@318:                 val writesDb = does WriteDb
adamc@318: 
adamc@318:                 fun verifyUnused eff =
adamc@318:                     case eff of
adamc@318:                         UseRel r => r <> 0
adamc@318:                       | Unsure => false
adamc@318:                       | _ => true
adamc@318: 
adamc@318:                 fun verifyCompatible effs =
adamc@318:                     case effs of
adamc@318:                         [] => false
adamc@318:                       | eff :: effs =>
adamc@318:                         case eff of
adamc@318:                             Unsure => false
adamc@318:                           | UseRel r =>
adamc@318:                             if r = 0 then
adamc@318:                                 List.all verifyUnused effs
adamc@318:                             else
adamc@318:                                 verifyCompatible effs
adamc@318:                           | WritePage => not writesPage andalso verifyCompatible effs
adamc@318:                           | ReadDb => not writesDb andalso verifyCompatible effs
adamc@318:                           | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
adamc@318:             in
adamc@318:                 (*Print.prefaces "verifyCompatible"
adamc@318:                 [("e'", MonoPrint.p_exp env e'),
adamc@318:                  ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
adamc@318:                  ("effs_e'", Print.p_list p_event effs_e'),
adamc@318:                  ("effs_b", Print.p_list p_event effs_b)];*)
adamc@318:                 if verifyCompatible effs_b then
adamc@318:                     #1 (reduceExp env (subExpInExp (0, e') b))
adamc@318:                 else
adamc@318:                     e
adamc@318:             end
adamc@252:         else
adamc@252:             #1 (reduceExp env (subExpInExp (0, e') b))
adamc@252: 
adamc@268:       | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) =>
adamc@268:         EPrim (Prim.String (s1 ^ s2))
adamc@268: 
adamc@133:       | _ => e
adamc@133: 
adamc@252: and bind (env, b) =
adamc@252:     case b of
adamc@252:         U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
adamc@252:       | U.Decl.RelE (x, t) => E.pushERel env x t NONE
adamc@252:       | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t (Option.map (reduceExp env) eo) s
adamc@252: 
adamc@133: and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
adamc@133: 
adamc@133: fun decl env d = d
adamc@133: 
adamc@133: val reduce = U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty
adamc@133: 
adamc@133: end