Index: trunk/CspCASL/SignCSP.hs =================================================================== --- trunk/CspCASL/SignCSP.hs (revision 10827) +++ trunk/CspCASL/SignCSP.hs (revision 11215) @@ -17,13 +17,20 @@ module CspCASL.SignCSP where -import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME) - -import CASL.AS_Basic_CASL (SORT) +import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME, + PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..)) + +import CspCASL.AS_CspCASL () +import CspCASL.Print_CspCASL + +import CASL.AS_Basic_CASL (FORMULA, SORT) import CASL.Sign (emptySign, Sign, extendedInfo, sortRel) import CASL.Morphism (Morphism) -import qualified Common.Doc as Doc -import qualified Common.DocUtils as DocUtils -import Common.Id (Id, SIMPLE_ID) +import Common.AS_Annotation (Named) + +import Common.Doc +import Common.DocUtils + +import Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange) import Common.Lib.Rel (predecessors) import Common.Result @@ -38,20 +45,8 @@ deriving (Eq, Show) --- | A process communication alphabet consists of a set of sort names --- and typed channel names. -data TypedChanName = TypedChanName CHANNEL_NAME SORT - deriving (Eq, Ord, Show) -data CommType = CommTypeSort SORT - | CommTypeChan TypedChanName - deriving (Eq, Ord) -instance Show CommType where - show (CommTypeSort s) = show s - show (CommTypeChan (TypedChanName c s)) = show (c, s) - -type CommAlpha = Set.Set CommType - type ChanNameMap = Map.Map CHANNEL_NAME SORT type ProcNameMap = Map.Map PROCESS_NAME ProcProfile type ProcVarMap = Map.Map SIMPLE_ID SORT +type ProcVarList = [(SIMPLE_ID, SORT)] -- Close a communication alphabet under CASL subsort @@ -99,4 +94,7 @@ { chans :: ChanNameMap , procSet :: ProcNameMap + -- | Added for uniformity to the CASL static analysis. After + -- static analysis this is the empty list. + , ccSentences :: [Named CspCASLSen] } deriving (Eq, Show) @@ -107,4 +105,7 @@ ccSig2CASLSign :: CspCASLSign -> Sign () () ccSig2CASLSign sigma = sigma { extendedInfo = () } + +ccSig2CspSign :: CspCASLSign -> CspSign +ccSig2CspSign sigma = extendedInfo sigma -- | Empty CspCASL signature. @@ -117,4 +118,5 @@ { chans = Map.empty , procSet = Map.empty + , ccSentences =[] } @@ -170,6 +172,43 @@ -- dummy instances, need to be elaborated! -instance DocUtils.Pretty CspSign where - pretty = Doc.text . show -instance DocUtils.Pretty CspAddMorphism where - pretty = Doc.text . show +instance Pretty CspSign where + pretty = text . show +instance Pretty CspAddMorphism where + pretty = text . show + +-- Sentences + +-- A CspCASl senetence is either a CASL formula or a Procsses +-- equation. A process equation has on the LHS a process name, a list +-- of parameters which are qualified variables (which are terms), a +-- constituent communication alphabet and finally on the RHS a fully +-- qualified process. +data CspCASLSen = CASLSen (FORMULA ()) + | ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS + deriving (Show, Eq, Ord) + +instance Pretty CspCASLSen where + -- Not implemented yet - the pretty printing of the casl sentences + pretty(CASLSen _) = text "Pretty printing for CASLSen not implemented yet" + pretty(ProcessEq pn varList alpha proc) = + let varDoc = if (null varList) + then empty + else parens $ sepByCommas $ map pretty (map fst varList) + in pretty pn <+> varDoc <+> equals <+> pretty proc + +emptyCCSen :: CspCASLSen +emptyCCSen = + let emptyProcName = mkSimpleId "empty" + emptyVarList = [] + emptyAlphabet = Set.empty + emptyProc = Skip nullRange + in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc + +isCASLSen :: CspCASLSen -> Bool +isCASLSen (CASLSen _) = True +isCASLSen _ = False + +isProcessEq :: CspCASLSen -> Bool +isProcessEq (ProcessEq _ _ _ _) = True +isProcessEq _ = False + Index: trunk/CspCASL/Trans_Consts.hs =================================================================== --- trunk/CspCASL/Trans_Consts.hs (revision 10619) +++ trunk/CspCASL/Trans_Consts.hs (revision 11215) @@ -19,12 +19,72 @@ import CASL.AS_Basic_CASL +import CspCASL.AS_CspCASL_Process (PROCESS_NAME) import Isabelle.IsaConsts import Isabelle.IsaSign +import Isabelle.Translate(showIsaTypeT) +-- Name for the PreAlphabet +preAlphabetS :: String +preAlphabetS = "PreAlphabet" + +-- Type for the PreAlphabet +preAlphabetType :: Typ +preAlphabetType = Type {typeId = preAlphabetS, + typeSort = [], + typeArgs =[]} + +-- Name for the Alphabet alphabetS :: String alphabetS = "Alphabet" +-- Type for the Alphabet +alphabetType :: Typ +alphabetType = Type {typeId = alphabetS, + typeSort = [], + typeArgs =[]} + +-- Name for IsabelleHOL quot type +quotS :: String +quotS = "quot" + +-- Type for preAlphabet quot +preAlphabetQuotType :: Typ +preAlphabetQuotType = Type {typeId = quotS, + typeSort = [], + typeArgs =[preAlphabetType]} + +-- Name for the datatype of process names +procNameS :: String +procNameS = "ProcName" + +-- Type for the datatype of process names +procNameType :: Typ +procNameType = Type {typeId = procNameS, + typeSort = [], + typeArgs =[]} + +-- name for CspProvers ('pn, 'a) proc type +procS :: String +procS = "proc" + +-- Type for (ProcName,Alpahbet) proc +cCProverProcType :: Typ +cCProverProcType = Type {typeId = procS, + typeSort = [], + typeArgs =[procNameType, alphabetType]} + +-- Name for the function for mapping process names to real processes +procMapS :: String +procMapS = "ProcMap" + +-- Type for the function for mapping process names to real processes +procMapType :: Typ +procMapType = mkFunType procNameType cCProverProcType + barExtS :: String barExtS = "_Bar" + +baseSign :: BaseSig +baseSign = Main_thy classS :: String @@ -36,3 +96,6 @@ -- Convert a SORT to a string convertSort2String :: SORT -> String -convertSort2String s = show s +convertSort2String s = showIsaTypeT s baseSign + +convertProcessName2String :: PROCESS_NAME -> String +convertProcessName2String pn = (show pn) Index: trunk/CspCASL/AS_CspCASL_Process.der.hs =================================================================== --- trunk/CspCASL/AS_CspCASL_Process.der.hs (revision 10428) +++ trunk/CspCASL/AS_CspCASL_Process.der.hs (revision 11215) @@ -21,8 +21,12 @@ PROCESS_NAME, RENAMING, + CommAlpha(..), + CommType(..), + TypedChanName(..) ) where import CASL.AS_Basic_CASL (FORMULA, SORT, TERM, VAR) import Common.Id +import qualified Data.Set as Set -- DrIFT command @@ -47,5 +51,4 @@ type RENAMING = [Id] - type CHANNEL_NAME = SIMPLE_ID @@ -54,4 +57,18 @@ type COMM_TYPE = SIMPLE_ID +-- | A process communication alphabet consists of a set of sort names +-- and typed channel names. +data TypedChanName = TypedChanName CHANNEL_NAME SORT + deriving (Eq, Ord, Show) + +data CommType = CommTypeSort SORT + | CommTypeChan TypedChanName + deriving (Eq, Ord) + +instance Show CommType where + show (CommTypeSort s) = show s + show (CommTypeChan (TypedChanName c s)) = show (c, s) + +type CommAlpha = Set.Set CommType -- |CSP-CASL process expressions. @@ -96,3 +113,6 @@ -- | Named process | NamedProcess PROCESS_NAME [TERM ()] Range + -- | Fully qualified process. The range here shall be the same as + -- | in the process. + | FQProcess PROCESS CommAlpha Range deriving (Eq, Ord, Show) Index: trunk/CspCASL/AS_CspCASL.der.hs =================================================================== --- trunk/CspCASL/AS_CspCASL.der.hs (revision 10471) +++ trunk/CspCASL/AS_CspCASL.der.hs (revision 11215) @@ -14,12 +14,12 @@ module CspCASL.AS_CspCASL where +import Common.Doc +import Common.DocUtils import Common.Id -import CASL.AS_Basic_CASL (SORT, VAR) +import CASL.AS_Basic_CASL (SORT, VAR, FORMULA) import CspCASL.AS_CspCASL_Process (CHANNEL_NAME, COMM_TYPE, PROCESS(..), PROCESS_NAME) - -import Common.Id -- DrIFT command @@ -34,4 +34,7 @@ deriving Show +data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range + deriving (Show,Ord, Eq) + data PROC_ITEM = Proc_Decl PROCESS_NAME PROC_ARGS PROC_ALPHABET | Proc_Eq PARM_PROCNAME PROCESS @@ -42,17 +45,2 @@ data PARM_PROCNAME = ParmProcname PROCESS_NAME [VAR] deriving Show - -data PROC_ALPHABET = ProcAlphabet [COMM_TYPE] Range - deriving Show - --- Sentences - -data CspCASLSentence = CspCASLSentence PROCESS_NAME [VAR] PROCESS - deriving (Show, Eq, Ord) - -emptyProcName :: PROCESS_NAME -emptyProcName = mkSimpleId "empty" - -emptyCCSentence :: CspCASLSentence -emptyCCSentence = CspCASLSentence emptyProcName [] - (NamedProcess emptyProcName [] nullRange) Index: trunk/CspCASL/Trans_CspProver.hs =================================================================== --- trunk/CspCASL/Trans_CspProver.hs (revision 10931) +++ trunk/CspCASL/Trans_CspProver.hs (revision 11215) @@ -15,7 +15,11 @@ module CspCASL.Trans_CspProver where -import CASL.AS_Basic_CASL (SORT, VAR) +import qualified CASL.AS_Basic_CASL as CASL_AS_Basic_CASL +import qualified CASL.Fold as CASL_Fold +import qualified CASL.Sign as CASL_Sign import Common.Id + +import qualified Comorphisms.CFOL2IsabelleHOL as CFOL2IsabelleHOL import CspCASL.AS_CspCASL_Process @@ -26,6 +30,6 @@ import Isabelle.IsaConsts -transProcess :: PROCESS -> Term -transProcess pr = case pr of +transProcess :: CASL_Sign.Sign () () -> PROCESS -> Term +transProcess caslSign pr = case pr of -- precedence 0 Skip _ -> cspProver_skipOp @@ -41,43 +45,52 @@ -- precedence 1 ConditionalProcess _ p q _ -> - cspProver_conditionalOp true (transProcess p) (transProcess q) + cspProver_conditionalOp true (transProcess caslSign p) + (transProcess caslSign q) -- precedence 2 Hiding p es _ -> - cspProver_hidingOp (transProcess p) (transEventSet es) + cspProver_hidingOp (transProcess caslSign p) (transEventSet es) RenamingProcess p r _ -> - cspProver_renamingOp (transProcess p) (transRenaming r) + cspProver_renamingOp (transProcess caslSign p) (transRenaming r) -- precedence 3 Sequential p q _ -> - cspProver_sequenceOp (transProcess p) (transProcess q) + cspProver_sequenceOp (transProcess caslSign p) (transProcess caslSign q) PrefixProcess ev p _ -> - cspProver_action_prefixOp (transEvent ev) (transProcess p) + cspProver_action_prefixOp (transEvent caslSign ev) + (transProcess caslSign p) InternalPrefixProcess v s p _ -> cspProver_internal_prefix_choiceOp (transVar v) (transSort s) - (transProcess p) + (transProcess caslSign p) ExternalPrefixProcess v s p _ -> cspProver_external_prefix_choiceOp (transVar v) (transSort s) - (transProcess p) + (transProcess caslSign p) -- precedence 4 InternalChoice p q _ -> - cspProver_internal_choiceOp (transProcess p) (transProcess q) + cspProver_internal_choiceOp (transProcess caslSign p) + (transProcess caslSign q) ExternalChoice p q _ -> - cspProver_external_choiceOp (transProcess p) (transProcess q) + cspProver_external_choiceOp (transProcess caslSign p) + (transProcess caslSign q) -- precedence 5 Interleaving p q _ -> - cspProver_interleavingOp (transProcess p) (transProcess q) + cspProver_interleavingOp (transProcess caslSign p) + (transProcess caslSign q) SynchronousParallel p q _ -> - cspProver_synchronousOp (transProcess p) (transProcess q) + cspProver_synchronousOp (transProcess caslSign p) + (transProcess caslSign q) GeneralisedParallel p es q _ -> - cspProver_general_parallelOp (transProcess p) + cspProver_general_parallelOp (transProcess caslSign p) (transEventSet es) - (transProcess q) + (transProcess caslSign q) AlphabetisedParallel p les res q _ -> - cspProver_alphabetised_parallelOp (transProcess p) + cspProver_alphabetised_parallelOp (transProcess caslSign p) (transEventSet les) (transEventSet res) - (transProcess q) + (transProcess caslSign q) + -- BUG not done right yet + FQProcess p _ _ -> + transProcess caslSign p transEventSet :: EVENT_SET -> Term @@ -88,16 +101,16 @@ EventSet commTypes _ -> Set $ FixedSet $ map tranCommType commTypes -transEvent :: EVENT -> Term -transEvent ev = +transEvent :: CASL_Sign.Sign () () -> EVENT -> Term +transEvent caslSign ev = case ev of - TermEvent _caslTerm _ -> conDouble "not yet done" - ChanSend _ _ _ -> conDouble "not yet done" - ChanNonDetSend _ _ _ _ -> conDouble "not yet done" - ChanRecv _ _ _ _ -> conDouble "not yet done" + TermEvent caslTerm _ -> transTerm_with_class caslSign caslTerm + ChanSend _ _ _ -> conDouble "ChanSendNotYetDone" + ChanNonDetSend _ _ _ _ -> conDouble "ChanNonDetSendNotYetDone" + ChanRecv _ _ _ _ -> conDouble "ChanRecvNotYetDone" -transVar :: VAR -> Term +transVar :: CASL_AS_Basic_CASL.VAR -> Term transVar v = conDouble $ tokStr v -transSort :: SORT -> Term +transSort :: CASL_AS_Basic_CASL.SORT -> Term transSort sort = let sortBarString = convertSort2String sort ++ barExtS in conDouble sortBarString @@ -105,2 +118,68 @@ transRenaming :: RENAMING -> Term transRenaming _ = conDouble "not yet done" + + + +-- BUG - I dont think these functions are correct +transTerm_with_class :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> + Term +transTerm_with_class caslSign caslTerm = + case caslTerm of + -- if the term is just a variable then we just translate the + -- variable to isabelle + CASL_AS_Basic_CASL.Qual_var _ _ _ -> transCaslTerm caslSign caslTerm + -- otherwise we add a classOp around it and translate the inside of + -- it with the translator that adds a chooseOp + _ -> classOp (transTerm_with_choose caslSign caslTerm) + +transTerm_with_choose :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> + Term +transTerm_with_choose caslSign caslTerm = + case caslTerm of + -- if the term is just a variable then we need to apply the choose + -- function + CASL_AS_Basic_CASL.Qual_var _ _ _ -> termAppl (conDouble "choose") + (transCaslTerm caslSign caslTerm) + -- otherwise we just translate it to Isabelle + _ -> transCaslTerm caslSign caslTerm + +-- | Translate a CASL Term to an Isabelle Term using the exact +-- translation as is done in the comorphism composition +-- CASL2PCFOL;defaultCASL2SubCFOL;CFOL2IsabelleHOL +transCaslTerm :: CASL_Sign.Sign () () -> CASL_AS_Basic_CASL.TERM () -> Term +transCaslTerm caslSign caslTerm = + let tyToks = CFOL2IsabelleHOL.typeToks caslSign + trForm = CFOL2IsabelleHOL.formTrCASL + strs = CFOL2IsabelleHOL.getAssumpsToks caslSign + in CASL_Fold.foldTerm (CFOL2IsabelleHOL.transRecord + caslSign tyToks trForm strs) caslTerm + + +-- My own version of transRecord +-- transRecord_Term :: CASL.Sign.Sign f e -> Set.Set String -> FormulaTranslator f e +-- -> Set.Set String -> Record f Term Term +-- transRecord_Term sign tyToks tr toks = Record +-- { foldSimpleId = error "transRecord_Term: Simple_id" +-- , foldQual_var = \ _ v _ _ -> mkFree $ transVar toks v +-- , foldApplication = \ _ opsymb args _ -> +-- foldl termAppl (con $ transOP_SYMB sign tyToks opsymb) args +-- , foldSorted_term = \ _ t _ _ -> t -- no subsorting assumed +-- , foldCast = \ _ t _ _ -> t -- no subsorting assumed +-- , foldConditional = \ _ t1 phi t2 _ -> -- equal types assumed +-- If phi t1 t2 NotCont +-- , foldMixfix_qual_pred = error "transRecord_Term: Mixfix_qual_pred" +-- , foldMixfix_term = error "transRecord_Term: Mixfix_term" +-- , foldMixfix_token = error "transRecord_Term: Mixfix_token" +-- , foldMixfix_sorted_term = error "transRecord_Term: Mixfix_sorted_term" +-- , foldMixfix_cast = error "transRecord_Term: Mixfix_cast" +-- , foldMixfix_parenthesized = error "transRecord_Term: Mixfix_parenthesized" +-- , foldMixfix_bracketed = error "transRecord_Term: Mixfix_bracketed" +-- , foldMixfix_braced = error "transRecord_Term: Mixfix_braced" +-- } + +-- transVar :: Set.Set String -> VAR -> String +-- transVar toks v = let +-- s = showIsaConstT (simpleIdToId v) baseSign +-- renVar t = if Set.member t toks then renVar $ "X_" ++ t else t +-- in renVar s + Index: trunk/CspCASL/StatAnaCSP.hs =================================================================== --- trunk/CspCASL/StatAnaCSP.hs (revision 11201) +++ trunk/CspCASL/StatAnaCSP.hs (revision 11215) @@ -21,5 +21,7 @@ import qualified Data.Maybe as Maybe import qualified Data.Set as S - +-- liam added the following, they should be deleted from imports when +-- liams temp code is removed: Op_name mkSimpleId mkInfix OP_SYMB(..), +-- OP_TYPE(..) import CASL.AS_Basic_CASL (FORMULA(..), OpKind(..), SORT, TERM(..), VAR, VAR_DECL(..)) @@ -34,5 +36,5 @@ import Common.ConvertGlobalAnnos import qualified Common.Lib.Rel as Rel -import Common.Id (getRange, Id, simpleIdToId, nullRange, mkSimpleId) +import Common.Id (getRange, Id, simpleIdToId, nullRange) import Common.Lib.State import Common.ExtSign @@ -44,8 +46,10 @@ import CspCASL.SignCSP +import qualified Data.Set as Set + basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos) -> Result (CspBasicSpec, ExtSign CspCASLSign (), - [Named CspCASLSentence]) -basicAnalysisCspCASL (cc, sigma, ga) = do + [Named CspCASLSen]) +basicAnalysisCspCASL (cc, sigma, ga) = let Result es mga = mergeGlobalAnnos ga $ globAnnos sigma (_, accSig) = runState (ana_BASIC_CSP cc) $ case mga of @@ -53,24 +57,12 @@ Just nga -> sigma { globAnnos = nga } ds = reverse $ envDiags accSig - Result (es ++ ds) (Just ()) -- insert diagnostics - return (cc, mkExtSign accSig, [makeNamed "empty_sentence" emptyCCSentence, - makeNamed "StopProcSen" stopProc, - makeNamed "GParProcSen" gParProc, - makeNamed "AParProcSen" aParProc, - makeNamed "StopProcSen" seqProc]) - where - stopProc = CspCASLSentence (mkSimpleId "stopProc") [] (Stop nullRange) - seqProc = CspCASLSentence (mkSimpleId "seqProc") [] - (Sequential (Stop nullRange) - (Stop nullRange) nullRange) - gParProc = CspCASLSentence (mkSimpleId "gParProc") [] - (GeneralisedParallel (Stop nullRange) - (EventSet [mkSimpleId "S"] nullRange) - (Skip nullRange) nullRange) - aParProc = CspCASLSentence (mkSimpleId "gParProc") [] - (AlphabetisedParallel (Stop nullRange) - (EventSet [mkSimpleId "T"] nullRange) - (EventSet [mkSimpleId "U"] nullRange) - (Skip nullRange) nullRange) + -- Extract process equations only. + ext = extendedInfo accSig + ccsents = reverse $ ccSentences ext + -- Clean signature here + cleanSig = accSig + { extendedInfo = ext { ccSentences = []}} + in Result (es ++ ds) $ + Just (cc, mkExtSign cleanSig, ccsents) ana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign () @@ -102,5 +94,5 @@ -- | Statically analyse a CspCASL channel declaration. -anaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL +anaChanDecl :: CHANNEL_DECL -> State CspCASLSign () anaChanDecl (ChannelDecl chanNames chanSort) = do checkSorts [chanSort] -- check channel sort is known @@ -113,5 +105,5 @@ , envDiags = vds } - return (ChannelDecl chanNames chanSort) + return () -- | Statically analyse a CspCASL channel name. @@ -178,142 +170,181 @@ sig <- get let ext = extendedInfo sig + ccsens = ccSentences ext procDecls = procSet ext prof = pn `Map.lookup` procDecls case prof of - -- Only analyse a process if its name (and thus profile) is known - Just (ProcProfile procArgs procAlpha) -> - do gVars <- anaProcVars pn procArgs vs -- compute global vars - termAlpha <- anaProcTerm proc gVars Map.empty - checkCommAlphaSub termAlpha procAlpha proc "process equation" - return () - Nothing -> - do addDiags [mkDiag Error "process equation for unknown process" pn] - return () - vds <- gets envDiags - put sig { envDiags = vds } + -- Only analyse a process if its name (and thus profile) is known + Just (ProcProfile procArgs procAlpha) -> + do gVars <- anaProcVars pn procArgs vs -- compute global vars + (termAlpha, fqProc) <- anaProcTerm proc (Map.fromList gVars) Map.empty + checkCommAlphaSub termAlpha procAlpha proc "process equation" + -- Save the diags from the checkCommAlphaSub + vds <- gets envDiags + -- put CspCASL Sentences back in to the state with new sentence + put sig {envDiags = vds, extendedInfo = + ext { ccSentences = + -- BUG - What should the constituent + -- alphabet be for this process? + -- probably the same as the inner one! + (makeNamed ("ProcHugo") + (ProcessEq pn gVars + Set.empty + fqProc)):ccsens + } + } + return () + Nothing -> + do addDiags [mkDiag Error "process equation for unknown process" pn] + return () return () -- | Statically analyse a CspCASL process equation's global variable -- names. -anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarMap +anaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarList anaProcVars pn ss vs = do case (compare (length ss) (length vs)) of LT -> do addDiags [mkDiag Error "too many process arguments" pn] - return Map.empty + return [] GT -> do addDiags [mkDiag Error "not enough process arguments" pn] - return Map.empty - EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss) + return [] + EQ -> Monad.foldM anaProcVar [] (zip vs ss) -- | Statically analyse a CspCASL process-global variable name. -anaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspCASLSign ProcVarMap +anaProcVar :: ProcVarList -> (VAR, SORT) -> State CspCASLSign ProcVarList anaProcVar old (v, s) = do - if v `Map.member` old - then do addDiags [mkDiag Error "process arg declared more than once" v] + if v `elem` (map fst old) + then do addDiags [mkDiag Error "process argument declared more than once" v] return old - else return (Map.insert v s old) + else return (old ++ [(v, s)]) -- Static analysis of process terms +-- BUG in fucntion below +-- not returing FQProcesses -- | Statically analyse a CspCASL process term. +-- The process that is returned is a fully qualified process. anaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> - State CspCASLSign CommAlpha + State CspCASLSign (CommAlpha, PROCESS) anaProcTerm proc gVars lVars = case proc of - NamedProcess name args _ -> + NamedProcess name args range -> do addDiags [mkDiag Debug "Named process" proc] al <- anaNamedProc proc name args (lVars `Map.union` gVars) - return al - Skip _ -> + return (al, + FQProcess (NamedProcess name args range) al range) + Skip range -> do addDiags [mkDiag Debug "Skip" proc] - return S.empty - Stop _ -> + return (S.empty, + FQProcess (Skip range) S.empty range) + Stop range -> do addDiags [mkDiag Debug "Stop" proc] - return S.empty - Div _ -> + return (S.empty, + FQProcess (Stop range) S.empty range) + Div range -> do addDiags [mkDiag Debug "Div" proc] - return S.empty - Run es _ -> + return (S.empty, + FQProcess (Div range) S.empty range) + Run es range -> do addDiags [mkDiag Debug "Run" proc] comms <- anaEventSet es - return comms - Chaos es _ -> + return (comms, + FQProcess (Run es range) comms range) + Chaos es range -> do addDiags [mkDiag Debug "Chaos" proc] comms <- anaEventSet es - return comms - PrefixProcess e p _ -> + return (comms, + FQProcess (Chaos es range) comms range) + PrefixProcess e p range -> do addDiags [mkDiag Debug "Prefix" proc] (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars) - comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars) - return (comms `S.union` evComms) - InternalPrefixProcess v s p _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (rcvMap `Map.union` lVars) + return (comms `S.union` evComms, + FQProcess (PrefixProcess e pFQTerm range) (comms `S.union` evComms) range) + InternalPrefixProcess v s p range -> do addDiags [mkDiag Debug "Internal prefix" proc] checkSorts [s] -- check sort is known - comms <- anaProcTerm p gVars (Map.insert v s lVars) - return (S.insert (CommTypeSort s) comms) - ExternalPrefixProcess v s p _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) + return (S.insert (CommTypeSort s) comms, + FQProcess (InternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) + ExternalPrefixProcess v s p range -> do addDiags [mkDiag Debug "External prefix" proc] checkSorts [s] -- check sort is known - comms <- anaProcTerm p gVars (Map.insert v s lVars) - return (S.insert (CommTypeSort s) comms) - Sequential p q _ -> + (comms, pFQTerm) <- anaProcTerm p gVars (Map.insert v s lVars) + return (S.insert (CommTypeSort s) comms, + FQProcess (ExternalPrefixProcess v s pFQTerm range) (S.insert (CommTypeSort s) comms) range) + Sequential p q range -> do addDiags [mkDiag Debug "Sequential" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars Map.empty - return (pComms `S.union` qComms) - InternalChoice p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars Map.empty + return (pComms `S.union` qComms, + FQProcess (Sequential pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + InternalChoice p q range -> do addDiags [mkDiag Debug "InternalChoice" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - ExternalChoice p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (InternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + ExternalChoice p q range -> do addDiags [mkDiag Debug "ExternalChoice" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - Interleaving p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (ExternalChoice pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + Interleaving p q range -> do addDiags [mkDiag Debug "Interleaving" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - SynchronousParallel p q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (Interleaving pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + SynchronousParallel p q range -> do addDiags [mkDiag Debug "Synchronous" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars - return (pComms `S.union` qComms) - GeneralisedParallel p es q _ -> + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (pComms `S.union` qComms, + FQProcess (SynchronousParallel pFQTerm qFQTerm range) (pComms `S.union` qComms) range) + GeneralisedParallel p es q range -> do addDiags [mkDiag Debug "Generalised parallel" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars synComms <- anaEventSet es - qComms <- anaProcTerm q gVars lVars - return (S.unions [pComms, qComms, synComms]) - AlphabetisedParallel p esp esq q _ -> + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + return (S.unions [pComms, qComms, synComms], + FQProcess (GeneralisedParallel pFQTerm es qFQTerm range) (S.unions [pComms, qComms, synComms]) range) + AlphabetisedParallel p esp esq q range -> do addDiags [mkDiag Debug "Alphabetised parallel" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars pSynComms <- anaEventSet esp checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left" qSynComms <- anaEventSet esq - qComms <- anaProcTerm q gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars checkCommAlphaSub qSynComms qComms proc "alphabetised parallel, right" - return (pComms `S.union` qComms) - Hiding p es _ -> + return (pComms `S.union` qComms, + FQProcess (AlphabetisedParallel pFQTerm esp esq qFQTerm range) (pComms `S.union` qComms) range) + Hiding p es range -> do addDiags [mkDiag Debug "Hiding" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars hidComms <- anaEventSet es - return (pComms `S.union` hidComms) - RenamingProcess p r _ -> + return (pComms `S.union` hidComms, + FQProcess (Hiding pFQTerm es range) (pComms `S.union` hidComms) range) + RenamingProcess p r range -> do addDiags [mkDiag Debug "Renaming" proc] - pComms <- anaProcTerm p gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars renAlpha <- anaRenaming r - return (pComms `S.union` renAlpha) - ConditionalProcess f p q _ -> + return (pComms `S.union` renAlpha, + FQProcess (RenamingProcess pFQTerm r range) (pComms `S.union` renAlpha) range) + ConditionalProcess f p q range -> do addDiags [mkDiag Debug "Conditional" proc] - pComms <- anaProcTerm p gVars lVars - qComms <- anaProcTerm q gVars lVars + (pComms, pFQTerm) <- anaProcTerm p gVars lVars + (qComms, qFQTerm) <- anaProcTerm q gVars lVars + -- mfs is the fully qualified formula version of f mfs <- anaFormulaCspCASL (gVars `Map.union` lVars) f + addDiags [mkDiag Debug "Formula" f] + addDiags [mkDiag Debug "FQFormula" (Maybe.fromJust mfs)] let fComms = case mfs of Nothing -> S.empty Just fs -> formulaComms fs - return (S.unions [pComms, qComms, fComms]) + return (S.unions [pComms, qComms, fComms], + FQProcess (ConditionalProcess (Maybe.fromJust mfs) pFQTerm qFQTerm range) + (S.unions [pComms, qComms, fComms]) range) -- | Statically analyse a CspCASL "named process" term. @@ -582,6 +613,5 @@ ga = globAnnos sig mix = emptyMix { mixRules = makeRules ga allIds } - resF <- resolveFormula (putParen mix) (mixResolve mix) - ga (mixRules mix) frm + resF <- resolveFormula (putParen mix) (mixResolve mix) ga (mixRules mix) frm minExpFORMULA (const return) sig resF Index: trunk/CspCASL/Print_CspCASL.hs =================================================================== --- trunk/CspCASL/Print_CspCASL.hs (revision 10428) +++ trunk/CspCASL/Print_CspCASL.hs (revision 11215) @@ -24,6 +24,6 @@ import CspCASL.CspCASL_Keywords -instance Pretty CspCASLSentence where - pretty _ = empty +import qualified Data.Set as S + instance Pretty CspBasicSpec where @@ -145,4 +145,13 @@ alpar_close <+> (glue pr q) ) + FQProcess p commAlpha _ -> + let commAlphaList = S.toList commAlpha + prettyComms cs = sepByCommas (map pretty cs) + in brackets(pretty p) <> text "_" <> braces (prettyComms commAlphaList) + +instance Pretty CommType where + pretty (CommTypeSort s) = pretty s + pretty (CommTypeChan (TypedChanName c s)) = parens (sepByCommas [pretty c, pretty s]) + -- glue and prec_comp decide whether the child in the parse tree needs Index: trunk/CspCASL/Logic_CspCASL.hs =================================================================== --- trunk/CspCASL/Logic_CspCASL.hs (revision 10910) +++ trunk/CspCASL/Logic_CspCASL.hs (revision 11215) @@ -72,6 +72,6 @@ -- | Instance of Sentences for CspCASL (missing) instance Sentences CspCASL - AS_CspCASL.CspCASLSentence -- sentence (missing) - SignCSP.CspCASLSign -- signature + SignCSP.CspCASLSen -- sentence (missing) + SignCSP.CspCASLSign -- signature SignCSP.CspMorphism -- morphism () -- symbol (?) @@ -102,5 +102,5 @@ () -- Sublogics (missing) AS_CspCASL.CspBasicSpec -- basic_spec - AS_CspCASL.CspCASLSentence -- sentence (missing) + SignCSP.CspCASLSen -- sentence (missing) SYMB_ITEMS -- symb_items SYMB_MAP_ITEMS -- symb_map_items @@ -118,5 +118,5 @@ instance StaticAnalysis CspCASL AS_CspCASL.CspBasicSpec -- basic_spec - AS_CspCASL.CspCASLSentence -- sentence (missing) + SignCSP.CspCASLSen -- sentence (missing) SYMB_ITEMS -- symb_items SYMB_MAP_ITEMS -- symb_map_items