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@470: structure IM = IntBinaryMap
adamc@470: 
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@338:       | ENextval _ => true
adamc@463:       | EUnurlify _ => 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@462:       | EFfiApp ("Basis", "set_cookie", _) => true
adamc@252:       | EFfiApp _ => false
adamc@252:       | EApp ((EFfi _, _), _) => false
adamc@252:       | EApp _ => true
adamc@252: 
adamc@387:       | EUnop (_, e) => impure e
adamc@387:       | EBinop (_, e1, e2) => impure e1 orelse impure e2
adamc@387: 
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@341: val swapExpVarsPat =
adamc@341:     U.Exp.mapB {typ = fn t => t,
adamc@341:                 exp = fn (lower, len) => fn e =>
adamc@341:                                      case e of
adamc@341:                                          ERel xn =>
adamc@341:                                          if xn = lower then
adamc@341:                                              ERel (lower + 1)
adamc@341:                                          else if xn >= lower + 1 andalso xn < lower + 1 + len then
adamc@341:                                              ERel (xn - 1)
adamc@341:                                          else
adamc@341:                                              e
adamc@341:                                        | _ => e,
adamc@341:                 bind = fn ((lower, len), U.Exp.RelE _) => (lower+1, len)
adamc@341:                         | (st, _) => st}
adamc@341: 
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@481:        | UseRel
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@481:           | UseRel => string "UseRel"
adamc@318:           | Unsure => string "Unsure"
adamc@318:     end
adamc@318: 
adamc@470: val p_events = Print.p_list p_event
adamc@470: 
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@470: fun reduce file =
adamc@470:     let
adamc@470:         fun countAbs (e, _) =
adamc@470:             case e of
adamc@470:                 EAbs (_, _, _, e) => 1 + countAbs e
adamc@470:               | _ => 0
adamc@318: 
adamc@470:         val absCounts =
adamc@470:             foldl (fn ((d, _), absCounts) =>
adamc@470:                       case d of
adamc@470:                           DVal (_, n, _, e, _) =>
adamc@470:                           IM.insert (absCounts, n, countAbs e)
adamc@470:                         | DValRec vis =>
adamc@470:                           foldl (fn ((_, n, _, e, _), absCounts) =>
adamc@470:                                     IM.insert (absCounts, n, countAbs e))
adamc@470:                           absCounts vis
adamc@470:                         | _ => absCounts)
adamc@470:             IM.empty file
adamc@387: 
adamc@470:         fun summarize d (e, _) =
adamc@398:             case e of
adamc@470:                 EPrim _ => []
adamc@481:               | ERel n => if n = d then [UseRel] else []
adamc@470:               | ENamed _ => []
adamc@470:               | ECon (_, _, NONE) => []
adamc@470:               | ECon (_, _, SOME e) => summarize d e
adamc@470:               | ENone _ => []
adamc@470:               | ESome (_, e) => summarize d e
adamc@470:               | EFfi _ => []
adamc@470:               | EFfiApp ("Basis", "set_cookie", _) => [Unsure]
adamc@470:               | EFfiApp (_, _, es) => List.concat (map (summarize d) es)
adamc@470:               | EApp ((EFfi _, _), e) => summarize d e
adamc@470:               | EApp _ =>
adamc@398:                 let
adamc@470:                     fun unravel (e, ls) =
adamc@470:                         case e of
adamc@470:                             ENamed n =>
adamc@470:                             let
adamc@470:                                 val ls = rev ls
adamc@470:                             in
adamc@470:                                 case IM.find (absCounts, n) of
adamc@470:                                     NONE => [Unsure]
adamc@470:                                   | SOME len =>
adamc@470:                                     if length ls < len then
adamc@470:                                         ls
adamc@470:                                     else
adamc@470:                                         [Unsure]
adamc@470:                             end
adamc@481:                           | ERel n => List.revAppend (ls,
adamc@481:                                                       if n = d then
adamc@481:                                                           [UseRel, Unsure]
adamc@481:                                                       else
adamc@481:                                                           [Unsure])
adamc@470:                           | EApp (f, x) =>
adamc@470:                             unravel (#1 f, summarize d x @ ls)
adamc@470:                           | _ => [Unsure]
adamc@398:                 in
adamc@470:                     unravel (e, [])
adamc@398:                 end
adamc@252: 
adamc@470:               | EAbs _ => []
adamc@316: 
adamc@470:               | EUnop (_, e) => summarize d e
adamc@470:               | EBinop (_, e1, e2) => summarize d e1 @ summarize d e2
adamc@470: 
adamc@470:               | ERecord xets => List.concat (map (summarize d o #2) xets)
adamc@470:               | EField (e, _) => summarize d e
adamc@470: 
adamc@470:               | ECase (e, pes, _) =>
adamc@398:                 let
adamc@470:                     val lss = map (fn (p, e) => summarize (d + patBinds p) e) pes
adamc@398:                 in
adamc@470:                     case lss of
adamc@470:                         [] => raise Fail "Empty pattern match"
adamc@470:                       | ls :: lss =>
adamc@470:                         if List.all (fn ls' => ls' = ls) lss then
adamc@470:                             summarize d e @ ls
adamc@470:                         else
adamc@470:                             [Unsure]
adamc@398:                 end
adamc@470:               | EStrcat (e1, e2) => summarize d e1 @ summarize d e2
adamc@316: 
adamc@470:               | EError (e, _) => summarize d e @ [Unsure]
adamc@318: 
adamc@470:               | EWrite e => summarize d e @ [WritePage]
adamc@470:                             
adamc@470:               | ESeq (e1, e2) => summarize d e1 @ summarize d e2
adamc@470:               | ELet (_, _, e1, e2) => summarize d e1 @ summarize (d + 1) e2
adamc@456: 
adamc@470:               | EClosure (_, es) => List.concat (map (summarize d) es)
adamc@470: 
adamc@470:               | EQuery {query, body, initial, ...} =>
adamc@470:                 List.concat [summarize d query,
adamc@470:                              summarize (d + 2) body,
adamc@470:                              summarize d initial,
adamc@470:                              [ReadDb]]
adamc@470: 
adamc@470:               | EDml e => summarize d e @ [WriteDb]
adamc@470:               | ENextval e => summarize d e @ [WriteDb]
adamc@470:               | EUnurlify (e, _) => summarize d e
adamc@470: 
adamc@470: 
adamc@470:         fun exp env e =
adamc@470:             let
adamc@470:                 (*val () = Print.prefaces "exp" [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan))]*)
adamc@470: 
adamc@470:                 val r =
adamc@470:                     case e of
adamc@470:                         ERel n =>
adamc@470:                         (case E.lookupERel env n of
adamc@470:                              (_, _, SOME e') => #1 e'
adamc@470:                            | _ => e)
adamc@470:                       | ENamed n =>
adamc@470:                         (case E.lookupENamed env n of
adamc@470:                              (_, _, SOME e', _) => ((*Print.prefaces "Switch" [("n", Print.PD.string (Int.toString n)),
adamc@470:                                                                                ("e'", MonoPrint.p_exp env e')];*)
adamc@470:                                                     #1 e')
adamc@470:                            | _ => e)
adamc@470: 
adamc@470:                       | EApp ((EAbs (x, t, _, e1), loc), e2) =>
adamc@470:                         ((*Print.prefaces "Considering" [("e1", MonoPrint.p_exp (E.pushERel env x t NONE) e1),
adamc@470:                                                          ("e2", MonoPrint.p_exp env e2),
adamc@470:                                                          ("sub", MonoPrint.p_exp env (reduceExp env (subExpInExp (0, e2) e1)))];*)
adamc@470:                          if impure e2 then
adamc@470:                              #1 (reduceExp env (ELet (x, t, e2, e1), loc))
adamc@470:                          else
adamc@470:                              #1 (reduceExp env (subExpInExp (0, e2) e1)))
adamc@470: 
adamc@470:                       | ECase (e', pes, {disc, result}) =>
adamc@442:                         let
adamc@470:                             fun push () =
adamc@470:                                 case result of
adamc@470:                                     (TFun (dom, result), loc) =>
adamc@470:                                     if List.all (fn (_, (EAbs _, _)) => true | _ => false) pes then
adamc@470:                                         EAbs ("_", dom, result,
adamc@470:                                               (ECase (liftExpInExp 0 e',
adamc@470:                                                       map (fn (p, (EAbs (_, _, _, e), _)) =>
adamc@470:                                                               (p, swapExpVarsPat (0, patBinds p) e)
adamc@470:                                                             | _ => raise Fail "MonoReduce ECase") pes,
adamc@470:                                                       {disc = disc, result = result}), loc))
adamc@470:                                     else
adamc@470:                                         e
adamc@470:                                   | _ => e
adamc@318: 
adamc@470:                             fun search pes =
adamc@470:                                 case pes of
adamc@470:                                     [] => push ()
adamc@470:                                   | (p, body) :: pes =>
adamc@470:                                     case match (env, p, e') of
adamc@470:                                         No => search pes
adamc@470:                                       | Maybe => push ()
adamc@470:                                       | Yes env => #1 (reduceExp env body)
adamc@470:                         in
adamc@470:                             search pes
adamc@470:                         end
adamc@318: 
adamc@470:                       | EField ((ERecord xes, _), x) =>
adamc@470:                         (case List.find (fn (x', _, _) => x' = x) xes of
adamc@470:                              SOME (_, e, _) => #1 e
adamc@470:                            | NONE => e)
adamc@398: 
adamc@470:                       | ELet (x1, t1, (ELet (x2, t2, e1, b1), loc), b2) =>
adamc@470:                         let
adamc@470:                             val e' = (ELet (x2, t2, e1,
adamc@470:                                             (ELet (x1, t1, b1,
adamc@470:                                                    liftExpInExp 1 b2), loc)), loc)
adamc@442:                         in
adamc@470:                             (*Print.prefaces "ELet commute" [("e", MonoPrint.p_exp env (e, loc)),
adamc@470:                                                              ("e'", MonoPrint.p_exp env e')];*)
adamc@470:                             #1 (reduceExp env e')
adamc@470:                         end
adamc@470:                       | EApp ((ELet (x, t, e, b), loc), e') =>
adamc@470:                         #1 (reduceExp env (ELet (x, t, e,
adamc@470:                                                  (EApp (b, liftExpInExp 0 e'), loc)), loc))
adamc@470: 
adamc@470:                       | ELet (x, t, e', (EAbs (x', t' as (TRecord [], _), ran, e''), loc)) =>
adamc@470:                         (*if impure e' then
adamc@470:                               e
adamc@470:                           else*)
adamc@470:                         (* Seems unsound in general without the check... should revisit later *)
adamc@470:                         EAbs (x', t', ran, (ELet (x, t, liftExpInExp 0 e', swapExpVars 0 e''), loc))
adamc@470: 
adamc@470:                       | ELet (x, t, e', b) =>
adamc@470:                         let
adamc@470:                             fun doSub () =
adamc@470:                                 #1 (reduceExp env (subExpInExp (0, e') b))
adamc@470: 
adamc@470:                             fun trySub () =
adamc@470:                                 case t of
adamc@470:                                     (TFfi ("Basis", "string"), _) => doSub ()
adamc@470:                                   | _ =>
adamc@470:                                     case e' of
adamc@470:                                         (ECase _, _) => e
adamc@470:                                       | _ => doSub ()
adamc@470:                         in
adamc@470:                             if impure e' then
adamc@470:                                 let
adamc@470:                                     val effs_e' = summarize 0 e'
adamc@489:                                     val effs_e' = List.filter (fn x => x <> UseRel) effs_e'
adamc@470:                                     val effs_b = summarize 0 b
adamc@470: 
adamc@470:                                     (*val () = Print.prefaces "Try"
adamc@489:                                                             [("e", MonoPrint.p_exp env (e, ErrorMsg.dummySpan)),
adamc@489:                                                              ("e'", p_events effs_e'),
adamc@489:                                                              ("b", p_events effs_b)]*)
adamc@470: 
adamc@470:                                     fun does eff = List.exists (fn eff' => eff' = eff) effs_e'
adamc@470:                                     val writesPage = does WritePage
adamc@470:                                     val readsDb = does ReadDb
adamc@470:                                     val writesDb = does WriteDb
adamc@470: 
adamc@470:                                     fun verifyUnused eff =
adamc@470:                                         case eff of
adamc@481:                                             UseRel => false
adamc@470:                                           | _ => true
adamc@470: 
adamc@470:                                     fun verifyCompatible effs =
adamc@470:                                         case effs of
adamc@470:                                             [] => false
adamc@470:                                           | eff :: effs =>
adamc@470:                                             case eff of
adamc@470:                                                 Unsure => false
adamc@481:                                               | UseRel => List.all verifyUnused effs
adamc@470:                                               | WritePage => not writesPage andalso verifyCompatible effs
adamc@470:                                               | ReadDb => not writesDb andalso verifyCompatible effs
adamc@470:                                               | WriteDb => not writesDb andalso not readsDb andalso verifyCompatible effs
adamc@470:                                 in
adamc@470:                                     (*Print.prefaces "verifyCompatible"
adamc@470:                                                      [("e'", MonoPrint.p_exp env e'),
adamc@470:                                                       ("b", MonoPrint.p_exp (E.pushERel env x t NONE) b),
adamc@470:                                                       ("effs_e'", Print.p_list p_event effs_e'),
adamc@470:                                                       ("effs_b", Print.p_list p_event effs_b)];*)
adamc@481:                                     if List.null effs_e' orelse verifyCompatible effs_b then
adamc@470:                                         trySub ()
adamc@470:                                     else
adamc@470:                                         e
adamc@470:                                 end
adamc@470:                             else
adamc@442:                                 trySub ()
adamc@442:                         end
adamc@252: 
adamc@470:                       | EStrcat ((EPrim (Prim.String s1), _), (EPrim (Prim.String s2), _)) =>
adamc@470:                         EPrim (Prim.String (s1 ^ s2))
adamc@268: 
adamc@470:                       | _ => e
adamc@470:             in
adamc@470:                 (*Print.prefaces "exp'" [("r", MonoPrint.p_exp env (r, ErrorMsg.dummySpan))];*)
adamc@470:                 r
adamc@470:             end
adamc@470: 
adamc@470:         and bind (env, b) =
adamc@470:             case b of
adamc@470:                 U.Decl.Datatype (x, n, xncs) => E.pushDatatype env x n xncs
adamc@470:               | U.Decl.RelE (x, t) => E.pushERel env x t NONE
adamc@470:               | U.Decl.NamedE (x, n, t, eo, s) => E.pushENamed env x n t (Option.map (reduceExp env) eo) s
adamc@470: 
adamc@470:         and reduceExp env = U.Exp.mapB {typ = typ, exp = exp, bind = bind} env
adamc@470: 
adamc@470:         fun decl env d = d
adamc@398:     in
adamc@470:         U.File.mapB {typ = typ, exp = exp, decl = decl, bind = bind} E.empty file
adamc@398:     end
adamc@133: 
adamc@133: end