diff --git a/CSPM-Frontend.cabal b/CSPM-Frontend.cabal --- a/CSPM-Frontend.cabal +++ b/CSPM-Frontend.cabal @@ -1,70 +1,54 @@ Name: CSPM-Frontend -Version: 0.4.1.1 +Version: 0.6.8.0 -Synopsis: A CSP-M parser compatible with FDR-2.83 +Synopsis: A CSP-M parser compatible with FDR-2.91 Description: CSP-M is the machine readable syntax of CSP (concurrent sequential processes) as used by the formal methods tools FDR, Probe and ProB. This Package contains functions for lexing, parsing, renaming and pretty-printing CSP-M specifications. - The parser is (almost) 100% compatible with the FDR-2.83 parser. + The parser is (almost) 100% compatible with the FDR-2.91 parser. License: BSD3 category: Language,Formal Methods,Concurrency License-File: LICENSE -Author: Marc Fontaine -Maintainer: Marc Fontaine +Author: Marc Fontaine 2007 - 2011 +Maintainer: Marc Fontaine , me@dobrikov.biz Homepage: http://www.stups.uni-duesseldorf.de/~fontaine/csp -Stability: unstable -Tested-With: GHC == 6.12.3 +Stability: maintained +Tested-With: GHC == 7.0.2 -cabal-Version: >= 1.6 +cabal-Version: >= 1.10 build-type: Simple -Extra-source-files: -flag testing { - description : Testing mode - default: False -} - - library - if flag(testing) { - buildable: False - } - Build-Depends: base >=4.0 && < 5.0 - ,containers >= 0.3 && < 0.4 + ,containers >= 0.4 && < 0.5 ,array >= 0.3 && < 0.4 - ,parsec >= 2.1.0.0 && < 3.0 - ,old-time >= 1.0 && < 1.1 - ,template-haskell >= 2.4 && < 2.5 + ,parsec2 >= 1.0.0 && < 1.1.0 ,pretty >= 1.0 && < 1.1 - ,mtl >= 1.1 && < 1.2 - ,haskell98 >= 1.0 && < 1.1 - ,syb >= 0.1 && < 0.2 + ,mtl (>= 2.0 && < 2.1 ) || (>= 1.1 && < 1.2) + ,syb >= 0.3 && < 0.4 - GHC-Options: -funbox-strict-fields -O2 -fasm -optl-Wl,-s -Wall - Extensions: DeriveDataTypeable, GeneralizedNewtypeDeriving - Hs-Source-Dirs: src,dist/build/autogen + Default-Language: Haskell2010 + Other-Extensions: DeriveDataTypeable + GHC-Options: -funbox-strict-fields -O2 -Wall + Hs-Source-Dirs: src Exposed-modules: Language.CSPM.Frontend - Language.CSPM.Utils - Language.CSPM.AST Language.CSPM.Parser + Language.CSPM.AST + Language.CSPM.PrettyPrinter + Language.CSPM.SrcLoc Language.CSPM.Rename + Language.CSPM.Utils Language.CSPM.Token - Language.CSPM.SrcLoc Language.CSPM.AstUtils Language.CSPM.TokenClasses - Language.CSPM.PrettyPrinter - Language.CSPM.PatternCompiler + Language.CSPM.LexHelper Other-modules: - Paths_CSPM_Frontend - Language.CSPM.Version + Text.ParserCombinators.Parsec.ExprM Language.CSPM.Lexer Language.CSPM.AlexWrapper - Language.CSPM.LexHelper - Text.ParserCombinators.Parsec.ExprM diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) Marc Fontaine 2007-2009 +Copyright (c) Marc Fontaine 2007-2011 All rights reserved. diff --git a/src/Language/CSPM/AST.hs b/src/Language/CSPM/AST.hs --- a/src/Language/CSPM/AST.hs +++ b/src/Language/CSPM/AST.hs @@ -1,8 +1,8 @@ ---------------------------------------------------------------------------- -- | -- Module : Language.CSPM.AST --- Copyright : (c) Fontaine 2008 --- License : BSD +-- Copyright : (c) Fontaine 2008 - 2011 +-- License : BSD3 -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental @@ -11,7 +11,10 @@ -- This Module defines an Abstract Syntax Tree for CSPM. -- This is the AST that is computed by the parser. -- For historycal reasons, it is rather unstructured + {-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving #-} +{-# LANGUAGE EmptyDataDecls, RankNTypes #-} + module Language.CSPM.AST where @@ -30,7 +33,7 @@ type FreeNames = IntMap UniqueIdent newtype NodeId = NodeId {unNodeId :: Int} - deriving (Show,Eq,Ord,Enum,Ix, Typeable, Data) + deriving ( Eq, Ord, Show,Enum,Ix, Typeable, Data) mkNodeId :: Int -> NodeId mkNodeId = NodeId @@ -39,13 +42,7 @@ nodeId :: NodeId ,srcLoc :: SrcLoc ,unLabel :: t - } deriving (Typeable, Data,Show) - -instance Eq (Labeled t) where - (==) a b = (nodeId a) == (nodeId b) - -instance Ord (Labeled t) where - compare a b = compare (nodeId a) (nodeId b) + } deriving ( Eq, Ord, Typeable, Data,Show) -- | Wrap a node with a dummyLabel -- | todo: redo we need a specal case in DataConstructor Labeled @@ -65,9 +62,15 @@ data Ident = Ident {unIdent :: String} - | UIdent {unUIdent :: UniqueIdent} - deriving (Show,Eq,Ord,Typeable, Data) +-- | UIdent {unUIdent :: UniqueIdent} + | UIdent UniqueIdent + deriving ( Eq, Ord, Show,Typeable, Data) +unUIdent :: Ident -> UniqueIdent +unUIdent (UIdent u) = u +unUIdent other + = error $ "Identifier is not of variant UIdent (missing Renaming) " ++ show other + identId :: LIdent -> Int identId = uniqueIdentId . unUIdent . unLabel @@ -81,30 +84,37 @@ ,newName :: String ,prologMode :: PrologMode ,bindType :: BindType - } deriving (Show,Eq,Ord,Typeable, Data) + } deriving ( Eq, Ord, Show,Typeable, Data) data IDType = VarID | ChannelID | NameTypeID | FunID Int | ConstrID String | DataTypeID | TransparentID - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) {- actually BindType and PrologMode are semantically aquivalent -} data BindType = LetBound | NotLetBound - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) isLetBound :: BindType -> Bool isLetBound x = x==LetBound data PrologMode = PrologGround | PrologVariable - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) -type LModule = Labeled Module -data Module = Module { +data Module a = Module { moduleDecls :: [LDecl] ,moduleTokens :: Maybe [Token] - } deriving (Show,Eq,Ord,Typeable, Data) + ,moduleSrcLoc :: SrcLoc + } deriving ( Eq, Ord, Show,Typeable, Data) +data FromParser deriving Typeable +instance Data FromParser +instance Eq FromParser +castModule :: Module a -> Module b +castModule (Module t d s) = Module t d s + +type ModuleFromParser = Module FromParser {- LProc is just a typealias for better readablility todo : maybe use a real type @@ -132,6 +142,7 @@ | Events | BoolSet | IntSet + | ProcSet | TupleExp [LExp] | Parens LExp | AndExp LExp LExp @@ -146,50 +157,50 @@ | ProcAParallel LExp LExp LProc LProc | ProcLinkParallel LLinkList LProc LProc | ProcRenaming [LRename] (Maybe LCompGenList) LProc --- | ProcRenamingComprehension [LRename] [LCompGen] LProc + | ProcException LExp LProc LProc | ProcRepSequence LCompGenList LProc | ProcRepInternalChoice LCompGenList LProc | ProcRepExternalChoice LCompGenList LProc | ProcRepInterleave LCompGenList LProc | ProcRepAParallel LCompGenList LExp LProc | ProcRepLinkParallel LCompGenList LLinkList LProc - | ProcRepSharing LCompGenList LExp LProc - | PrefixExp LExp [LCommField] LProc + | ProcRepSharing LCompGenList LExp LProc-- + | PrefixExp LExp [LCommField] LProc-- -- only used in later stages | PrefixI FreeNames LExp [LCommField] LProc | LetI [LDecl] FreeNames LExp -- freenames of all localBound names | LambdaI FreeNames [LPattern] LExp | ExprWithFreeNames FreeNames LExp - deriving (Show, Eq, Ord, Typeable, Data) + deriving ( Eq, Ord, Show, Typeable, Data) type LRange = Labeled Range data Range = RangeEnum [LExp] | RangeClosed LExp LExp | RangeOpen LExp - deriving (Show, Eq, Ord, Typeable, Data) + deriving ( Eq, Ord, Show, Typeable, Data) type LCommField = Labeled CommField data CommField = InComm LPattern | InCommGuarded LPattern LExp | OutComm LExp - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) type LLinkList = Labeled LinkList data LinkList = LinkList [LLink] | LinkListComprehension [LCompGen] [LLink] - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) type LLink = Labeled Link -data Link = Link LExp LExp deriving (Show,Eq,Ord,Typeable, Data) +data Link = Link LExp LExp deriving ( Eq, Ord, Show,Typeable, Data) type LRename = Labeled Rename -data Rename = Rename LExp LExp deriving (Show,Eq,Ord,Typeable, Data) +data Rename = Rename LExp LExp deriving ( Eq, Ord, Show,Typeable, Data) type LBuiltIn = Labeled BuiltIn -data BuiltIn = BuiltIn Const deriving (Show,Eq,Ord,Typeable, Data) +data BuiltIn = BuiltIn Const deriving ( Eq, Ord, Show,Typeable, Data) lBuiltInToConst :: LBuiltIn -> Const lBuiltInToConst = h . unLabel where @@ -200,8 +211,7 @@ data CompGen = Generator LPattern LExp | Guard LExp - deriving (Show,Eq,Ord,Typeable, Data) - + deriving ( Eq, Ord, Show,Typeable, Data) type LPattern = Labeled Pattern data Pattern @@ -224,7 +234,7 @@ selectors :: Array Int Selector ,idents :: Array Int (Maybe LIdent) } | Selector Selector (Maybe LIdent) - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) {- a Selector is a path in a Pattern/Expression -} data Selector @@ -246,21 +256,19 @@ | TailSel Selector | SliceSel Int Int Selector | SuffixSel Int Int Selector - deriving (Show, Eq, Ord, Typeable, Data) + deriving ( Eq, Ord, Show, Typeable, Data) type LDecl = Labeled Decl data Decl = PatBind LPattern LExp | FunBind LIdent [FunCase] - | AssertRef LExp String LExp - | AssertBool LExp + | Assert LAssertDecl | Transparent [LIdent] | SubType LIdent [LConstructor] | DataType LIdent [LConstructor] | NameType LIdent LTypeDef | Channel [LIdent] (Maybe LTypeDef) | Print LExp --- | FunBindI LIdent FreeNames [FunCase] deriving (Show,Eq,Ord,Typeable, Data) {- @@ -274,55 +282,64 @@ -} type FunArgs = [[LPattern]] -- CSPM confusion of currying/tuples data FunCase - = FunCase FunArgs LExp -- osolete version + = FunCase FunArgs LExp -- oldVersion (returned by parser) | FunCaseI [LPattern] LExp -- newVersion for interpreter - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) type LTypeDef = Labeled TypeDef data TypeDef = TypeTuple [LExp] | TypeDot [LExp] - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) type LConstructor = Labeled Constructor data Constructor = Constructor LIdent (Maybe LTypeDef) - deriving (Show,Eq,Ord,Typeable, Data) - - - -{- -some helper functions --} -{- does not make sense if nodId should be unique -} -instance Functor Labeled where - fmap f x = x {unLabel = f $ unLabel x } + deriving ( Eq, Ord, Show,Typeable, Data) withLabel :: ( NodeId -> a -> b ) -> Labeled a -> Labeled b withLabel f x = x {unLabel = f (nodeId x) (unLabel x) } -mkLabeledNode :: (NodeIdSupply m) => SrcLoc -> t -> m (Labeled t) -mkLabeledNode loc node = do - i <- getNewNodeId - return $ Labeled { - nodeId = i - ,srcLoc = loc - ,unLabel = node } +type LAssertDecl = Labeled AssertDecl +data AssertDecl + = AssertBool LExp + | AssertRefine Bool LExp LRefineOp LExp + | AssertTauPrio Bool LExp LTauRefineOp LExp LExp + | AssertModelCheck Bool LExp LFDRModels (Maybe LFdrExt) + deriving ( Eq, Ord, Show,Typeable,Data) -{- --- user must supply a unique NodeId -unsafeMkLabeledNode :: NodeId -> SrcLoc -> t -> Labeled t -unsafeMkLabeledNode i loc node - = Labeled { - nodeId = i - ,srcLoc = loc - ,unLabel = node } --} +type LFDRModels = Labeled FDRModels +data FDRModels + = DeadlockFree + | Deterministic + | LivelockFree + deriving ( Eq, Ord, Show,Typeable,Data) -class (Monad m) => NodeIdSupply m where - getNewNodeId :: m NodeId +type LFdrExt = Labeled FdrExt +data FdrExt + = F + | FD + | T + deriving ( Eq, Ord, Show,Typeable,Data) +type LTauRefineOp = Labeled TauRefineOp +data TauRefineOp + = TauTrace + | TauRefine + deriving ( Eq, Ord, Show,Typeable, Data) +type LRefineOp = Labeled RefineOp +data RefineOp + = Trace + | Failure + | FailureDivergence + | RefusalTesting + | RefusalTestingDiv + | RevivalTesting + | RevivalTestingDiv + | TauPriorityOp + deriving ( Eq, Ord, Show,Typeable, Data) + data Const = F_true | F_false @@ -373,4 +390,4 @@ | F_Hiding | F_Timeout | F_Interleave - deriving (Show,Eq,Ord,Typeable, Data) + deriving ( Eq, Ord, Show,Typeable, Data) diff --git a/src/Language/CSPM/AstUtils.hs b/src/Language/CSPM/AstUtils.hs --- a/src/Language/CSPM/AstUtils.hs +++ b/src/Language/CSPM/AstUtils.hs @@ -1,8 +1,8 @@ ----------------------------------------------------------------------------- -- | -- Module : Language.CSPM.AstUtils --- Copyright : (c) Fontaine 2008 --- License : BSD +-- Copyright : (c) Fontaine 2008 - 2011 +-- License : BSD3 -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental @@ -10,6 +10,7 @@ -- -- Some utility functions for converting the AST +{-# LANGUAGE RankNTypes #-} module Language.CSPM.AstUtils ( removeSourceLocations @@ -17,24 +18,24 @@ ,removeModuleTokens ,unUniqueIdent ,showAst - ,relabelAst ,computeFreeNames + ,getModuleAsserts + ,setNodeIdsZero ) where import Language.CSPM.AST hiding (prologMode) -import qualified Language.CSPM.AST as AST import qualified Language.CSPM.SrcLoc as SrcLoc -import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Data.Data +import Data.Maybe import Data.Generics.Schemes (everywhere,listify) import Data.Generics.Aliases (mkT,extQ) -import Data.Generics.Basics (gmapQ,toConstr,showConstr) +--import Data.Generics.Basics (gmapQ,toConstr,showConstr) -- | 'removeSourceLocations' sets all locationsInfos to 'NoLocation' -removeSourceLocations :: LModule -> LModule +removeSourceLocations :: Data a => Labeled (Module a) -> Labeled (Module a) removeSourceLocations ast = everywhere (mkT patchLabel) ast where @@ -42,12 +43,12 @@ patchLabel _ = SrcLoc.NoLocation -- | set the tokenlist in the module datatype to Nothing -removeModuleTokens :: LModule -> LModule +removeModuleTokens :: Labeled (Module a) -> Labeled (Module a) removeModuleTokens t = t {unLabel = m} where m = (unLabel t ) {moduleTokens = Nothing} -- | 'removeParens' removes all occurences of of Parens,i.e. explicit parentheses from the AST -removeParens :: LModule -> LModule +removeParens :: Data a => Labeled (Module a) -> Labeled (Module a) removeParens ast = everywhere (mkT patchExp) ast where @@ -56,10 +57,18 @@ Parens e -> e _ -> x +-- | Set all NodeIds to zero. +setNodeIdsZero :: Data a => Labeled (Module a) -> Labeled (Module a) +setNodeIdsZero ast + = everywhere (mkT nID) ast + where + nID :: NodeId -> NodeId + nID _ = NodeId { unNodeId = 0 } + -- | unUniqueIdent replaces the all UIdent with the Ident of the the new name, thus forgetting -- | additional information like the bindingside, etc. -- | Usefull to get a smaller AST. -unUniqueIdent :: LModule -> LModule +unUniqueIdent :: Data a => Labeled (Module a) -> Labeled (Module a) unUniqueIdent ast = everywhere (mkT patchIdent) ast where @@ -67,13 +76,6 @@ patchIdent (UIdent u) = Ident $ newName u patchIdent _ = error "unUniqueIdent : did not expect and 'Ident' in the AST" --- | 'relabelAst' compute an AST with new NodeIds starting with the given NodeId -relabelAst :: - NodeId - -> LModule - -> LModule -relabelAst = error "relabel not yet implemented (TODO)" - -- | 'a show function that omits the node labeles. -- | TODO : fix this is very buggy. -- | this does not work for Compiles pattern / Arrays @@ -90,31 +92,46 @@ ++ concat (gmapQ ((++) " " . gshow) t) ++ ")" - - -- | Compute the "FreeNames" of an Expression. -- | This function does only work after renaming has been done. -- | This implementation is inefficient. computeFreeNames :: Data a => a -> FreeNames computeFreeNames syntax - = IntMap.difference (toIntMap used) (toIntMap def) + = IntMap.difference (IntMap.fromList used) (IntMap.fromList def) where - toIntMap :: [UniqueIdent] -> IntMap UniqueIdent - toIntMap - = IntMap.fromList . map (\x -> (uniqueIdentId x,x)) - used :: [UniqueIdent] - used = map (\(Var x) -> unUIdent $ unLabel x) $ listify isUse syntax - def :: [UniqueIdent] - def = (map (\(VarPat x) -> unUIdent $ unLabel x) $ listify isDef syntax) - ++(map (\(FunBind x _) -> unUIdent $ unLabel x) $ listify isFunDef syntax) + used :: [(Int, UniqueIdent)] + used = map (getIdent . unUse) $ listify isUse syntax + def :: [(Int, UniqueIdent)] + def = (map (getIdent . unDef) $ listify isDef syntax) + ++ (map (getIdent . unDecl) $ listify isDecl syntax) + getIdent :: LIdent -> (Int, UniqueIdent) + getIdent x = (uniqueIdentId h, h) + where h = unUIdent $ unLabel x + isUse :: Exp -> Bool isUse (Var {}) = True isUse _ = False + unUse (Var x) = x + unUse _ = error "computeFreeNames : expecting Var" + isDef :: Pattern -> Bool isDef (VarPat {}) = True isDef _ = False - - isFunDef :: Decl -> Bool - isFunDef (FunBind {}) = True - isFunDef _ = False + + isDecl (FunBind {}) = True + isDecl _ = False + + unDef (VarPat x) = x + unDef _ = error "computeFreeNames : expecting VarPar" + + unDecl (FunBind x _) = x + unDecl _ = error "computeFreeNames : expecting FunBind" + +-- | Get the assert declarations of a module +getModuleAsserts :: Module a -> [LAssertDecl] +getModuleAsserts = mapMaybe justAssert . moduleDecls + where + justAssert decl = case unLabel decl of + Assert a -> Just a + _ -> Nothing diff --git a/src/Language/CSPM/Frontend.hs b/src/Language/CSPM/Frontend.hs --- a/src/Language/CSPM/Frontend.hs +++ b/src/Language/CSPM/Frontend.hs @@ -1,8 +1,8 @@ ----------------------------------------------------------------------------- -- | -- Module : Language.CSPM.Frontend --- Copyright : (c) Fontaine 2008 --- License : BSD +-- Copyright : (c) Fontaine 2008 - 2011 +-- License : BSD3 -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental @@ -12,57 +12,73 @@ module Language.CSPM.Frontend ( - testFrontend + -- Language.CSPM.Parser + parse + ,ParseError(..) + + -- Language.CSPM.Utils ,parseFile + ,benchmarkFrontend + ,eitherToExc + ,handleLexError + ,handleParseError + ,handleRenameError + +-- Language.CSPM.Token ,Token + ,LexError(..) + +-- Language.CSPM.LexHelper ,Lexer.lexInclude ,Lexer.lexPlain ,Lexer.filterIgnoredToken - ,LexError(..) - ,parse - ,ParseError(..) + +-- Language.CSPM.AST ,Module - ,LModule - ,Labeled(..) + ,ModuleFromParser + ,ModuleFromRenaming + ,Labeled (..) + ,castModule + ,Bindings ,SrcLoc (..) + +-- Language.CSPM.Rename + ,renameModule + ,RenameInfo (..) ,getRenaming ,applyRenaming - -- AstUtils + ,RenameError (..) + +-- AstUtils ,removeSourceLocations ,removeParens ,removeModuleTokens ,unUniqueIdent ,showAst - ,relabelAst ,computeFreeNames - -- - ,RenameError(..) - ,eitherToExc - ,handleLexError - ,handleParseError - ,handleRenameError - ,compilePattern - ,version + ,setNodeIdsZero + +-- PrettyPrinter ,pp + ,prettyPrintFile ) where -import Language.CSPM.Parser (ParseError(..),parse) -import Language.CSPM.Rename (RenameError(..),getRenaming,applyRenaming) -import Language.CSPM.PatternCompiler (compilePattern) -import Language.CSPM.Token (Token,LexError(..)) -import Language.CSPM.AST (Labeled(..),LModule,Module(..),Bindings) +import Language.CSPM.Parser (ParseError(..), parse) +import Language.CSPM.Rename + (RenameError (..), RenameInfo (..), renameModule, getRenaming, applyRenaming + ,ModuleFromRenaming) +import Language.CSPM.Token (Token, LexError(..)) +import Language.CSPM.AST + (Labeled (..), Module (..), Bindings, castModule, ModuleFromParser) import Language.CSPM.SrcLoc (SrcLoc(..)) import Language.CSPM.AstUtils - (removeSourceLocations,removeModuleTokens,removeParens,relabelAst - ,unUniqueIdent,showAst,computeFreeNames) - + (removeSourceLocations, removeModuleTokens, removeParens + ,unUniqueIdent, showAst, computeFreeNames, setNodeIdsZero) import qualified Language.CSPM.LexHelper as Lexer - (lexInclude,lexPlain,filterIgnoredToken) -import Language.CSPM.Version - -import Language.CSPM.PrettyPrinter (pp) + (lexInclude, lexPlain, filterIgnoredToken) +import Language.CSPM.PrettyPrinter (pp, prettyPrintFile) import Language.CSPM.Utils - (eitherToExc,handleLexError,handleParseError,handleRenameError - ,parseFile,testFrontend) + (eitherToExc, handleLexError, handleParseError, handleRenameError + ,parseFile, benchmarkFrontend) diff --git a/src/Language/CSPM/LexHelper.hs b/src/Language/CSPM/LexHelper.hs --- a/src/Language/CSPM/LexHelper.hs +++ b/src/Language/CSPM/LexHelper.hs @@ -3,20 +3,20 @@ lexInclude ,lexPlain ,filterIgnoredToken - ,tokenIsIgnored ,tokenIsComment - ,tokenIsFDR ) where import qualified Language.CSPM.Lexer as Lexer (scanner) -import Language.CSPM.Token (Token(..), LexError(..) ) +import Language.CSPM.Token (Token(..), LexError(..)) import Language.CSPM.TokenClasses (PrimToken(..)) ---import qualified Language.CSPM.Token as Token --- (Token(..), LexError(..)) +import qualified Data.Set as Set -{- todo : use an error monad -} +-- | lex a String . +lexPlain :: String -> Either LexError [Token] +lexPlain src = fmap reverse $ Lexer.scanner src +-- | lex a String and process CSP-M include statements. lexInclude :: String -> IO (Either LexError [Token]) lexInclude src = do case Lexer.scanner src of @@ -27,9 +27,7 @@ Left err -> return $ Left err Right t -> return $ Right t -lexPlain :: String -> Either LexError [Token] -lexPlain src = fmap reverse $ Lexer.scanner src - +-- | Monsterfunction : todo refactor processIncludeAndReverse :: [Token] -> IO (Either LexError [Token] ) processIncludeAndReverse tokens = picl_acc tokens [] where @@ -53,21 +51,56 @@ } picl_acc (h:rest) acc = picl_acc rest $ h:acc +-- | remove newlines, that do not end a declaration from the token stream. +-- For example newlines next to binary operators. +soakNewlines :: [Token] -> [Token] +soakNewlines = worker + where + worker [] = [] + worker [x] = case tokenClass x of + L_Newline -> [] + _ -> [x] + worker (h1:h2:t) = case (tokenClass h1, tokenClass h2) of + (L_Newline, L_Newline) -> worker (h1:t) + (L_Newline, _) | isH2NewLineConsumer -> worker $ h2:t + (L_Newline, _) -> h1 : (worker $ h2:t) + (_, L_Newline) | isH1NewLineConsumer -> worker $ h1:t + (_, L_Newline) -> h1: (worker $ h2:t) + _ -> h1: (worker $ h2:t) + where + isH2NewLineConsumer = tokenClass h2 `Set.member` consumeNLBeforeToken + isH1NewLineConsumer = tokenClass h1 `Set.member` consumeNLAfterToken + binaryOperators = + [T_is, T_hat, T_hash, T_times, T_slash, + T_percent, T_plus, T_minus, T_eq, T_neq, + T_ge, T_le, T_not, T_amp, T_semicolon, + T_comma, T_triangle, T_box, T_rhd, T_exp, + T_sqcap, T_interleave, T_backslash, T_parallel, + T_mid, T_at, T_atat, T_rightarrow, T_leftarrow, + T_leftrightarrow, T_dot, T_dotdot, T_exclamation, + T_questionmark, T_colon, T_openBrack, T_closeBrack, + T_openOxBrack, T_closeOxBrack,T_openPBrace, + T_openBrackBrack, T_if, T_then,T_else, T_let, T_and, + T_or, T_Refine, T_trace,T_failure, T_failureDivergence, + T_refusalTesting, T_refusalTestingDiv, T_revivalTesting, + T_revivalTestingDiv,T_tauPriorityOp, T_within] + consumeNLBeforeToken + = Set.fromList ( + [T_closeParen, T_gt, T_closeBrace, T_closeBrackBrack, T_closePBrace] + ++ binaryOperators) + consumeNLAfterToken + = Set.fromList ( [T_openParen, T_openBrace, T_lt] ++ binaryOperators) + +-- | Remove comments and unneeded newlines. filterIgnoredToken :: [Token] -> [Token] -filterIgnoredToken = filter ( not . tokenIsIgnored) +filterIgnoredToken = soakNewlines . removeComments -tokenIsIgnored :: Token -> Bool -tokenIsIgnored (Token _ _ _ L_LComment _) = True -tokenIsIgnored (Token _ _ _ L_CSPFDR _) = True -tokenIsIgnored (Token _ _ _ L_BComment _) = True -tokenIsIgnored _ = False +-- | Remove comments from the token stream. +removeComments :: [Token] -> [Token] +removeComments = filter (not . tokenIsComment) +-- | Is the token a line-comment or block-comment ? tokenIsComment :: Token -> Bool -tokenIsComment (Token _ _ _ L_LComment _) = True -tokenIsComment (Token _ _ _ L_BComment _) = True -tokenIsComment _ = False - -tokenIsFDR :: Token -> Bool -tokenIsFDR (Token _ _ _ L_CSPFDR _) = True -tokenIsFDR _ = False +tokenIsComment t = tc == L_LComment || tc == L_BComment + where tc = tokenClass t diff --git a/src/Language/CSPM/Lexer.x b/src/Language/CSPM/Lexer.x --- a/src/Language/CSPM/Lexer.x +++ b/src/Language/CSPM/Lexer.x @@ -15,12 +15,12 @@ import Language.CSPM.AlexWrapper } -$whitechar = [\ \t\n\r\f\v] - +$whitechar = [\ \t\r\n\f\v] +$whitechar' = [\ \t\r\f\v] $digit = 0-9 $symbol = [\!\#\$\%\&\*\+\.\/\<\=\>\?\@\\\^\|\-\~\(\)\,\;\[\]\`\{\}\_\:\'] - +$symbol1 = [\_\'] --$large = [A-Z \xc0-\xd6 \xd8-\xde] --$small = [a-z \xdf-\xf6 \xf8-\xff \_] $large = [A-Z] @@ -28,8 +28,8 @@ $alpha = [$small $large] $graphic = [$small $large $symbol $digit] - -$octit = 0-7 +$graphic1 = [$small $large $symbol1 $digit] +$octit = 0-7 $hexit = [0-9 A-F a-f] $idchar = [$alpha $digit \' \_] @@ -40,12 +40,9 @@ @hexadecimal = $hexit+ @string = $graphic # [\"\\] | " " $whitechar - -@assertExts = $whitechar+ "[FD]" | $whitechar+ "[F]" -@assertCore = "deterministic" @assertExts? - | "livelock" $whitechar+ "free" @assertExts? - | "deadlock" $whitechar+ "free" @assertExts? - | "divergence" $whitechar+ "free" @assertExts? +@str = $graphic # [ \[ \] ] +@w = $whitechar* +$nl = [\n] csp :- @@ -56,14 +53,14 @@ <0> "subtype" { mkL T_subtype } <0> "assert" { mkL T_assert } <0> "pragma" { mkL T_pragma } -<0> "transparent" { mkL T_transparent } +<0> "transparent" { mkL T_transparent } <0> "external" { mkL T_external } -<0> "print" { mkL T_print } -<0> "if" { mkL T_if } -<0> "then" { mkL T_then } -<0> "else" { mkL T_else } -<0> "let" { mkL T_let } -<0> "within" { mkL T_within } +<0> "print" { mkL T_print } +<0> "if" { mkL T_if } +<0> "then" { mkL T_then } +<0> "else" { mkL T_else } +<0> "let" { mkL T_let } +<0> "within" { mkL T_within } -- CSP-M builtIns @@ -76,6 +73,7 @@ <0> "or" { mkL T_or } <0> "Int" { mkL T_Int } <0> "Bool" { mkL T_Bool } +<0> "Proc" { mkL T_Proc } <0> "Events" { mkL T_Events } <0> "CHAOS" { mkL T_CHAOS } <0> "union" { mkL T_union } @@ -96,6 +94,18 @@ <0> "elem" { mkL T_elem } <0> "length" { mkL T_length } +-- assetion Lists refinement operators +<0> "[=" { mkL T_Refine } +<0> "[T=" { mkL T_trace } +<0> "[F=" { mkL T_failure } +<0> "[FD=" { mkL T_failureDivergence } +<0> "[R=" { mkL T_refusalTesting } +<0> "[RD=" { mkL T_refusalTestingDiv } +<0> "[V=" { mkL T_revivalTesting } +<0> "[VD=" { mkL T_revivalTestingDiv } +<0> "[TP=" { mkL T_tauPriorityOp } +<0> ":[" { begin ref } -- jump to the other lexer specification ref + -- symbols <0> "^" { mkL T_hat } <0> "#" { mkL T_hash } @@ -108,7 +118,7 @@ <0> "!=" { mkL T_neq } <0> ">=" { mkL T_ge } <0> "<=" { mkL T_le } -<0> "<" { mkL T_lt } +<0> "<" { mkL T_lt } <0> ">" { mkL T_gt } <0> "&" { mkL T_amp } <0> ";" { mkL T_semicolon } @@ -116,6 +126,7 @@ <0> "/\" { mkL T_triangle } <0> "[]" { mkL T_box } <0> "[>" { mkL T_rhd } +<0> "|>" { mkL T_exp } <0> "|~|" { mkL T_sqcap } <0> "|||" { mkL T_interleave } <0> "\" { mkL T_backslash } @@ -145,14 +156,14 @@ <0> "=" { mkL T_is } <0> "[[" { mkL T_openBrackBrack } <0> "]]" { mkL T_closeBrackBrack } - -<0> $white+ { skip } -<0> "--".* { mkL L_LComment } -"{-" { block_comment } +<0> $nl { mkL L_Newline} +<0> $whitechar'+ { skip } +<0> "--".* { mkL L_LComment } +"{-" { block_comment } -- Fixme : tread this properly -<0> ":[" $whitechar* @assertCore $whitechar* "]" { mkL L_CSPFDR } + <0> "include" { mkL L_Include } <0> @ident { mkL L_Ident} -- ambiguity for wildcardpattern _ @@ -164,10 +175,21 @@ <0> \" @string* \" { mkL L_String } -<0> "[" $large + "=" { mkL T_Refine } -<0> "[=" { mkL T_Refine } - - + "deadlock" { mkL T_deadlock } + "deterministic" { mkL T_deterministic } + "livelock" { mkL T_livelock } + "divergence" { mkL T_livelock } + "free" { mkL T_free } + "[FD]" { mkL T_FD } + "[F]" { mkL T_F } + "[T]" { mkL T_T } + "tau" { mkL T_tau } + "priority" { mkL T_priority } + "over" { mkL T_over } + "]:" { begin 0 } + "]" { begin 0 } + $white+ { skip } + @str { skip } { alexMonadScan = do diff --git a/src/Language/CSPM/Parser.hs b/src/Language/CSPM/Parser.hs --- a/src/Language/CSPM/Parser.hs +++ b/src/Language/CSPM/Parser.hs @@ -1,26 +1,22 @@ ----------------------------------------------------------------------------- -- | -- Module : Language.CSPM.Parser --- Copyright : (c) Fontaine 2008 --- License : BSD +-- Copyright : (c) Fontaine 2008 - 2011 +-- License : BSD3 -- --- Maintainer : Fontaine@cs.uni-duesseldorf.de +-- Maintainer : fontaine@cs.uni-duesseldorf.de, me@dobrikov.biz -- Stability : experimental -- Portability : GHC-only -- --- This modules defines a Parser for CSPM +-- This modules defines a Parser for CSP-M -- ----------------------------------------------------------------------------- -{- todo: -* add Autoversion to packet -* add wrappers for functions that throw dynamic exceptions --} -{-# OPTIONS_GHC -fglasgow-exts #-} +{-# LANGUAGE DeriveDataTypeable #-} + module Language.CSPM.Parser ( parse ,ParseError(..) - ,PState() -- need to export this to satisfy haddock ) where import Language.CSPM.AST @@ -35,7 +31,7 @@ import Text.ParserCombinators.Parsec.ExprM import Text.ParserCombinators.Parsec - hiding (parse,eof,notFollowedBy,anyToken,label,ParseError,errorPos,token) + hiding (parse,eof,notFollowedBy,anyToken,label,ParseError,errorPos,token,newline) import Text.ParserCombinators.Parsec.Pos (newPos) import qualified Text.ParserCombinators.Parsec.Error as ParsecError import Data.Typeable (Typeable) @@ -44,7 +40,7 @@ import Prelude hiding (exp) import Control.Exception (Exception) -type PT a= GenParser Token PState a +type PT a = GenParser Token PState a -- | The 'parse' function parses a List of 'Token'. -- It returns a 'ParseError' or a 'Labled' 'Module'. @@ -52,11 +48,12 @@ parse :: SourceName -> [Token] - -> Either ParseError LModule + -> Either ParseError ModuleFromParser parse filename tokenList = wrapParseError tokenList $ runParser (parseModule tokenList) initialPState filename $ filterIgnoredToken tokenList +-- | ParseError data type. This is an instance of Excpetion data ParseError = ParseError { parseErrorMsg :: String ,parseErrorToken :: Token @@ -69,7 +66,7 @@ = PState { lastTok :: Token ,gtCounter :: Int - ,gtMode :: GtMode + ,gtLimit :: Maybe Int ,nodeIdSupply :: NodeId } deriving Show @@ -77,27 +74,23 @@ initialPState = PState { lastTok = Token.tokenSentinel ,gtCounter = 0 - ,gtMode = GtNoLimit + ,gtLimit = Nothing ,nodeIdSupply = mkNodeId 0 } -setGtMode :: GtMode-> PState -> PState -setGtMode mode env = env {gtMode = mode} - -countGt :: PState -> PState -countGt env = env {gtCounter = gtCounter env +1 } - -data GtMode=GtNoLimit | GtLimit Int deriving Show - -instance NodeIdSupply (GenParser Token PState) where - getNewNodeId = do - i <- gets nodeIdSupply - modify $ \s -> s { nodeIdSupply = succ $ nodeIdSupply s} - return i +mkLabeledNode :: SrcLoc -> t -> PT (Labeled t) +mkLabeledNode loc node = do + i <- getStates nodeIdSupply + updateState $ \s -> s { nodeIdSupply = succ $ nodeIdSupply s} + return $ Labeled { + nodeId = i + ,srcLoc = loc + ,unLabel = node } -instance MonadState PState (GenParser Token PState) where - get = getState - put = setState +getStates :: (PState -> x) -> PT x +getStates sel = do + st <- getState + return $ sel st getNextPos :: PT Token getNextPos = do @@ -135,13 +128,18 @@ e <- getLastPos mkLabeledNode (mkSrcSpan s e) $ constr l -parseModule :: [Token.Token] -> PT (Labeled Module) -parseModule tokenList = withLoc $ do - decl<-topDeclList - eof "end of module" - return $ Module { - moduleDecls = decl - ,moduleTokens = Just tokenList +parseModule :: [Token.Token] -> PT ModuleFromParser +parseModule tokenList = do + s <- getNextPos + skipMany newline + decl<-topDeclList + skipMany newline + eof "end of module" + e <- getLastPos + return $ Module { + moduleDecls = decl + ,moduleTokens = Just tokenList + ,moduleSrcLoc = mkSrcSpan s e } token :: TokenClasses.PrimToken -> PT () @@ -160,6 +158,23 @@ T_elem, T_length, T_CHAOS ] -} +newline :: PT () +newline = token L_Newline + +refineOp :: PT LRefineOp +refineOp = withLoc $ do + tok <- tokenPrimExDefault (\t -> Just $ tokenClass t) + case tok of + T_trace -> return Trace + T_failure -> return Failure + T_failureDivergence -> return FailureDivergence + T_refusalTesting -> return RefusalTesting + T_refusalTestingDiv -> return RefusalTestingDiv + T_revivalTesting -> return RevivalTesting + T_revivalTestingDiv -> return RevivalTestingDiv + T_tauPriorityOp -> return TauPriorityOp + _ -> fail "Unexpected Token" + anyBuiltIn :: PT Const anyBuiltIn = do tok <- tokenPrimExDefault (\t -> Just $ tokenClass t) @@ -184,13 +199,11 @@ T_CHAOS -> return F_CHAOS _ -> fail "not a built-in function" - blockBuiltIn :: PT a blockBuiltIn = do bi <- try anyBuiltIn fail $ "can not use built-in '"++ show bi ++ "' here" -- todo fix: better error -message - lIdent :: PT String lIdent = tokenPrimExDefault testToken @@ -215,6 +228,9 @@ sepBy1Comma :: PT x -> PT [x] sepBy1Comma a = sepBy1 a commaSeperator +sepByNewLine :: PT x -> PT [x] +sepByNewLine d = sepBy d newline + parseComprehension :: PT [LCompGen] parseComprehension = token T_mid >> sepByComma (compGenerator <|> compGuard ) @@ -238,7 +254,7 @@ repGenerator :: PT LCompGen repGenerator = try $ withLoc $ do pat <- parsePattern - token T_colon + (token T_colon) <|> (token T_leftarrow) exp <- parseExp_noPrefix return $ Generator pat exp @@ -279,7 +295,6 @@ token T_dotdot return $ RangeOpen s - closureExp :: PT LExp closureExp = withLoc $ do token T_openPBrace @@ -317,10 +332,10 @@ letExp :: PT LExp letExp = withLoc $ do token T_let - decl <- parseDeclList + declList <- sepByNewLine (funBind <|> patBind) token T_within exp <- parseExp - return $ Let decl exp + return $ Let declList exp ifteExp :: PT LExp ifteExp = withLoc $ do @@ -385,6 +400,7 @@ <|> withLoc ( token T_Events >> return Events) <|> withLoc ( token T_Bool >> return BoolSet) <|> withLoc ( token T_Int >> return IntSet) + <|> withLoc ( token T_Proc >> return ProcSet) <|> ifteExp <|> letExp <|> try litExp -- -10 is Integer(-10) @@ -469,6 +485,7 @@ ,[infixM (nfun2 T_box F_ExtChoice ) AssocLeft] ,[infixM (nfun2 T_rhd F_Timeout ) AssocLeft] ,[infixM (nfun2 T_sqcap F_IntChoice ) AssocLeft] + ,[infixM procOpException AssocLeft] ,[infixM (nfun2 T_interleave F_Interleave ) AssocLeft] ] ) @@ -500,12 +517,45 @@ posFromTo :: LExp -> LExp -> SrcLoc.SrcLoc posFromTo a b = SrcLoc.srcLocFromTo (srcLoc a) (srcLoc b) + procOpSharing :: PT (LProc -> LProc -> PT LProc) + procOpSharing = try $ do + spos <- getNextPos + al <- between ( token T_openOxBrack) (token T_closeOxBrack) parseExp + epos <- getLastPos + return $ (\a b -> mkLabeledNode (mkSrcSpan spos epos) $ ProcSharing al a b) + + procOpException :: PT (LProc -> LProc -> PT LProc) + procOpException = do + spos <- getNextPos + al <- between ( token T_openOxBrack) (token T_exp) parseExp + epos <- getLastPos + return $ (\a b -> mkLabeledNode (mkSrcSpan spos epos) $ ProcException al a b) + +{- +We count the occurences of gt-symbols +and accept it only if it is followed by an expression. +If a gtLimit is set, we only accept a maximum number of gt symbols +-} + gtSym :: PT () + gtSym = try $ do + token T_gt + updateState (\env -> env {gtCounter = gtCounter env +1 }) + next <- testFollows parseExp + case next of + Nothing -> fail "Gt token not followed by an expression" + Just _ -> do + mode <- getStates gtLimit + case mode of + Nothing -> return () + Just x -> do + cnt <- getStates gtCounter + if cnt < x then return () + else fail "(Gt token belongs to sequence expression)" + + parseExp :: PT LExp -parseExp = - (parseDotExpOf $ - buildExpressionParser procTable parseProcReplicatedExp --- buildExpressionParser opTable parseProcReplicatedExp - ) +parseExp + = (parseDotExpOf $ buildExpressionParser procTable parseProcReplicatedExp) "expression" @@ -544,23 +594,6 @@ pos <-getPos return $ (\fkt -> mkLabeledNode pos $ CallFunction fkt args ) - --- this is complicated and meight as well be buggy ! -gtSym :: PT () -gtSym = try $ do - token T_gt - updateState countGt --we count the occurences of gt-symbols - next <- testFollows parseExp -- and accept it only if it is followed by an expression - case next of - Nothing -> fail "Gt token not followed by an expression" - (Just _) -> do -- - mode <- getStates gtMode - case mode of - GtNoLimit -> return () - (GtLimit x) -> do - cnt <- getStates gtCounter - if cnt < x then return () - else fail "(Gt token belongs to sequence expression)" {- parse an sequenceexpression <...> we have to be carefull not to parse the end of sequence ">" @@ -591,29 +624,31 @@ return s {- parse an expression which contains as most count Greater-symbols (">" -used to leave the last ">" as end of sequence +the last ">" is left as end of sequence attention: this can be nested !! -} parseWithGtLimit :: Int -> PT a -> PT a parseWithGtLimit maxGt parser = do - oldLimit <- getStates gtMode - updateState $ setGtMode $ GtLimit maxGt + oldLimit <- getStates gtLimit + setGtLimit $ Just maxGt res <- optionMaybe parser - updateState $ setGtMode oldLimit + setGtLimit oldLimit case res of Just p -> return p Nothing -> fail "contents of sequence expression" + where + setGtLimit g = updateState $ \env -> env {gtLimit = g} proc_op_aparallel :: PT (LExp -> LExp -> PT LExp) proc_op_aparallel = try $ do s <- getNextPos token T_openBrack - a1<-parseExp_noPrefix + a1 <- parseExp_noPrefix token T_parallel - a2<-parseExp_noPrefix + a2 <- parseExp_noPrefix token T_closeBrack - e<-getLastPos + e <- getLastPos return $ (\p1 p2 -> mkLabeledNode (mkSrcSpan s e ) $ ProcAParallel a1 a2 p1 p2 ) proc_op_lparallel :: PT (LExp -> LExp -> PT LExp) @@ -723,36 +758,14 @@ exp <-parseExp return $ PatBind pat exp --- parse all fundefs and merge consecutive case alternatives -funBind :: PT [LDecl] -funBind = do - flist <-many1 sfun - -- group functioncases by the name of the function - let flgr = groupBy - (\a b -> (unIdent $ unLabel $ fst $ a) == (unIdent $ unLabel $ fst b)) - flist - mapM mkFun flgr - where - mkFun :: [(LIdent,(FunArgs,LExp))] -> PT LDecl - mkFun l = do - let - fname = fst $ head l - pos = srcLoc fname - cases = map ((uncurry FunCase) . snd ) l - mkLabeledNode pos $ FunBind fname cases - -- parse a single function-case -sfun :: PT (LIdent,(FunArgs,LExp)) -sfun = do - (fname,patl) <- try sfunHead +funBind :: PT LDecl +funBind = try $ do + fname <- ident + patl <- parseFktCurryPat token_is "rhs of function clause" exp <-parseExp - return (fname,(patl,exp)) - where - sfunHead = do - fname <- ident - patl <- parseFktCurryPat - return (fname,patl) + mkLabeledNode (srcLoc fname) $ FunBind fname [FunCase patl exp] {- in CSP f(x)(y), f(x,y) , f((x,y)) are all different @@ -768,63 +781,100 @@ parseFktCspPat :: PT [LPattern] parseFktCspPat = inParens $ sepByComma parsePattern -parseDeclList :: PT [LDecl] -parseDeclList = do - decl<- many1 parseDecl - return $ concat decl - - -singleList :: PT a -> PT [a] -singleList a = do - av <-a - return [av] - -{- -returns a list of decls -because funBind can't easily parse a single function -ToDo : PatBinds are actually different from varbind -example x={} with patbind will not be polymorphic --} -parseDecl :: PT [LDecl] -parseDecl = - funBind - <|> singleList patBind - "declaration" - topDeclList :: PT [LDecl] -topDeclList = do - decl<- many1 topDecl - return $ concat decl - where - - topDecl :: PT [LDecl] - topDecl = +topDeclList = sepByNewLine topDecl + where + topDecl :: PT LDecl + topDecl = choice + [ funBind - <|> singleList patBind - <|> singleList parseAssert - <|> singleList parseTransparent - <|> singleList parseDatatype - <|> singleList parseSubtype - <|> singleList parseNametype - <|> singleList parseChannel - <|> singleList parsePrint - "top-level declaration" + , patBind + , parseAssertDecl + , parseTransparent + , parseDatatype + , parseSubtype + , parseNametype + , parseChannel + , parsePrint + ] "top-level declaration" + + assertPolarity = fmap (odd . length) $ many $ token T_not - assertRef = withLoc $ do + assertListRef = withLoc $ do token T_assert - p1<-parseExp - op<- token T_Refine {- ToDo: fix this -} - p2<-parseExp - return $ AssertRef p1 "k" p2 + negated <- assertPolarity + p1 <- parseExp + op <- refineOp + p2 <- parseExp + return $ AssertRefine negated p1 op p2 assertBool = withLoc $ do token T_assert - b<-parseExp + b <- parseExp return $ AssertBool b - parseAssert :: PT LDecl - parseAssert = (try assertRef) <|> assertBool + assertTauPrio = withLoc $ do + token T_assert + negated <- assertPolarity + p1 <- parseExp + op <- tauRefineOp + p2 <- parseExp + token T_tau + token T_priority + token T_over + set <- parseExp + return $ AssertTauPrio negated p1 op p2 set + where + tauRefineOp :: PT LTauRefineOp + tauRefineOp = withLoc $ do + tok <- tokenPrimExDefault (\t -> Just $ tokenClass t) + case tok of + T_trace -> return TauTrace + T_Refine -> return TauRefine + _ -> fail "Unexpected Token" + assertIntFDRChecks = withLoc $ do + token T_assert + negated <- assertPolarity + p <- parseExp + model <- fdrModel + extmode <- many $ extsMode + ext <- case extmode of + [] -> return Nothing + [x] -> return $ Just x + _ -> fail "More than one model extension." + return $ AssertModelCheck negated p model ext + where + fdrModel :: PT LFDRModels + fdrModel = withLoc $ do + tok <- tokenPrimExDefault (\t -> Just $ tokenClass t) + case tok of + T_deadlock -> token T_free >> return DeadlockFree + T_deterministic -> return Deterministic + T_livelock -> token T_free >> return LivelockFree + _ -> fail "Modus is not supported by this parser." + + extsMode :: PT LFdrExt + extsMode = withLoc $ tokenPrimExDefault test + where + test tok = case tokenClass tok of + T_F -> Just F + T_FD -> Just FD + T_T -> Just T + _ -> Nothing + + parseAssert :: PT LAssertDecl + parseAssert = try assertTauPrio + <|> try assertIntFDRChecks + <|> try assertListRef + <|> assertBool + "assert Declaration" + + parseAssertDecl :: PT LDecl + parseAssertDecl = withLoc $ do + e <- parseAssert + return $ Assert e + parseTransparent :: PT LDecl parseTransparent = withLoc $ do token T_transparent @@ -860,7 +910,7 @@ token T_nametype i <- ident token_is - t<-typeExp + t <- typeExp return $ NameType i t parseChannel :: PT LDecl @@ -876,8 +926,7 @@ typeTuple = inSpan TypeTuple $ inParens $ sepBy1Comma parseExp - typeDot = inSpan TypeDot $ - sepBy1 parseExpBase $ token T_dot + typeDot = inSpan TypeDot $ sepBy1 parseExpBase $ token T_dot parsePrint :: PT LDecl parsePrint = withLoc $ do @@ -885,27 +934,21 @@ e <- parseExp return $ Print e -procOpSharing :: PT (LProc -> LProc -> PT LProc) -procOpSharing = do - spos <- getNextPos - al <- between ( token T_openOxBrack) (token T_closeOxBrack) parseExp - epos <- getLastPos - return $ (\a b -> mkLabeledNode (mkSrcSpan spos epos) $ ProcSharing al a b) - {- Replicated Expressions in Prefix form -} parseProcReplicatedExp :: PT LProc -parseProcReplicatedExp = do +parseProcReplicatedExp + = choice + [ procRep T_semicolon ProcRepSequence - <|> procRep T_sqcap ProcRepInternalChoice - <|> procRep T_box ProcRepExternalChoice - <|> procRep T_interleave ProcRepInterleave - <|> procRepAParallel - <|> procRepLinkParallel - <|> procRepSharing - <|> parsePrefixExp -- two calls make exponential blowup ! --- <|> parseExpBase -- - "parseProcReplicatedExp" + , procRep T_sqcap ProcRepInternalChoice + , procRep T_box ProcRepExternalChoice + , procRep T_interleave ProcRepInterleave + , procRepAParallel + , procRepLinkParallel + , procRepSharing + , parsePrefixExp + ] "parseProcReplicatedExp" where -- todo : refactor all these to using inSpan procRep :: TokenClasses.PrimToken -> (LCompGenList -> LProc -> Exp) -> PT LProc @@ -1001,12 +1044,6 @@ _ <- setParserState oldState return res -getStates :: (PState -> x) -> PT x -getStates sel = do - st <- getState - return $ sel st - - primExUpdatePos :: SourcePos -> Token -> t -> SourcePos primExUpdatePos pos t@(Token {}) _ = newPos (sourceName pos) (-1) (Token.unTokenId $ Token.tokenId t) @@ -1022,15 +1059,16 @@ anyToken :: PT Token anyToken = tokenPrimEx Token.showToken primExUpdatePos (Just primExUpdateState) Just +notFollowedBy :: GenParser tok st Token -> GenParser tok st () notFollowedBy p = try (do{ c <- p; unexpected $ Token.showToken c } <|> return () ) +notFollowedBy' :: GenParser tok st a -> GenParser tok st () notFollowedBy' p - = try (do{ p; pzero } - <|> return () - ) + = try $ ( p >> pzero ) <|> return () + eof :: PT () eof = notFollowedBy anyToken "end of input" @@ -1040,8 +1078,10 @@ "expecting" "unexpected" "end of input" (ParsecError.errorMessages err) - -wrapParseError :: [Token] -> Either ParsecError.ParseError LModule -> Either ParseError LModule +wrapParseError :: + [Token] + -> Either ParsecError.ParseError ModuleFromParser + -> Either ParseError ModuleFromParser wrapParseError _ (Right ast) = Right ast wrapParseError tl (Left err) = Left $ ParseError { parseErrorMsg = pprintParsecError err @@ -1051,7 +1091,6 @@ where tokId = Token.mkTokenId $ sourceColumn $ ParsecError.errorPos err errorTok = maybe Token.tokenSentinel id $ find (\t -> tokenId t == tokId) tl - token_is :: PT () token_is = token T_is diff --git a/src/Language/CSPM/PatternCompiler.hs b/src/Language/CSPM/PatternCompiler.hs deleted file mode 100644 --- a/src/Language/CSPM/PatternCompiler.hs +++ /dev/null @@ -1,160 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Language.CSPM.PatternCompiler --- Copyright : (c) Fontaine 2008 --- License : BSD --- --- Maintainer : fontaine@cs.uni-duesseldorf.de --- Stability : experimental --- Portability : GHC-only --- --- replace nested patterns with a set of linear Selectors --- todo : benchmark if it pays off to introduce --- helperbindings and only atomic bindings (unlikely) --- todo : add testcases -{-# LANGUAGE ViewPatterns #-} - -module Language.CSPM.PatternCompiler - ( - compilePattern - ) -where - -import Language.CSPM.AST as AST - -import Control.Monad -import Data.Generics.Schemes (everywhere') -import Data.Generics.Aliases (mkT) -import Data.Array.IArray - --- | replace all pattern in the module with list of linear Selectors -compilePattern :: LModule -> LModule -compilePattern ast - = Data.Generics.Schemes.everywhere' (Data.Generics.Aliases.mkT compPat) ast - where --- pattern that consist only of a variable match remain unchanged - compPat :: LPattern -> LPattern - compPat x@(unLabel -> VarPat {}) = x - compPat pat = case cp id pat of - [(i,s)] -> setNode pat $ Selector s i - x -> setNode pat $ Selectors { --- origPat = pat - selectors = listToArr $ map snd x - ,idents = listToArr $ map fst x - } - - listToArr :: [a] -> Array Int a - listToArr l = array (0,length l -1) $ zip [0..] l - - cp :: (Selector -> Selector ) -> LPattern -> [(Maybe LIdent,Selector)] - cp path pat = case unLabel pat of - IntPat i -> return (Nothing, path $ IntSel i) - TruePat -> return (Nothing, path TrueSel ) - FalsePat -> return (Nothing, path FalseSel ) - WildCard -> return (Nothing, path SelectThis ) - VarPat x -> return (Just x , path SelectThis ) - ConstrPat x -> return (Nothing, path $ ConstrSel $ unUIdent $ unLabel x) - Also l -> concatMap (cp path) l - Append l -> do - let (prefix,suffix,variable) = analyzeAppendPattern l - msum [ concatMap (mkListPrefixPat path) prefix - , mkListVariablePat path variable - , concatMap (mkListSuffixPat path) suffix ] - DotPat l -> msum $ map - (\(x,i) -> cp (path . DotSel i) x) - (zip l [0..]) - SingleSetPat p -> cp (path . SingleSetSel) p - EmptySetPat -> return (Nothing, path EmptySetSel) - ListEnumPat [] -> return (Nothing, path $ ListLengthSel 0 $ SelectThis ) - ListEnumPat l -> do - let len = length l - msum $ map - (\(x,i) -> cp (path . ListLengthSel len . ListIthSel i) x) - (zip l [0..]) - TuplePat [] -> return (Nothing, path $ TupleLengthSel 0 $ SelectThis ) - TuplePat l -> do - let len = length l - msum $ map - (\(x,i) -> cp (path . TupleLengthSel len . TupleIthSel i) x) - (zip l [0..]) - Selector {} -> error "PatternCompiler.hs : didn't expect Selector" - Selectors {} -> error "PatternCompiler.hs : didn't expect Selectors" - - mkListPrefixPat - :: (Selector -> Selector ) - -> (Offset,Len,LPattern) - -> [(Maybe LIdent,Selector)] - mkListPrefixPat path l = case l of - (0,1,pat) -> let (unLabel -> ListEnumPat [r]) = pat - in cp (path . HeadSel) r - (0,n,pat) -> cp (path . HeadNSel n) pat - (o,s,pat) -> cp (path . PrefixSel o s) pat - - mkListSuffixPat - :: (Selector -> Selector ) - -> (Offset,Len,LPattern) - -> [(Maybe LIdent,Selector)] - mkListSuffixPat path (o,l,pat) - = cp (path . SuffixSel o l) pat - - mkListVariablePat - :: (Selector -> Selector ) - -> Maybe (Offset,Offset,LPattern) - -> [(Maybe LIdent,Selector)] - mkListVariablePat _path Nothing = [] - mkListVariablePat path (Just (l,r,pat)) = cp (path . SliceSel l r) pat - -type Offset = Int -type Len = Int -analyzeAppendPattern :: - [LPattern] -> - ([(Offset,Len,LPattern)] -- prefixpattern - ,[(Offset,Len,LPattern)] -- suffixpattern - ,Maybe (Offset,Offset,LPattern) - ) -analyzeAppendPattern pl - = let - taggedPatList = zip pl $ map lengthOfListPattern pl - prefixPat = computePrefixPattern taggedPatList - suffixPat = computeSuffixPattern taggedPatList - lenPrefix = sum $ map (\(_,l,_)-> l) prefixPat - lenSuffix = sum $ map (\(_,l,_)-> l) suffixPat - varPat = case filter (\(_,len) -> len == Nothing) taggedPatList of - [] -> Nothing - [(pat,_)] -> Just (lenPrefix,lenSuffix,pat) - l -> error $ "PatternCompiler.hs : alsopattern contains multiple " - ++ "variable length pattern " - ++ show l - in - (prefixPat,suffixPat,varPat) - where -{- compute the length of a list pattern - Just Int -> fixed length pattern - Nothing -> variable length pattern -} - - lengthOfListPattern :: LPattern -> Maybe Len - lengthOfListPattern p = case unLabel p of - ListEnumPat l -> return $ length l - Append patl -> do - l <- mapM lengthOfListPattern patl - return $ sum l - VarPat _ -> Nothing - Also patl -> do - let l = map lengthOfListPattern patl - -- todo: check that all length are equal: - error "PatternCompiler.hs: lengthOfListPat : also pattern: todo" - _ -> error $ "PatternCompiler.hs: lengthOfListPat : no list pattern " - ++ show p -{- -PrefixPattern are fixed-length pattern with a fixed offset from the front -return when the first variable length pattern occurs --} - computePrefixPattern :: [(LPattern,Maybe Len)] -> [(Offset,Len,LPattern)] - computePrefixPattern l = worker 0 l where - worker _ [] = [] - worker _ ((_ ,Nothing ) : _) = [] - worker offset ((pat,Just len): rest) - = (offset,len,pat) : worker (offset+len) rest - - computeSuffixPattern :: [(LPattern,Maybe Len)] -> [(Offset,Len,LPattern)] - computeSuffixPattern = computePrefixPattern . reverse diff --git a/src/Language/CSPM/PrettyPrinter.hs b/src/Language/CSPM/PrettyPrinter.hs --- a/src/Language/CSPM/PrettyPrinter.hs +++ b/src/Language/CSPM/PrettyPrinter.hs @@ -1,266 +1,375 @@ - -{-# LANGUAGE TypeSynonymInstances #-} - -{-# OPTIONS_GHC - -XTypeSynonymInstances - -XScopedTypeVariables #-} - - - - ---------------------------------------------------------------------------- -- | -- Module : Language.CSPM.PrettyPrinter --- Copyright : (c) Dobrikov 2008 +-- Copyright : (c) Ivaylo Dobrikov 2010 -- License : BSD -- --- Maintainer : me@dobrikov.biz +-- Maintainer : Ivaylo Dobrikov (me@dobrikov.biz) -- Stability : experimental -- Portability : GHC-only --- +-- +-- This module defines functions for pretty-printing the +-- Abstract Syntax Tree to CSPM syntax. +----------------------------------------------------------------------------- + module Language.CSPM.PrettyPrinter +( + PP (..) +,prettyPrintFile +) where -import Text.PrettyPrint as PrettyPrint hiding (char) -import qualified Text.PrettyPrint as PrettyPrint -import Language.CSPM.AST -import Language.CSPM.Utils - -import Data.Maybe - +import Text.PrettyPrint -class PP x where pp :: x-> Doc +import Language.CSPM.AST +import Language.CSPM.Utils(parseFile) -mapPP :: PP x => [x] -> [Doc] -mapPP = map pp +-- | run the pretty printer on a file and write the output to +-- | filename.ast and filename.pretty +prettyPrintFile :: FilePath -> IO () +prettyPrintFile f = do + ast <- parseFile f + writeFile (f ++ ".ast") (show ast) + writeFile (f ++ ".pretty") $ render $ pp ast -instance (PP x) => PP (Labeled x) where - pp = pp . unLabel +-- | The pretty print class used for AST types +class PP x where + pp :: x -> Doc -instance PP Ident where pp = text . unIdent +instance (PP x) => PP (Labeled x) where + pp = pp . unLabel -instance PP Exp where pp = prettyExp +instance PP (Module a) where + pp m = vcat $ map pp (moduleDecls m) -prettyExp :: Exp -> Doc -prettyExp x = case x of - Var x -> pp x - IntExp x -> integer x - SetExp a Nothing -> braces $ pp x - SetExp a (Just comp) -> braces ( pp a <+> text "|" <+> hcatCommaSpace comp) - ListExp a Nothing -> text "<" <+> pp a <+> text ">" - ListExp a (Just comp) - -> text "<" <+> pp a <+> text "|" <+> hcatCommaSpace comp <+> text ">" - ClosureComprehension (x,l) -> text "{|" <+> (hcat $ punctuate comma $ map pp x) <+> text "|" <+> (hcat $ punctuate comma $ map pp l) <+> text "|}" - Parens x -> parens (pp x) - BoolSet -> text "Bool" - IntSet -> text "Int" - Events -> text "Events" - Stop -> text "STOP" - Skip -> text "SKIP" - CTrue -> text "true" - CFalse -> text "false" - TupleExp xlist -> parens (hcat $ punctuate comma (map pp xlist)) - DotTuple x -> hcat $ punctuate (text ".") $ map pp x - Closure x -> text "{|" <+> (hcat $ punctuate (comma <+> empty) $ map pp x) <+> text "|}" - CallBuiltIn x [list] -> pp x <> parens (hcat $ punctuate comma $ map pp list) - Ifte x y z -> text "if" <+> pp x <+> text "then" $$ pp y $$ text "else" <+> pp z - AndExp x y -> pp x <+> text "and" <+> pp y - OrExp x y -> pp x <+> text "or" <+> pp y - NotExp x -> text "not" <+> pp x - Fun1 x y -> pp x <> pp y - Fun2 fun x y -> pp x <+> pp fun <+> pp y - Lambda patt x -> text "\\" <+> (hcat $ punctuate (comma <+> empty) $ map pp patt) <+> text "@" <+> pp x - PrefixExp x l_comm_field y -> pp x <> (hcat $ map pp l_comm_field) <+> text "->" <+> pp y - ProcSharing x_middle x_left x_right -> pp x_left <+> text "[|" <+> pp x_middle <+> text "|]" <> pp x_right - Let decl x -> text "let" $$ (vcat $ map pp decl) $$ text "within" <+> pp x --- TODO CallFunction: produce not the correct output in file: protocol.fix.csp - CallFunction x [list] -> pp x <> parens (hcat $ punctuate (comma <+> empty) $ map pp list) - ProcLinkParallel list x y -> pp x <+> pp list <+> pp y - ProcAParallel x1 x2 x3 x4 -> pp x3 <+> brackets (pp x1 <+> text "||" <+> pp x2) <+> pp x4 --- ProcRepInterleave (Labeled _ list _ :: (Labeled [LCompGen])) proc -> text "|||" <+> (hcat $ punctuate (space <> colon <> space) $ map pp list) <+> text "@" <+> pp proc --- ProcRepChoice (Labeled _ list _ :: (Labeled [LCompGen])) proc -> text "[]" <+> (hcat $ punctuate (space <> colon <> space) $ map pp list) <+> text "@" <+> pp proc --- pp (ProcRepSharing list x x_proc) = pp x <> text "[|" <> comp_gen_list list <> text "|]" <> pp x_proc -- nicht in die Beispiele vorhanden - ProcRenaming rlist Nothing proc -> pp proc <+> text "[[" <+> (hsep $ punctuate (space <> comma <> space) $ map pp rlist) <+> text "]]" - ProcRenaming rlist (Just lcomp) proc - -> pp proc <+> text "[[" <+> (hsep $ punctuate (space <> comma <> space) $ map pp rlist) <+> text "|" <+> (hsep $ punctuate (space <> comma <> space) $ map pp $ unLabel lcomp) <+> text "]]" --- ProcRepAParallel (Labeled _ list _ :: (Labeled [LCompGen])) alph body --- -> text "||" <+> (hsep $ punctuate (space <> comma <> space) $ map pp list) <+> text "@" <+> brackets (pp alph) <+> pp body --- pp (ProcRepSharing (Labeled s list v) x proc) = --- ProcRepInternalChoice (Labeled _ list _ :: (Labeled [LCompGen])) proc --- -> text "|~|" <+> (hsep $ punctuate (space <> comma <> space) $ map pp list) <+> text "@" <+> pp proc +-- help functions for the Instances of the Type-class PP +dot :: Doc +dot = text "." -hcatComma :: PP x => [x] -> Doc -hcatComma a = hcat $ punctuate comma $ mapPP a +ppListSet :: (PP r) => String -> String -> r -> Maybe [LCompGen] -> Doc +ppListSet str1 str2 range mgen = + case mgen of + Nothing -> text str1 <+> pp range <+> text str2 + Just gen -> text str1 <+> pp range <+> text "|" <+> (hsep $ punctuate comma (map (ppCompGen False) gen)) <+> text str2 --- Ivo ? what is the difference between comma and (comma <+> empty) ? -hcatCommaSpace :: PP x => [x] -> Doc -hcatCommaSpace a = hcat $ punctuate (comma <+> empty) $ mapPP a - +hsepPunctuate :: (PP t) => Doc -> [t] -> Doc +hsepPunctuate s l = hsep $ punctuate s $ map pp l -instance PP Rename where - pp (Rename x y) = pp x <> text "<-" <> pp y +hcatPunctuate :: (PP t) => Doc -> [t] -> Doc +hcatPunctuate s l = hcat $ punctuate s $ map pp l -instance PP Range where - pp x = case x of - RangeEnum l -> hcatCommaSpace l - RangeOpen a -> pp a <+> text ".." - RangeClosed a b -> pp a <+> text ".." <+> pp b +printFunBind :: LIdent -> [FunCase] -> Doc +printFunBind ident lcase = vcat $ map (printIdent (unLabel ident) <>) (map printCase lcase) -instance PP CompGen where - pp (Generator patt x) = pp patt <> {-text "<-"-}colon <> pp x - pp (Guard x) = space <> pp x +printCase :: FunCase -> Doc +printCase c = case c of + FunCaseI pat expr -> (parens $ hcatPunctuate comma pat) <+> equals <+> pp expr + FunCase list expr -> (hcat $ map mkPat list) <+> equals <+> pp expr + where + mkPat l = parens $ hcatPunctuate comma l -comp_gen_list :: [LCompGen] -> Doc -comp_gen_list l = hcat $ punctuate empty (map pp l) +instance PP Decl where + pp d = case d of + PatBind pat expr -> pp pat <+> equals <+> (pp expr) + FunBind ident lcase -> printFunBind ident lcase + Assert a -> text "assert" <+> pp a + Transparent ids + -> text "transparent" <+> (hsep $ punctuate comma (map (printIdent . unLabel) ids)) + SubType ident constrs + -> text "subtype" <+> printIdent (unLabel ident) <+> equals + <+> (vcat $ punctuate (text "|") (map printConstr (map unLabel constrs))) + DataType ident constrs + -> text "datatype" <+> printIdent (unLabel ident) <+> equals + <+> (hsep $ punctuate (text "|") (map printConstr (map unLabel constrs))) + NameType ident typ + -> text "nametype" <+> printIdent (unLabel ident) <+> equals <+> typeDef typ + Channel ids t + -> text "channel" <+> (hsep $ punctuate comma $ map (printIdent . unLabel) ids) <+> typ + where + typ = case t of + Nothing -> empty + Just x -> text ":" <+> typeDef x + Print expr -> text "print" <+> pp expr +printFunArgs :: [[LExp]] -> Doc +printFunArgs = hcat . map (parens . hsepPunctuate comma) -instance PP BuiltIn where - pp (BuiltIn const) = pp const +-- Contructors +printConstr :: Constructor -> Doc +printConstr (Constructor ident typ) = printIdent (unLabel ident) <> + case typ of + Nothing -> empty + Just t -> dot <> typeDef t ---type LCompGenList = Labeled [LCompGen] +-- Type Definitions +typeDef :: LTypeDef -> Doc +typeDef typ = case unLabel typ of + TypeTuple e -> parens $ hcatPunctuate comma e + TypeDot e -> hcatPunctuate dot e ---instance PP LCompGenList => (Labeled [LCompGen]) where --- pp list = list . unLabel +instance PP Exp where + pp expression = case expression of + Var ident -> printIdent $ unLabel ident + IntExp i -> integer i + SetExp range mgen -> ppListSet "{" "}" range mgen + ListExp range mgen -> ppListSet "<" ">" range mgen + ClosureComprehension (lexp,lcomp) + -> ppListSet "{|" "|}" (labeled $ RangeEnum lexp) (Just lcomp) + Let ldecl expr -> vcat + [ + nest 2 (text "let") + ,vcat $ punctuate (text "" $$ nest 4 (text "")) (map pp ldecl) + ,nest 2 (text "within" <+> pp expr) + ] + Ifte expr1 expr2 expr3 -> vcat + [ + nest 2 $ text "if" <+> pp expr1 + ,nest 4 $ text "then" <+> pp expr2 + ,nest 4 $ text "else" <+> pp expr3 + ] + CallFunction expr list -> pp expr <> printFunArgs list + CallBuiltIn builtin [expr] -> pp builtin <> (parens $ hsepPunctuate comma expr) + CallBuiltIn _ _ -> error "pp Exp: builtin must exactly have one argument" + Lambda pat expr -> text "\\" <+> hsepPunctuate comma pat <+> text "@" <+> pp expr + Stop -> text "STOP" + Skip -> text "SKIP" + CTrue -> text "true" + CFalse -> text "false" + Events -> text "Events" + BoolSet -> text "Bool" + IntSet -> text "Int" + ProcSet -> text "Proc" + TupleExp e -> parens $ hsepPunctuate comma e + Parens e -> parens $ pp e + AndExp a b -> pp a <+> text "and" <+> pp b + OrExp a b -> pp a<+> text "or" <+> pp b + NotExp e -> text "not" <+> pp e + NegExp e -> text " " <> text "-" <> pp e + Fun1 builtin e -> pp builtin <> pp e + Fun2 builtin a b -> pp a <+> pp builtin <+> pp b + DotTuple l -> hcatPunctuate dot l + Closure e -> text "{|" <+> hsepPunctuate comma e <+> text "|}" -instance PP Decl where - pp (PatBind x y) = pp x <+> equals <+> pp y - pp (DataType ident list_constr) = text "datatype" <+> pp ident <+> equals <+> (hcat $ punctuate (space <> text "|" <> space) $ map pp list_constr) - pp (AssertRef x s y) = text "assert" <+> pp x <+> ptext s <+> pp y - pp (AssertBool x) = text "assert" <+> pp x <+> text ":[livelock free]" - pp (Channel list_x ty_ref) = text "channel" <+> (hcat $ punctuate (comma <> space) $ map pp list_x) <> if isEmpty (pp ty_ref) - then empty - else space <> colon <> space <> pp ty_ref - pp (FunBind ident list) = {-pp ident {-<> text "("-} <>-} (vcat $ punctuate empty $ map (pp ident <>) (map pp list)) --TODO - pp (SubType ident list_constr) = text "subtype" <+> pp ident <+> equals <+> (hcat $ punctuate (space <> text "|" <> space) $ map pp list_constr) - pp (NameType ident ty_ref) = text "nametype" <+> pp ident <+> equals <+> pp ty_ref - pp (Transparent list) = text "transparent" <+> (hcat $ punctuate (comma <> space) $ map pp list) - pp (Print x) = text "print" <+> pp x +-- process expressions + ProcSharing e p1 p2 -> pp p1 <> text "[|" <+> pp e <+> text "|]" <> pp p2 + ProcAParallel expr1 expr2 p1 p2 + -> pp p1 <> (brackets $ pp expr1 <+> text "||" <+> pp expr2) <> pp p2 + ProcLinkParallel llist p1 p2 -> pp p1 <> pp llist <> pp p2 + ProcRenaming renames mgen proc + -> pp proc <> text "[[" <+> hsepPunctuate comma renames <+> gens <+> text "]]" + where + gens = case mgen of + Nothing -> empty + Just lgen -> text "|" <+> (separateGen False (unLabel lgen)) + + ProcException e p1 p2 -> pp p1 <+> text "[|" <+> pp e <+> text "|>" <+> pp p2 + ProcRepSequence lgen proc -> replicatedProc (text ";") (unLabel lgen) proc + ProcRepInternalChoice lgen proc -> replicatedProc (text "|~|") (unLabel lgen) proc + ProcRepExternalChoice lgen proc -> replicatedProc (text "[]") (unLabel lgen) proc + ProcRepInterleave lgen proc -> replicatedProc (text "|||") (unLabel lgen) proc + PrefixExp expr fields proc + -> pp expr <> (hcat $ map pp fields) <+> text "->" <+> pp proc + ProcRepSharing lgen expr proc + -> text "[|" <+> pp expr <+> text "|]" + <+> (separateGen True (unLabel lgen)) <+> text "@" <+> pp proc + ProcRepAParallel lgen expr proc + -> text "||" <+> (separateGen True (unLabel lgen)) <+> text "@" + <+> (brackets $ pp expr) <+> pp proc + ProcRepLinkParallel lgen llist proc + -> pp llist <+> (separateGen True (unLabel lgen)) <+> text "@" <+> pp proc -instance PP Module where - pp m= vcat $ map pp (moduleDecls m) +-- only used in later stages +-- this do not affect the CSPM notation: same outputs as above + PrefixI _ expr fields proc -> pp expr <> (hcat $ map pp fields) <+> text "->" <+> pp proc + LetI decls _ expr -> hcat + [ + nest 2 $ text "let" + ,nest 4 $ hcat $ map pp decls + ,nest 2 $ text "within" <+> pp expr + ] + LambdaI _ pat expr + -> text "\\" <+> hsepPunctuate comma pat <+> text "@" <+> pp expr + ExprWithFreeNames _ expr -> pp expr -instance PP FunCase where - pp (FunCase [l_fun_args] x) = text "(" <> (hcat $ punctuate (comma <+> empty) $ map pp l_fun_args ) <> text ")" <+> equals <+> pp x +replicatedProc :: Doc -> [LCompGen] -> LProc -> Doc +replicatedProc op lgen proc = op <+> (separateGen True lgen) <+> text "@" <+> pp proc instance PP LinkList where - pp (LinkList list_link) = brackets (hcat $ punctuate (comma <+> empty) $ map pp list_link) + pp (LinkList list) = brackets $ hsepPunctuate comma list + pp (LinkListComprehension lgen list) + = brackets (hsepPunctuate comma list <+> text "|" <+> separateGen False lgen) instance PP Link where - pp (Link x y) = pp x <> text "<->" <> pp y + pp (Link expr1 expr2) = pp expr1 <+> text "<->" <+> pp expr2 -instance PP Constructor where - pp (Constructor ident ty_ref) = pp ident <> if isEmpty (pp ty_ref) - then empty - else {-text "." <>-} pp ty_ref +instance PP Rename where + pp (Rename expr1 expr2) = pp expr1 <+> text "<-" <+> pp expr2 -instance (PP x) => PP (Maybe x) where - pp (Just x) = pp x - pp Nothing = empty +separateGen :: Bool -> [LCompGen] -> Doc +separateGen b lgen = hsep $ punctuate comma $ map (ppCompGen b) lgen ---instance PP Funcase where -- siehe emptySet --- pp (Funcase [[arg]] x) = text "(" <> <> text ")" <+> equals <+> pp x +-- the generators of the comprehension sets, lists (all after the |) and +-- inside replicated processes (like "x: {1..10}", in this case the bool variable must be true, +-- otherwise false) +ppCompGen :: Bool -> LCompGen -> Doc +ppCompGen b gen = case unLabel gen of + (Generator pat expr) -> (pp pat) <+> case b of + False -> text "<-" <+> (pp expr) + True -> text ":" <+> (pp expr) + (Guard expr) -> pp expr -instance PP TypeDef where - pp (TypeTuple x) = text "." <> parens (hcat $ punctuate comma $ map pp x) - pp (TypeDot x) = (hcat $ punctuate (text ".") $ map pp x) +-- the range of sets and lists +instance PP Range where + pp r = case r of + RangeEnum expr -> hsepPunctuate comma expr + RangeClosed a b -> pp a <> text ".." <> pp b + RangeOpen expr -> pp expr <> text ".." -instance PP Pattern where - pp (IntPat x) = integer x - pp (VarPat x) = pp x - pp EmptySetPat = braces empty - pp WildCard = text "_" - pp (SingleSetPat patt) = brackets (pp patt) - pp (ListEnumPat list) = text "<" <> (hcat $ (punctuate (comma) $ map pp list)) <> text ">" - pp (TuplePat list) = parens (hcat $ (punctuate (comma) $ map pp list)) - pp (DotPat list) = hcat $ punctuate (text ".") $ map pp list +-- unwrapp the BuiltIn-oparator +instance PP BuiltIn where + pp (BuiltIn c) = pp c +-- the communication fields instance PP CommField where - pp (InComm x) = space <> text "?" <+> pp x - pp (OutComm x) = empty <> text "."{-"!"-} <> pp x - pp (InCommGuarded pattern x {-LPattern LExp-}) = space <> text "?" <+> pp pattern <+> colon <+> pp x + pp (InComm pat) = text "?" <> pp pat + pp (InCommGuarded pat expr) = text "?" <> pp pat <> text ":" <> pp expr + pp (OutComm expr) = text "!" <> pp expr -instance PP Const where - pp F_true = text "true" - pp F_false = text "false" - pp F_not = text "not" - pp F_and = text "and" - pp F_or = text "or" - pp F_STOP = text "STOP" - pp F_SKIP = text "SKIP" - pp F_Mult = text "*" - pp F_Div = colon - pp F_Add = text "+" - pp F_Sub = text "-" - pp F_Eq = text "==" - pp F_NEq = text "!=" - pp F_ExtChoice = text "[]" - pp F_Union = text "Union" - pp F_concat = text "concat" - pp F_Concat = text "^" - pp F_union = text "union" - pp F_inter = text "inter" - pp F_diff = text "diff" - pp F_Inter = text "Inter" - pp F_member = text "member" - pp F_card = text "card" - pp F_empty = text "empty" - pp F_set = text "set" - pp F_Set = text "Set" - pp F_null = text "null" - pp F_Seq = text "Seq" - pp F_head = text "head" - pp F_tail = text "tail" - pp F_elem = text "elem" - pp F_Events = text "Events" - pp F_Int = text "Int" - pp F_Bool = text "Bool" - pp F_GE = text ">=" - pp F_LE = text "<=" - pp F_LT = text "<" - pp F_GT = text ">" - pp F_Sequential = text "Sequential" - pp F_Guard = text "&" - pp F_Interrupt = text "/\\" - pp F_Len2 = text "#" - pp F_CHAOS = text "CHAOS" - pp F_Timeout = text "[>" - pp F_IntChoice = text "|~|" - pp F_Interleave = text "|||" - pp F_Hiding = text "\\" - pp F_length = text "length" - pp F_Mod = text "%" +-- pretty-printing for CSPM-Patterns +instance PP Pattern where + pp pattern = case pattern of + IntPat n -> integer n + TruePat -> text "true" + FalsePat -> text "false" + WildCard -> text "_" + ConstrPat ident -> printIdent $ unLabel ident + Also pat -> ppAlso (Also pat) + Append pat -> hcatPunctuate (text "^") pat + DotPat [] -> error "pp Pattern: empty dot pattern" + DotPat [pat] -> pp pat + DotPat l -> hcat $ punctuate dot $ map nestedDotPat l + SingleSetPat pat -> text "{" <+> (pp pat) <+> text "}" + EmptySetPat -> text "{ }" + ListEnumPat pat -> text "<" <+> hsepPunctuate comma pat <+> text ">" + TuplePat pat -> text "(" <> hsepPunctuate comma pat <> text ")" + VarPat ident -> printIdent $ unLabel ident + Selectors _ _ -> error "pp Pattern Seclectors" + Selector _ _ -> error "pp Pattern Seclector" + where + nestedDotPat p = case unLabel p of + DotPat {} ->parens $ pp p + x -> pp x -to_PString :: LModule -> String -to_PString my_mod = render (pp my_mod) +-- external function for Also-Patterns for a better look +ppAlso :: Pattern -> Doc +ppAlso (Also []) = text "" +ppAlso (Also (h:t)) = + case unLabel h of + DotPat _ -> if length t > 0 then (pp h) <> text "@@" <> ppAlso (Also t) + else pp h + Append _ -> if length t > 0 then (pp h) <> text "@@" <> ppAlso (Also t) + else pp h + _ -> if length t > 0 then pp h <> text "@@" <> ppAlso (Also t) + else pp h +ppAlso _ = text "" +-- disticts the cases for different syntax-records for the Ident datatype +printIdent :: Ident -> Doc +printIdent ident = + case ident of + Ident _ -> text $ unIdent ident + UIdent _ -> text $ realName $ unUIdent ident -runPretty :: FilePath -> IO String -runPretty fname = - do - my_mod <- parseFile fname - return (to_PString my_mod) --(render (pp mod)) +instance PP AssertDecl where + pp a = case a of + AssertBool expr -> pp expr + AssertRefine n expr1 op expr2 + -> negated n $ pp expr1 <+> pp op <+> pp expr2 + AssertTauPrio n expr1 op expr2 expr3 + -> negated n $ pp expr1 <+> pp op <+> pp expr2 <+> text ":[tau priority over]:" <+> pp expr3 + AssertModelCheck n expr m mb + -> negated n $ pp expr <+> text ":[" <+> pp m <+> maybe empty pp mb <+> text "]" + where + negated ar doc = if ar then text "not" <+> doc else doc -compareTrees :: FilePath -> IO Bool -compareTrees file = - do - parsedFile <- parseFile file - let prettyFile = to_PString parsedFile - writeFile (file ++ ".pp") prettyFile - secondPFile <- parseFile file - if (parsedFile == secondPFile) - then - return True - else - return False +instance PP FdrExt where + pp F = text "[F]" + pp FD = text "[FD]" + pp T = text "[T]" -simpleCompare :: FilePath -> FilePath -> IO Bool -simpleCompare file1 file2 = - do - tree1 <- readFile file1 - tree2 <- readFile file2 - if (tree1 == tree2) - then - return True - else - return False +instance PP FDRModels where + pp DeadlockFree = text "deadlock free" + pp Deterministic = text "deterministic" + pp LivelockFree = text "livelock free" +instance PP RefineOp where + pp Trace = text "[T=" + pp Failure = text "[F=" + pp FailureDivergence = text "[FD=" + pp RefusalTesting = text "[R=" + pp RefusalTestingDiv = text "[RD=" + pp RevivalTesting = text "[V=" + pp RevivalTestingDiv = text "[VD=" + pp TauPriorityOp = text "[TP=" + +instance PP TauRefineOp where + pp TauTrace = text "[T=" + pp TauRefine = text "[=" + +instance PP Const where +-- Booleans + pp F_true = text "true" + pp F_false = text "false" + pp F_not = text "not" + pp F_and = text "and" + pp F_or = text "or" +-- Numbers + pp F_Mult = text "*" + pp F_Div = text "/" + pp F_Mod = text "%" + pp F_Add = text "+" + pp F_Sub = text "" <+> text "-" +-- Equality + pp F_GE = text ">=" + pp F_LE = text "<=" + pp F_LT = text "<" + pp F_GT = text ">" + pp F_Eq = text "==" + pp F_NEq = text "!=" +-- Sets + pp F_union = text "union" + pp F_inter = text "inter" + pp F_diff = text "diff" + pp F_Union = text "Union" + pp F_Inter = text "Inter" + pp F_member = text "member" + pp F_card = text "card" + pp F_empty = text "empty" + pp F_set = text "set" + pp F_Set = text "Set" + pp F_Seq = text "Seq" +-- Types + pp F_Int = text "Int" + pp F_Bool = text "Bool" +--Sequences + pp F_null = text "null" + pp F_head = text "head" + pp F_tail = text "tail" + pp F_concat = text "concat" + pp F_elem = text "elem" + pp F_length = text "length" + pp F_Concat = text "^" + pp F_Len2 = text "#" +--process oprators + pp F_STOP = text "STOP" + pp F_SKIP = text "SKIP" + pp F_Events = text "Events" + pp F_CHAOS = text "CHAOS" + pp F_Guard = text "&" + pp F_Sequential = text ";" + pp F_Interrupt = text "/\\" + pp F_ExtChoice = text "[]" + pp F_IntChoice = text "|~|" + pp F_Hiding = text "\\" + pp F_Timeout = text "[>" + pp F_Interleave = text "|||" diff --git a/src/Language/CSPM/Rename.hs b/src/Language/CSPM/Rename.hs --- a/src/Language/CSPM/Rename.hs +++ b/src/Language/CSPM/Rename.hs @@ -1,9 +1,8 @@ -{-# LANGUAGE DeriveDataTypeable #-} ----------------------------------------------------------------------------- -- | -- Module : Language.CSPM.Rename --- Copyright : (c) Fontaine 2008 --- License : BSD +-- Copyright : (c) Fontaine 2008 - 2011 +-- License : BSD3 -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : experimental @@ -19,18 +18,26 @@ todo :: check idType in useIdent fix topleveldecls to toplevel ? -> allready done by parser -} + +{-# LANGUAGE EmptyDataDecls, DeriveDataTypeable #-} + module Language.CSPM.Rename ( - getRenaming + renameModule + ,getRenaming ,applyRenaming - ,RenameError(..) + ,RenameError (..) + ,RenameInfo (..) + ,ModuleFromRenaming + ,FromRenaming ) where - -import Language.CSPM.AST hiding (prologMode,bindType) +import Language.CSPM.AST hiding (prologMode, bindType) import qualified Language.CSPM.AST as AST import qualified Language.CSPM.SrcLoc as SrcLoc +import Data.Generics.Basics (Data(..)) +import Data.Data (mkDataType) import Data.Generics.Schemes (everywhere) import Data.Generics.Aliases (mkT) import Data.Typeable (Typeable) @@ -39,30 +46,57 @@ import Control.Monad.Error import Control.Monad.State import Data.Set (Set) -import qualified Data.Set as Set import qualified Data.Map as Map +import qualified Data.Set as Set import qualified Data.IntMap as IntMap +import Data.List as List +instance Data FromRenaming + where + gunfold = error "instance Data FromRenaming gunfold" + toConstr = error "instance Data FromRenaming toConstr" + dataTypeOf _ = mkDataType "Language.CSPM.Rename.FromRenaming" [] + +-- | A module that has gone through renaming +type ModuleFromRenaming = Module FromRenaming +{-# DEPRECATED applyRenaming, getRenaming "use renameModule instead" #-} + +-- | Tag that a module has gone through renameing. +data FromRenaming deriving Typeable + +-- | 'renameModule' renames a 'Module'. +-- | (also calls mergeFunBinds) +renameModule :: + ModuleFromParser + -> Either RenameError (ModuleFromRenaming, RenameInfo) +renameModule m = do + let m' = mergeFunBinds m + st <- execStateT (rnModule m') initialRState + return + ( + applyRenamingNew m' (identDefinition st) (identUse st) + ,st) + -- | 'getRenaming' computes two 'AstAnnotation's. -- The first one contains all the defining occurences of identifier -- The second one contains all the using occurences of identitier. -- 'getRename' returns an 'RenameError' if the 'Module' contains unbound -- identifiers or illegal redefinitions. getRenaming :: - LModule - -> Either RenameError (Bindings,AstAnnotation UniqueIdent,AstAnnotation UniqueIdent) -getRenaming m - = case execStateT (rnModule m) initialRState of - Right state -> Right (visible state,identDefinition state, identUse state) - Left e -> Left e + ModuleFromParser + -> Either RenameError (Bindings, AstAnnotation UniqueIdent, AstAnnotation UniqueIdent) +getRenaming m = do + st <- execStateT (rnModule m) initialRState + return (visible st,identDefinition st, identUse st) -type RM x = StateT RState (Either RenameError) x +type RM x = StateT RenameInfo (Either RenameError) x type UniqueName = Int -data RState = RState +-- | Gather all information about an renaming. +data RenameInfo = RenameInfo { - nameSupply :: UniqueName + nameSupply :: Int -- used to check that we do not bind a name twice inside a pattern ,localBindings :: Bindings ,visible :: Bindings -- everything that is visible @@ -73,8 +107,8 @@ ,bindType :: BindType } deriving Show -initialRState :: RState -initialRState = RState +initialRState :: RenameInfo +initialRState = RenameInfo { nameSupply = 0 ,localBindings = Map.empty @@ -225,8 +259,8 @@ nop :: RM () nop = return () -rnModule :: LModule -> RM () -rnModule m = rnDeclList $ moduleDecls $ unLabel m +rnModule :: ModuleFromParser -> RM () +rnModule = rnDeclList . moduleDecls rnExpList :: [LExp] -> RM () rnExpList = mapM_ rnExp @@ -253,6 +287,7 @@ Events -> nop BoolSet -> nop IntSet -> nop + ProcSet -> nop TupleExp l -> rnExpList l Parens a -> rnExp a AndExp a b -> rnExp a >> rnExp b @@ -269,6 +304,7 @@ ProcRenaming rlist gen proc -> case gen of Nothing -> mapM_ reRename rlist >> rnExp proc Just comp -> inCompGenL comp (mapM_ reRename rlist) >> rnExp proc + ProcException p1 e p2 -> rnExp p1 >> rnExp e >> rnExp p2 ProcRepSequence a p -> inCompGenL a (rnExp p) ProcRepInternalChoice a p -> inCompGenL a (rnExp p) ProcRepInterleave a p -> inCompGenL a (rnExp p) @@ -320,7 +356,7 @@ rnCommField :: LCommField -> RM () rnCommField f = case unLabel f of InComm pat -> rnPattern pat - InCommGuarded p g -> rnPattern p >> rnExp g + InCommGuarded p g -> rnExp g >> rnPattern p OutComm e -> rnExp e inCompGenL :: LCompGenList -> RM () -> RM () @@ -365,8 +401,7 @@ PatBind pat _ -> rnPattern pat --todo : proper type-checking/counting number of Funargs FunBind i _ -> bindNewUniqueIdent (FunID (-1)) i - AssertRef {} -> nop - AssertBool {} -> nop + Assert {} -> nop Transparent tl -> mapM_ (bindNewTopIdent TransparentID) tl SubType i clist -> do bindNewTopIdent DataTypeID i -- fix this @@ -392,8 +427,11 @@ declRHS d = case unLabel d of PatBind _ e -> rnExp e FunBind _ cases -> mapM_ rnFunCase cases - AssertRef a _ b -> rnExp a >> rnExp b - AssertBool e -> rnExp e + Assert a -> case unLabel a of + AssertBool e -> rnExp e + AssertRefine _ p1 _ p2 -> rnExp p1 >> rnExp p2 + AssertTauPrio _ p1 _ p2 e -> rnExp p1 >> rnExp p2 >> rnExp e + AssertModelCheck _ p _ _ -> rnExp p Transparent _ -> nop SubType _ clist -> forM_ clist rnConstructorRHS DataType _ clist -> forM_ clist rnConstructorRHS @@ -423,10 +461,18 @@ -- the 'AstAnnotation's. applyRenaming :: (Bindings,AstAnnotation UniqueIdent,AstAnnotation UniqueIdent) - -> LModule - -> LModule + -> ModuleFromParser + -> ModuleFromRenaming applyRenaming (_,defIdent,usedIdent) ast - = everywhere (mkT patchVarPat . mkT patchIdent) ast + = applyRenamingNew ast defIdent usedIdent + +applyRenamingNew :: + ModuleFromParser + -> AstAnnotation UniqueIdent + -> AstAnnotation UniqueIdent + -> ModuleFromRenaming +applyRenamingNew ast defIdent usedIdent + = castModule $ everywhere (mkT patchVarPat . mkT patchIdent) ast where patchIdent :: LIdent -> LIdent patchIdent l = @@ -442,3 +488,35 @@ VarID -> p _ -> ConstrPat x patchVarPat x = x + +-- | If function is defined via pattern matching for serveral cases, +-- | the parser returns each case as a individual declaration. +-- | mergeFunBinds merges contiguous cases of the same function into one declaration. +mergeFunBinds :: ModuleFromParser -> ModuleFromParser +mergeFunBinds = everywhere (mkT patchModule . mkT patchLet) + where + patchModule :: ModuleFromParser -> ModuleFromParser + patchModule m = m {moduleDecls = mergeDecls $ moduleDecls m} + + patchLet :: Exp -> Exp + patchLet (Let decls expr) = Let (mergeDecls decls) expr + patchLet x = x + + mergeDecls :: [LDecl] -> [LDecl] + mergeDecls = map joinGroup . List.groupBy sameFunction + + sameFunction a b = case (unLabel a, unLabel b) of + (FunBind n1 _, FunBind n2 _) -> unLabel n1 == unLabel n2 + _ -> False + + joinGroup :: [LDecl] -> LDecl + joinGroup l@(firstCase : _) = case unLabel firstCase of + FunBind fname _ -> setNode firstCase $ FunBind fname $ map getFunCase l + _ -> firstCase + joinGroup [] = error "unreachable : groupBy empty group ?" + + getFunCase :: LDecl -> FunCase + getFunCase d = case unLabel d of + FunBind _ [funCase] -> funCase + FunBind _ _ -> error "mergeFunBinds: function already has several cases !" + _ -> error "mergeFunBinds : internal error" diff --git a/src/Language/CSPM/Token.hs b/src/Language/CSPM/Token.hs --- a/src/Language/CSPM/Token.hs +++ b/src/Language/CSPM/Token.hs @@ -8,7 +8,7 @@ -- Stability : provisional -- Portability : GHC-only -- --- This module contains the datatype Tokens. +-- This module contains the data type Tokens and some helper functions {-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving #-} @@ -24,7 +24,7 @@ import Control.Exception (Exception) newtype TokenId = TokenId {unTokenId :: Int} - deriving (Show,Eq,Ord,Enum,Ix, Typeable, Data) + deriving (Show, Eq, Ord, Enum, Ix, Typeable, Data) mkTokenId :: Int -> TokenId mkTokenId = TokenId @@ -59,7 +59,7 @@ , tokenLen :: Int , tokenClass :: PrimToken , tokenString :: String - } deriving (Show,Eq,Ord, Typeable, Data) + } deriving (Show, Eq, Ord, Typeable, Data) tokenSentinel :: Token tokenSentinel = Token @@ -73,5 +73,4 @@ showPosn (AlexPn _ line col) = show line ++ ':': show col showToken :: Token -> String -showToken Token {tokenString=str} = "'"++str++"'" - +showToken Token {tokenString = str} = "'" ++ str ++ "'" diff --git a/src/Language/CSPM/TokenClasses.hs b/src/Language/CSPM/TokenClasses.hs --- a/src/Language/CSPM/TokenClasses.hs +++ b/src/Language/CSPM/TokenClasses.hs @@ -1,14 +1,14 @@ ----------------------------------------------------------------------------- -- | -- Module : Language.CSPM.TokenClasses --- Copyright : (c) Fontaine 2008 +-- Copyright : (c) Fontaine 2008 - 2011 -- License : BSD -- -- Maintainer : Fontaine@cs.uni-duesseldorf.de -- Stability : provisional -- Portability : GHC-only -- --- This module contains the datatype Tokens. +-- This module contains the data type PrimToken. {-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving #-} @@ -19,16 +19,16 @@ import Data.Generics.Basics (Data) import Data.Generics.Instances () +-- | The token classes of the CSP-M lexer data PrimToken = L_Integer | L_String | L_Ident - | L_CSPFDR -- needed for special assertions | L_LComment | L_BComment | L_EOF | L_Include - | T_Refine + | L_Newline -- keywords | T_channel | T_datatype @@ -71,6 +71,7 @@ | T_SKIP | T_Events | T_Int + | T_Proc | T_Bool | T_CHAOS -- symbols @@ -93,6 +94,7 @@ | T_triangle -- "/\\" | T_box -- "[]" | T_rhd -- "[>" + | T_exp -- "|>" | T_sqcap -- "|~|" | T_interleave -- "|||" | T_backslash -- "\\" @@ -114,6 +116,7 @@ | T_closeBrace -- "}" | T_openBrack -- "[" | T_closeBrack -- "]" + | T_startAssert -- ":[" | T_openOxBrack -- "[|" | T_closeOxBrack -- "|]" | T_openBrackBrack -- "[[" @@ -122,4 +125,24 @@ | T_closePBrace -- "|}" | T_underscore -- "_" | T_is -- "=" +-- assert List refinement Operators + | T_Refine -- "[=" + | T_trace -- "[T=" + | T_failure -- "[F=" + | T_failureDivergence -- "[FD=" + | T_refusalTesting -- "[R=" + | T_refusalTestingDiv -- "[RD=" + | T_revivalTesting -- "[V=" + | T_revivalTestingDiv -- "[VD=" + | T_tauPriorityOp -- "[TP=" + | T_tau + | T_priority + | T_over + | T_deadlock + | T_deterministic + | T_livelock + | T_free + | T_F + | T_T + | T_FD deriving (Show,Eq,Ord,Typeable, Data) diff --git a/src/Language/CSPM/Utils.hs b/src/Language/CSPM/Utils.hs --- a/src/Language/CSPM/Utils.hs +++ b/src/Language/CSPM/Utils.hs @@ -15,15 +15,14 @@ ,handleLexError ,handleParseError ,handleRenameError - ,parseFile,testFrontend) + ,parseFile, benchmarkFrontend, parseString) where -import Language.CSPM.Parser (ParseError(..),parse) -import Language.CSPM.Rename (RenameError(..),getRenaming,applyRenaming) -import Language.CSPM.Token (Token, LexError(..)) -import Language.CSPM.AST (LModule) -import qualified Language.CSPM.LexHelper as Lexer - (lexInclude,lexPlain,filterIgnoredToken) +import Language.CSPM.Parser (ParseError(..), parse) +import Language.CSPM.Rename (RenameError(..), renameModule, ModuleFromRenaming) +import Language.CSPM.Token (LexError(..)) +import Language.CSPM.AST (ModuleFromParser) +import qualified Language.CSPM.LexHelper as Lexer (lexInclude) import Control.Exception as Exception import System.CPUTime @@ -46,14 +45,24 @@ handleRenameError handler proc = Exception.catch proc handler -- | Lex and parse a file and return a "LModule", throw an exception in case of an error -parseFile :: FilePath -> IO LModule +parseFile :: FilePath -> IO ModuleFromParser parseFile fileName = do src <- readFile fileName - tokenList <- Lexer.lexInclude src >>= eitherToExc - eitherToExc $ parse fileName tokenList + parseNamedString fileName src -testFrontend :: FilePath -> IO (LModule,LModule) -testFrontend fileName = do +-- | Small test function which just parses a String. +parseString :: String -> IO ModuleFromParser +parseString = parseNamedString "no-file-name" + +parseNamedString :: FilePath -> String -> IO ModuleFromParser +parseNamedString name str = do + tokenList <- Lexer.lexInclude str >>= eitherToExc + eitherToExc $ parse name tokenList + +-- | Lex and parse File. +-- | Return the module and print some timing infos +benchmarkFrontend :: FilePath -> IO (ModuleFromParser, ModuleFromRenaming) +benchmarkFrontend fileName = do src <- readFile fileName putStrLn $ "Reading File " ++ fileName @@ -64,8 +73,7 @@ ast <- eitherToExc $ parse fileName tokenList time_have_ast <- getCPUTime - renaming <- eitherToExc $ getRenaming ast - let astNew = applyRenaming renaming ast + (astNew, _renaming) <- eitherToExc $ renameModule ast time_have_renaming <- getCPUTime putStrLn $ "Parsing OK" diff --git a/src/Language/CSPM/Version.hs b/src/Language/CSPM/Version.hs deleted file mode 100644 --- a/src/Language/CSPM/Version.hs +++ /dev/null @@ -1,48 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Language.CSPM.Version --- Copyright : (c) Fontaine 2008 --- License : BSD --- --- Maintainer : Fontaine@cs.uni-duesseldorf.de --- Stability : experimental --- Portability : GHC-only --- --- Use Template Haskell to gather some info a compile-time. --- (Template-Haskell makes problems with haddock) -{-# LANGUAGE TemplateHaskell #-} -module Language.CSPM.Version -( - version -) -where - -import qualified Paths_CSPM_Frontend as Paths -import Language.Haskell.TH -import System.Time -import System.Info -import Data.List ---import Network.BSD --check if this is the reason why we have to link to network ? -import Data.Version - --- | "version" returns a "String" with some info about the, on which the libray was built. -version :: IO String -version = return $( let - mkVersion :: IO String - mkVersion = do - timeDate <- getClockTime --- hn <- getHostName - let sysInfo = concat $ intersperse " " [ - "CSPM-Fronted" - ,show Paths.version - ,"\nCompiled at",show timeDate --- ,"\non",hn - ,"\n(",os,arch,compilerName,showVersion compilerVersion ,")" - ] - putStrLn "\n\n" - putStrLn "version :" - putStrLn sysInfo - putStrLn "\n\n" - return sysInfo - in stringE =<< runIO mkVersion - )