CSPM-Frontend 0.4.1.1 → 0.6.8.0

raw patch · 15 files changed

+1016/−879 lines, 15 filesdep +parsec2dep −haskell98dep −old-timedep −parsecdep ~containersdep ~mtldep ~sybPVP ok

version bump matches the API change (PVP)

Dependencies added: parsec2

Dependencies removed: haskell98, old-time, parsec, template-haskell

Dependency ranges changed: containers, mtl, syb

API changes (from Hackage documentation)

Files

• CSPM-Frontend.cabal +22/−38
• LICENSE +1/−1
• src/Language/CSPM/AST.hs +85/−68
• src/Language/CSPM/AstUtils.hs +49/−32
• src/Language/CSPM/Frontend.hs +48/−32
• src/Language/CSPM/LexHelper.hs +55/−22
• src/Language/CSPM/Lexer.x +50/−28
• src/Language/CSPM/Parser.hs +218/−179
• src/Language/CSPM/PatternCompiler.hs +0/−160
• src/Language/CSPM/PrettyPrinter.hs +328/−219
• src/Language/CSPM/Rename.hs +107/−29
• src/Language/CSPM/Token.hs +4/−5
• src/Language/CSPM/TokenClasses.hs +27/−4
• src/Language/CSPM/Utils.hs +22/−14
• src/Language/CSPM/Version.hs +0/−48

@@ -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 <fontaine@cs.uni-duesseldorf.de>+Author:              Marc Fontaine 2007 - 2011+Maintainer:          Marc Fontaine <fontaine@cs.uni-duesseldorf.de>, 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

@@ -1,4 +1,4 @@-Copyright (c) Marc Fontaine 2007-2009+Copyright (c) Marc Fontaine 2007-2011  All rights reserved. 

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

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

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

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

@@ -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 }--+<ref> "deadlock"      { mkL T_deadlock  }+<ref> "deterministic" { mkL T_deterministic }+<ref> "livelock"      { mkL T_livelock  }+<ref> "divergence"    { mkL T_livelock  }+<ref> "free"          { mkL T_free      }+<ref> "[FD]"          { mkL T_FD        }+<ref> "[F]"           { mkL T_F         }+<ref> "[T]"           { mkL T_T         }+<ref> "tau"           { mkL T_tau       }+<ref> "priority"      { mkL T_priority  }+<ref> "over"          { mkL T_over      }+<ref> "]:"            { begin 0         }+<ref> "]"             { begin 0         }+<ref> $white+         { skip            }+<ref> @str            { skip            }  { alexMonadScan = do

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

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

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

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

@@ -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 ++ "'"

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

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

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