  | Module      : ./GMP / GMP - CoLoSS / Main.hs 
  -   Description : Implemenation of main file for the prover 
  -   Copyright    : ( c )  Calin & Lutz Schroeder , DFKI Lab Bremen 
  -   License      : GPLv2 or higher , see LICENSE.txt 
  -   Maintainer   :  
  -   Stability    : provisional 
  -   Portability : portable 
  - 
  -   Provides the implementation of the user interaction " interface " 
 
 -  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  : 
 -  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

 ------------------------------------------------------------------------------
make use of these logics:
------------------------------------------------------------------------------ 
 | Runs the parser and the prover and prints the result(s) of obtained.
 show formula that is given to the sequent calculus
 | Function for displaying user help
 | main program function
  | Module      : ./GMP / GMP - CoLoSS / Main.hs 
  -   Description : Implemenation of main file for the prover 
  -   Copyright    : ( c )  Calin & Lutz Schroeder , DFKI Lab Bremen 
  -   License      : GPLv2 or higher , see LICENSE.txt 
  -   Maintainer   :  
  -   Stability    : provisional 
  -   Portability : portable 
  - 
  -   Provides the implementation of the user interaction " interface " 
 
 -  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  : 
 -  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


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

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
                   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 ()

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 :: 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
