From a489bbd5fb9f6a2a97243dd95b580080bb83272d Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Thu, 12 Jul 2012 09:10:59 +1000 Subject: Functions to linearise a graph into a proof trace (currently include removing unused portions and resolving single-output commands) --- WriteProofMain.hs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) create mode 100644 WriteProofMain.hs (limited to 'WriteProofMain.hs') 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 + -- cgit