Main.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner - Description : Implemenation of main file for the prover
81d182b21020b815887e9057959228546cf61b6bChristian Maeder - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder - License : GPLv2 or higher, see LICENSE.txt
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - Maintainer : daniel.hausmann@dfki.de
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder - Stability : provisional
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder - Portability : portable
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder - Provides the implementation of the user interaction "interface"
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maedermodule Main where
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder{- ------------------------------------------------------------------------------
ad270004874ce1d0697fb30d7309f180553bb315Christian Maedermake use of these logics:
4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder------------------------------------------------------------------------------ -}
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder-- | Runs the parser and the prover and prints the result(s) of obtained.
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederrunLex :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d))),
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder NonEmptyFeature a b c d, NonEmptySigFeature a b c d) =>
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian MaederrunLex p_rL = run (do spaces
35597678f1c9da703de8d0b6b66ea63247ebe884Christian Maederrun :: (SigFeature b c d, SigFeature a b (c d), Eq (a (b (c d))),
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder NonEmptyFeature a b c d, NonEmptySigFeature a b c d) =>
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder Parser (Formula (a (b (c d)))) -> String -> [Bool] -> IO ()
2ac1742771a267119f1d839054b5e45d0a468085Christian Maederrun p_r input flags = case parse p_r "" input of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Left err -> do putStr "parse error at "
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Right y -> do let x = preparse y
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder -- show formula that is given to the sequent calculus
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder putStrLn (" Current Formula: " ++ pretty x)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder putStrLn " Trying to show satisfiability..."
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder let isS = satisfiable x flags
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder putStrLn $ if isS then " ... The formula is satisfiable"
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder else " ... The formula is not satisfiable"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder putStrLn " Trying to show provability..."
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let isP = provable x flags
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder putStrLn $ if isP then " ... The formula is provable"
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder else " ... The formula is not provable"
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder-- | Parse formula according to the selected modal logic.
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian MaederrunTest :: Int -> String -> [Bool] -> IO ()
2ac1742771a267119f1d839054b5e45d0a468085Christian MaederrunTest ml input flags = do
522913d1d69be804c9579bbc77868ec6b501b608Christian 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
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder 2 -> runLex (parser (KD [] :: KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD (KD ())))))))))))))) Sqr) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 3 -> runLex (parser (C [1] [] :: C (C (C (C (C (C (C (C (C (C (C (C (C (C ())))))))))))))) Sqr) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 4 -> runLex (parser (G 1 [] :: G (G (G (G (G (G (G (G (G (G (G (G (G (G ())))))))))))))) Ang) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 5 -> runLex (parser (P 1 [] :: P (P (P (P (P (P (P (P (P (P (P (P (P (P ())))))))))))))) Ang) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 6 -> runLex (parser (HM 'a' [] :: HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM (HM ())))))))))))))) Sqr) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 7 -> runLex (parser (Mon [] :: Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon (Mon ())))))))))))))) Sqr) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 8 -> runLex (parser (Con [] :: Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con (Con ())))))))))))))) Sqr) input flags
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder 9 -> runLex (parser (SysS [] :: SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS (SysS ())))))))))))))) Ang) input flags
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder 10 -> runLex (parser (K [] :: K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD ())))))))))))))) Sqr) input flags
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder 11 -> runLex (parser (KD [] :: KD (K (KD (K (KD (K (KD (K (KD (K (KD (K (KD (K ())))))))))))))) Sqr) input flags
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder 12 -> runLex (parser (Con [] :: Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon (K (Con (Mon ())))))))))))))) Sqr) input flags
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian 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
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder 14 -> runLex (parser (CKCM [] :: CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM (CKCM ())))))))))))))) Ang) input flags
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder _ -> showHelp
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian Maeder-- | Function for displaying user help
74a946e10a4b324c10d7a59f84298afbcae9b3cfChristian MaedershowHelp :: IO ()
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder putStrLn ( "Usage:\n" ++
b1bd8688a1ce545444792a307412711c2c61df5fChristian Maeder " ./main <ML> -[v/nv] -p <path> or ./main <ML> -[v/nv] -t <test>\n\n" ++
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder "<ML>: 1 for K Modal Logic\n" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder " 2 for KD Modal Logic\n" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder " 3 for Coalition Logic\n" ++
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder " 4 for Graded Modal Logic\n" ++
ce7653c9c71e23bf04a5ec0ca5cb600c3738a909Christian Maeder " 5 for Probabilistic Modal Logic\n" ++
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder " 6 for Hennessy-Milner Modal Logic\n" ++
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder " 7 for Monotonic Modal Logic\n" ++
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder " 8 for Conditional Modal Logic (CK+CEM)\n" ++
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder " 9 for System S (CK+ID+CM+DisjElim)\n" ++
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder " 10 for Combined Logic (K KD)\n" ++
7c35990c03276d1e675ea6f4ba38f47081620d77Christian Maeder " 11 for Combined Logic (KD K)\n" ++
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder " 12 for Combined Logic (Con Mon K)\n" ++
4aad9879e208b4ebc32b47b551a94a5e13e4f716Christian Maeder " 13 for (K + KD)\n" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder " 14 for CK+CM\n" ++
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder "<path>: path to input file\n" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder "<test>: test given as a string\n" ++
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder "-[v/nv]: either verbose or non-verbose output\n")
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- | main program function
840b2a6f37ec58f3281da16fafbc4121462c856aChristian Maeder args <- getArgs
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder if null args || head args == "--help" || length args < 4
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder then showHelp
0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder else let ml : fl : it : test : [] = take 4 args
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder in case it of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder "-p" -> case fl of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder "-v" -> do input <- readFile test
5ba383b1607c20c57e14324e72cee2c789436d5fChristian Maeder runTest (read ml) input [False, True]
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder "-nv" -> do input <- readFile test
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder runTest (read ml) input [True, False]
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder _ -> showHelp
14a1af9d9909dc47dc7fee6b0170b7ac0aef85daChristian Maeder "-t" -> case fl of
f26a1fc3851297e6483cf3fb56e9c0967b8f8b13Christian Maeder "-v" -> runTest (read ml) test [False, True]
72909c6c1cfe9702f5910d0a135c8b55729c7917Christian Maeder "-nv" -> runTest (read ml) test [True, False]
2ac1742771a267119f1d839054b5e45d0a468085Christian Maeder _ -> showHelp
d5b008ac61f0f3d99f41ad3476f945e2b65bd3c0Christian Maeder _ -> showHelp