blob: 3b9a1c70bf8e05961104e4650a2fe0834d6cd77b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
import System.Environment( getArgs )
import Text.Printf
import Library.Parse
import Library.ProofGraph
import Library.WriteProof
import qualified Data.Graph.Inductive.Graph as Graph
main = do
args <- getArgs
list <- getLines (head args)
let graph = doGraphGen (map (stripReturn) list)
initList = filter (\x -> Graph.indeg graph x == 0) (Graph.nodes graph)
thmList = (map (\(_,y) -> y)) .
(filter (\(x,y) -> (show x) `notElem` (tail args))) .
(zip [1..]) $ initList
trace = writeAll graph thmList
output trace
|