e83ed59502a681713982f25c559aae77a4145734Christian Maeder{- | Module : $Header$

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder - Description : Implemenation of main file for the prover

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

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

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder - Stability : provisional

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder - Portability : portable

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder -

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder - Provides the implementation of the user interaction "interface"

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder -}

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskimodule Main where

eb483f2216949400bfef8f6deb5320f071445626Christian Maeder

585094c4284ed39eb8024cc1178c823c403200faChristian Maederimport Text.ParserCombinators.Parsec

eb483f2216949400bfef8f6deb5320f071445626Christian Maederimport System.Environment

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport IO

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport GMP.Parser

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederimport GMP.Generic

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | Runs the parser and the prover and prints the result(s) of obtained.

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrunLex :: (Logic a, Eq a, Show a) => Parser (L a) -> String -> IO ()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrunLex p_rL input = run (do spaces

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder x <- p_rL

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder eof

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder return x

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder ) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder

e83ed59502a681713982f25c559aae77a4145734Christian Maederrun :: (Logic a, Eq a, Show a) => Parser (L a) -> String -> IO ()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederrun p_r input = case (parse p_r "" input) of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Left err -> do putStr "parse error at "

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder print err

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder Right x -> do putStrLn ({-show x++" <=> "-}++input)

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder let isS = sat x

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder case isS of

e83ed59502a681713982f25c559aae77a4145734Christian Maeder True -> putStrLn "... is Satisfiable"

e83ed59502a681713982f25c559aae77a4145734Christian Maeder _ -> putStrLn "... is Not Satisfiable"

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder let isP = provable x

e83ed59502a681713982f25c559aae77a4145734Christian Maeder case isP of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder True -> putStrLn "... is Provable"

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> putStrLn "... is Not Provable"

e83ed59502a681713982f25c559aae77a4145734Christian Maeder

e83ed59502a681713982f25c559aae77a4145734Christian Maeder-- | Auxiliary run function for testing

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrunTest :: Int -> FilePath -> IO ()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian MaederrunTest ml path = do

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder input <- readFile path

e83ed59502a681713982f25c559aae77a4145734Christian Maeder case ml of

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 1 -> runLex ((par5er Sqr parseKindex) :: Parser (L K)) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input

e83ed59502a681713982f25c559aae77a4145734Christian Maeder 3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input

e83ed59502a681713982f25c559aae77a4145734Christian Maeder 5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder 7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder _ -> help

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder return ()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | Function for displying user help

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederhelp :: IO()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maederhelp = do

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder putStrLn ( "Usage:\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " ./main <ML> <path>\n\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder "<ML>: 1 for K Modal Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 2 for KD Modal Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 3 for Coalition Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 4 for Graded Modal Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 5 for Probability Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 6 for Hennessy-Milner Modal Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder " 7 for Monotonic Logic\n" ++

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder "<path>: path to input file\n" )

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maeder-- | main program function

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maedermain :: IO()

9929f81562adecc8aafaefb14a0159afcf4a3351Christian Maedermain = do

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder args <- getArgs

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder if (args == [])||(head args == "--help")||(length args < 2)

2eb84fc82d3ffa9116bc471fda3742bd9e5a24bbChristian Maeder then help

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder else let ml = head args

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder path = head (tail args)

35db0960aa2e2a13652381c756fae5fb2b27213bChristian Maeder in runTest (read ml) path

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski