CSPM-cspm 0.4.4.1 → 0.5.6.0
raw patch · 13 files changed
+1079/−275 lines, 13 filesdep +hsluadep +sybdep +xmldep ~CSPM-CoreLanguagedep ~CSPM-FiringRulesdep ~CSPM-Frontend
Dependencies added: hslua, syb, xml
Dependency ranges changed: CSPM-CoreLanguage, CSPM-FiringRules, CSPM-Frontend, CSPM-Interpreter, CSPM-ToProlog, cmdargs
Files
- CSPM-cspm.cabal +65/−16
- src/CSPM/Assert.hs +1/−1
- src/CSPM/LTS/LTS.hs +5/−2
- src/CSPM/LTS/MkLtsDFS.hs +78/−0
- src/CSPM/LTS/MkLtsPar.hs +1/−1
- src/CSPM/LTS/ToDot.hs +4/−0
- src/CSPM/Lua.hs +188/−0
- src/Language/CSPM/AstToXML.hs +116/−0
- src/Main.hs +6/−255
- src/Main/Args.hs +193/−0
- src/Main/ExceptionHandler.hs +93/−0
- src/Main/ExecCommand.hs +154/−0
- src/Scripting/LuaUtils.hs +175/−0
CSPM-cspm.cabal view
@@ -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 <fontaine@cs.uni-duesseldorf.de>-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
src/CSPM/Assert.hs view
@@ -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)
src/CSPM/LTS/LTS.hs view
@@ -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 {
+ src/CSPM/LTS/MkLtsDFS.hs view
@@ -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
src/CSPM/LTS/MkLtsPar.hs view
@@ -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
src/CSPM/LTS/ToDot.hs view
@@ -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)
+ src/CSPM/Lua.hs view
@@ -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]
+ src/Language/CSPM/AstToXML.hs view
@@ -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
src/Main.hs view
@@ -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
+ src/Main/Args.hs view
@@ -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."]
+ src/Main/ExceptionHandler.hs view
@@ -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
+ src/Main/ExecCommand.hs view
@@ -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"
+ src/Scripting/LuaUtils.hs view
@@ -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