c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin - Description : Implementation of main file for the prover
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin - Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu - License : GPLv2 or higher, see LICENSE.txt
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin - Maintainer : g.calin@jacobs-university.de
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin - Stability : provisional
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin - Portability : portable
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin - Provides the implementation of the user interaction "interface"
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmodule Main where
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calinimport GenericSequent
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport ModalLogic
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinimport CombLogic
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Control.Exception (bracket, bracket_)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- | Main parsing unit for checking provability/satisfiability
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calinrun :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maederrun parser input =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case parse parser "" input of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin Left err -> do putStr "parse error at "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Right x -> do -- putStrLn (show x{-++" <=> "++input-})
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin let isP = provable x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder putStrLn $ if isP then "... is Provable"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else if sat x then "... is not Provable but Satisfiable"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else "... is not Satisfiable"
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- | Runs the main parsing unit (probably superfluous)
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinrunLex :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrunLex parser = run (do spaces
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin-- | Auxiliary run function for testing with the input given as string
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinrunTest :: [Int] -> String -> IO ()
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel CalinrunTest logics input =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder {- do case (head logics) of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 1 -> runLex (parseKindex{-(par5er Sqr parseKindex) :: Parser (L K)-}) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin 7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin _ -> showHelp
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- | Map logic indexes from [Char] to Int
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederindexToInt :: String -> Int
f00edd94c598adc73dc4f6005d79d2295e463da5Georgel CalinindexToInt c = case c of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "K" -> 1; "KD" -> 2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "C" -> 3; "G" -> 4
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "P" -> 5; "HM" -> 6
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "M" -> 7; _ -> error "Main.indexToInt"
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder-- | Function for displying user help
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedershowHelp :: IO ()
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin putStrLn ( "Usage:\n" ++
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin " ./main -p <path> <N> <L1> <L2> .. <LN>\n" ++
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin " ./main -t <test> <N> <L1> <L2> .. <LN>\n\n" ++
9a80079e082fdf4fe8e19f8fc61e6cd8799b47a7Christian Maeder "<N>: a natural number >0 specifing the number of " ++
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin "<Lx>: each logic can be one of the following cases:\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " K - K Modal Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " KD - KD Modal Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " C - Coalition Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " G - Graded Modal Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " P - Probability Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " HM - Hennessy-Milner Modal Logic\n" ++
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin " M - Monotonic Logic\n" ++
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin "<path>: path to input file\n" ++
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin "<test>: test given as a string\n")
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- | Main program function
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin args <- getArgs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if null args || head args == "--help" || length args < 4
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin then showHelp
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else let it : test : n : [] = take 3 args
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder rest = tail . tail . tail $ args
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in if length rest < read n
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin then showHelp
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin else let list = take (read n) rest
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin in case it of
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin "-p" -> do let logics = map indexToInt rest
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin test <- readFile test
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin putStrLn test -- run prover with given input
2416ff1b5e23a72da496ab79aa1a7df85db32308Georgel Calin "-t" -> do let logics = map indexToInt rest
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin putStrLn test -- run prover with given input