---------------------------------------------------------------------------- -- | -- Module : Main -- Copyright : (c) Fontaine 2010-2011 -- License : BSD -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental -- Portability : GHC-only -- -- Comand line interface for the CSPM tools. ---------------------------------------------------------------------------- {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -fno-cse #-} module Main where import CSPM.Interpreter import CSPM.Interpreter.Test.CLI (evalEnv) import CSPM.FiringRules.Trace (trace) import CSPM.FiringRules.HelperClasses import CSPM.LTS.MkLtsPar (mkLtsPar) import CSPM.LTS.ToCsp (ltsToCsp) import CSPM.LTS.ToDot (mkDotFile) import CSPM.Assert (checkFileAsserts, formatAssertResults) import Language.CSPM.Frontend (LexError(..),ParseError(..),RenameError(..)) import Language.CSPM.Token (pprintAlexPosn, Token(..)) import Language.CSPM.TranslateToProlog (translateToProlog) import System.Console.CmdArgs import Control.Exception import System.Exit (exitSuccess, exitFailure) instance EqOrd INT instance CSP1 INT instance CSP2 INT instance FShow INT -- | main-funtion for the command line. main :: IO () main = do arguments <- cmdArgsRun argParser handleException $ execCommand arguments exitSuccess -- definition of the command line parser argParser :: Mode (CmdArgs Args) argParser = cmdArgsMode $ modes [evalMode, traceMode, assertMode, fdrMode, dotMode, toPrologMode] &= program "cspm" &= summary "cspm command line utility V0.4.3.0" data Args = ToProlog { inFile :: FilePath ,outFile :: FilePath } |Eval { evalContext :: Maybe FilePath ,evalExpr :: String ,verbose :: Bool } |Trace { src :: FilePath ,entry :: String ,verbose :: Bool } |FDR { src :: FilePath ,entry :: String ,out :: Maybe FilePath ,verbose :: Bool } |Dot { src :: FilePath ,entry :: String ,out :: Maybe FilePath ,verbose :: Bool } |Assert { src :: FilePath ,verbose :: Bool } deriving (Data,Typeable,Show,Eq) toPrologMode :: Args toPrologMode = ToProlog { inFile = def &= argPos 0 &= typ "File" ,outFile = def &= argPos 1 &= typ "File" } &= groupname "translate a CSP-M file to Prolog" evalMode :: Args evalMode = Eval { evalContext = def &= help "optional: CSPM specification to load into context" &= typFile &= explicit &= name "s" &= name "src" ,evalExpr = def &= argPos 0 &= typ "EXPR" -- &= help "the expression to evaluate" ,verbose = def &= help "verbose" &= name "v" &= name "verbose" } &= groupname "evaluate an expression" traceMode :: Args traceMode = Trace { src = def &= argPos 0 &= typFile -- &= help "CSPM specification" ,entry = "MAIN" &= help "optional: the main process" &= typ "PROCESS" &= explicit &= name "main" &= name "m" ,verbose = def &= help "verbose" &= name "v" &= name "verbose" } &= groupname "trace a process" fdrMode :: Args fdrMode = FDR { src = def -- &= help "CSPM specification" &= typFile &= argPos 0 ,entry = "MAIN" &= help "optional: the main process" &= typ "PROCESS" &= explicit &= name "main" &= name "m" ,out = def &= help "optional: name of the generated fdr file" &= typFile &= explicit &= name "out" &= name "o" ,verbose = def &= help "verbose" &= name "v" &= name "verbose" } &= groupname "compute the LTS and dump it as fdr script" dotMode :: Args dotMode = Dot { src = def -- &= help "CSPM specification" &= typFile &= argPos 0 ,entry = "MAIN" &= help "optional: the main process" &= typ "PROCESS" &= explicit &= name "main" &= name "m" ,out = def &= help "optional: name of the generated dot file" &= typFile &= explicit &= name "out" &= name "o" ,verbose = def &= help "verbose" &= name "v" &= name "verbose" } &= groupname "compute the LTS and dump it as dot graph" assertMode :: Args assertMode = Assert { src = def &= typFile &= argPos 0 ,verbose = def &= help "verbose" &= name "v" &= name "verbose" } &= groupname "check the assert declarations of a specification" -- execute the command according to command line arguments execCommand :: Args -> IO () execCommand ToProlog {..} = translateToProlog inFile outFile execCommand Eval {..} = do (val,_) <- evalEnv verbose evalContext evalExpr print val execCommand Trace {..} = do (proc,sigma) <- mkProcess src entry trace sigma proc execCommand Assert {..} = do results <- checkFileAsserts src verbose putStrLn $ show $ formatAssertResults results execCommand FDR {..} = do (proc,sigma) <- mkProcess src entry let lts = mkLtsPar sigma proc outFile = case out of Just f -> f Nothing -> src ++ ".fdr" ltsToCsp proc lts outFile return () execCommand Dot {..} = do (proc,sigma) <- mkProcess src entry let lts = mkLtsPar sigma proc outFile = case out of Just f -> f Nothing -> src ++ ".dot" mkDotFile outFile lts return () mkProcess :: FilePath -> String -> IO (Process, Sigma) mkProcess file expr = do isVerbose <- isLoud (proc, env) <- evalEnv isVerbose (Just file) expr case proc of VProcess p -> return (p, getSigma env) _ -> error "type-error : entry-point is not a process" -- example exception handler handleException :: IO () -> IO () handleException x = x `catches` allHandler where allHandler = [ Handler lexError, Handler parseError, Handler renameError ,Handler interpreterError ,Handler errCall ,Handler async ,Handler ioExc ,Handler someExc ] lexError :: LexError -> IO () lexError LexError {..} = do putStrLn "lexError" putStrLn $ pprintAlexPosn lexEPos putStrLn $ lexEMsg exitFailure parseError :: ParseError -> IO () parseError ParseError {..} = do putStrLn "parseError" putStrLn $ parseErrorMsg putStrLn $ pprintAlexPosn parseErrorPos putStrLn $ "at token : " ++ (show $ tokenString parseErrorToken) exitFailure renameError :: RenameError -> IO () renameError RenameError {..} = do putStrLn "renameError" putStrLn $ renameErrorMsg putStrLn $ show renameErrorLoc exitFailure interpreterError :: InterpreterError -> IO () interpreterError err = do putStrLn "InterpreterError :" putStrLn $ errMsg err putStrLn $ show $ errLoc err putStrLn "" putStrLn $ show err exitFailure ioExc :: IOException -> IO () ioExc err = do putStrLn $ show err exitFailure errCall :: ErrorCall -> IO () errCall err = flip catches allHandler $ do putStrLn "unexpected error call" putStrLn $ show err exitFailure async :: AsyncException -> IO () async err = do putStrLn "AsyncException (Pressing CRTL-C ?)" putStrLn $ show err exitFailure someExc :: SomeException -> IO () someExc err = do putStrLn $ show err exitFailure