summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--WriteProof.hs167
-rw-r--r--WriteProofMain.hs21
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
+