Mercurial > urweb

annotate src/effectize.sml @ 1034:a779402841f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hooks for measuring how much interesting proving is going on in elaboration
author Adam Chlipala <adamc@hcoop.net>
date Tue, 17 Nov 2009 12:44:14 -0500
parents dfe34fad749d
children 72670131dace
rev   line source
adamc@732 1 (* Copyright (c) 2009, Adam Chlipala
adamc@732 2 * All rights reserved.
adamc@732 3 *
adamc@732 4 * Redistribution and use in source and binary forms, with or without
adamc@732 5 * modification, are permitted provided that the following conditions are met:
adamc@732 6 *
adamc@732 7 * - Redistributions of source code must retain the above copyright notice,
adamc@732 8 * this list of conditions and the following disclaimer.
adamc@732 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@732 10 * this list of conditions and the following disclaimer in the documentation
adamc@732 11 * and/or other materials provided with the distribution.
adamc@732 12 * - The names of contributors may not be used to endorse or promote products
adamc@732 13 * derived from this software without specific prior written permission.
adamc@732 14 *
adamc@732 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@732 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@732 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@732 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@732 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@732 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@732 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@732 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@732 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@732 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@732 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@732 26 *)
adamc@732 27
adamc@732 28 structure Effective :> EFFECTIZE = struct
adamc@732 29
adamc@732 30 open Core
adamc@732 31
adamc@732 32 structure U = CoreUtil
adamc@732 33
adamc@732 34 structure IM = IntBinaryMap
adamc@732 35 structure SS = BinarySetFn(struct
adamc@732 36 type ord_key = string
adamc@732 37 val compare = String.compare
adamc@732 38 end)
adamc@732 39
adamc@765 40 fun effectful x = Settings.isEffectful x andalso not (Settings.isClientOnly x)
adamc@732 41
adamc@732 42 fun effectize file =
adamc@732 43 let
adamc@782 44 fun expOnload evs e =
adamc@782 45 case e of
adamc@782 46 EFfi f => effectful f
adamc@782 47 | EFfiApp (m, x, _) => effectful (m, x)
adamc@782 48 | ENamed n => IM.inDomain (evs, n)
adamc@1020 49 | EServerCall (n, _, _) => IM.inDomain (evs, n)
adamc@782 50 | _ => false
adamc@782 51
adamc@782 52 fun couldWriteOnload evs = U.Exp.exists {kind = fn _ => false,
adamc@782 53 con = fn _ => false,
adamc@782 54 exp = expOnload evs}
adamc@782 55
adamc@732 56 fun exp evs e =
adamc@732 57 case e of
adamc@765 58 EFfi f => effectful f
adamc@765 59 | EFfiApp (m, x, _) => effectful (m, x)
adamc@732 60 | ENamed n => IM.inDomain (evs, n)
adamc@782 61 | ERecord xets => List.exists (fn ((CName "Onload", _), e, _) => couldWriteOnload evs e
adamc@782 62 | _ => false) xets
adamc@732 63 | _ => false
adamc@732 64
adamc@732 65 fun couldWrite evs = U.Exp.exists {kind = fn _ => false,
adamc@732 66 con = fn _ => false,
adamc@732 67 exp = exp evs}
adamc@732 68
adamc@735 69 fun exp evs e =
adamc@735 70 case e of
adamc@735 71 EFfi ("Basis", "getCookie") => true
adamc@735 72 | ENamed n => IM.inDomain (evs, n)
adamc@1020 73 | EServerCall (n, _, _) => IM.inDomain (evs, n)
adamc@735 74 | _ => false
adamc@735 75
adamc@735 76 fun couldReadCookie evs = U.Exp.exists {kind = fn _ => false,
adamc@735 77 con = fn _ => false,
adamc@735 78 exp = exp evs}
adamc@735 79
adamc@735 80 fun doDecl (d, evs as (writers, readers)) =
adamc@732 81 case #1 d of
adamc@732 82 DVal (x, n, t, e, s) =>
adamc@735 83 (d, (if couldWrite writers e then
adamc@735 84 IM.insert (writers, n, (#2 d, s))
adamc@735 85 else
adamc@735 86 writers,
adamc@735 87 if couldReadCookie readers e then
adamc@735 88 IM.insert (readers, n, (#2 d, s))
adamc@735 89 else
adamc@735 90 readers))
adamc@732 91 | DValRec vis =>
adamc@732 92 let
adamc@732 93 fun oneRound evs =
adamc@735 94 foldl (fn ((_, n, _, e, s), (changed, (writers, readers))) =>
adamc@735 95 let
adamc@735 96 val (changed, writers) =
adamc@735 97 if couldWrite writers e andalso not (IM.inDomain (writers, n)) then
adamc@735 98 (true, IM.insert (writers, n, (#2 d, s)))
adamc@735 99 else
adamc@735 100 (changed, writers)
adamc@735 101
adamc@735 102 val (changed, readers) =
adamc@735 103 if couldReadCookie readers e andalso not (IM.inDomain (readers, n)) then
adamc@735 104 (true, IM.insert (readers, n, (#2 d, s)))
adamc@735 105 else
adamc@735 106 (changed, readers)
adamc@735 107 in
adamc@735 108 (changed, (writers, readers))
adamc@735 109 end) (false, evs) vis
adamc@732 110
adamc@732 111 fun loop evs =
adamc@732 112 let
adamc@732 113 val (b, evs) = oneRound evs
adamc@732 114 in
adamc@732 115 if b then
adamc@732 116 loop evs
adamc@732 117 else
adamc@732 118 evs
adamc@732 119 end
adamc@732 120 in
adamc@735 121 (d, loop (writers, readers))
adamc@732 122 end
adamc@732 123 | DExport (Link, n) =>
adamc@735 124 (case IM.find (writers, n) of
adamc@732 125 NONE => ()
adamc@732 126 | SOME (loc, s) => ErrorMsg.errorAt loc ("A link (" ^ s ^ ") could cause side effects; try implementing it with a form instead");
adamc@732 127 (d, evs))
adamc@732 128 | DExport (Action _, n) =>
adamc@735 129 ((DExport (Action (if IM.inDomain (writers, n) then
adamc@735 130 if IM.inDomain (readers, n) then
adamc@735 131 ReadCookieWrite
adamc@735 132 else
adamc@735 133 ReadWrite
adamc@732 134 else
adamc@732 135 ReadOnly), n), #2 d),
adamc@732 136 evs)
adamc@732 137 | DExport (Rpc _, n) =>
adamc@735 138 ((DExport (Rpc (if IM.inDomain (writers, n) then
adamc@735 139 if IM.inDomain (readers, n) then
adamc@735 140 ReadCookieWrite
adamc@735 141 else
adamc@735 142 ReadWrite
adamc@732 143 else
adamc@732 144 ReadOnly), n), #2 d),
adamc@732 145 evs)
adamc@732 146 | _ => (d, evs)
adamc@732 147
adamc@735 148 val (file, _) = ListUtil.foldlMap doDecl (IM.empty, IM.empty) file
adamc@732 149 in
adamc@732 150 file
adamc@732 151 end
adamc@732 152
adamc@732 153 end