Main.hs revision 9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7
967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- | Module : $Header$
967e5f3c25249c779575864692935627004d3f9eChristian Maeder - Description : Implementation of main file for the prover
81d182b21020b815887e9057959228546cf61b6bChristian Maeder - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder - Maintainer : g.calin@jacobs-university.de
967e5f3c25249c779575864692935627004d3f9eChristian Maeder - Stability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder - Portability : portable
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder - Provides the implementation of the user interaction "interface"
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedermodule Main where
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport GenericSequent
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport ModalLogic
967e5f3c25249c779575864692935627004d3f9eChristian Maederimport CombLogic
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder-- | Main parsing unit for checking provability/satisfiability
8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederrun :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederrun parser input =
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder case (parse parser "" input) of
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder Left err -> do putStr "parse error at "
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Right x -> do --putStrLn (show x{-++" <=> "++input-})
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder let isP = provable x
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder True -> putStrLn "... is Provable"
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder _ -> let isS = sat x
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in case isS of
967e5f3c25249c779575864692935627004d3f9eChristian Maeder True -> putStrLn ("... is not Provable" ++
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder " but Satisfiable")
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder _ -> putStrLn "... is not Satisfiable"
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder-- | Runs the main parsing unit (probably superfluous)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederrunLex :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederrunLex parser input = run (do spaces
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder res <- parser
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder-- | Auxiliary run function for testing with the input given as string
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian MaederrunTest :: [Int] -> String -> IO ()
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian MaederrunTest logics input =
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder do {-case (head logics) of
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder 1 -> runLex (parseKindex{-(par5er Sqr parseKindex) :: Parser (L K)-}) input
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder 2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder 3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder 4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder 5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder 6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder 7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder _ -> showHelp
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder-- | Map logic indexes from [Char] to Int
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederindexToInt :: [Char] -> Int
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederindexToInt c = case c of
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder "K" -> 1; "KD" -> 2
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder "C" -> 3; "G" -> 4
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder "P" -> 5; "HM" -> 6
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder "M" -> 7; _ -> error "Main.indexToInt"
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder-- | Function for displying user help
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian MaedershowHelp :: IO()
67086e0fe40a985c5e8a3cf50e611f43234580c2Christian Maeder putStrLn ( "Usage:\n" ++
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder " ./main -p <path> <N> <L1> <L2> .. <LN>\n" ++
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder " ./main -t <test> <N> <L1> <L2> .. <LN>\n\n" ++
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder "<N>: a natural number >0 specifing the number of " ++
d48085f765fca838c1d972d2123601997174583dChristian Maeder "<Lx>: each logic can be one of the following cases:\n" ++
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder " K - K Modal Logic\n" ++
d48085f765fca838c1d972d2123601997174583dChristian Maeder " KD - KD Modal Logic\n" ++
d48085f765fca838c1d972d2123601997174583dChristian Maeder " C - Coalition Logic\n" ++
588c0c022a0f4e129a89c3bc569daf6a835e182dChristian Maeder " G - Graded Modal Logic\n" ++
d48085f765fca838c1d972d2123601997174583dChristian Maeder " P - Probability Logic\n" ++
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder " HM - Hennessy-Milner Modal Logic\n" ++
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder " M - Monotonic Logic\n" ++
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder "<path>: path to input file\n" ++
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder "<test>: test given as a string\n")
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder-- | Main program function
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder args <- getArgs
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder if (args == [])||(head args == "--help")||(length args < 4)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder then showHelp
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder else let it:test:n:[] = take 3 args
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder in if (length rest < read n)
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder then showHelp
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder else let list = take (read n) rest
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder in case it of
b66eb6038bfbcd2fe520d87c151bb4f1f510e985Christian Maeder "-p" -> do let logics = map indexToInt rest
f11f713bebd8e1e623a0a4361065df256033de47Christian Maeder test <- readFile test
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder putStrLn test -- run prover with given input
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder putStrLn $ show logics
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder "-t" -> do let logics = map indexToInt rest
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder putStrLn test -- run prover with given input
967e5f3c25249c779575864692935627004d3f9eChristian Maeder putStrLn $ show logics
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder _ -> showHelp