blob: ad65911128d585cd91fbc9fe67589198866b8696 (
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( getArgs )
import Text.Printf
import Parse
import ProofGraph
import WriteProof
import Semantic
import 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
|