changeset 732:5819fb63c93a

Effectness analysis
author Adam Chlipala <adamc@hcoop.net>
date Thu, 16 Apr 2009 15:29:39 -0400
parents e0dd85ea58e1
children 15ddd64a5113
files demo/chat.ur demo/crud.ur demo/ref.ur demo/sql.ur demo/tree.ur src/compiler.sig src/compiler.sml src/core_print.sig src/core_print.sml src/effectize.sig src/effectize.sml src/export.sig src/export.sml src/mono_print.sml src/sources
diffstat 15 files changed, 229 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/demo/chat.ur	Thu Apr 16 14:49:25 2009 -0400
+++ b/demo/chat.ur	Thu Apr 16 15:29:39 2009 -0400
@@ -6,7 +6,7 @@
 table t : { Id : int, Title : string, Room : Room.topic }
   PRIMARY KEY Id
 
-fun chat id =
+fun chat id () =
     r <- oneRow (SELECT t.Title, t.Room FROM t WHERE t.Id = {[id]});
     ch <- Room.subscribe r.T.Room;
 
@@ -55,12 +55,13 @@
         count <- Room.subscribers r.T.Room;
         return <xml><tr>
           <td>{[r.T.Id]}</td>
-          <td><a link={chat r.T.Id}>{[r.T.Title]}</a></td>
+          <td>{[r.T.Title]}</td>
           <td>{[count]}</td>
-          <td><a link={delete r.T.Id}>[delete]</a></td>
+          <td><form><submit action={chat r.T.Id} value="Enter"/></form></td>
+          <td><form><submit action={delete r.T.Id} value="Delete"/></form></td>
         </tr></xml>)
 
-and delete id =
+and delete id () =
     dml (DELETE FROM t WHERE Id = {[id]});
     main ()
 
--- a/demo/crud.ur	Thu Apr 16 14:49:25 2009 -0400
+++ b/demo/crud.ur	Thu Apr 16 15:29:39 2009 -0400
@@ -167,7 +167,7 @@
             return <xml><body>
               <p>Are you sure you want to delete ID #{[id]}?</p>
               
-              <p><a link={delete ()}>I was born sure!</a></p>
+              <form><submit action={delete} value="I was born sure!"/></form>
             </body></xml>
         end    
 
--- a/demo/ref.ur	Thu Apr 16 14:49:25 2009 -0400
+++ b/demo/ref.ur	Thu Apr 16 15:29:39 2009 -0400
@@ -6,7 +6,7 @@
                                type data = string
                            end)
 
-fun main () =
+fun mutate () =
     ir <- IR.new 3;
     ir' <- IR.new 7;
     sr <- SR.new "hi";
