# HG changeset patch # User Adam Chlipala # Date 1239910179 14400 # Node ID 5819fb63c93af560e23709377bd0e9bf070b5bb3 # Parent e0dd85ea58e12e0935722b6d795736a27fe610b1 Effectness analysis diff -r e0dd85ea58e1 -r 5819fb63c93a demo/chat.ur --- 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 {[r.T.Id]} - {[r.T.Title]} + {[r.T.Title]} {[count]} - [delete] + ) -and delete id = +and delete id () = dml (DELETE FROM t WHERE Id = {[id]}); main () diff -r e0dd85ea58e1 -r 5819fb63c93a demo/crud.ur --- 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

Are you sure you want to delete ID #{[id]}?

+ end diff -r e0dd85ea58e1 -r 5819fb63c93a demo/ref.ur --- 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 {[iv]}, {[iv']}, {[sv]} + +fun main () = return + diff -r e0dd85ea58e1 -r 5819fb63c93a demo/sql.ur --- 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 => {[row.T.A]} {[row.T.B]} {[row.T.C]} {[row.T.D]} - [delete] + ); return @@ -36,7 +36,7 @@ {xml} -and delete a = +and delete a () = dml (DELETE FROM t WHERE t.A = {[a]}); xml <- list (); diff -r e0dd85ea58e1 -r 5819fb63c93a demo/tree.ur --- 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 = - #{[r.Id]}: {[r.Nam]} [Delete] + #{[r.Id]}: {[r.Nam]} Add child: @@ -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 () diff -r e0dd85ea58e1 -r 5819fb63c93a src/compiler.sig --- 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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/compiler.sml --- 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, diff -r e0dd85ea58e1 -r 5819fb63c93a src/core_print.sig --- 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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/core_print.sml --- 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, diff -r e0dd85ea58e1 -r 5819fb63c93a src/effectize.sig --- /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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/effectize.sml --- /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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/export.sig --- /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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/export.sml --- 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 diff -r e0dd85ea58e1 -r 5819fb63c93a src/mono_print.sml --- 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, diff -r e0dd85ea58e1 -r 5819fb63c93a src/sources --- 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