# HG changeset patch # User Adam Chlipala # Date 1225589083 14400 # Node ID 9163f8014f9b7d38cbf6b253b5ca0ecbe983855b # Parent 787d4931fb070cee9c1f1b6f2fe59ac781592b70 Nested save compiles diff -r 787d4931fb07 -r 9163f8014f9b src/compiler.sig --- a/src/compiler.sig Sat Nov 01 21:19:43 2008 -0400 +++ b/src/compiler.sig Sat Nov 01 21:24:43 2008 -0400 @@ -63,6 +63,7 @@ val explify : (Elab.file, Expl.file) phase val corify : (Expl.file, Core.file) phase val especialize : (Core.file, Core.file) phase + val core_untangle : (Core.file, Core.file) phase val shake : (Core.file, Core.file) phase val tag : (Core.file, Core.file) phase val reduce : (Core.file, Core.file) phase @@ -86,6 +87,7 @@ val toExplify : (string, Expl.file) transform val toCorify : (string, Core.file) transform val toEspecialize : (string, Core.file) transform + val toCore_untangle : (string, Core.file) transform val toShake1 : (string, Core.file) transform val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform diff -r 787d4931fb07 -r 9163f8014f9b src/compiler.sml --- a/src/compiler.sml Sat Nov 01 21:19:43 2008 -0400 +++ b/src/compiler.sml Sat Nov 01 21:24:43 2008 -0400 @@ -418,12 +418,19 @@ val toEspecialize = transform especialize "especialize" o toCorify +val core_untangle = { + func = CoreUntangle.untangle, + print = CorePrint.p_file CoreEnv.empty +} + +val toCore_untangle = transform core_untangle "core_untangle" o toEspecialize + val shake = { func = Shake.shake, print = CorePrint.p_file CoreEnv.empty } -val toShake1 = transform shake "shake1" o toEspecialize +val toShake1 = transform shake "shake1" o toCore_untangle val tag = { func = Tag.tag, diff -r 787d4931fb07 -r 9163f8014f9b src/core_untangle.sig --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/core_untangle.sig Sat Nov 01 21:24:43 2008 -0400 @@ -0,0 +1,32 @@ +(* Copyright (c) 2008, 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 CORE_UNTANGLE = sig + + val untangle : Core.file -> Core.file + +end diff -r 787d4931fb07 -r 9163f8014f9b src/core_untangle.sml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/core_untangle.sml Sat Nov 01 21:24:43 2008 -0400 @@ -0,0 +1,215 @@ +(* Copyright (c) 2008, 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 CoreUntangle :> CORE_UNTANGLE = struct + +open Core + +structure U = CoreUtil +structure E = CoreEnv + +structure IS = IntBinarySet +structure IM = IntBinaryMap + +fun default (k, s) = s + +fun exp (e, s) = + case e of + ENamed n => IS.add (s, n) + + | _ => s + +fun untangle file = + let + fun decl (dAll as (d, loc)) = + case d of + DValRec vis => + let + val thisGroup = foldl (fn ((_, n, _, _, _), thisGroup) => + IS.add (thisGroup, n)) IS.empty vis + + val used = foldl (fn ((_, n, _, e, _), used) => + let + val usedHere = U.Exp.fold {con = default, + kind = default, + exp = exp} IS.empty e + in + IM.insert (used, n, IS.intersection (usedHere, thisGroup)) + end) + IM.empty vis + + fun p_graph reachable = + IM.appi (fn (n, reachableHere) => + (print (Int.toString n); + print ":"; + IS.app (fn n' => (print " "; + print (Int.toString n'))) reachableHere; + print "\n")) reachable + + (*val () = print "used:\n" + val () = p_graph used*) + + fun expand reachable = + let + val changed = ref false + + val reachable = + IM.mapi (fn (n, reachableHere) => + IS.foldl (fn (n', reachableHere) => + let + val more = valOf (IM.find (reachable, n')) + in + if IS.isEmpty (IS.difference (more, reachableHere)) then + reachableHere + else + (changed := true; + IS.union (more, reachableHere)) + end) + reachableHere reachableHere) reachable + in + (reachable, !changed) + end + + fun iterate reachable = + let + val (reachable, changed) = expand reachable + in + if changed then + iterate reachable + else + reachable + end + + val reachable = iterate used + + (*val () = print "reachable:\n" + val () = p_graph reachable*) + + fun sccs (nodes, acc) = + case IS.find (fn _ => true) nodes of + NONE => acc + | SOME rep => + let + val reachableHere = valOf (IM.find (reachable, rep)) + + val (nodes, scc) = IS.foldl (fn (node, (nodes, scc)) => + if node = rep then + (nodes, scc) + else + let + val reachableThere = + valOf (IM.find (reachable, node)) + in + if IS.member (reachableThere, rep) then + (IS.delete (nodes, node), + IS.add (scc, node)) + else + (nodes, scc) + end) + (IS.delete (nodes, rep), IS.singleton rep) reachableHere + in + sccs (nodes, scc :: acc) + end + + val sccs = sccs (thisGroup, []) + (*val () = app (fn nodes => (print "SCC:"; + IS.app (fn i => (print " "; + print (Int.toString i))) nodes; + print "\n")) sccs*) + + fun depends nodes1 nodes2 = + let + val node1 = valOf (IS.find (fn _ => true) nodes1) + val node2 = valOf (IS.find (fn _ => true) nodes2) + val reachable1 = valOf (IM.find (reachable, node1)) + in + IS.member (reachable1, node2) + end + + fun findReady (sccs, passed) = + case sccs of + [] => raise Fail "Untangle: Unable to topologically sort 'val rec'" + | nodes :: sccs => + if List.exists (depends nodes) passed + orelse List.exists (depends nodes) sccs then + findReady (sccs, nodes :: passed) + else + (nodes, List.revAppend (passed, sccs)) + + fun topo (sccs, acc) = + case sccs of + [] => rev acc + | _ => + let + val (node, sccs) = findReady (sccs, []) + in + topo (sccs, node :: acc) + end + + val sccs = topo (sccs, []) + (*val () = app (fn nodes => (print "SCC':"; + IS.app (fn i => (print " "; + print (Int.toString i))) nodes; + print "\n")) sccs*) + + fun isNonrec nodes = + case IS.find (fn _ => true) nodes of + NONE => NONE + | SOME node => + let + val nodes = IS.delete (nodes, node) + val reachableHere = valOf (IM.find (reachable, node)) + in + if IS.isEmpty nodes then + if IS.member (reachableHere, node) then + NONE + else + SOME node + else + NONE + end + + val ds = map (fn nodes => + case isNonrec nodes of + SOME node => + let + val vi = valOf (List.find (fn (_, n, _, _, _) => n = node) vis) + in + (DVal vi, loc) + end + | NONE => + (DValRec (List.filter (fn (_, n, _, _, _) => IS.member (nodes, n)) vis), loc)) + sccs + in + ds + end + | _ => [dAll] + in + ListUtil.mapConcat decl file + end + +end diff -r 787d4931fb07 -r 9163f8014f9b src/sources --- a/src/sources Sat Nov 01 21:19:43 2008 -0400 +++ b/src/sources Sat Nov 01 21:24:43 2008 -0400 @@ -99,6 +99,9 @@ especialize.sig especialize.sml +core_untangle.sig +core_untangle.sml + tag.sig tag.sml