@@ -24,3 +24,7 @@
     return <xml><body>
       {[iv]}, {[iv']}, {[sv]}
     </body></xml>
+
+fun main () = return <xml><body>
+  <form><submit action={mutate} value="Do some pointless stuff"/></form>
+</body></xml>
--- a/demo/sql.ur	Thu Apr 16 14:49:25 2009 -0400
+++ b/demo/sql.ur	Thu Apr 16 15:29:39 2009 -0400
@@ -5,7 +5,7 @@
     rows <- queryX (SELECT * FROM t)
             (fn row => <xml><tr>
               <td>{[row.T.A]}</td> <td>{[row.T.B]}</td> <td>{[row.T.C]}</td> <td>{[row.T.D]}</td>
-              <td><a link={delete row.T.A}>[delete]</a></td>
+              <td><form><submit action={delete row.T.A} value="Delete"/></form></td>
             </tr></xml>);
     return <xml>
       <table border=1>
@@ -36,7 +36,7 @@
       {xml}
     </body></xml>
 
-and delete a =
+and delete a () =
     dml (DELETE FROM t
          WHERE t.A = {[a]});
     xml <- list ();
--- a/demo/tree.ur	Thu Apr 16 14:49:25 2009 -0400
+++ b/demo/tree.ur	Thu Apr 16 15:29:39 2009 -0400
@@ -8,7 +8,7 @@
                   end)
 
 fun row r = <xml>
-  #{[r.Id]}: {[r.Nam]} <a link={del r.Id}>[Delete]</a>
+  #{[r.Id]}: {[r.Nam]} <form><submit action={del r.Id} value="Delete"/></form>
 
   <form>
     Add child: <textbox{#Nam}/> <submit action={add (Some r.Id)}/>
@@ -30,6 +30,6 @@
     dml (INSERT INTO t (Id, Parent, Nam) VALUES ({[id]}, {[parent]}, {[r.Nam]}));
     main ()
 
-and del id =
+and del id () =
     dml (DELETE FROM t WHERE Id = {[id]});
     main ()
--- a/src/compiler.sig	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/compiler.sig	Thu Apr 16 15:29:39 2009 -0400
@@ -73,6 +73,7 @@
     val unpoly : (Core.file, Core.file) phase
     val specialize : (Core.file, Core.file) phase
     val marshalcheck : (Core.file, Core.file) phase
+    val effectize : (Core.file, Core.file) phase
     val monoize : (Core.file, Mono.file) phase
     val mono_opt : (Mono.file, Mono.file) phase
     val untangle : (Mono.file, Mono.file) phase
@@ -105,6 +106,7 @@
     val toSpecialize : (string, Core.file) transform 
     val toShake3 : (string, Core.file) transform
     val toMarshalcheck : (string, Core.file) transform
+    val toEffectize : (string, Core.file) transform
     val toMonoize : (string, Mono.file) transform
     val toMono_opt1 : (string, Mono.file) transform
     val toUntangle : (string, Mono.file) transform
--- a/src/compiler.sml	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/compiler.sml	Thu Apr 16 15:29:39 2009 -0400
@@ -505,12 +505,19 @@
 
 val toMarshalcheck = transform marshalcheck "marshalcheck" o toShake3
 
+val effectize = {
+    func = Effective.effectize,
+    print = CorePrint.p_file CoreEnv.empty
+}
+
+val toEffectize = transform effectize "effectize" o toMarshalcheck
+
 val monoize = {
     func = Monoize.monoize CoreEnv.empty,
     print = MonoPrint.p_file MonoEnv.empty
 }
 
-val toMonoize = transform monoize "monoize" o toMarshalcheck
+val toMonoize = transform monoize "monoize" o toEffectize
 
 val mono_opt = {
     func = MonoOpt.optimize,
--- a/src/core_print.sig	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/core_print.sig	Thu Apr 16 15:29:39 2009 -0400
@@ -34,7 +34,6 @@
     val p_exp : CoreEnv.env -> Core.exp Print.printer
     val p_decl : CoreEnv.env -> Core.decl Print.printer
     val p_file : CoreEnv.env -> Core.file Print.printer
-    val p_export_kind : Core.export_kind Print.printer
 
     val debug : bool ref
 end
--- a/src/core_print.sml	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/core_print.sml	Thu Apr 16 15:29:39 2009 -0400
@@ -467,12 +467,6 @@
              p_exp env e]
     end
 
-fun p_export_kind ck =
-    case ck of
-        Link => string "link"
-      | Action _ => string "action"
-      | Rpc _ => string "rpc"
-
 fun p_datatype env (x, n, xs, cons) =
     let
         val k = (KType, ErrorMsg.dummySpan)
@@ -538,7 +532,7 @@
         end
       | DExport (ek, n) => box [string "export",
                                 space,
-                                p_export_kind ek,
+                                Export.p_export_kind ek,
                                 space,
                                 p_enamed env n,
                                 space,
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/effectize.sig	Thu Apr 16 15:29:39 2009 -0400
@@ -0,0 +1,32 @@
+(* Copyright (c) 2009, 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.
+ *)
+
+signature EFFECTIZE = sig
+
+    val effectize : Core.file -> Core.file
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/effectize.sml	Thu Apr 16 15:29:39 2009 -0400
@@ -0,0 +1,109 @@
+(* Copyright (c) 2009, 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.
+ *)
+
+structure Effective :> EFFECTIZE = struct
+
+open Core
+
+structure U = CoreUtil
+
+structure IM = IntBinaryMap
+structure SS = BinarySetFn(struct
+                           type ord_key = string
+                           val compare = String.compare
+                           end)
+
+val effectful = ["dml", "nextval", "send"]
+val effectful = SS.addList (SS.empty, effectful)
+
+fun effectize file =
+    let
+        fun exp evs e =
+            case e of
+                EFfi ("Basis", s) => SS.member (effectful, s)
+              | EFfiApp ("Basis", s, _) => SS.member (effectful, s)
+              | ENamed n => IM.inDomain (evs, n)
+              | EServerCall (n, _, _, _) => IM.inDomain (evs, n)
+              | _ => false
+
+        fun couldWrite evs = U.Exp.exists {kind = fn _ => false,
+                                           con = fn _ => false,
+                                           exp = exp evs}
+
+        fun doDecl (d, evs) =
+            case #1 d of
+                DVal (x, n, t, e, s) =>
+                (d, if couldWrite evs e then
+                        IM.insert (evs, n, (#2 d, s))
+                    else
+                        evs)
+              | DValRec vis =>
+                let
+                    fun oneRound evs =
+                        foldl (fn ((_, n, _, e, s), (changed, evs)) =>
+                                if couldWrite evs e andalso not (IM.inDomain (evs, n)) then
+                                    (true, IM.insert (evs, n, (#2 d, s)))
+                                else
+                                    (changed, evs)) (false, evs) vis
+
+                    fun loop evs =
+                        let
+                            val (b, evs) = oneRound evs
+                        in
+                            if b then
+                                loop evs
+                            else
+                                evs
+                        end
+                in
+                    (d, loop evs)
+                end
+              | DExport (Link, n) =>
+                (case IM.find (evs, n) of
+                     NONE => ()
+                   | SOME (loc, s) => ErrorMsg.errorAt loc ("A link (" ^ s ^ ") could cause side effects; try implementing it with a form instead");
+                 (d, evs))
+              | DExport (Action _, n) =>
+                ((DExport (Action (if IM.inDomain (evs, n) then
+                                       ReadWrite
+                                   else
+                                       ReadOnly), n), #2 d),
+                 evs)
+              | DExport (Rpc _, n) =>
+                ((DExport (Rpc (if IM.inDomain (evs, n) then
+                                    ReadWrite
+                                else
+                                    ReadOnly), n), #2 d),
+                 evs)
+              | _ => (d, evs)
+
+        val (file, _) = ListUtil.foldlMap doDecl IM.empty file
+    in
+        file
+    end
+
+end
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/export.sig	Thu Apr 16 15:29:39 2009 -0400
@@ -0,0 +1,42 @@
+(* Copyright (c) 2009, 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.
+ *)
+
+signature EXPORT = sig
+
+datatype effect =
+         ReadOnly
+       | ReadWrite
+
+datatype export_kind =
+         Link
+       | Action of effect
+       | Rpc of effect
+
+val p_effect : effect Print.printer
+val p_export_kind : export_kind Print.printer
+
+end
--- a/src/export.sml	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/export.sml	Thu Apr 16 15:29:39 2009 -0400
@@ -27,6 +27,9 @@
 
 structure Export = struct
 
+open Print.PD
+open Print
+
 datatype effect =
          ReadOnly
        | ReadWrite
@@ -36,4 +39,15 @@
        | Action of effect
        | Rpc of effect
 
+fun p_effect ef =
+    case ef of
+        ReadOnly => string "r"
+      | ReadWrite => string "rw"
+
+fun p_export_kind ck =
+    case ck of
+        Link => string "link"
+      | Action ef => box [string "action(", p_effect ef, string ")"]
+      | Rpc ef => box [string "rpc(", p_effect ef, string ")"]
+
 end
--- a/src/mono_print.sml	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/mono_print.sml	Thu Apr 16 15:29:39 2009 -0400
@@ -387,7 +387,7 @@
 
       | DExport (ek, s, n, ts, t) => box [string "export",
                                           space,
-                                          CorePrint.p_export_kind ek,
+                                          Export.p_export_kind ek,
                                           space,
                                           p_enamed env n,
                                           space,
--- a/src/sources	Thu Apr 16 14:49:25 2009 -0400
+++ b/src/sources	Thu Apr 16 15:29:39 2009 -0400
@@ -20,6 +20,8 @@
 prim.sml
 
 datatype_kind.sml
+
+export.sig
 export.sml
 
 source.sml
@@ -114,6 +116,9 @@
 tag.sig
 tag.sml
 
+effectize.sig
+effectize.sml
+
 marshalcheck.sig
 marshalcheck.sml