diff --git a/CSPM-cspm.cabal b/CSPM-cspm.cabal --- a/CSPM-cspm.cabal +++ b/CSPM-cspm.cabal @@ -1,5 +1,5 @@ Name: CSPM-cspm -Version: 0.4.4.1 +Version: 0.5.6.0 Synopsis: cspm command line tool for analyzing CSPM specifications. Description: @@ -13,16 +13,13 @@ . * 'cspm trace spec.csp' -> interactively trace a process. . - * 'cspm assert spec.csp' -> check the assertions of a specification. + * 'cspm assert spec.csp' -> check the assertions of a specification (only some assertions are supported). . - * 'cspm dot spec.csp' -> compute the labeled transition system of a process - and dump it as dot-file. + * 'cspm lts spec.csp --dotOut spec.csp.dot' -> compute the labeled transition system of a process and dump it as dot-file. . - * 'cspm fdr spec.csp' -> compute the LTS + * 'cspm lts spec.csp --fdrOut spec.csp.fdr' -> compute the LTS and dump it a fdr script suitable for refinement checking. . - * 'cspm toprolog spec.csp' -> generate prolog output for ProB - . cspm is not a full featured FDR replacement. The main purpose of cspm is to show how the different CSPM-packages work together. LTS computation can demonstrate nice speed-ups on multi-core machines. @@ -34,28 +31,30 @@ License-File: LICENSE Author: Marc Fontaine Maintainer: Marc Fontaine -Homepage: http://www.stups.uni-duesseldorf.de/~fontaine/csp cabal-Version: >= 1.10 build-type: Simple -Tested-With: GHC == 7.0.2 +Tested-With: GHC == 7.0.3 Stability: experimental Executable cspm Build-Depends: - CSPM-Frontend >= 0.6 && < 0.7 - ,CSPM-CoreLanguage >= 0.2 && < 0.3 - ,CSPM-FiringRules >= 0.3 && < 0.4 - ,CSPM-Interpreter >= 0.4 && < 0.5 - ,CSPM-ToProlog >= 0.3 && < 0.4 - ,cmdargs == 0.6.8 + CSPM-Frontend >= 0.7 && < 0.8 + ,CSPM-CoreLanguage >= 0.3 && < 0.4 + ,CSPM-FiringRules >= 0.4 && < 0.5 + ,CSPM-Interpreter >= 0.5 && < 0.6 + ,CSPM-ToProlog >= 0.4 && < 0.5 + ,cmdargs >= 0.7 && < 0.8 + ,xml >= 1.3 && < 1.4 ,containers >= 0.4 && < 0.5 ,parallel >=3.1 && < 3.2 ,base >= 4.0 && < 5.0 ,pretty >=1.0 && <1.1 ,transformers >=0.2 && <0.3 + ,syb >= 0.3 && <0.4 + ,hslua == 0.3.3 GHC-Options: - -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans + -threaded -funbox-strict-fields -O2 -Wall -fno-warn-orphans -- -funbox-strict-fields -O2 -Wall -fno-warn-orphans -rtsopts Default-Language: Haskell2010 @@ -65,10 +64,60 @@ Main-is: Main.hs Other-modules: + Main.Args + Main.ExceptionHandler + Main.ExecCommand CSPM.Assert CSPM.LTS.LTS CSPM.LTS.MkLtsPar + CSPM.LTS.MkLtsDFS CSPM.LTS.ToCsp CSPM.LTS.ToDot CSPM.LTS.Utils CSPM.LTS.Deadlock + CSPM.Lua + Language.CSPM.AstToXML + Scripting.LuaUtils + Paths_CSPM_cspm + +Library + Build-Depends: + CSPM-Frontend >= 0.7 && < 0.8 + ,CSPM-CoreLanguage >= 0.3 && < 0.4 + ,CSPM-FiringRules >= 0.4 && < 0.5 + ,CSPM-Interpreter >= 0.5 && < 0.6 + ,CSPM-ToProlog >= 0.4 && < 0.5 + ,cmdargs >= 0.7 && < 0.8 + ,xml >= 1.3 && < 1.4 + ,containers >= 0.4 && < 0.5 + ,parallel >=3.1 && < 3.2 + ,base >= 4.0 && < 5.0 + ,pretty >=1.0 && <1.1 + ,transformers >=0.2 && <0.3 + ,syb >= 0.3 && <0.4 + ,hslua == 0.3.3 + GHC-Options: + -funbox-strict-fields -O2 -Wall -fno-warn-orphans + Default-Language: Haskell2010 + Other-Extensions: + DeriveDataTypeable, StandaloneDeriving, TypeSynonymInstances, RecordWildCards + Hs-Source-Dirs: src + + Exposed-Modules: + Main.Args + Main.ExceptionHandler + Main.ExecCommand + CSPM.Assert + CSPM.LTS.LTS + CSPM.LTS.MkLtsPar + CSPM.LTS.MkLtsDFS + CSPM.LTS.ToCsp + CSPM.LTS.ToDot + CSPM.LTS.Utils + CSPM.LTS.Deadlock + CSPM.Lua + Language.CSPM.AstToXML + + Other-modules: + Paths_CSPM_cspm + Scripting.LuaUtils diff --git a/src/CSPM/Assert.hs b/src/CSPM/Assert.hs --- a/src/CSPM/Assert.hs +++ b/src/CSPM/Assert.hs @@ -18,7 +18,7 @@ import Language.CSPM.AST as AST import Language.CSPM.AstUtils import Language.CSPM.Frontend -import Language.CSPM.PrettyPrinter () +import Language.CSPM.PrettyPrinter (pp) import CSPM.Interpreter.Eval import CSPM.Interpreter.Types (Env) diff --git a/src/CSPM/LTS/LTS.hs b/src/CSPM/LTS/LTS.hs --- a/src/CSPM/LTS/LTS.hs +++ b/src/CSPM/LTS/LTS.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE BangPatterns #-} ---------------------------------------------------------------------------- -- | -- Module : CSPM.LTS.LTS @@ -9,12 +8,16 @@ -- Stability : experimental -- Portability : GHC-only -- +{-# LANGUAGE BangPatterns #-} +{-# Language DeriveDataTypeable #-} + module CSPM.LTS.LTS where import CSPM.FiringRules.Rules import CSPM.Interpreter as Interpreter import CSPM.Interpreter.Hash +import Data.Typeable import Data.Map (Map) import Data.Ord (comparing) import Data.Function (on) @@ -23,7 +26,7 @@ = LtsNode { nodeDigest :: ! Interpreter.Digest ,nodeProcess :: Interpreter.Process - } + } deriving Typeable mkLtsNode :: Interpreter.Process -> LtsNode mkLtsNode p = LtsNode { diff --git a/src/CSPM/LTS/MkLtsDFS.hs b/src/CSPM/LTS/MkLtsDFS.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/LTS/MkLtsDFS.hs @@ -0,0 +1,78 @@ +---------------------------------------------------------------------------- +-- | +-- Module : CSPM.LTS.mkLtsDFS +-- Copyright : (c) Fontaine 2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- Compute the labled transition system of a process. +-- Uses depth first search and runs in the IO-Monad. +-- A Timeout can be set and the function can return a partial LTS +---------------------------------------------------------------------------- +module CSPM.LTS.MkLtsDFS +( + dfsStep + ,mkLtsDFS +) +where + +import CSPM.CoreLanguage +import CSPM.FiringRules.Rules +import CSPM.FiringRules.Verifier (viewProcAfter) +import CSPM.FiringRules.FieldConstraints (computeTransitions) + +import CSPM.Interpreter (INT) + +import CSPM.LTS.LTS + +import qualified Data.Map as Map + +import System.Timeout as Timeout +import Control.Exception +import Data.IORef + +-- | Generate an LTS with a DFS +{-# WARNING mkLtsDFS "mkLts leaks memory: TODO : fix this" #-} +mkLtsDFS :: Bool -> Maybe Double -> Sigma INT -> Process INT -> IO (LTS, Bool) +mkLtsDFS progressReport maxTime sigma process = do + ltsPtr <- newIORef ([mkLtsNode process],Map.empty) + let tout = case maxTime of + Nothing -> (-1) + Just seconds -> round $ seconds * 1000000 + res <- Timeout.timeout tout $ dfsLoop ltsPtr sigma + case res of + Nothing -> do + state <- readIORef ltsPtr + return (snd state, False) + Just () -> do + state <- readIORef ltsPtr + return (snd state, True) + + +dfsLoop :: IORef DFSState -> Sigma INT -> IO () +dfsLoop ltsPtr sigma = loop + where + loop = do + lts <- fmap snd $ readIORef ltsPtr + evaluate lts + finish <- atomicModifyIORef ltsPtr $ dfsStep sigma + if finish then return () else loop + +type DFSState = ([LtsNode],LTS) + +-- | perform one iteration of the DFS loop +dfsStep :: Sigma INT -> DFSState -> (DFSState,Bool) +dfsStep _ ([],lts) = (([],lts),True) +dfsStep sigma (proc:restQueue,lts) + = if proc `Map.member` lts + then ((restQueue,lts),False) + else ((newQueue,newLts),False) + where + transitions :: [Rule INT] + transitions = computeTransitions sigma $ nodeProcess proc + newNodes = map (mkLtsNode . viewProcAfter) transitions + newLts = Map.insert proc transitions lts + newQueue = newNodes ++ restQueue diff --git a/src/CSPM/LTS/MkLtsPar.hs b/src/CSPM/LTS/MkLtsPar.hs --- a/src/CSPM/LTS/MkLtsPar.hs +++ b/src/CSPM/LTS/MkLtsPar.hs @@ -31,7 +31,7 @@ import Data.Set (Set) import Data.List as List --- | Compute the LTS of a Process. +-- | Compute the LTS of a Process using parallel strategies mkLtsPar :: Sigma INT -> Process INT -> LTS mkLtsPar events process = wave [mkLtsNode process] Map.empty diff --git a/src/CSPM/LTS/ToDot.hs b/src/CSPM/LTS/ToDot.hs --- a/src/CSPM/LTS/ToDot.hs +++ b/src/CSPM/LTS/ToDot.hs @@ -94,5 +94,9 @@ fieldToCsp f = case f of Interpreter.VChannel chan -> Interpreter.chanName chan Interpreter.VInt i -> show i + Interpreter.VBool True -> "true" + Interpreter.VBool False -> "false" Interpreter.VConstructor c -> Interpreter.constrName c + Interpreter.VTuple l -> "(" ++ (concat $ intersperse "," $ List.map fieldToCsp l) ++ ")" + Interpreter.VDotTuple l -> (concat $ intersperse "." $ List.map fieldToCsp l) _ -> error ("ToDot : fieldToCsp missing match" ++ show f) diff --git a/src/CSPM/Lua.hs b/src/CSPM/Lua.hs new file mode 100644 --- /dev/null +++ b/src/CSPM/Lua.hs @@ -0,0 +1,188 @@ +---------------------------------------------------------------------------- +-- | +-- Module : CSPM.Lua +-- Copyright : (c) Fontaine 2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- A Lua interface for the CSPM tool. +---------------------------------------------------------------------------- +{-# Language DeriveDataTypeable #-} +{-# Language ViewPatterns, RecordWildCards #-} +{-# Language ScopedTypeVariables, RankNTypes, GADTs, KindSignatures #-} +{-# Language FlexibleInstances #-} +module CSPM.Lua +( + runLua +) +where + +import CSPM.Interpreter as Interpreter +import CSPM.Interpreter.Test.CLI (evalString) + +import CSPM.LTS.MkLtsPar (mkLtsPar) +import CSPM.CoreLanguage.Event +import CSPM.FiringRules.Rules +import CSPM.FiringRules.FieldConstraints (computeTransitions) +import CSPM.FiringRules.Verifier (viewRule) + + +import Scripting.LuaUtils +import qualified Scripting.Lua as Lua + +import Foreign.StablePtr +import Control.Exception.Base +import Data.Dynamic +import System.Environment +import Control.Monad +import Data.List as List +import Data.Maybe + +runLua :: String -> String -> [String] -> IO () +runLua src chunkName args = bracket (Lua.newstate) (Lua.close) $ \l -> do + Lua.openlibs l + registerHsFunctions l exportList + loadRes <- fmap fromIntegral $ Lua.loadstring l src chunkName + if loadRes /= 0 then do + err <- Lua.peek l 1 + case err of + Nothing -> throwIO $ ErrorFromLua loadRes "Lua.loadstring failed" + Just msg -> throwIO $ ErrorFromLua loadRes msg + else do + Lua.push l $ LuaArray args + Lua.setglobal l "arg" + forM_ args $ Lua.push l + err <- call_debug l (length args) (Just 0) + maybe (return ()) throwIO err + +exportList :: [Export] +exportList = + [ luaHsExports + , luaExportInfo + , luaToString + , luaTypeOf + , luaEval + , luaMakeLTS + , Export "rawCmdArgs" "get the raw list of command args " (fmap LuaArray getArgs) + , luaTransitions + , luaValueToProcess + , luaViewProofTree + ] + + +luaExportInfo :: Export +luaExportInfo = Export "exportInfo" "information about exported functions" + $ (return helpMsg :: IO String) + where + helpMsg = concat [ + "Lua API for CSPM",nl + ,"Haskell exported functions :" ,nl + ] ++ concatMap mkFunMsg exportList + nl = "\n" + mkFunMsg Export {..} = concat [ + " * " , exportName ," : ",nl + ," ", exportHelp ,nl + ] + +luaHsExports :: Export +luaHsExports = Export "hsExports" "return a table with all exported functions" + (return $ LuaArray $ map exportName exportList :: IO (LuaArray String)) + where exportName (Export n _ _) = "_cspm_" ++ n + +luaToString :: Export +luaToString = Export "toString" "convert an Object to a String" fkt + where + fkt :: LuaObject -> IO (LuaReturn String) + fkt ptr = handleException $ do + dyn <- deRefStablePtr $ castPtrToStablePtr ptr + return $ case dyn of + (fromDynamic -> Just (v :: Interpreter.Value)) -> show v + (fromDynamic -> Just (v :: Interpreter.Process)) -> show v + (fromDynamic -> Just (LuaError err)) -> show err + (fromDynamic -> Just (e :: (TTE INT))) -> showTTE e + _ -> "val:" ++ (show $ dynTypeRep dyn) + +luaTypeOf :: Export +luaTypeOf = Export "reflectType" "get the type of an Object" fkt + where + fkt :: LuaObject -> IO (LuaReturn String) + fkt ptr = handleException $ do + typeRep <- fmap dynTypeRep $ deRefStablePtr $ castPtrToStablePtr ptr + case List.lookup typeRep shortTypes of + Just t -> return t + Nothing -> return $ show typeRep + shortTypes = [ +-- (typeOf (undefined :: LuaValue), "Value") +-- ,(typeOf (undefined :: LuaTransition ), "Transistion") +-- ,(typeOf (undefined :: LuaEvent ), "Event") +-- (typeOf (undefined :: LuaLTS ), "LTS") + ] + + +luaEval :: Export +luaEval = Export "eval" + "eval an expression in the context of an specification" fkt + where + fkt :: Bool -> Maybe String -> String -> IO (LuaReturn AssocTable) + fkt verbose spec expr = handleException $ do + (value,env) <- evalString verbose (fromMaybe "spec" spec) "spec from lua" expr + lValue <- toLuaObject value + lEnv <- toLuaObject env + lSigma <- toLuaObject $ getSigma env + return $ AssocTable + [ "value" :-> lValue + , "env" :-> lEnv + , "sigma" :-> lSigma] + +luaMakeLTS :: Export +luaMakeLTS = Export "makeLTS" "compute the LTS of a Process" fkt + where + fkt :: LuaObject -> LuaObject -> IO (LuaReturn LuaObject) + fkt lSigma lProc = handleException $ do + (sigma :: Interpreter.ClosureSet) <- fromLuaObject lSigma + proc <- fromLuaObject lProc + toLuaObject $ mkLtsPar sigma proc + +luaValueToProcess :: Export +luaValueToProcess = Export "valueToProcess" "cast a Value to a Process" fkt + where + fkt :: LuaObject -> IO (LuaReturn LuaObject) + fkt a = do + val <- fromLuaObject a + case val of + VProcess p -> fmap LuaReturnOK $ toLuaObject p + _ -> error "typeError expecting VProcess" + +luaTransitions :: Export +luaTransitions = Export + "transitions" + "compute the transitions of a Process" + fkt + where + fkt :: LuaObject -> LuaObject -> IO (LuaReturn (LuaArray LuaObject)) + fkt lSigma lProc = handleException $ do + (sigma :: Interpreter.ClosureSet) <- fromLuaObject lSigma + proc <- fromLuaObject lProc + let (proofs :: [Rule INT]) = computeTransitions sigma proc + fmap LuaArray $ mapM toLuaObject proofs + +luaViewProofTree :: Export +luaViewProofTree = Export + "viewProofTree" + "compute (PrevState,Event,SuccState)" + fkt + where + fkt :: LuaObject -> IO (LuaReturn AssocTable) + fkt t = handleException $ do + (rule :: Rule INT) <- fromLuaObject t + let (a, event ,b) = viewRule rule + lA <- toLuaObject a + lEvent <- toLuaObject event + lB <- toLuaObject b + return $ AssocTable + [ "predState" :-> lA + , "event" :-> lEvent + , "succState" :-> lB] diff --git a/src/Language/CSPM/AstToXML.hs b/src/Language/CSPM/AstToXML.hs new file mode 100644 --- /dev/null +++ b/src/Language/CSPM/AstToXML.hs @@ -0,0 +1,116 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Language.CSPM.AstToXml +-- Copyright : (c) Fontaine 2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- Convert an AST to XML + +module Language.CSPM.AstToXML + ( + moduleToXML + ,astToXML + ,showTopElement + ) +where + +import Text.XML.Light +import Data.Data +import Data.Generics.Aliases (extQ, ext1Q) +import Language.CSPM.AST +import Language.CSPM.SrcLoc as SrcLoc + +-- | Translate a Module to XML +moduleToXML :: Module a -> Element +moduleToXML m + = unode "Module" + [ + unode "moduleDecls" $ astToXML $ moduleDecls m + ,unode "modulePragmas" $ map + (unode "Pragma" . Attr (unqual "val")) + (modulePragmas m) + ,unode "moduleComments" $ astToXML $ moduleComments m + ] + +-- | Translate an AST node to an XML Element. +-- This is an 'almost' totally generic translation which +-- works for any Haskell type, but it handles some special cases. +astToXML :: Data a => a -> Element +astToXML + = genericCase `extQ` identToXML `ext1Q` labelToXML + `ext1Q` listToXML `extQ` intToXML `extQ` commentToXML + where + genericCase :: Data a => a -> Element + genericCase n = unode (showConstr $ toConstr n) $ gmapQ astToXML n + + identToXML :: Ident -> Element + identToXML x = case x of + Ident s -> unode "Ident" (Attr (unqual "unIdent") s) + UIdent u -> unode "UIdent" $ uniqueIdentToXML u + + labelToXML :: Data a => Labeled a -> Element + labelToXML l = add_attrs + ( idAttr : location) + ( astToXML $ unLabel l) + where + idAttr = strAttr "nodeId" $ show $ unNodeId $ nodeId l + location = srcLocAttr $ srcLoc l + + listToXML :: Data a => [a] -> Element + listToXML = unode "list" . map astToXML + + intToXML :: Integer -> Element + intToXML i = unode "Integer" $ strAttr "val" $ show i + + uniqueIdentToXML n = unode "UniqueIdent" + [ + strAttr "uniqueIdentId" $ show $ uniqueIdentId n + ,strAttr "bindingSide" $ show $ bindingSide n + ,strAttr "bindingLoc" $ "todo: bindingLoc" + ,strAttr "idType" $ show $ idType n + ,strAttr "realName" $ realName n + ,strAttr "newName" $ newName n + ,strAttr "prologMode" $ show $ prologMode n + ,strAttr "bindType" $ show $ bindType n + ] + + strAttr a s = Attr (unqual a) s + + srcLocAttr :: SrcLoc.SrcLoc -> [Attr] + srcLocAttr loc = case loc of + SrcLoc.TokPos {} -> [ + locAttr "sLine" $ SrcLoc.getStartLine loc + , locAttr "sCol" $ SrcLoc.getStartCol loc + , locAttr "sPos" $ SrcLoc.getStartOffset loc + , locAttr "len" $ SrcLoc.getTokenLen loc + ] + SrcLoc.TokSpan {} -> [ + locAttr "sLine" $ SrcLoc.getStartLine loc + , locAttr "sCol" $ SrcLoc.getStartCol loc + , locAttr "eLine" $ SrcLoc.getEndLine loc + , locAttr "eCol" $ SrcLoc.getEndCol loc + , locAttr "sPos" $ SrcLoc.getStartOffset loc + , locAttr "len" $ SrcLoc.getTokenLen loc + ] + SrcLoc.FixedLoc {} -> [ + locAttr "sLine" $ SrcLoc.getStartLine loc + , locAttr "sCol" $ SrcLoc.getStartCol loc + , locAttr "eLine" $ SrcLoc.getEndLine loc + , locAttr "eCol" $ SrcLoc.getEndCol loc + , locAttr "sPos" $ SrcLoc.getStartOffset loc + , locAttr "len" $ SrcLoc.getTokenLen loc + ] + _ -> [] + + locAttr s i = Attr (unqual s) $ show i + + commentToXML :: (Comment,SrcLoc.SrcLoc) -> Element + commentToXML (comment,loc) + = add_attrs (srcLocAttr loc) $ case comment of + LineComment c -> unode "LineComment" $ strAttr "val" c + BlockComment c -> unode "BlockComment" $ strAttr "val" c + PragmaComment c -> unode "PragmaComment" $ strAttr "val" c diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -2,45 +2,26 @@ -- | -- Module : Main -- Copyright : (c) Fontaine 2010-2011 --- License : BSD --- +-- License : BSD3 +-- -- 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 Main.ExceptionHandler (handleException) +import Main.Args (argParser) +import Main.ExecCommand (execCommand) import System.Console.CmdArgs -import Control.Exception -import System.Exit (exitSuccess, exitFailure) -instance EqOrd INT -instance CSP1 INT -instance CSP2 INT -instance FShow INT +import System.Exit (exitSuccess) -- | main-funtion for the command line. main :: IO () @@ -48,233 +29,3 @@ 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.4.1" - -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 diff --git a/src/Main/Args.hs b/src/Main/Args.hs new file mode 100644 --- /dev/null +++ b/src/Main/Args.hs @@ -0,0 +1,193 @@ +---------------------------------------------------------------------------- +-- | +-- Module : Main.Args +-- Copyright : (c) Fontaine 2010-2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- Argument parser for the command line interface +---------------------------------------------------------------------------- +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -fno-cse #-} + +module Main.Args +( + Args(..) + ,argParser +) +where + +import System.Console.CmdArgs +import Paths_CSPM_cspm (version) +import Data.Version (showVersion) + +-- | Command line argument parser using cmdargs library. +argParser :: Mode (CmdArgs Args) +argParser = cmdArgsMode + $ modes [ + infoMode, evalMode, traceMode, assertMode, ltsMode + , translateMode, luaMode] + &= program "cspm" + &= summary ("cspm command line utility version " ++ showVersion version) + +data Args = + Info { + verbose :: Bool + } + |Eval { + evalContext :: Maybe FilePath + ,evalExpr :: String + ,verbose :: Bool + } + |Trace { + src :: FilePath + ,entry :: String + ,verbose :: Bool + } + |LTS { + src :: FilePath + ,timeout:: Maybe Double + ,dfs :: Bool + ,entry :: String + ,fdrOut :: Maybe FilePath + ,dotOut :: Maybe FilePath + ,verbose :: Bool + } + |Assert { + src :: FilePath + ,verbose :: Bool + } + |Translate { + src :: FilePath + ,rename :: Bool + ,xmlOut :: Maybe FilePath + ,prettyOut :: Maybe FilePath + ,addUnicode :: Maybe FilePath + ,removeUnicode :: Maybe FilePath + ,prologOut :: Maybe FilePath + } + |Lua { + file :: FilePath + ,rest :: [String] + } + deriving (Data,Typeable,Show,Eq) + +infoMode :: Args +infoMode = Info { + verbose = def + &= help "verbose" + &= name "v" &= name "verbose" + } &= details ["print some information about the program"] &= auto + +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" + } &= details ["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" + } &= details ["trace a process"] + +ltsMode :: Args +ltsMode = LTS { + src = def +-- &= help "CSPM specification" + &= typFile + &= argPos 0 + ,entry = "MAIN" + &= help "optional: the main process" + &= typ "PROCESS" + &= explicit &= name "main" &= name "m" + ,timeout = def + &= help "optional: timeout in seconds" + &= typ "DOUBLE" + &= explicit &= name "timeout" + ,dfs = def + &= help "use DFS algorithm (can compute a partial LTS)" + &= explicit &= name "dfs" &= name "partial" + ,dotOut = def + &= help "optional: write output-file in dot format" + &= typFile + &= explicit &= name "dotOut" + ,fdrOut = def + &= help "optional: write output-file suitable for fdr refinement checking" + &= typFile + &= explicit &= name "fdrOut" + ,verbose = def + &= help "verbose" + &= name "v" &= name "verbose" + } &= details ["compute the LTS and dump it in various formats"] + +luaMode :: Args +luaMode = Lua { + file = def + &= typFile + &= argPos 0 + ,rest = def &= args + } &= details ["run a lua script"] + +assertMode :: Args +assertMode = Assert { + src = def + &= typFile + &= argPos 0 + ,verbose = def + &= help "verbose" + &= name "v" &= name "verbose" + } &= details ["check the assert declarations of a specification"] + +translateMode :: Args +translateMode = Translate { + src = def + &= typFile + &= argPos 0 + ,rename = False + &= help "run renaming on the AST" + &= explicit &= name "rename" + ,xmlOut = def + &= help "optional: write a file with containing XML" + &= typFile + &= explicit &= name "xmlOut" + ,addUnicode = def + &= help "optional: replace some CSPM symbols with unicode" + &= typFile + &= explicit &= name "addUnicode" + ,removeUnicode = def + &= help "optional: replace some unicode symbols with default CSPM encoding" + &= typFile + &= explicit &= name "removeUnicode" + ,prettyOut = def + &= help "optional: prettyPrint to a file" + &= typFile + &= explicit &= name "prettyOut" + ,prologOut = def + &= help "translate a CSP-M file to Prolog" + &= typFile + &= explicit &= name "prologOut" + } &= details ["Parse a specification and write the parse result to a file."] diff --git a/src/Main/ExceptionHandler.hs b/src/Main/ExceptionHandler.hs new file mode 100644 --- /dev/null +++ b/src/Main/ExceptionHandler.hs @@ -0,0 +1,93 @@ +---------------------------------------------------------------------------- +-- | +-- Module : Main.ExceptionHandler +-- Copyright : (c) Fontaine 2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- ExceptionHandler for the command line interface +---------------------------------------------------------------------------- +{-# LANGUAGE RecordWildCards #-} + +module Main.ExceptionHandler +( + handleException +) + +where + +import CSPM.Interpreter + + +import Language.CSPM.Frontend + (LexError(..), ParseError(..), RenameError(..)) +import Language.CSPM.Token (pprintAlexPosn, Token(..)) + +import Control.Exception +import System.Exit (exitFailure, ExitCode) +import System.IO + +-- | The top-level exception handler. +handleException :: IO () -> IO () +handleException x + = x `catches` allHandler + where + putStrLnErr = hPutStrLn stderr + allHandler = [ + Handler propagateExitCode + ,Handler lexError, Handler parseError, Handler renameError + ,Handler interpreterError + ,Handler errCall + ,Handler async + ,Handler ioExc + ,Handler someExc ] + propagateExitCode :: ExitCode -> IO () + propagateExitCode = throwIO + lexError :: LexError -> IO () + lexError LexError {..} = do + putStrLnErr "lexError" + putStrLnErr $ pprintAlexPosn lexEPos + putStrLnErr lexEMsg + exitFailure + parseError :: ParseError -> IO () + parseError ParseError {..} = do + putStrLnErr "parseError" + putStrLnErr parseErrorMsg + putStrLnErr $ pprintAlexPosn parseErrorPos + putStrLnErr $ "at token : " ++ (show $ tokenString parseErrorToken) + exitFailure + renameError :: RenameError -> IO () + renameError RenameError {..} = do + putStrLnErr "renameError" + putStrLnErr renameErrorMsg + putStrLnErr $ show renameErrorLoc + exitFailure + interpreterError :: InterpreterError -> IO () + interpreterError err = do + putStrLnErr "InterpreterError :" + putStrLnErr $ errMsg err + putStrLnErr $ show $ errLoc err + hPutStrLn stderr "" + putStrLnErr $ show err + exitFailure + ioExc :: IOException -> IO () + ioExc err = do + putStrLnErr $ show err + exitFailure + errCall :: ErrorCall -> IO () + errCall err = flip catches allHandler $ do + putStrLnErr "unexpected error call" + putStrLnErr $ show err + exitFailure + async :: AsyncException -> IO () + async err = do + putStrLnErr "AsyncException (Pressing CRTL-C ?)" + putStrLnErr $ show err + exitFailure + someExc :: SomeException -> IO () + someExc err = do + putStrLnErr $ show err + exitFailure diff --git a/src/Main/ExecCommand.hs b/src/Main/ExecCommand.hs new file mode 100644 --- /dev/null +++ b/src/Main/ExecCommand.hs @@ -0,0 +1,154 @@ +---------------------------------------------------------------------------- +-- | +-- Module : Main.ExecCommand +-- Copyright : (c) Fontaine 2010-2011 +-- License : BSD3 +-- +-- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Stability : experimental +-- Portability : GHC-only +-- +-- Comand line interface for the CSPM tools. +---------------------------------------------------------------------------- +{-# LANGUAGE RecordWildCards #-} + +module Main.ExecCommand +where + +import Main.Args (Args(..)) +import Paths_CSPM_cspm (version) + +import CSPM.Interpreter (INT,interpreterVersion,getSigma,Process,Sigma,Value(..),evalFile) +import CSPM.FiringRules.Trace (trace) +import CSPM.FiringRules.HelperClasses +import CSPM.CoreLanguage (coreLanguageVersion) + +import CSPM.LTS.MkLtsPar (mkLtsPar) +import CSPM.LTS.MkLtsDFS (mkLtsDFS) +import CSPM.LTS.ToCsp (ltsToCsp) +import CSPM.LTS.ToDot (mkDotFile) +import CSPM.Assert (checkFileAsserts, formatAssertResults) +import CSPM.Lua (runLua) + +import Language.CSPM.Frontend + (parseFile, frontendVersion + ,eitherToExc, renameModule, castModule, lexInclude) +import Language.CSPM.LexHelper (unicodeTokenString,asciiTokenString) +import Language.CSPM.PrettyPrinter (toPrettyString) + +import Language.CSPM.TranslateToProlog (translateToProlog) +import Language.CSPM.AstToXML (moduleToXML, showTopElement) + +import System.Console.CmdArgs (isLoud) -- todo: fix this + +import qualified System.Timeout as Timeout +import Control.Exception (evaluate) +import System.Exit (exitSuccess) +import Data.Version (showVersion) +import Control.Monad +import Data.Maybe +import Data.List as List + +instance EqOrd INT +instance CSP1 INT +instance CSP2 INT +instance FShow INT + +-- | execute the command according to command line arguments +execCommand :: Args -> IO () +execCommand Info {..} = do + putStr $ concat + [ + "Versions :",nl + ," cspm command line utility : ", showVersion version, nl + ," CSPM-Frontend : ", showVersion frontendVersion, nl + ," CSPM-CoreLanguage : ", showVersion coreLanguageVersion, nl + ," CSPM-FiringRules : ", nl + ," CSPM-Interpreter : ", showVersion interpreterVersion, nl + ,nl + ,"Usage examples:",nl + ," cspm --help",nl + ," cspm eval --help",nl + ," cspm info",nl + ," cspm eval '3+2'",nl + ] + where nl = "\n" + +execCommand Lua {..} = do + src <- readFile file + runLua src file rest +execCommand Translate {..} = do + when (null $ catMaybes + [prologOut, xmlOut, prettyOut, addUnicode, removeUnicode]) $ do + putStrLn "No output option is set" + putStrLn "Set '--xmlOut', '--prettyOut' or an other output option" + when (isJust xmlOut || isJust prettyOut) $ do + -- AST transformations + ast <- do + ast1 <- parseFile src + if rename + then fmap fst $ eitherToExc $ renameModule ast1 + else return $ castModule ast1 + whenJust xmlOut $ \outFile -> do + writeFile outFile $ showTopElement $ moduleToXML ast + whenJust prettyOut $ \outFile -> do + writeFile outFile $ toPrettyString ast + when (isJust addUnicode || isJust removeUnicode) $ do + -- Token stream transformations + tokens <- readFile src >>= lexInclude >>= eitherToExc + whenJust addUnicode $ \outFile -> do + writeFile outFile $ List.concatMap unicodeTokenString tokens + whenJust removeUnicode $ \outFile -> do + writeFile outFile $ List.concatMap asciiTokenString tokens + whenJust prologOut $ \outFile -> do + translateToProlog src outFile -- translateToProlog does not return ! + error "unreachable" + where + whenJust a action = case a of + Just v -> action v + Nothing -> return () + +execCommand Eval {..} = do + (val,_) <- evalFile 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 LTS {..} = do + (proc,sigma) <- mkProcess src entry + lts <- if dfs then do + (res,complete) <- mkLtsDFS True timeout sigma proc + when (not complete) $ putStrLn "timeout occured: LTS only partial" + return res + else do + let tout = case timeout of + Nothing -> (-1) + Just seconds -> round $ seconds * 1000000 + res <- Timeout.timeout tout $ evaluate $ mkLtsPar sigma proc + case res of + Nothing -> do + putStrLn "timeout occured: no output will be generated" + exitSuccess + Just x -> return x + + case fdrOut of + Nothing -> return () + Just outFile -> ltsToCsp proc lts outFile + case dotOut of + Nothing -> return () + Just outFile -> mkDotFile outFile lts + return () + +mkProcess :: FilePath -> String -> IO (Process, Sigma) +mkProcess file expr = do + isVerbose <- isLoud + (proc, env) <- evalFile isVerbose (Just file) expr + case proc of + VProcess p -> return (p, getSigma env) + _ -> error "type-error : entry-point is not a process" diff --git a/src/Scripting/LuaUtils.hs b/src/Scripting/LuaUtils.hs new file mode 100644 --- /dev/null +++ b/src/Scripting/LuaUtils.hs @@ -0,0 +1,175 @@ +---------------------------------------------------------------------------- +-- | +-- Module : Scripting.LuaUtils +-- +-- Utility function for Lua Scripting +---------------------------------------------------------------------------- +{-# Language DeriveDataTypeable #-} +{-# Language ViewPatterns, RecordWildCards #-} +{-# Language ScopedTypeVariables, RankNTypes, GADTs, KindSignatures #-} +{-# Language FlexibleInstances #-} +module Scripting.LuaUtils +where + +import qualified Scripting.Lua as Lua + +import Control.Monad +import Data.Dynamic +import Foreign.StablePtr +import Foreign.Ptr +import Foreign.C +import Control.Exception + +data ErrorFromLua = ErrorFromLua Int String + deriving Typeable + +instance Show ErrorFromLua where + show (ErrorFromLua err msg) = "lua-error " ++ show err ++ " :" ++ msg + +instance Exception ErrorFromLua + +data Export = forall a. Lua.LuaImport a => Export { + exportName :: String + ,exportHelp :: String + ,exportFun :: a + } + +registerHsFunctions :: Lua.LuaState -> [Export] -> IO () +registerHsFunctions l exportList = forM_ exportList + $ \(Export name _help fun) -> Lua.registerhsfunction l ("_cspm_"++name) fun + +type LuaObject = Ptr () + +-- this is crap +-- either we return something of type a +-- or a Error +-- but we loose the type info +data LuaReturn a + = LuaReturnOK a + | LuaReturnError LuaError + +instance Lua.StackValue a => Lua.StackValue (LuaReturn a) + where + push l v = case v of + LuaReturnOK a -> Lua.push l a + LuaReturnError err -> toLuaObject err >>= Lua.pushlightuserdata l + peek = error "peek: cannot read back value of type LuaReturn" + valuetype = error "peek: cannot read back value of type LuaReturn" + +newtype LuaError = LuaError {unLuaError :: SomeException } + deriving Typeable + +instance Lua.StackValue a => Lua.StackValue (Maybe a) + where + push l v = case v of + Just a -> Lua.push l a + Nothing -> Lua.push l () + + peek l n = do + t <- fmap (fmap $ \() -> Nothing) $ Lua.peek l n + case t of + Nothing -> fmap (fmap Just) $ Lua.peek l n + _ -> return t + + valuetype _ = error "Maybe value type" + +newtype LuaArray x = LuaArray {unLuaArray :: [x]} + +instance Lua.StackValue a => Lua.StackValue (LuaArray a) + where + push s (LuaArray l) = do + Lua.createtable s (length l) 0 + forM_ (zip [1..] l) $ \(ix::Int,val) -> do + Lua.push s val + Lua.rawseti s (-2) ix + + peek = error "peek LuaArray" + valuetype = error "valuetype LuaArray" + +newtype AssocTable = AssocTable {unAssocTable :: [Assoc]} +data Assoc = forall a b. (Lua.StackValue a, Lua.StackValue b) + => a :-> b + +instance Lua.StackValue AssocTable where + push l (AssocTable t) = do + Lua.createtable l (length t) 0 + forM_ t $ \(key :-> val) -> do + Lua.push l key + Lua.push l val + Lua.rawset l (-3) + + peek = error "peek AssocTable" + valuetype = error "valuetype AssocTable" + + +toLuaObject :: Typeable a => a -> IO LuaObject +toLuaObject + = fmap castStablePtrToPtr . newStablePtr . toDyn + +fromLuaObject :: forall a. Typeable a => LuaObject -> IO a +fromLuaObject ptr = do + v <- deRefStablePtr $ castPtrToStablePtr ptr + case fromDynamic v of + Just a -> return a + Nothing -> error $ "fromLuaObject: typeError expected : " + ++ expect ++ " found : " ++ found + where + expect = show $ typeOf (undefined :: a) + found = show $ dynTypeRep v + +-- todo: we have memory leaks, if we create +-- stablepointer and then throw an exception!! +handleException :: forall a. Lua.StackValue a => IO a -> IO (LuaReturn a) +handleException x + = fmap LuaReturnOK x `catches` allHandler + where + allHandler = [ Handler someExc ] + + someExc :: SomeException -> IO (LuaReturn a) + someExc = return . LuaReturnError . LuaError + + +foreign import ccall "lua.h lua_pcall" c_lua_pcall :: Lua.LuaState -> CInt -> CInt -> CInt -> IO CInt +foreign import ccall "wrapper" mkDebug :: (Lua.LuaState -> IO CInt) -> IO (FunPtr Lua.LuaCFunction) + +call_debug :: Lua.LuaState -> Int -> Maybe Int -> IO (Maybe ErrorFromLua) +call_debug = \l narg nres -> do + base <- fmap (subtract narg) $ Lua.gettop l + debugFun <- mkDebug haskell_traceback + Lua.pushcfunction l debugFun + Lua.insert l base + status <- fmap fromIntegral $ + c_lua_pcall l (fromIntegral narg) (fromIntegral $ maybe Lua.multret id nres) (fromIntegral base) + Lua.remove l base + when (status /= 0) $ void $ Lua.gc l Lua.GCCOLLECT 0 + freeHaskellFunPtr debugFun + if status == 0 + then return Nothing + else do + t <- Lua.ltype l (-1) + if t == Lua.TSTRING + then do + (Just s) <- Lua.peek l 1 + Lua.pop l 1 + return $ Just $ ErrorFromLua status s + else do + Lua.pop l 1 + return $ Just $ ErrorFromLua status ("no error string (type: " ++ show t ++ ")") + where + haskell_traceback :: Lua.LuaState -> IO CInt + haskell_traceback l = do + isString <- Lua.isstring l 1 + if not isString then return 1 + else do + Lua.getglobal l "debug" + isTable <- Lua.istable l (-1) + if not isTable then Lua.pop l 1 >> return 1 + else do + Lua.getfield l (-1) "traceback" + isFunction <- Lua.isfunction l (-1) + if not isFunction then Lua.pop l 2 >> return 1 + else do + Lua.pushvalue l 1 + Lua.pushinteger l 2 + void $ Lua.call l 2 1 + return 1