2796N/A{- | Module : $Header$

2796N/A - Description : Implemenation of main file for the prover

2796N/A - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen

2796N/A - License : GPLv2 or higher, see LICENSE.txt

2796N/A - Maintainer : daniel.hausmann@dfki.de

2796N/A - Stability : provisional

2796N/A - Portability : portable

2796N/A -

2796N/A - Provides the implementation of the user interaction "interface"

2796N/A -}

2796N/A

2796N/Amodule Main where

2796N/A

2796N/Aimport Text.ParserCombinators.Parsec

2796N/Aimport System.Environment

2796N/Aimport IO

2796N/A

2796N/Aimport GMP.Logics.Generic

2796N/Aimport GMP.Parser

2796N/Aimport GMP.Prover

2796N/A

2796N/A--------------------------------------------------------------------------------

2796N/A-- make use of these logics:

2796N/A--------------------------------------------------------------------------------

2796N/A

2796N/Aimport GMP.Logics.K

2796N/Aimport GMP.Logics.KD

2796N/Aimport GMP.Logics.HM

2796N/Aimport GMP.Logics.Mon

2796N/Aimport GMP.Logics.C

2796N/Aimport GMP.Logics.P

2796N/Aimport GMP.Logics.G

import GMP.Logics.Con

import GMP.Logics.CKCM

import GMP.Logics.SysS

import GMP.Logics.DisjUnion

--import GMP.Logics.Product

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

runLex :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d)))) => Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()

runLex p_rL input flags = run (do spaces

x <- p_rL

eof

return x

) input flags

run :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d)))) => Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()

run p_r input flags = case (parse p_r "" input) of

Left err -> do putStr "parse error at "

print err

Right y -> do let x = preparse y

-- show formula that is given to the sequent calculus

putStrLn (" Current Formula: " ++ pretty x)

putStrLn (" Trying to show satisfiability...")

let isS = satisfiable x flags

case isS of

True -> putStrLn " ... The formula is satisfiable"

_ -> putStrLn " ... The formula is not satisfiable"

putStrLn (" Trying to show provability...")

let isP = provable x flags

case isP of

True -> putStrLn " ... The formula is provable"

_ -> putStrLn " ... The formula is not provable"

-- | Parse formula according to the selected modal logic.

runTest :: Int -> String -> [Bool] -> IO ()

runTest ml input flags = do

case ml of

1 -> runLex ((parser ((K [])::K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K (K ()))))))))))))))))))))))))))))))))))))))))))) Sqr) ) input flags

2 -> runLex ((parser ((KD [])::KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD ())))))))))))))) Sqr) ) input flags

3 -> runLex ((parser ((C [1] [])::C (C (C (C (C (C (C (C (C (C (C (C (C (C ())))))))))))))) Sqr) ) input flags

4 -> runLex ((parser ((G 1 [])::G (G (G (G (G (G (G (G (G (G (G (G (G (G ())))))))))))))) Ang) ) input flags

5 -> runLex ((parser ((P 1 [])::P (P (P (P (P (P (P (P (P (P (P (P (P (P ())))))))))))))) Ang) ) input flags

6 -> runLex ((parser ((HM 'a' [])::HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM ())))))))))))))) Sqr) ) input flags

7 -> runLex ((parser ((Mon [])::Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon ())))))))))))))) Sqr) ) input flags

8 -> runLex ((parser ((Con [])::Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con ())))))))))))))) Sqr) ) input flags

9 -> runLex ((parser ((SysS [])::SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS ())))))))))))))) Ang) ) input flags

10 -> runLex ((parser ((K [])::K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD ())))))))))))))) Sqr) ) input flags

11 -> runLex ((parser ((KD [])::KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K ())))))))))))))) Sqr) ) input flags

12 -> runLex ((parser ((Con []):: Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon ())))))))))))))) Sqr) ) input flags

13 -> runLex ((parser (((DisjUnion ((K [Mod (DisjUnion (K [Mod (DisjUnion (K [Mod (DisjUnion (K [], KD []))], KD [Mod (DisjUnion (K [], KD []))]))], KD [Mod (DisjUnion (K [Mod (DisjUnion (K [], KD []))], KD [Mod (DisjUnion (K [], KD []))]))]))]),(KD [Mod (DisjUnion (K [Mod (DisjUnion (K [Mod (DisjUnion (K [], KD []))], KD [Mod (DisjUnion (K [], KD []))]))], KD [Mod (DisjUnion (K [Mod (DisjUnion (K [], KD []))], KD [Mod (DisjUnion (K [], KD []))]))]))]))))::DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD ( DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD (DisjUnion K KD ())))))))))))))) Sqr) ) input flags

14 -> runLex ((parser ((CKCM [])::CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM ())))))))))))))) Ang) ) input flags

_ -> showHelp

return ()

-- | Function for displaying user help

showHelp :: IO()

showHelp = do

putStrLn ( "Usage:\n" ++

" ./main <ML> -[v/nv] -p <path> or ./main <ML> -[v/nv] -t <test>\n\n" ++

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

" 2 for KD Modal Logic\n" ++

" 3 for Coalition Logic\n" ++

" 4 for Graded Modal Logic\n" ++

" 5 for Probabilistic Modal Logic\n" ++

" 6 for Hennessy-Milner Modal Logic\n" ++

" 7 for Monotonic Modal Logic\n" ++

" 8 for Conditional Modal Logic (CK+CEM)\n" ++

" 9 for System S (CK+ID+CM+DisjElim)\n" ++

" 10 for Combined Logic (K KD)\n" ++

" 11 for Combined Logic (KD K)\n" ++

" 12 for Combined Logic (Con Mon K)\n" ++

" 13 for (K + KD)\n" ++

" 14 for CK+CM\n" ++

"<path>: path to input file\n" ++

"<test>: test given as a string\n" ++

"-[v/nv]: either verbose or non-verbose output\n")

-- | main program function

main :: IO()

main = do

args <- getArgs

if (args == [])||(head args == "--help")||(length args < 4)

then showHelp

else let ml:fl:it:test:[] = take 4 args

in case it of

"-p" -> case fl of

"-v" -> do input <- readFile test

runTest (read ml) input [False,True]

"-nv" -> do input <- readFile test

runTest (read ml) input [True,False]

_ -> showHelp

"-t" -> case fl of

"-v" -> runTest (read ml) test [False,True]

"-nv" -> runTest (read ml) test [True,False]

_ -> showHelp

_ -> showHelp