Mercurial > urweb

annotate src/core_untangle.sml @ 714:0f42461273cf

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
CHECK constraints
author Adam Chlipala <adamc@hcoop.net>
date Thu, 09 Apr 2009 15:30:15 -0400
parents 23a88d81a1b5
children ef6de4075dc1
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@519 40 fun exp thisGroup (e, s) =
adamc@454 41 case e of
adamc@519 42 ENamed n =>
adamc@519 43 if IS.member (thisGroup, n) then
adamc@519 44 IS.add (s, n)
adamc@519 45 else
adamc@519 46 s
adamc@454 47
adamc@454 48 | _ => s
adamc@454 49
adamc@454 50 fun untangle file =
adamc@454 51 let
adamc@519 52 fun expUsed thisGroup = U.Exp.fold {con = default,
adamc@519 53 kind = default,
adamc@519 54 exp = exp thisGroup} IS.empty
adamc@455 55
adamc@454 56 fun decl (dAll as (d, loc)) =
adamc@454 57 case d of
adamc@454 58 DValRec vis =>
adamc@454 59 let
adamc@454 60 val thisGroup = foldl (fn ((_, n, _, _, _), thisGroup) =>
adamc@454 61 IS.add (thisGroup, n)) IS.empty vis
adamc@454 62
adamc@519 63 val edefs = foldl (fn ((_, n, _, e, _), edefs) =>
adamc@519 64 IM.insert (edefs, n, expUsed thisGroup e))
adamc@519 65 IM.empty vis
adamc@455 66
adamc@519 67 val used = edefs
adamc@454 68
adamc@455 69 fun expand used =
adamc@455 70 IS.foldl (fn (n, used) =>
adamc@455 71 case IM.find (edefs, n) of
adamc@455 72 NONE => used
adamc@519 73 | SOME usedHere =>
adamc@519 74 if IS.isEmpty (IS.difference (usedHere, used)) then
adamc@519 75 used
adamc@519 76 else
adamc@519 77 expand (IS.union (usedHere, used)))
adamc@455 78 used used
adamc@455 79
adamc@454 80 fun p_graph reachable =
adamc@454 81 IM.appi (fn (n, reachableHere) =>
adamc@454 82 (print (Int.toString n);
adamc@454 83 print ":";
adamc@454 84 IS.app (fn n' => (print " ";
adamc@454 85 print (Int.toString n'))) reachableHere;
adamc@454 86 print "\n")) reachable
adamc@454 87
adamc@454 88 (*val () = print "used:\n"
adamc@454 89 val () = p_graph used*)
adamc@454 90
adamc@454 91 fun expand reachable =
adamc@454 92 let
adamc@454 93 val changed = ref false
adamc@454 94
adamc@454 95 val reachable =
adamc@454 96 IM.mapi (fn (n, reachableHere) =>
adamc@454 97 IS.foldl (fn (n', reachableHere) =>
adamc@454 98 let
adamc@454 99 val more = valOf (IM.find (reachable, n'))
adamc@454 100 in
adamc@454 101 if IS.isEmpty (IS.difference (more, reachableHere)) then
adamc@454 102 reachableHere
adamc@454 103 else
adamc@454 104 (changed := true;
adamc@454 105 IS.union (more, reachableHere))
adamc@454 106 end)
adamc@454 107 reachableHere reachableHere) reachable
adamc@454 108 in
adamc@454 109 (reachable, !changed)
adamc@454 110 end
adamc@454 111
adamc@454 112 fun iterate reachable =
adamc@454 113 let
adamc@454 114 val (reachable, changed) = expand reachable
adamc@454 115 in
adamc@454 116 if changed then
adamc@454 117 iterate reachable
adamc@454 118 else
adamc@454 119 reachable
adamc@454 120 end
adamc@454 121
adamc@454 122 val reachable = iterate used
adamc@454 123
adamc@454 124 (*val () = print "reachable:\n"
adamc@454 125 val () = p_graph reachable*)
adamc@454 126
adamc@454 127 fun sccs (nodes, acc) =
adamc@454 128 case IS.find (fn _ => true) nodes of
adamc@454 129 NONE => acc
adamc@454 130 | SOME rep =>
adamc@454 131 let
adamc@454 132 val reachableHere = valOf (IM.find (reachable, rep))
adamc@454 133
adamc@454 134 val (nodes, scc) = IS.foldl (fn (node, (nodes, scc)) =>
adamc@454 135 if node = rep then
adamc@454 136 (nodes, scc)
adamc@454 137 else
adamc@454 138 let
adamc@454 139 val reachableThere =
adamc@454 140 valOf (IM.find (reachable, node))
adamc@454 141 in
adamc@454 142 if IS.member (reachableThere, rep) then
adamc@454 143 (IS.delete (nodes, node),
adamc@454 144 IS.add (scc, node))
adamc@454 145 else
adamc@454 146 (nodes, scc)
adamc@454 147 end)
adamc@454 148 (IS.delete (nodes, rep), IS.singleton rep) reachableHere
adamc@454 149 in
adamc@454 150 sccs (nodes, scc :: acc)
adamc@454 151 end
adamc@454 152
adamc@454 153 val sccs = sccs (thisGroup, [])
adamc@519 154
adamc@454 155 (*val () = app (fn nodes => (print "SCC:";
adamc@454 156 IS.app (fn i => (print " ";
adamc@454 157 print (Int.toString i))) nodes;
adamc@454 158 print "\n")) sccs*)
adamc@454 159
adamc@454 160 fun depends nodes1 nodes2 =
adamc@454 161 let
adamc@454 162 val node1 = valOf (IS.find (fn _ => true) nodes1)
adamc@454 163 val node2 = valOf (IS.find (fn _ => true) nodes2)
adamc@454 164 val reachable1 = valOf (IM.find (reachable, node1))
adamc@454 165 in
adamc@454 166 IS.member (reachable1, node2)
adamc@454 167 end
adamc@454 168
adamc@454 169 fun findReady (sccs, passed) =
adamc@454 170 case sccs of
adamc@454 171 [] => raise Fail "Untangle: Unable to topologically sort 'val rec'"
adamc@454 172 | nodes :: sccs =>
adamc@454 173 if List.exists (depends nodes) passed
adamc@454 174 orelse List.exists (depends nodes) sccs then
adamc@454 175 findReady (sccs, nodes :: passed)
adamc@454 176 else
adamc@454 177 (nodes, List.revAppend (passed, sccs))
adamc@454 178
adamc@454 179 fun topo (sccs, acc) =
adamc@454 180 case sccs of
adamc@454 181 [] => rev acc
adamc@454 182 | _ =>
adamc@454 183 let
adamc@454 184 val (node, sccs) = findReady (sccs, [])
adamc@454 185 in
adamc@454 186 topo (sccs, node :: acc)
adamc@454 187 end
adamc@454 188
adamc@454 189 val sccs = topo (sccs, [])
adamc@519 190
adamc@454 191 (*val () = app (fn nodes => (print "SCC':";
adamc@454 192 IS.app (fn i => (print " ";
adamc@454 193 print (Int.toString i))) nodes;
adamc@454 194 print "\n")) sccs*)
adamc@454 195
adamc@454 196 fun isNonrec nodes =
adamc@454 197 case IS.find (fn _ => true) nodes of
adamc@454 198 NONE => NONE
adamc@454 199 | SOME node =>
adamc@454 200 let
adamc@454 201 val nodes = IS.delete (nodes, node)
adamc@454 202 val reachableHere = valOf (IM.find (reachable, node))
adamc@454 203 in
adamc@454 204 if IS.isEmpty nodes then
adamc@454 205 if IS.member (reachableHere, node) then
adamc@454 206 NONE
adamc@454 207 else
adamc@454 208 SOME node
adamc@454 209 else
adamc@454 210 NONE
adamc@454 211 end
adamc@454 212
adamc@454 213 val ds = map (fn nodes =>
adamc@454 214 case isNonrec nodes of
adamc@454 215 SOME node =>
adamc@454 216 let
adamc@454 217 val vi = valOf (List.find (fn (_, n, _, _, _) => n = node) vis)
adamc@454 218 in
adamc@454 219 (DVal vi, loc)
adamc@454 220 end
adamc@454 221 | NONE =>
adamc@454 222 (DValRec (List.filter (fn (_, n, _, _, _) => IS.member (nodes, n)) vis), loc))
adamc@454 223 sccs
adamc@454 224 in
adamc@454 225 ds
adamc@454 226 end
adamc@454 227 | _ => [dAll]
adamc@454 228 in
adamc@454 229 ListUtil.mapConcat decl file
adamc@454 230 end
adamc@454 231
adamc@454 232 end