Main.hs revision f04dbee44fb71ec868f409099d983f7f3771e0d2
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder{- | Module : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner - Description : Implemenation of main file for the prover
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - Maintainer : daniel.hausmann@dfki.de
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder - Stability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder - Portability : portable
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder - Provides the implementation of the user interaction "interface"
ca010363454de207082dfaa4b753531ce2a34551Christian Maedermodule Main where
ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder--------------------------------------------------------------------------------
ca010363454de207082dfaa4b753531ce2a34551Christian Maeder-- make use of these logics:
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder--------------------------------------------------------------------------------
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder-- | Runs the parser and the prover and prints the result(s) of obtained.
53301de22afd7190981b363b57c48df86fcb50f7Christian MaederrunLex :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d)))) => Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
028f19cdb09d52bb2fd207399b6fa874540d1670Christian MaederrunLex p_rL input flags = run (do spaces
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder ) input flags
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maederrun :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d)))) => Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederrun p_r input flags = case (parse p_r "" input) of
83cc27e4ca7cf1a4bb5f4a8df17d3e6d44e6f1eaChristian Maeder Left err -> do putStr "parse error at "
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder Right y -> do let x = preparse y
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder -- show formula that is given to the sequent calculus
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder putStrLn (" Current Formula: " ++ pretty x)
49fc18b4bb1d4a8d3ec05e0cffd5f0475b289592Christian Maeder putStrLn (" Trying to show satisfiability...")
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder let isS = satisfiable x flags
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder True -> putStrLn " ... The formula is satisfiable"
da2b959c50c95309d8eb8b24174249c2847e74b5Christian Maeder _ -> putStrLn " ... The formula is not satisfiable"
0a39036fa485579a7b7c81cdd44a412392571927Christian Maeder putStrLn (" Trying to show provability...")
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder let isP = provable x flags
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder True -> putStrLn " ... The formula is provable"
962036a37b92afb04ac0725cde9f20e599c04c5fChristian Maeder _ -> putStrLn " ... The formula is not provable"
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder-- | Parse formula according to the selected modal logic.
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrunTest :: Int -> String -> [Bool] -> IO ()
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian MaederrunTest ml input flags = do
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder 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
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 2 -> runLex ((parser ((KD [])::KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD ())))))))))))))) Sqr) ) input flags
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 3 -> runLex ((parser ((C [1] [])::C (C (C (C (C (C (C (C (C (C (C (C (C (C ())))))))))))))) Sqr) ) input flags
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 4 -> runLex ((parser ((G 1 [])::G (G (G (G (G (G (G (G (G (G (G (G (G (G ())))))))))))))) Ang) ) input flags
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 5 -> runLex ((parser ((P 1 [])::P (P (P (P (P (P (P (P (P (P (P (P (P (P ())))))))))))))) Ang) ) input flags
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 6 -> runLex ((parser ((HM 'a' [])::HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM ())))))))))))))) Sqr) ) input flags
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder 7 -> runLex ((parser ((Mon [])::Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon ())))))))))))))) Sqr) ) input flags
59a2f25e7d71b91b4eda6fa4da753473ad629619Christian Maeder 8 -> runLex ((parser ((Con [])::Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con ())))))))))))))) Sqr) ) input flags
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder 9 -> runLex ((parser ((SysS [])::SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS ())))))))))))))) Ang) ) input flags
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder 10 -> runLex ((parser ((K [])::K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD ())))))))))))))) Sqr) ) input flags
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder 11 -> runLex ((parser ((KD [])::KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K ())))))))))))))) Sqr) ) input flags
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder 12 -> runLex ((parser ((Con []):: Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon ())))))))))))))) Sqr) ) input flags
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder 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
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder 14 -> runLex ((parser ((CKCM [])::CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM ())))))))))))))) Ang) ) input flags
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder _ -> showHelp
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder-- | Function for displaying user help
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian MaedershowHelp :: IO()
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder putStrLn ( "Usage:\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " ./main <ML> -[v/nv] -p <path> or ./main <ML> -[v/nv] -t <test>\n\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder "<ML>: 1 for K Modal Logic\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " 2 for KD Modal Logic\n" ++
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder " 3 for Coalition Logic\n" ++
1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder " 4 for Graded Modal Logic\n" ++
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder " 5 for Probabilistic Modal Logic\n" ++
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder " 6 for Hennessy-Milner Modal Logic\n" ++
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder " 7 for Monotonic Modal Logic\n" ++
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder " 8 for Conditional Modal Logic (CK+CEM)\n" ++
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder " 9 for System S (CK+ID+CM+DisjElim)\n" ++
c4d4df505f3ca488978629c65f4fd15a3ba2833aChristian Maeder " 10 for Combined Logic (K KD)\n" ++
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder " 11 for Combined Logic (KD K)\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " 12 for Combined Logic (Con Mon K)\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " 13 for (K + KD)\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " 14 for CK+CM\n" ++
6e2c88c65d50b2e44f7afa165e6a5fac0724f08cChristian Maeder "<path>: path to input file\n" ++
d591a82b32594f0992b27477cacb00b97226c9c8Christian Maeder "<test>: test given as a string\n" ++
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder "-[v/nv]: either verbose or non-verbose output\n")
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder-- | main program function
6fc65e097da8013f5f4f96c8b343b9b48cd3d9e1Christian Maeder args <- getArgs
add9c81ed5250ba046a8581ff75b2284bd69e219Christian Maeder if (args == [])||(head args == "--help")||(length args < 4)
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder then showHelp
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder else let ml:fl:it:test:[] = take 4 args
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder in case it of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-p" -> case fl of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-v" -> do input <- readFile test
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder runTest (read ml) input [False,True]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-nv" -> do input <- readFile test
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder runTest (read ml) input [True,False]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> showHelp
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-t" -> case fl of
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-v" -> runTest (read ml) test [False,True]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder "-nv" -> runTest (read ml) test [True,False]
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> showHelp
4b8e74c68d62fc4e5a1739b11f8df09beaecbee8Christian Maeder _ -> showHelp