hets/GMP/Main.hs

	Main.hs revision edbee37fd0c724e09c8471d25d0dc48ac84ac12c
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin{- | Module     : $Header$
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin -  Description : Implementation of main file for the prover
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  Copyright   : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  License     : Similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  Maintainer  : g.calin@jacobs-university.de
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  Stability   : provisional
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  Portability : portable
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -  Provides the implementation of the user interaction "interface"
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin -}
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmodule Main where
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calinimport GenericSequent
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport Parser
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport System.Environment
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calinimport IO
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- | Map logic indexes from [Char] to Int
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalintransformLogicIndex :: [Char] -> Int
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel CalintransformLogicIndex c = case c of
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "K"  -> 1
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "KD" -> 2
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "C"  -> 3
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "G"  -> 4
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "P"  -> 5
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "HM" -> 6
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         "M"  -> 7
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                         _    -> error "Main.transformLogicIndex"
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin-- | Function for displying user help
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinshowHelp :: IO()
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel CalinshowHelp = do
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" ++
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin               "<N>:     a natural number >0 specifing the number of combined/embedded logics\n" ++
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
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin-- | Main program function
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmain :: IO()
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calinmain = do
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin    args <- getArgs
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin    if (args == [])||(head args == "--help")||(length args < 4)
ace3d0483eaadd85e5c7b59d2be8b316b4f897d2Georgel Calin     then showHelp
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin     else let it:test:n:[] = take 3 args
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin              rest = tail.tail.tail $ args
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin          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
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                       "-p" -> do test <- readFile test
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                                  putStrLn test -- run prover with given input
edbee37fd0c724e09c8471d25d0dc48ac84ac12cGeorgel Calin                       "-t" -> putStrLn test -- run prover with given input
c4ae37349f31bb57fba21eb842ea3f2e439abb1cGeorgel Calin                       _    -> showHelp