-------------------------------------------------------------------------------

-- GMP

-- Copyright 2007, Lutz Schroeder and Georgel Calin

-------------------------------------------------------------------------------

module Main where

import Text.ParserCombinators.Parsec

import System.Environment

import IO

import GMPAS

import GMPSAT

import GMPParser

import ModalLogic

import ModalK()

import ModalKD()

import GradedML()

import CoalitionL()

import GenericML()

import Lexer

import qualified Data.Set as Set

-------------------------------------------------------------------------------

-- Funtion to run parser & print

-------------------------------------------------------------------------------

runLex :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

runLex p input = run (do

whiteSpace

; x <- p

; eof

; return x

) input

run :: (Ord a, Show a, ModalLogic a b) => Parser (Formula a) -> String -> IO ()

run p input

= case (parse p "" input) of

Left err -> do putStr "parse error at "

;print err

Right x -> do print "PV list:"

let ls = guessPV x ---------------------------

print ls

let h = if ((not.null) ls) then head(ls)------

else Set.empty-----

-- print h ------------ FOR TESTING ----------

let lro = map roFromPV ls --------------------

print "Rho val from the above PV:"

print lro ------------------------------------

print "the Formula:"

print x

print "SAT test answer:"

let sat = checksat x

print sat

-------------------------------------------------------------------------------

-- For Testing

-------------------------------------------------------------------------------

runTest :: Int -> FilePath -> IO ()

runTest ml p = do

input <- readFile (p)

case ml of

1 -> runLex ((par5er parseIndex) :: Parser (Formula ModalK)) input

2 -> runLex ((par5er parseIndex) :: Parser (Formula ModalKD)) input

3 -> runLex ((par5er parseIndex) :: Parser (Formula CL)) input

4 -> runLex ((par5er parseIndex) :: Parser (Formula Integer)) input

_ -> runLex ((par5er parseIndex) :: Parser (Formula Kars)) input

return ()

help :: IO()

help = do

putStrLn ( "Usage:\n" ++

" ./main <ML> <path>\n\n" ++

"<ML>: 1 for K ML\n" ++

" 2 for KD ML\n" ++

" 3 for Coalition L\n" ++

" 4 for Graded ML\n" ++

" _ for Generic ML\n" ++

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

-------------------------------------------------------------------------------

main :: IO()

main = do

args <- getArgs

if (args == [])||(head args == "--help")||(length args < 2)

then help

else let ml = head args

p = head (tail args)

in runTest (read ml) p