CSPM-cspm-0.1.0.0: src/Main.hs

----------------------------------------------------------------------------
-- |
-- Module      :  Main
-- Copyright   :  (c) Fontaine 2010
-- License     :  BSD
-- 
-- Maintainer  :  Fontaine@cs.uni-duesseldorf.de
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Comand line interface for the CSPM tools.
----------------------------------------------------------------------------
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}

module Main
where

import System.Console.CmdArgs hiding (args)
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)


instance EqOrd INT
instance CSP1 INT
instance CSP2 INT
instance FShow INT

-- | main-funtion for the command line.
main :: IO ()
main = cmdArgs "CSPM Tools V0.1" modes >>= execCommand
  where modes = [evalMode, traceMode, fdrMode, dotMode ]
data Args = 
   Eval {
     evalContext :: FilePath
    ,evalExpr :: String
    }
  |Trace {
     src    :: FilePath
    ,entry  :: String
    }
  |FDR {
     src    :: FilePath
    ,entry  :: String
    ,out :: FilePath
    }
  |Dot {
     src    :: FilePath
    ,entry  :: String
    ,out :: FilePath
    } deriving (Data,Typeable,Show,Eq)

srcArg :: Attrib
srcArg
  = text "CSPM specification"
    & typFile
    & empty "" 
    & argPos 0

mainArg :: Attrib
mainArg
  = text "optional: the main process" 
    & typ "PROCESS"
    & empty "MAIN"
    & explicit & flag "main" & flag "m"

outArg :: Attrib
outArg
  = text "optional: name of the output file"
    & typFile
    & explicit & flag "out" & flag "o"


evalMode :: Mode Args
evalMode = mode $ Eval {
   evalContext = def
       &= text "optional: CSPM specification to load into context"
       & typFile 
       & empty "" & explicit & flag "src"
  ,evalExpr = def 
       &= text "the expression to evaluate"
       & typ "EXPR"
       & argPos 0
  } &= prog "eval"
    & text "evaluate an expression"

traceMode :: Mode Args
traceMode = mode $ Trace {
   src = def &= srcArg
  ,entry = "MAIN" &= mainArg
  } &= prog "trace"
    & text "trace a process"

fdrMode :: Mode Args
fdrMode = mode $ FDR {
   src = def &= srcArg
  ,entry = "MAIN" &= mainArg
  ,out = def &= outArg
  } &= prog "fdr"
    & text "compute the LTS and dump it as fdr script"

dotMode :: Mode Args
dotMode = mode $ Dot {
   src = def &= srcArg
  ,entry = "MAIN" &= mainArg
  ,out = def &= outArg
  } &= prog "dot"
    & text "compute the LTS and dump it as dot graph"

myDefault :: String -> String -> String
myDefault a b = if null a then b else a

execCommand :: Args -> IO ()
execCommand args@Eval {} = do
  let context = if null $ evalContext args then Nothing else Just $ evalContext args
  isVerbose <- isLoud
  (val,_) <- evalEnv isVerbose context $ evalExpr args
  print val

execCommand args@Trace {} = do
  (proc,sigma) <- mkProcess (src args) (entry args)
  trace sigma proc

execCommand args@FDR {} = do
  (proc,sigma) <- mkProcess (src args) (entry args)
  let
    lts = mkLtsPar sigma proc
    outFile = myDefault (out args) (src args ++ ".fdr")
  ltsToCsp proc lts outFile
  return ()

execCommand args@Dot {} = do
  (proc,sigma) <- mkProcess (src args) (entry args)
  let
    lts = mkLtsPar sigma proc
    outFile = myDefault (out args) (src args ++ ".dot")
  mkDotFile outFile lts
  return ()

mkProcess :: FilePath -> String -> IO (Process, ClosureSet)
mkProcess file expr = do
  isVerbose <- isLoud
  (proc, env) <- evalEnv isVerbose (Just file) expr
  case proc of
    VProcess p -> return (p, getAllEvents env)
    _ -> error "type-error : entry-point is not a process"