summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Library/Cost.hs29
-rw-r--r--Library/Usage.hs81
-rw-r--r--Library/WriteProof.hs214
3 files changed, 239 insertions, 85 deletions
diff --git a/Library/Cost.hs b/Library/Cost.hs
new file mode 100644
index 0000000..86cabdc
--- /dev/null
+++ b/Library/Cost.hs
@@ -0,0 +1,29 @@
+module Library.Cost(
+ cost,
+ nodeCost,
+ listCost
+ ) where
+
+
+
+import Data.Maybe
+import Data.Graph.Inductive.Graph( Node )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Library.ProofGraph
+
+
+
+cost :: String -> Int
+cost x = 1
+
+
+nodeCost :: PGraph -> Node -> Int
+nodeCost graph node =
+ let label = fromJust (Graph.lab graph node)
+ nextCostLayer = map (nodeCost graph) (Graph.suc graph node)
+ in (cost label) + (sum nextCostLayer)
+
+
+listCost :: [String] -> Int
+listCost = sum . (map cost)
+
diff --git a/Library/Usage.hs b/Library/Usage.hs
new file mode 100644
index 0000000..58fb0e0
--- /dev/null
+++ b/Library/Usage.hs
@@ -0,0 +1,81 @@
+module Library.Usage(
+ UsageMap,
+ usageMap,
+ useSort,
+ nodeOutput,
+ getArg
+ ) where
+
+
+
+import Data.Map( Map )
+import qualified Data.Map as Map
+import Data.Set( Set )
+import qualified Data.Set as Set
+import Data.List
+import Data.Maybe
+import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
+import qualified Data.Graph.Inductive.Graph as Graph
+import Library.Parse
+import Library.ProofGraph
+
+
+
+type UsageMap = Map Node (Map (LEdge (Int,Int)) (Int,[Int]))
+
+
+-- Takes a graph, a starting list of nodes, a set of nodes of interest, and
+-- follows the starting nodes up the graph to find which edges the starting nodes
+-- will encounter the nodes of interest through.
+usageMap :: PGraph -> [Node] -> Set Node -> UsageMap
+usageMap graph order interest =
+ let unionFunc = (\a b ->
+ Map.unionWith min a b)
+
+ addFunc = (\index prev umap edge ->
+ let node = snd3 edge
+ curIn = Graph.outdeg graph (fst3 edge)
+ prev' = (curIn - (fst . thd3 $ edge)):prev
+ toAdd = Map.singleton node (Map.singleton edge (index,prev'))
+ in if (Set.member node interest)
+ then Map.unionWith unionFunc toAdd umap
+ else umap)
+
+ f = (\umap (index,node,prev) ->
+ let edgeList = Graph.out graph node
+ sucMapList = map (f Map.empty) (map (\x -> (index, snd3 x, (length edgeList - (fst . thd3 $ x)):prev)) edgeList)
+ umap' = foldl' (addFunc index prev) umap edgeList
+ in Map.unionsWith unionFunc (umap':sucMapList))
+
+ in foldl' f Map.empty (zip3 [1..] order (repeat []))
+
+
+
+useSort :: (LEdge a, (Int,[Int])) -> (LEdge a, (Int,[Int])) -> Ordering
+useSort (_,(w,x)) (_,(y,z)) =
+ let check = compare w y
+ in if (check == EQ)
+ then compare (reverse x) (reverse z)
+ else check
+
+
+
+nodeOutput :: PGraph -> Node -> Int
+nodeOutput graph node =
+ let label = fromJust (Graph.lab graph node)
+ in case label of
+ "thm" -> 0
+ "pop" -> 0
+ "defineConst" -> 2
+ "defineTypeOp" -> 5
+ x -> 1
+
+
+
+getArg :: PGraph -> Node -> Int -> Maybe Node
+getArg graph node arg =
+ let edge = filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node)
+ in if (edge == [])
+ then Nothing
+ else Just (snd3 . head $ edge)
+
diff --git a/Library/WriteProof.hs b/Library/WriteProof.hs
index 0f4f80f..1057199 100644
--- a/Library/WriteProof.hs
+++ b/Library/WriteProof.hs
@@ -3,7 +3,9 @@ module Library.WriteProof (
writeAll,
doWriteProof,
singleCommands,
-
+ next,
+ genPart,
+ writeGraph
) where
@@ -14,26 +16,20 @@ import qualified Data.Graph.Inductive.Graph as Graph
import Data.Graph.Inductive.Tree
import Data.Map( Map, (!) )
import qualified Data.Map as Map
+import Data.Set( Set )
+import qualified Data.Set as Set
import Data.List
import Library.Stack( Stack, at, (<:>) )
import qualified Library.Stack as Stack
import Library.Parse( isNumber, fst3, snd3, thd3 )
+import Library.Cost
+import Library.ProofGraph
+import Library.GraphPart
+import Library.Usage
-output :: Gr String (Int,Int) -> Node -> Int
-output graph node =
- let label = fromJust (Graph.lab graph node)
- in case label of
- "thm" -> 0
- "pop" -> 0
- "defineConst" -> 2
- "defineTypeOp" -> 5
- x -> 1
-
-
-
-reuse :: Gr String (Int,Int) -> Node -> Int
+reuse :: PGraph -> Node -> Int
reuse graph node =
let labels = map snd (Graph.lpre graph node)
f = (\x y -> length (filter (\z -> fst y == fst z) x))
@@ -42,13 +38,7 @@ reuse graph node =
-cost :: Gr String (Int,Int) -> Node -> Int
-cost graph node =
- length (subGraph graph node)
-
-
-
-next :: Int -> Gr String (Int,Int) -> [String]
+next :: Int -> PGraph -> [String]
next num graph =
let nodeList = filter (isNumber . snd) (Graph.labNodes graph)
numList = nub . (map (read . snd)) $ nodeList
@@ -65,13 +55,13 @@ subGraph graph node =
-orderNodes :: Gr String (Int,Int) -> [Node] -> [Node]
+orderNodes :: PGraph -> [Node] -> [Node]
orderNodes graph nodeList = nodeList
--placeholder
-removeOverlap :: Gr String (Int,Int) -> Node -> [Node] -> [Node]
+removeOverlap :: PGraph -> Node -> [Node] -> [Node]
removeOverlap graph node list =
let nubFunc = (\x y -> (getArg graph node x) == (getArg graph node y))
in nubBy nubFunc list
@@ -88,35 +78,64 @@ removeOverlap graph node list =
---multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
---multiCommands graph nodeList =
--- let trace = (\g n cn ca ->)
+--trace :: Gr String (Int,Int) -> Node -> [Node] -> Maybe (Int,Node,Int)
+--trace graph node history =
+-- let tr = (\g n curnode curarg hist ->
+-- if (curarg > output g n)
+-- then Nothing
+-- else let argToFollow = if (n == curnode) then curarg else 1
+-- outputsFromArg = filter (\(x,y) -> snd y == argToFollow) (Graph.lpre g curnode)
+--
+-- in case outputFromCurArg of
+-- 0 ->
+-- if (filter (\(x,y) -> snd y == curarg) (Graph.lpre g n) > 1)
+-- if (curarg > output g n)
+-- then Nothing
+-- else if (n == curnode)
+-- then let curnode' = filter (\(x,y) -> ) (Graph.lpre g n)
+-- in tr g n curnode' curarg
+-- else )
--
--- r = (\g n p -> let g' = if ((output g n) <= 1)
--- then g
--- else let (argToUseDict, (place, placeArg)) = trace g n n 1
--- edgesToRemove =
--- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove
--- defSubGraph =
--- edgesToRef =
--- new =
--- refsToAdd =
--- done = foldl' insertSubGraph edgesRemoved refsToAdd
--- in done
--- in f g' n)
+-- f = (\g n curarg h ->
+-- if (curarg > output g n)
+-- then Nothing
+-- else let hist = if
+-- place = tr g n n hist
+-- in if (isJust place)
+-- then place
+-- else f g n (curarg+1) hist
+--
+-- in f graph node 1 history
+
+-- higher numbers -> deeper in the stack
+
+--multiCommands :: Gr String (Int,Int) -> [Node] -> (Gr String (Int,Int), [Node])
+--multiCommands graph nodeList =
+-- let f = (\g n p ->
+-- if ((output g n) <= 1)
+-- then g
+-- else let changed = do (argToUseDict, place, placeArg) <- trace g n
+-- let edgesToRemove =
+-- edgesRemoved = foldl' (\x y -> Graph.delLEdge y x) g edgesToRemove
+-- defSubGraph =
+-- edgesToRef =
+-- new =
+-- refsToAdd =
+-- return (foldl' insertSubGraph edgesRemoved refsToAdd)
+-- in if (isNothing changed) then g else fromJust changed
--
--- f = (\g n -> let argList = (removeOverlap g) . reverse $ [1 .. (Graph.outdeg g n)]
--- in foldl' (\x y -> r x (getArg x n y) n) g argList)
+-- multiOutputNodes = filter (\x -> output graph x > 1) (Graph.nodes graph)
+-- bestCase = foldl' f graph multiOutputNodes
--
--- in foldl' f graph nodeList
+-- in
-multiCommandsSimple :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+multiCommandsSimple :: PGraph -> [Node] -> PGraph
multiCommandsSimple graph nodeList =
- let r = (\g n p -> let g' = if ((output g n) <= 1)
+ let r = (\g n p -> let g' = if ((nodeOutput g n) <= 1)
then g
- else let ou = output g n
+ else let ou = nodeOutput g n
index = next ou g
new = Graph.newNodes (5 * ou + 2) g -- 3 for num/def/pop, 2 for num/ref, per output plus an extra num/ref
(defNew,refNew) = splitAt (3 * ou + 2) new
@@ -150,43 +169,68 @@ multiCommandsSimple graph nodeList =
in f g' n)
f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)]
- in foldl' (\x y -> r x (getArg x n y) n) g argList)
+ in foldl' (\x y -> r x (fromJust (getArg x n y)) n) g argList)
in foldl' f graph nodeList
-singleCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
-singleCommands graph nodeList =
- let r = (\g n p -> let g' = if (((output g n) /= 1) || ((Graph.indeg g n) == 1) || ((cost g n) < 3) || ((cost g n) == 3 && (Graph.indeg g n) < 3))
- then g
- else let index = head (next 1 g)
- new = Graph.newNodes 4 g -- 2 new nodes for def and 2 new nodes for ref
-
- oldEdge = head $ (filter (\x -> fst3 x == p) (Graph.inn g n))
- defNodes = [(new!!0, "def"), (new!!1, index)]
- defEdges = [(p, fst (defNodes!!0), (fst . thd3 $ oldEdge, 1)),
- (fst (defNodes!!0), fst (defNodes!!1), (1,1)),
- (fst (defNodes!!1), n, (1,1))]
- defAdded = (Graph.insEdges defEdges) . (Graph.insNodes defNodes) . (Graph.delLEdge oldEdge) $ g
+singleCommands :: PGraph -> UsageMap -> [Node] -> PGraph
+singleCommands graph usemap nodeList =
+ let singleNodes = filter (\x -> nodeOutput graph x == 1 && Graph.indeg graph x > 1) (Graph.nodes graph)
+ umap = Map.filterWithKey (\n _ -> n `elem` singleNodes) usemap
- refNodes = [(new!!2, "ref"), (new!!3, index)]
- refEdge = (fst (refNodes!!0), fst (refNodes!!1), (1,1))
- refAdded = (Graph.insEdge refEdge) . (Graph.insNodes refNodes) $ defAdded
- convertEdge = (\g e -> let new = (fst3 e, fst (refNodes!!0), thd3 e)
- in (Graph.insEdge new) . (Graph.delLEdge e) $ g)
- done = foldl' convertEdge refAdded (filter (\x -> fst3 x /= fst (defNodes!!1)) (Graph.inn refAdded n))
- in done
- in f g' n)
+ s = (\graph node edgemap ->
+ let index = head (next 1 graph)
+ edgeList = Map.toList edgemap
- f = (\g n -> let argList = reverse $ [1 .. (Graph.outdeg g n)]
- in foldl' (\x y -> r x (getArg x n y) n) g argList)
+ defEdge = fst (minimumBy useSort edgeList)
+ removeEdge = fst (maximumBy useSort edgeList)
+ refEdgeList = filter (\x -> x /= defEdge && x /= removeEdge) (map fst edgeList)
- in foldl' f graph nodeList
+ defPart = genPart [index, "def"] True
+ refPart = genPart [index, "ref"] False
+ removePart = genPart [index, "remove"] False
+
+ defNode = (fst3 defEdge, fst . thd3 $ defEdge)
+ removeNode = (fst3 removeEdge, fst . thd3 $ removeEdge)
+ refNodeList = map (\x -> (fst3 x, fst . thd3 $ x)) refEdgeList
+
+ partList = [(defPart, Just (node, 1), [defNode]), (removePart, Nothing, [removeNode])]
+ partList' = if (refNodeList == []) then partList else (refPart, Nothing, refNodeList):partList
+
+ edgesRemoved = foldl' (\x (y,z) -> Graph.delLEdge y x) graph edgeList
+ partsAdded = graphAddList partList' edgesRemoved
+ in partsAdded)
+ f = (\gr node edgemap ->
+ let reuse = Graph.indeg graph node
+ costToStore = (nodeCost graph node) + (listCost ["def","0"]) + (reuse - 1) * (listCost ["ref","0"])
+ costToIgnore = reuse * (nodeCost graph node)
+ in if (costToStore >= costToIgnore)
+ then gr
+ else s gr node edgemap)
+ in foldl' (\g n -> f g n (fromJust (Map.lookup n umap))) graph singleNodes
-removeUnused :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+
+
+genPart :: [String] -> Bool -> GraphPart
+genPart labels hasInput =
+ let nodeList = zip [1..] labels
+ edgeFunc = (\edges nodes ->
+ if (nodes == [] || (tail nodes) == [])
+ then edges
+ else let newEdge = (fst (nodes!!1), fst (nodes!!0), (1,1))
+ in edgeFunc (newEdge:edges) (tail nodes))
+ edgeList = edgeFunc [] nodeList
+ input = if (hasInput) then Just (1,1) else Nothing
+ output = Just (length labels, 1)
+ in graphPart nodeList edgeList input output
+
+
+
+removeUnused :: PGraph -> [Node] -> PGraph
removeUnused graph nodeList =
let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph)
in if (unused == [])
@@ -195,46 +239,46 @@ removeUnused graph nodeList =
-resolve :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+resolve :: PGraph -> [Node] -> PGraph
resolve graph nodeList =
- foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommandsSimple]
-
-
-
-getArg :: Gr String (Int,Int) -> Node -> Int -> Node
-getArg graph node arg =
- snd3 . head $ (filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node))
+ let liveGraph = removeUnused graph nodeList
+ umap = usageMap graph nodeList (Set.fromList (Graph.nodes liveGraph))
+ in foldl' (\g f -> f g umap nodeList) liveGraph [singleCommands]
-writeGraph :: Gr String (Int,Int) -> Node -> [String]
+writeGraph :: PGraph -> Node -> [String]
writeGraph graph node =
let label = fromJust (Graph.lab graph node)
argList = [1 .. (Graph.outdeg graph node)]
- in foldl' (\s a -> (writeGraph graph (getArg graph node a)) ++ s) [label] argList
+ f = (\s a -> let arg = getArg graph node a
+ in if (isNothing arg)
+ then s
+ else (writeGraph graph (fromJust arg)) ++ s)
+ in foldl' f [label] argList
-write :: Gr String (Int,Int) -> Node -> [String]
+write :: PGraph -> Node -> [String]
write graph node =
writeGraph (resolve graph [node]) node
-writeAll :: Gr String (Int,Int) -> [Node] -> [String]
+writeAll :: PGraph -> [Node] -> [String]
writeAll graph nodeList =
let ordered = orderNodes graph nodeList
- graph' = resolve graph ordered
+ resolved = resolve graph ordered
f = (\g n -> if (n == [])
then []
else (writeGraph g (head n)) ++ (f g (tail n)))
- in f graph' ordered
+ in f resolved ordered
-- metric relates to minimum amount of work done not-on-top of the stack
-doWriteProof :: Gr String (Int,Int) -> [String]
+doWriteProof :: PGraph -> [String]
doWriteProof graph =
let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph)
in writeAll graph initList