c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Description : Implemenation of main file for the prover
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - License : GPLv2 or higher, see LICENSE.txt
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Maintainer : daniel.hausmann@dfki.de
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Stability : provisional
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Portability : portable
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann - Provides the implementation of the user interaction "interface"
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmannmodule Main where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------------------------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermake use of these logics:
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------------ -}
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- | Runs the parser and the prover and prints the result(s) of obtained.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrunLex :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d))),
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder NonEmptyFeature a b c d, NonEmptySigFeature a b c d) =>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrunLex p_rL = run (do spaces
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederrun :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d))),
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder NonEmptyFeature a b c d, NonEmptySigFeature a b c d) =>
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederrun p_r input flags = case parse p_r "" input of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Left err -> do putStr "parse error at "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Right y -> do let x = preparse y
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- show formula that is given to the sequent calculus
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn (" Current Formula: " ++ pretty x)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn " Trying to show satisfiability..."
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let isS = satisfiable x flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn $ if isS then " ... The formula is satisfiable"
2ffa94a49389096aa73aaf93a8a5dc13ccb41ae0Christian Maeder else " ... The formula is not satisfiable"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn " Trying to show provability..."
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let isP = provable x flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn $ if isP then " ... The formula is provable"
2ffa94a49389096aa73aaf93a8a5dc13ccb41ae0Christian Maeder else " ... The formula is not provable"
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- | Parse formula according to the selected modal logic.
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannrunTest :: Int -> String -> [Bool] -> IO ()
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel HausmannrunTest ml input flags = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 2 -> runLex (parser (KD [] :: KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 3 -> runLex (parser (C [1] [] :: C (C (C (C (C (C (C (C (C (C (C (C (C (C ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 4 -> runLex (parser (G 1 [] :: G (G (G (G (G (G (G (G (G (G (G (G (G (G ())))))))))))))) Ang) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 5 -> runLex (parser (P 1 [] :: P (P (P (P (P (P (P (P (P (P (P (P (P (P ())))))))))))))) Ang) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 6 -> runLex (parser (HM 'a' [] :: HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 7 -> runLex (parser (Mon [] :: Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 8 -> runLex (parser (Con [] :: Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 9 -> runLex (parser (SysS [] :: SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS ())))))))))))))) Ang) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 10 -> runLex (parser (K [] :: K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 11 -> runLex (parser (KD [] :: KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 12 -> runLex (parser (Con [] :: Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon ())))))))))))))) Sqr) input flags
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 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
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder 14 -> runLex (parser (CKCM [] :: CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM ())))))))))))))) Ang) input flags
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann _ -> showHelp
d024d9de9b6e7a7cfd72ef72d8efb0e57da5a01bChristian Maeder-- | Function for displaying user help
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedershowHelp :: IO ()
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann putStrLn ( "Usage:\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " ./main <ML> -[v/nv] -p <path> or ./main <ML> -[v/nv] -t <test>\n\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann "<ML>: 1 for K Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 2 for KD Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 3 for Coalition Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 4 for Graded Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 5 for Probabilistic Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 6 for Hennessy-Milner Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 7 for Monotonic Modal Logic\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 8 for Conditional Modal Logic (CK+CEM)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 9 for System S (CK+ID+CM+DisjElim)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 10 for Combined Logic (K KD)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 11 for Combined Logic (KD K)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 12 for Combined Logic (Con Mon K)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 13 for (K + KD)\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann " 14 for CK+CM\n" ++
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann "<path>: path to input file\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann "<test>: test given as a string\n" ++
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann "-[v/nv]: either verbose or non-verbose output\n")
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann-- | main program function
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann args <- getArgs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null args || head args == "--help" || length args < 4
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann then showHelp
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else let ml : fl : it : test : [] = take 4 args
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann in case it of
c8cc43106ea9a9bd1890ed81fc40b9877a4414d0Daniel Hausmann "-p" -> case fl of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "-v" -> do input <- readFile test
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder runTest (read ml) input [False, True]
093f1948e37cc2e9be32cae0a4913fc1bac0c84bDaniel Hausmann "-nv" -> do input <- readFile test
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder runTest (read ml) input [True, False]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "-t" -> case fl of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "-v" -> runTest (read ml) test [False, True]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "-nv" -> runTest (read ml) test [True, False]