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