CSPM-cspm-0.4.4.0: src/Main.hs

----------------------------------------------------------------------------
-- |
-- 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