Functions to linearise a graph into a proof trace (currently include removing unused portions and resolving single-output commands)

2 files changed, 188 insertions, 0 deletions

diff --git a/WriteProof.hs b/WriteProof.hs
new file mode 100644
index 0000000..db69aa1
--- /dev/null
+++ b/WriteProof.hs
@@ -0,0 +1,167 @@
+module WriteProof (
+    write,
+    writeAll,
+    doWriteProof,
+    singleCommands
+    ) where
+
+
+
+import Data.Maybe
+import Data.Graph.Inductive.Graph( LNode, LEdge, Node, Edge, (&) )
+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.List
+import Stack( Stack, at, (<:>) )
+import qualified Stack as Stack
+import Parse( isNumber )
+
+
+
+output :: Gr String (Int,Int) -> Node -> Int
+output graph node =
+    let label = fromJust (Graph.lab graph node)
+    in case label of
+           "defineConst" -> 2
+           "defineTypeOp" -> 5
+           x -> 1
+
+
+
+reuse :: Gr String (Int,Int) -> Node -> Int
+reuse graph node =
+    let labels = map snd (Graph.lpre graph node)
+        f = (\x y -> length (filter (\z -> fst y == fst z) x))
+        reuseList = map (f labels) labels
+    in maximum reuseList
+
+
+
+cost :: Gr String (Int,Int) -> Node -> Int
+cost graph node =
+    length (subGraph graph node)
+
+
+
+next :: Eq a => [a] -> a -> (a -> a) -> a
+next list start suc =
+    let f = (\x y -> if (x `elem` y) then f (suc x) y else x)
+    in f start list
+
+
+
+subGraph :: Gr a b -> Node -> [Node]
+subGraph graph node =
+    let sucList = nub (Graph.suc graph node)
+    in nub (node : (foldl' (++) [] (map (subGraph graph) sucList)))
+
+
+
+fst3 :: (a,b,c) -> a
+fst3 (a,_,_) = a
+
+snd3 :: (a,b,c) -> b
+snd3 (_,b,_) = b
+
+thd3 :: (a,b,c) -> c
+thd3 (_,_,c) = c
+
+
+
+orderNodes :: Gr String (Int,Int) -> [Node] -> [Node]
+orderNodes graph nodeList = nodeList
+--placeholder
+
+
+
+multiCommands :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+multiCommands graph nodeList = graph
+--placeholder
+
+
+
+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 = show . length . nub $ (filter (isNumber . snd) (Graph.labNodes 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
+
+                                         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)
+
+        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' f graph nodeList
+
+
+
+removeUnused :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+removeUnused graph nodeList =
+    let unused = filter (\x -> Graph.indeg graph x == 0 && x `notElem` nodeList) (Graph.nodes graph)
+    in if (unused == [])
+       then graph
+       else removeUnused (Graph.delNodes unused graph) nodeList
+
+
+
+resolve :: Gr String (Int,Int) -> [Node] -> Gr String (Int,Int)
+resolve graph nodeList =
+    foldl' (\g f -> f g nodeList) graph [removeUnused, singleCommands, multiCommands]
+
+
+
+getArg :: Gr String (Int,Int) -> Node -> Int -> Node
+getArg graph node arg =
+    snd3 . head $ (filter (\x -> (fst . thd3 $ x) == arg) (Graph.out graph node))
+
+
+
+writeGraph :: Gr String (Int,Int) -> 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
+
+
+
+write :: Gr String (Int,Int) -> Node -> [String]
+write graph node =
+    writeGraph (resolve graph [node]) node
+
+
+
+writeAll :: Gr String (Int,Int) -> [Node] -> [String]
+writeAll graph nodeList =
+    let ordered = orderNodes graph nodeList
+        graph' = resolve graph ordered
+        f = (\g n -> if (n == [])
+                     then []
+                     else (writeGraph g (head n)) ++ (f g (tail n)))
+    in f graph' ordered
+
+
+-- metric relates to minimum amount of work done not-on-top of the stack
+
+
+doWriteProof :: Gr String (Int,Int) -> [String]
+doWriteProof graph =
+    let initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph)
+    in writeAll graph initList
+
diff --git a/WriteProofMain.hs b/WriteProofMain.hs
new file mode 100644
index 0000000..745ad21
--- /dev/null
+++ b/WriteProofMain.hs
@@ -0,0 +1,21 @@
+import System( getArgs )
+import Text.Printf
+import Parse
+import ProofGraph
+import WriteProof
+
+
+output :: [String] -> IO ()
+output [] = return ()
+output list = do
+	putStrLn (head list)
+	output (tail list)
+
+
+main = do
+    args <- getArgs
+    list <- getLines $ head args
+    let graph = doGraphGen (map (stripReturn) list)
+        trace = doWriteProof graph
+    output trace
+