{- | Module : $Header$

- Description : Implementation of main file for the prover

- Copyright : (c) Georgel Calin & Lutz Schroeder, DFKI Lab Bremen

- License : GPLv2 or higher, see LICENSE.txt

- Maintainer : g.calin@jacobs-university.de

- Stability : provisional

- Portability : portable

-

- Provides the implementation of the user interaction "interface"

-}

module Main where

import GenericSequent

import ModalLogic

import CombLogic

import Parser

import Text.ParserCombinators.Parsec

import System.Environment

import System.IO

import System.IO.Error

import Control.Exception (bracket, bracket_)

-- | Main parsing unit for checking provability/satisfiability

run :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()

run parser input =

case parse parser "" input of

Left err -> do putStr "parse error at "

print err

Right x -> do -- putStrLn (show x{-++" <=> "++input-})

let isP = provable x

putStrLn $ if isP then "... is Provable"

else if sat x then "... is not Provable but Satisfiable"

else "... is not Satisfiable"

-- | Runs the main parsing unit (probably superfluous)

runLex :: (Eq a, Form a b c) => Parser (Boole a) -> String -> IO ()

runLex parser = run (do spaces

res <- parser

eof

return res)

-- | Auxiliary run function for testing with the input given as string

runTest :: [Int] -> String -> IO ()

runTest logics input =

{- do case (head logics) of

1 -> runLex (parseKindex{-(par5er Sqr parseKindex) :: Parser (L K)-}) input

2 -> runLex ((par5er Sqr parseKDindex) :: Parser (L KD)) input

3 -> runLex ((par5er Sqr parseCindex) :: Parser (L C)) input

4 -> runLex ((par5er Ang parseGindex) :: Parser (L G)) input

5 -> runLex ((par5er Ang parsePindex) :: Parser (L P)) input

6 -> runLex ((par5er Sqr parseHMindex) :: Parser (L HM)) input

7 -> runLex ((par5er Sqr parseMindex) :: Parser (L Mon)) input

_ -> showHelp

-}

return ()

-- | Map logic indexes from [Char] to Int

indexToInt :: String -> Int

indexToInt c = case c of

"K" -> 1; "KD" -> 2

"C" -> 3; "G" -> 4

"P" -> 5; "HM" -> 6

"M" -> 7; _ -> error "Main.indexToInt"

-- | Function for displying user help

showHelp :: IO ()

showHelp =

putStrLn ( "Usage:\n" ++

" ./main -p <path> <N> <L1> <L2> .. <LN>\n" ++

" ./main -t <test> <N> <L1> <L2> .. <LN>\n\n" ++

"<N>: a natural number >0 specifing the number of " ++

"combined/embedded logics\n" ++

"<Lx>: each logic can be one of the following cases:\n" ++

" K - K Modal Logic\n" ++

" KD - KD Modal Logic\n" ++

" C - Coalition Logic\n" ++

" G - Graded Modal Logic\n" ++

" P - Probability Logic\n" ++

" HM - Hennessy-Milner Modal Logic\n" ++

" M - Monotonic Logic\n" ++

"<path>: path to input file\n" ++

"<test>: test given as a string\n")

-- | Main program function

main :: IO ()

main = do

args <- getArgs

if null args || head args == "--help" || length args < 4

then showHelp

else let it : test : n : [] = take 3 args

rest = tail . tail . tail $ args

in if length rest < read n

then showHelp

else let list = take (read n) rest

in case it of

"-p" -> do let logics = map indexToInt rest

test <- readFile test

putStrLn test -- run prover with given input

print logics

"-t" -> do let logics = map indexToInt rest

putStrLn test -- run prover with given input

print logics

_ -> showHelp