57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{- | Module : $Header$

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach - Description : Implemenation of main file for the prover

8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen

e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach - Maintainer : g.calin@jacobs-university.de

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder - Stability : provisional

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach - Portability : portable

b4fbc96e05117839ca409f5f20f97b3ac872d1edTill Mossakowski -

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach - Provides the implementation of the user interaction "interface"

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach -}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule Main where

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Text.ParserCombinators.Parsec

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport System.Environment

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport IO

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyimport GMP.Parser

57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maederimport GMP.Generic

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly-- | Runs the parser and the prover and prints the result(s) of obtained.

816c50f9135a598dfdcfb2af8a80390bc42a9b24Liam O'ReillyrunLex :: (Logic a, Eq a, Show a) => Parser (L a) -> String -> IO ()

fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'ReillyrunLex p_rL input = run (do spaces

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly x <- p_rL

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly eof

fd8af3ecf2dff782cb2496c1c9bf9d0a76faa98bLiam O'Reilly return x

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder ) input

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyrun :: (Logic a, Eq a, Show a) => Parser (L a) -> String -> IO ()

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reillyrun p_r input = case (parse p_r "" input) of

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Left err -> do putStr "parse error at "

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly print err

d3c9318c22fcf44d9135a3b2c64f880b9a785babChristian Maeder Right x -> do putStrLn (show x)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett {-

afd6ed16928bbd774b6c6c5b3f440a917dd638a1Andy Gimblett let isS = sat x

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder case isS of

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

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett _ -> putStrLn "... is Not Satisfiable"

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let isP = provable x

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett case isP of

f18cf8a4e7d512a2f57365ab1e9e7fdbb98ba257Andy Gimblett True -> putStrLn "... is Provable"

16e124196c6b204769042028c74f533509c9b5d3Christian Maeder _ -> putStrLn "... is Not Provable"

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -}

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- | Auxiliary run function for testing

d04c328b10f17ec78001a94d694f7188ebd8c03cAndy GimblettrunTest :: Int -> FilePath -> IO ()

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'ReillyrunTest ml path = do

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett input <- readFile path

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett case ml of

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett 1 -> runLex ((par5er K parseKindex) :: Parser (L K)) input

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly 2 -> runLex ((par5er KD parseKDindex) :: Parser (L KD)) input

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly 3 -> runLex ((par5er (C []) parseCindex) :: Parser (L C)) input

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett 4 -> runLex ((par5er (G 0) parseGindex) :: Parser (L G)) input

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett 5 -> runLex ((par5er (P 0) parsePindex) :: Parser (L P)) input

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett 6 -> runLex ((par5er (HM ' ') parseHMindex) :: Parser (L HM)) input

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder 7 -> runLex ((par5er Mon parseMindex) :: Parser (L Mon)) input

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder _ -> help

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly return ()

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly-- | Function for displying user help

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maederhelp :: IO()

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyhelp = do

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly putStrLn ( "Usage:\n" ++

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly " ./main <ML> <path>\n\n" ++

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly "<ML>: 1 for K Modal Logic\n" ++

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder " 2 for KD Modal Logic\n" ++

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett " 3 for Coalition Logic\n" ++

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett " 4 for Graded Modal Logic\n" ++

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett " 5 for Probability Logic\n" ++

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett " 6 for Hennessy-Milner Modal Logic\n" ++

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder " 7 for Monotonic Logic\n" ++

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

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett-- | main program function

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettmain :: IO()

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblettmain = do

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett args <- getArgs

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

b6e474220ddcf68a75ca3dc26093c5ac21e31747Christian Maeder then help

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett else let ml = head args

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett path = head (tail args)

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett in runTest (read ml) path

8528886a04f14abe0ddf80f50c853cc25bc821cdAndy Gimblett