Mercurial > urweb
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