diff options
Diffstat (limited to 'ListThm.hs')
-rw-r--r-- | ListThm.hs | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/ListThm.hs b/ListThm.hs deleted file mode 100644 index 540486d..0000000 --- a/ListThm.hs +++ /dev/null @@ -1,43 +0,0 @@ -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 |