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