7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-- GMP

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-- Copyright 2007, Lutz Schroeder and Georgel Calin

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekmodule Main where

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport Text.ParserCombinators.Parsec

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport System.Environment

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport IO

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.GMPAS

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.GMPSAT

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.GMPParser

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.ModalLogic

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.ModalK()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.ModalKD()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.GradedML()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.CoalitionL()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.MajorityL()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.GenericML()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekimport GMP.Lexer

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek--import qualified Data.Set as Set

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-- Funtion to run parser & print

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry JelinekrunLex p input = run (do

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek whiteSpace

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek ; x <- p

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek ; eof

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek ; return x

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek ) input

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekrun p input

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek = case (parse p "" input) of

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek Left err -> do putStr "parse error at "

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek ;print err

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek Right x -> do {-print "PV list:"

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek let ls = guessPV x ---------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print ls{-

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek else Set.empty-----

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print h ------------ FOR TESTING -------------}

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek let lro = map roFromPV ls --------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print "Rho val from the above PV:"

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print lro ------------------------------------}

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print "the Formula:"

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek print x

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek{- let sat = checkSAT x

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek if sat then print "is Satisfiable"

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek else print "is not Satisfiable"

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-}

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-- For Testing

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry JelinekrunTest :: Int -> FilePath -> IO ()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry JelinekrunTest ml p = do

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek input <- readFile (p)

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek case ml of

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

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

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek 4 -> runLex ((par5er parseIndex) :: Parser (Formula GML)) input

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek 5 -> runLex ((par5er parseIndex) :: Parser (Formula ML)) input

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek return ()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekhelp :: IO()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekhelp = do

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek putStrLn ( "Usage:\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " ./main <ML> <path>\n\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek "<ML>: 1 for K ML\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " 2 for KD ML\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " 3 for Coalition L\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " 4 for Graded ML\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " 5 for Majority L\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek " _ for Generic ML\n" ++

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek "<path>: path to input file\n" )

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek-------------------------------------------------------------------------------

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekmain :: IO()

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinekmain = do

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek args <- getArgs

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

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek then help

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek else let ml = head args

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek p = head (tail args)

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek in runTest (read ml) p

7b1019a6d29ccb7999dc76cba3dde1c627e8e609Jerry Jelinek