020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett{- | Module : ./GMP/Main.hs

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder - Description : Implementation of main file for the prover

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett - License : GPLv2 or higher, see LICENSE.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - Maintainer : g.calin@jacobs-university.de

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett - Stability : provisional

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett - Portability : portable

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett - Provides the implementation of the user interaction "interface"

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett -}

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettmodule Main where

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport GenericSequent

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport ModalLogic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport CombLogic

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport Parser

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy Gimblettimport Text.ParserCombinators.Parsec

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettimport System.Environment

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblettimport System.IO

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport System.IO.Error

9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport Control.Exception (bracket, bracket_)

f909337bf7012aca169c0b56b89efbd4a310f8daAndy Gimblett

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett-- | Main parsing unit for checking provability/satisfiability

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettrun :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblettrun parser input =

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett case parse parser "" input of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Left err -> do putStr "parse error at "

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett print err

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett Right x -> do -- putStrLn (show x{-++" <=> "++input-})

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett let isP = provable x

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett putStrLn $ if isP then "... is Provable"

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett else if sat x then "... is not Provable but Satisfiable"

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett else "... is not Satisfiable"

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-- | Runs the main parsing unit (probably superfluous)

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettrunLex :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()

20ed727452613e36c0a95ddabf7ecc81cf941ed2Andy GimblettrunLex parser = run (do spaces

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett res <- parser

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett eof

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett return res)

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett-- | Auxiliary run function for testing with the input given as string

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettrunTest :: [Int] -> String -> IO ()

020cdb5dad6b871aba61136a0e1567c00426de87Andy GimblettrunTest logics input =

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett {- do case (head logics) of

020cdb5dad6b871aba61136a0e1567c00426de87Andy Gimblett 1 -> runLex (parseKindex{-(par5er Sqr parseKindex) :: Parser (L K)-}) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input

2f06b54890375b6cac90394b80b07bd451d728fcAndy Gimblett 7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett _ -> showHelp

ac5ec613b786cd05f495b568ab5214c31a333e67Andy Gimblett -}

a09bfcbcb0fba5663fca1968aa82daebf2e092c4Andy Gimblett return ()

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian Maeder-- | Map logic indexes from [Char] to Int

fcd11c35e645b0744a308f7961a519826bbaa2f5Christian MaederindexToInt :: String -> Int

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian MaederindexToInt c = case c of

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder "K" -> 1; "KD" -> 2

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian Maeder "C" -> 3; "G" -> 4

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "P" -> 5; "HM" -> 6

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "M" -> 7; _ -> error "Main.indexToInt"

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder-- | Function for displying user help

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian MaedershowHelp :: IO ()

a88d32442096d4fd88fce34842ca6f8cf34d8160Christian MaedershowHelp =

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder putStrLn ( "Usage:\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder " ./main -p <path> <N> <L1> <L2> .. <LN>\n" ++

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder " ./main -t <test> <N> <L1> <L2> .. <LN>\n\n" ++

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder "<N>: a natural number >0 specifing the number of " ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "combined/embedded logics\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "<Lx>: each logic can be one of the following cases:\n" ++

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder " K - K Modal Logic\n" ++

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder " KD - KD Modal Logic\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder " C - Coalition Logic\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder " G - Graded Modal Logic\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder " P - Probability Logic\n" ++

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder " HM - Hennessy-Milner Modal Logic\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder " M - Monotonic Logic\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "<path>: path to input file\n" ++

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder "<test>: test given as a string\n")

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maeder-- | Main program function

7bf56dc23f635a1f3cd09e89649a1e7897a77c68Christian Maedermain :: IO ()

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maedermain = do

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder args <- getArgs

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder if null args || head args == "--help" || length args < 4

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder then showHelp

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder else let it : test : n : [] = take 3 args

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder rest = tail . tail . tail $ args

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder in if length rest < read n

38504dc968167ba2e82dd568edeae8d6af4dc145Christian Maeder then showHelp

else let list = take (read n) rest

in case it of

"-p" -> do let logics = map indexToInt rest

test <- readFile test

putStrLn test -- run prover with given input

print logics

"-t" -> do let logics = map indexToInt rest

putStrLn test -- run prover with given input

print logics

_ -> showHelp