annotate src/core_untangle.sml @ 456:1a4fa157fedd

Monoizing FFI transactions correctly
author Adam Chlipala <adamc@hcoop.net>
date Thu, 06 Nov 2008 09:21:34 -0500
parents d4a81273d4b1
children 23a88d81a1b5
rev   line source
adamc@454 1 (* Copyright (c) 2008, Adam Chlipala
adamc@454 2 * All rights reserved.
adamc@454 3 *
adamc@454 4 * Redistribution and use in source and binary forms, with or without
adamc@454 5 * modification, are permitted provided that the following conditions are met:
adamc@454 6 *
adamc@454 7 * - Redistributions of source code must retain the above copyright notice,
adamc@454 8 * this list of conditions and the following disclaimer.
adamc@454 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@454 10 * this list of conditions and the following disclaimer in the documentation
adamc@454 11 * and/or other materials provided with the distribution.
adamc@454 12 * - The names of contributors may not be used to endorse or promote products
adamc@454 13 * derived from this software without specific prior written permission.
adamc@454 14 *
adamc@454 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@454 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@454 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@454 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@454 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@454 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@454 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@454 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@454 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@454 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@454 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@454 26 *)
adamc@454 27
adamc@454 28 structure CoreUntangle :> CORE_UNTANGLE = struct
adamc@454 29
adamc@454 30 open Core
adamc@454 31
adamc@454 32 structure U = CoreUtil
adamc@454 33 structure E = CoreEnv
adamc@454 34
adamc@454 35 structure IS = IntBinarySet
adamc@454 36 structure IM = IntBinaryMap
adamc@454 37
adamc@454 38 fun default (k, s) = s
adamc@454 39
adamc@454 40 fun exp (e, s) =
adamc@454 41 case e of
adamc@454 42 ENamed n => IS.add (s, n)
adamc@454 43
adamc@454 44 | _ => s
adamc@454 45
adamc@454 46 fun untangle file =
adamc@454 47 let
adamc@455 48 val edefs = foldl (fn ((d, _), edefs) =>
adamc@455 49 case d of
adamc@455 50 DVal (_, n, _, e, _) => IM.insert (edefs, n, e)
adamc@455 51 | DValRec vis =>
adamc@455 52 foldl (fn ((_, n, _, e, _), edefs) =>
adamc@455 53 IM.insert (edefs, n, e)) edefs vis
adamc@455 54 | _ => edefs)
adamc@455 55 IM.empty file
adamc@455 56
adamc@454 57 fun decl (dAll as (d, loc)) =
adamc@454 58 case d of
adamc@454 59 DValRec vis =>
adamc@454 60 let
adamc@454 61 val thisGroup = foldl (fn ((_, n, _, _, _), thisGroup) =>
adamc@454 62 IS.add (thisGroup, n)) IS.empty vis
adamc@454 63
adamc@455 64 val expUsed = U.Exp.fold {con = default,
adamc@455 65 kind = default,
adamc@455 66 exp = exp} IS.empty
adamc@455 67
adamc@454 68 val used = foldl (fn ((_, n, _, e, _), used) =>
adamc@454 69 let
adamc@455 70 val usedHere = expUsed e
adamc@454 71 in
adamc@455 72 IM.insert (used, n, usedHere)
adamc@454 73 end)
adamc@454 74 IM.empty vis
adamc@454 75
adamc@455 76 fun expand used =
adamc@455 77 IS.foldl (fn (n, used) =>
adamc@455 78 case IM.find (edefs, n) of
adamc@455 79 NONE => used
adamc@455 80 | SOME e =>
adamc@455 81 let
adamc@455 82 val usedHere = expUsed e
adamc@455 83 in
adamc@455 84 if IS.isEmpty (IS.difference (usedHere, used)) then
adamc@455 85 used
adamc@455 86 else
adamc@455 87 expand (IS.union (usedHere, used))
adamc@455 88 end)
adamc@455 89 used used
adamc@455 90
adamc@455 91 val used = IM.map (fn s => IS.intersection (expand s, thisGroup)) used
adamc@455 92
adamc@454 93 fun p_graph reachable =
adamc@454 94 IM.appi (fn (n, reachableHere) =>
adamc@454 95 (print (Int.toString n);
adamc@454 96 print ":";
adamc@454 97 IS.app (fn n' => (print " ";
adamc@454 98 print (Int.toString n'))) reachableHere;
adamc@454 99 print "\n")) reachable
adamc@454 100
adamc@454 101 (*val () = print "used:\n"
adamc@454 102 val () = p_graph used*)
adamc@454 103
adamc@454 104 fun expand reachable =
adamc@454 105 let
adamc@454 106 val changed = ref false
adamc@454 107
adamc@454 108 val reachable =
adamc@454 109 IM.mapi (fn (n, reachableHere) =>
adamc@454 110 IS.foldl (fn (n', reachableHere) =>
adamc@454 111 let
adamc@454 112 val more = valOf (IM.find (reachable, n'))
adamc@454 113 in
adamc@454 114 if IS.isEmpty (IS.difference (more, reachableHere)) then
adamc@454 115 reachableHere
adamc@454 116 else
adamc@454 117 (changed := true;
adamc@454 118 IS.union (more, reachableHere))
adamc@454 119 end)
adamc@454 120 reachableHere reachableHere) reachable
adamc@454 121 in
adamc@454 122 (reachable, !changed)
adamc@454 123 end
adamc@454 124
adamc@454 125 fun iterate reachable =
adamc@454 126 let
adamc@454 127 val (reachable, changed) = expand reachable
adamc@454 128 in
adamc@454 129 if changed then
adamc@454 130 iterate reachable
adamc@454 131 else
adamc@454 132 reachable
adamc@454 133 end
adamc@454 134
adamc@454 135 val reachable = iterate used
adamc@454 136
adamc@454 137 (*val () = print "reachable:\n"
adamc@454 138 val () = p_graph reachable*)
adamc@454 139
adamc@454 140 fun sccs (nodes, acc) =
adamc@454 141 case IS.find (fn _ => true) nodes of
adamc@454 142 NONE => acc
adamc@454 143 | SOME rep =>
adamc@454 144 let
adamc@454 145 val reachableHere = valOf (IM.find (reachable, rep))
adamc@454 146
adamc@454 147 val (nodes, scc) = IS.foldl (fn (node, (nodes, scc)) =>
adamc@454 148 if node = rep then
adamc@454 149 (nodes, scc)
adamc@454 150 else
adamc@454 151 let
adamc@454 152 val reachableThere =
adamc@454 153 valOf (IM.find (reachable, node))
adamc@454 154 in
adamc@454 155 if IS.member (reachableThere, rep) then
adamc@454 156 (IS.delete (nodes, node),
adamc@454 157 IS.add (scc, node))
adamc@454 158 else
adamc@454 159 (nodes, scc)
adamc@454 160 end)
adamc@454 161 (IS.delete (nodes, rep), IS.singleton rep) reachableHere
adamc@454 162 in
adamc@454 163 sccs (nodes, scc :: acc)
adamc@454 164 end
adamc@454 165
adamc@454 166 val sccs = sccs (thisGroup, [])
adamc@454 167 (*val () = app (fn nodes => (print "SCC:";
adamc@454 168 IS.app (fn i => (print " ";
adamc@454 169 print (Int.toString i))) nodes;
adamc@454 170 print "\n")) sccs*)
adamc@454 171
adamc@454 172 fun depends nodes1 nodes2 =
adamc@454 173 let
adamc@454 174 val node1 = valOf (IS.find (fn _ => true) nodes1)
adamc@454 175 val node2 = valOf (IS.find (fn _ => true) nodes2)
adamc@454 176 val reachable1 = valOf (IM.find (reachable, node1))
adamc@454 177 in
adamc@454 178 IS.member (reachable1, node2)
adamc@454 179 end
adamc@454 180
adamc@454 181 fun findReady (sccs, passed) =
adamc@454 182 case sccs of
adamc@454 183 [] => raise Fail "Untangle: Unable to topologically sort 'val rec'"
adamc@454 184 | nodes :: sccs =>
adamc@454 185 if List.exists (depends nodes) passed
adamc@454 186 orelse List.exists (depends nodes) sccs then
adamc@454 187 findReady (sccs, nodes :: passed)
adamc@454 188 else
adamc@454 189 (nodes, List.revAppend (passed, sccs))
adamc@454 190
adamc@454 191 fun topo (sccs, acc) =
adamc@454 192 case sccs of
adamc@454 193 [] => rev acc
adamc@454 194 | _ =>
adamc@454 195 let
adamc@454 196 val (node, sccs) = findReady (sccs, [])
adamc@454 197 in
adamc@454 198 topo (sccs, node :: acc)
adamc@454 199 end
adamc@454 200
adamc@454 201 val sccs = topo (sccs, [])
adamc@454 202 (*val () = app (fn nodes => (print "SCC':";
adamc@454 203 IS.app (fn i => (print " ";
adamc@454 204 print (Int.toString i))) nodes;
adamc@454 205 print "\n")) sccs*)
adamc@454 206
adamc@454 207 fun isNonrec nodes =
adamc@454 208 case IS.find (fn _ => true) nodes of
adamc@454 209 NONE => NONE
adamc@454 210 | SOME node =>
adamc@454 211 let
adamc@454 212 val nodes = IS.delete (nodes, node)
adamc@454 213 val reachableHere = valOf (IM.find (reachable, node))
adamc@454 214 in
adamc@454 215 if IS.isEmpty nodes then
adamc@454 216 if IS.member (reachableHere, node) then
adamc@454 217 NONE
adamc@454 218 else
adamc@454 219 SOME node
adamc@454 220 else
adamc@454 221 NONE
adamc@454 222 end
adamc@454 223
adamc@454 224 val ds = map (fn nodes =>
adamc@454 225 case isNonrec nodes of
adamc@454 226 SOME node =>
adamc@454 227 let
adamc@454 228 val vi = valOf (List.find (fn (_, n, _, _, _) => n = node) vis)
adamc@454 229 in
adamc@454 230 (DVal vi, loc)
adamc@454 231 end
adamc@454 232 | NONE =>
adamc@454 233 (DValRec (List.filter (fn (_, n, _, _, _) => IS.member (nodes, n)) vis), loc))
adamc@454 234 sccs
adamc@454 235 in
adamc@454 236 ds
adamc@454 237 end
adamc@454 238 | _ => [dAll]
adamc@454 239 in
adamc@454 240 ListUtil.mapConcat decl file
adamc@454 241 end
adamc@454 242
adamc@454 243 end