blob: 540486d65c9a19f54f416ebfd853e4b8ead0cd01 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
import System.Environment( getArgs )
import Text.Printf
import Library.Parse
import Library.ProofGraph
import Library.WriteProof
import Library.Semantic
import Library.Stack
import Data.Maybe
import Data.Graph.Inductive.Graph( Node, LNode, Edge, LEdge )
import qualified Data.Graph.Inductive.Graph as Graph
fst4 :: (a,b,c,d) -> a
fst4 (a,_,_,_) = a
toThms :: PGraph -> [Node] -> [String]
toThms graph nodeList =
let hyp = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 2) (Graph.out g n)
node = snd3 . head $ edge
in write g node)
con = (\g n -> let edge = filter (\x -> (fst . thd3 $ x) == 1) (Graph.out g n)
node = snd3 . head $ edge
in write g node)
f = (\x -> (show . fst $ x) ++ ". " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (hyp graph (snd x)))) `at` 0)) ++
" |- " ++ (show . fromJust $ ((fst4 . fromJust $ (eval (con graph (snd x)))) `at` 0)))
in map f (zip [1..] nodeList)
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)
theorems = toThms graph initList
output theorems
|
