diff options
| -rw-r--r-- | WriteProof.hs | 167 | ||||
| -rw-r--r-- | WriteProofMain.hs | 21 |
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 + |