summaryrefslogtreecommitdiff
path: root/Delete.hs
blob: adeb5a5d9ce039468a41aca5e552232ab3fdef31 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
import System( getArgs )
import Text.Printf
import Parse
import ProofGraph
import 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