diff options
| author | Jed Barber <jjbarber@y7mail.com> | 2014-04-08 15:06:40 +1000 |
|---|---|---|
| committer | Jed Barber <jjbarber@y7mail.com> | 2014-04-08 15:06:40 +1000 |
| commit | 03d38eb3190eb5e51fb18847fe0792013285bde5 (patch) | |
| tree | 1060d26d3042b5c0c5b1c027fac45fe87f3d685a /ListThm.hs | |
| parent | f2c4e4614613ede497f19ef79dc7dc157eaca834 (diff) | |
Reorganising source code
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 |