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

1 files changed, 21 insertions, 0 deletions

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
+