Main.hs revision 2416ff1b5e23a72da496ab79aa1a7df85db32308
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder{- | Module : $Header$
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Description : Implementation of main file for the prover
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - License : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Maintainer : g.calin@jacobs-university.de
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Stability : provisional
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Portability : portable
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maeder - Provides the implementation of the user interaction "interface"
9d0567bda351efa4286f38e85fb3e41ecd3683eaChristian Maedermodule Main where
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport GenericSequent
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maederimport ModalLogic
9f93b2a8b552789cd939d599504d39732672dc84Christian Maederimport CombLogic
d3f192025f2836285d9705a959542350e057f281Christian Maeder-- | Main parsing unit for checking provability/satisfiability
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maederrun :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maederrun parser input =
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder case (parse parser "" input) of
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder Left err -> do putStr "parse error at "
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder Right x -> do --putStrLn (show x{-++" <=> "++input-})
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder let isP = provable x
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder True -> putStrLn "... is Provable"
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder _ -> let isS = sat x
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder in case isS of
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder True -> putStrLn ("... is not Provable" ++
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder " but Satisfiable")
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder _ -> putStrLn "... is not Satisfiable"
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder-- | Runs the main parsing unit (probably superfluous)
20bd79f8844604c145510c616fecdaf47eba2fdbChristian MaederrunLex :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian MaederrunLex parser input = run (do spaces
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder res <- parser
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder-- | Auxiliary run function for testing with the input given as string
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian MaederrunTest :: [Int] -> String -> IO ()
20bd79f8844604c145510c616fecdaf47eba2fdbChristian MaederrunTest logics input =
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder do {-case (head logics) of
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder 1 -> runLex (parseKindex{-(par5er Sqr parseKindex) :: Parser (L K)-}) input
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder 2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input
20bd79f8844604c145510c616fecdaf47eba2fdbChristian Maeder 3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder 4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder 5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder 6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder 7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder _ -> showHelp
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | Map logic indexes from [Char] to Int
ab0274ab68a174d3e92235b4c4ca865c03901583Christian MaederindexToInt :: [Char] -> Int
ab0274ab68a174d3e92235b4c4ca865c03901583Christian MaederindexToInt c = case c of
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder "K" -> 1; "KD" -> 2
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder "C" -> 3; "G" -> 4
3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian Maeder "P" -> 5; "HM" -> 6
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder "M" -> 7; _ -> error "Main.indexToInt"
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder-- | Function for displying user help
9f93b2a8b552789cd939d599504d39732672dc84Christian MaedershowHelp :: IO()
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder putStrLn ( "Usage:\n" ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder " ./main -p <path> <N> <L1> <L2> .. <LN>\n" ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder " ./main -t <test> <N> <L1> <L2> .. <LN>\n\n" ++
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder "<N>: a natural number >0 specifing the number of " ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder "<Lx>: each logic can be one of the following cases:\n" ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder " K - K Modal Logic\n" ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder " KD - KD Modal Logic\n" ++
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder " C - Coalition Logic\n" ++
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder " G - Graded Modal Logic\n" ++
9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder " P - Probability Logic\n" ++
23a0d43ca980983c7d7aebaa9f03bfe120be7de8Christian Maeder " HM - Hennessy-Milner Modal Logic\n" ++
ab0274ab68a174d3e92235b4c4ca865c03901583Christian Maeder " M - Monotonic Logic\n" ++
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder "<path>: path to input file\n" ++
d3f192025f2836285d9705a959542350e057f281Christian Maeder "<test>: test given as a string\n")
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder-- | Main program function
2119c0874c93fc1cdfea381bcfea69e8fdb8b6e2Christian Maeder args <- getArgs
d3f192025f2836285d9705a959542350e057f281Christian Maeder if (args == [])||(head args == "--help")||(length args < 4)
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder then showHelp
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder else let it:test:n:[] = take 3 args
d3f192025f2836285d9705a959542350e057f281Christian Maeder in if (length rest < read n)
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder then showHelp
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder else let list = take (read n) rest
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder in case it of
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder "-p" -> do let logics = map indexToInt rest
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder test <- readFile test
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder putStrLn test -- run prover with given input
d3f192025f2836285d9705a959542350e057f281Christian Maeder putStrLn $ show logics
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder "-t" -> do let logics = map indexToInt rest
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder putStrLn test -- run prover with given input
d3f192025f2836285d9705a959542350e057f281Christian Maeder putStrLn $ show logics
df15a183ca8bf1c25db69775979905198d7cc8bbChristian Maeder _ -> showHelp