Mercurial > urweb

annotate src/untangle.sml @ 1269:9f4b9315810d

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