SignCSP.hs revision 55a09617886a31d9a9cb04a583bc4d4ef91b6c71
1N/A{- |
1N/AModule : $Id$
1N/ADescription : CspCASL signatures
1N/ACopyright : (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
1N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
1N/A
1N/AMaintainer : M.Roggenbach@swansea.ac.uk
1N/AStability : provisional
1N/APortability : portable
1N/A
1N/Asignatures for CSP-CASL
1N/A
1N/A-}
1N/A
1N/A-- todo: implement isInclusion, computeExt
1N/A
1N/Amodule CspCASL.SignCSP where
1N/A
1N/Aimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME,
1N/A PROCESS(..), CommAlpha(..), CommType(..), TypedChanName(..))
1N/A
1N/Aimport CspCASL.AS_CspCASL ()
1N/Aimport CspCASL.CspCASL_Keywords
1N/Aimport CspCASL.Print_CspCASL
1N/A
1N/Aimport CASL.AS_Basic_CASL (FORMULA, SORT)
1N/Aimport CASL.Sign (emptySign, Sign, extendedInfo, sortRel)
1N/Aimport CASL.Morphism (Morphism)
1N/A
1N/Aimport Common.AS_Annotation (Named)
1N/A
1N/Aimport Common.Doc
1N/Aimport Common.DocUtils
1N/A
1N/Aimport Common.Id (Id, SIMPLE_ID, mkSimpleId, nullRange)
1N/Aimport Common.Lib.Rel (predecessors)
1N/Aimport Common.Result
1N/A
1N/Aimport Control.Monad (unless)
1N/Aimport qualified Data.Map as Map
1N/Aimport qualified Data.Set as Set
1N/A
1N/A-- | A process has zero or more parameter sorts, and a communication
1N/A-- alphabet.
1N/Adata ProcProfile = ProcProfile [SORT] CommAlpha
1N/A deriving (Eq, Show)
1N/A
1N/Atype ChanNameMap = Map.Map CHANNEL_NAME SORT
1N/Atype ProcNameMap = Map.Map PROCESS_NAME ProcProfile
1N/Atype ProcVarMap = Map.Map SIMPLE_ID SORT
1N/Atype ProcVarList = [(SIMPLE_ID, SORT)]
1N/A
1N/A-- Close a communication alphabet under CASL subsort
1N/AcloseCspCommAlpha :: CspCASLSign -> CommAlpha -> CommAlpha
1N/AcloseCspCommAlpha sig = Set.unions . Set.toList . Set.map (closeOneCspComm sig)
1N/A
1N/A-- Close one CommType under CASL subsort
1N/AcloseOneCspComm :: CspCASLSign -> CommType -> CommAlpha
1N/AcloseOneCspComm sig x = let
1N/A mkTypedChan c s = CommTypeChan $ TypedChanName c s
1N/A subsorts s' = Set.singleton s' `Set.union` predecessors (sortRel sig) s'
1N/A in case x of
1N/A CommTypeSort s -> Set.map CommTypeSort (subsorts s)
1N/A CommTypeChan (TypedChanName c s) -> Set.map CommTypeSort (subsorts s)
1N/A `Set.union` Set.map (mkTypedChan c) (subsorts s)
1N/A
1N/A{- Will probably be useful, but doesn't appear to be right now.
1N/A
1N/A-- Extract the sorts from a process alphabet
1N/AprocAlphaSorts :: CommAlpha -> Set.Set SORT
1N/AprocAlphaSorts a = stripMaybe $ Set.map justSort a
1N/A where justSort n = case n of
1N/A (CommTypeSort s) -> Just s
1N/A _ -> Nothing
1N/A-- Extract the typed channel names from a process alphabet
1N/AprocAlphaChans :: CommAlpha -> Set.Set TypedChanName
1N/AprocAlphaChans a = stripMaybe $ Set.map justChan a
1N/A where justChan n = case n of
1N/A (CommTypeChan c) -> Just c
1N/A _ -> Nothing
1N/A-- Given a set of Maybes, filter to keep only the Justs
1N/AstripMaybe :: Ord a => Set.Set (Maybe a) -> Set.Set a
1N/AstripMaybe x = Set.fromList $ Maybe.catMaybes $ Set.toList x
1N/A
1N/A-- Close a set of sorts under a subsort relation
1N/AcspSubsortCloseSorts :: CspCASLSign -> Set.Set SORT -> Set.Set SORT
1N/AcspSubsortCloseSorts sig sorts =
1N/A Set.unions subsort_sets
1N/A where subsort_sets = Set.toList $ Set.map (cspSubsortPreds sig) sorts
1N/A
1N/A-}
1N/A
1N/A-- | CSP process signature.
1N/Adata CspSign = CspSign
1N/A { chans :: ChanNameMap
1N/A , procSet :: ProcNameMap
1N/A -- | Added for uniformity to the CASL static analysis. After
1N/A -- static analysis this is the empty list.
1N/A , ccSentences :: [Named CspCASLSen]
1N/A } deriving (Eq, Show)
1N/A
1N/A-- | A CspCASL signature is a CASL signature with a CSP process
1N/A-- signature in the extendedInfo part.
1N/Atype CspCASLSign = Sign () CspSign
1N/A
1N/AccSig2CASLSign :: CspCASLSign -> Sign () ()
1N/AccSig2CASLSign sigma = sigma { extendedInfo = () }
1N/A
1N/AccSig2CspSign :: CspCASLSign -> CspSign
1N/AccSig2CspSign sigma = extendedInfo sigma
1N/A
1N/A-- | Empty CspCASL signature.
1N/AemptyCspCASLSign :: CspCASLSign
1N/AemptyCspCASLSign = emptySign emptyCspSign
1N/A
1N/A-- | Empty CSP process signature.
1N/AemptyCspSign :: CspSign
1N/AemptyCspSign = CspSign
1N/A { chans = Map.empty
1N/A , procSet = Map.empty
1N/A , ccSentences =[]
1N/A }
1N/A
1N/A-- | Compute union of two CSP process signatures.
1N/AaddCspProcSig :: CspSign -> CspSign -> CspSign
1N/AaddCspProcSig a b =
1N/A a { chans = chans a `Map.union` chans b
1N/A , procSet = procSet a `Map.union` procSet b
1N/A }
1N/A
1N/A-- | Compute difference of two CSP process signatures.
1N/AdiffCspProcSig :: CspSign -> CspSign -> CspSign
1N/AdiffCspProcSig a b =
1N/A a { chans = chans a `Map.difference` chans b
1N/A , procSet = procSet a `Map.difference` procSet b
1N/A }
1N/A
1N/A
1N/A-- XXX looks incomplete!
1N/AisInclusion :: CspSign -> CspSign -> Bool
1N/AisInclusion _ _ = True
1N/A
1N/A
1N/A-- XXX morphisms between CSP process signatures?
1N/A
1N/Adata CspAddMorphism = CspAddMorphism
1N/A { channelMap :: Map.Map Id Id
1N/A , processMap :: Map.Map Id Id
1N/A } deriving (Eq, Show)
1N/A
1N/AcomposeIdMaps :: Map.Map Id Id -> Map.Map Id Id -> Map.Map Id Id
1N/AcomposeIdMaps m1 m2 = Map.foldWithKey (\ i j -> case Map.lookup j m2 of
1N/A Nothing -> error "SignCsp.composeIdMaps"
1N/A Just k -> Map.insert i k) Map.empty m1
1N/A
1N/AcomposeCspAddMorphism :: CspAddMorphism -> CspAddMorphism
1N/A -> Result CspAddMorphism
1N/AcomposeCspAddMorphism m1 m2 = return emptyCspAddMorphism
1N/A { channelMap = composeIdMaps (channelMap m1) $ channelMap m2
1N/A , processMap = composeIdMaps (processMap m1) $ processMap m2 }
1N/A
1N/AinverseCspAddMorphism :: CspAddMorphism -> Result CspAddMorphism
1N/AinverseCspAddMorphism cm = do
1N/A let chL = Map.toList $ channelMap cm
1N/A prL = Map.toList $ processMap cm
1N/A swap = map $ \ (a, b) -> (b, a)
1N/A isInj l = length l == Set.size (Set.fromList $ map snd l)
1N/A unless (isInj chL) $ fail "invertCspAddMorphism.channelMap"
1N/A unless (isInj prL) $ fail "invertCspAddMorphism.processMap"
1N/A return emptyCspAddMorphism
1N/A { channelMap = Map.fromList $ swap chL
1N/A , processMap = Map.fromList $ swap prL }
1N/A
1N/Atype CspMorphism = Morphism () CspSign CspAddMorphism
1N/A
1N/AemptyCspAddMorphism :: CspAddMorphism
1N/AemptyCspAddMorphism = CspAddMorphism
1N/A { channelMap = Map.empty -- ???
1N/A , processMap = Map.empty
1N/A }
1N/A
1N/A-- | Pretty printing for CspCASL signatures
1N/Ainstance Pretty CspSign where
1N/A pretty = printCspSign
1N/A
1N/AprintCspSign :: CspSign -> Doc
1N/AprintCspSign sigma =
1N/A chan_part $+$ proc_part
1N/A where chan_part =
1N/A case (Map.size $ chans sigma) of
1N/A 0 -> empty
1N/A 1 -> (keyword channelS) <+> printChanNameMap (chans sigma)
1N/A _ -> (keyword channelsS) <+> printChanNameMap (chans sigma)
1N/A proc_part = (keyword processS) <+> printProcNameMap (procSet sigma)
1N/A
1N/A-- | Pretty printing for channel name maps
1N/Ainstance Pretty ChanNameMap where
1N/A pretty = printChanNameMap
1N/A
1N/AprintChanNameMap :: ChanNameMap -> Doc
1N/AprintChanNameMap chanMap =
1N/A vcat $ punctuate semi $ map printChan $ Map.toList chanMap
1N/A where printChan (chanName, sort) =
1N/A (pretty chanName) <+> colon <+> (pretty sort)
1N/A
1N/A-- | Pretty printing for process name maps
1N/Ainstance Pretty ProcNameMap where
1N/A pretty = printProcNameMap
1N/A
1N/AprintProcNameMap :: ProcNameMap -> Doc
1N/AprintProcNameMap procNameMap =
1N/A vcat $ punctuate semi $ map printProcName $ Map.toList procNameMap
1N/A where printProcName (procName, procProfile) =
1N/A (pretty procName) <+> pretty procProfile
1N/A
1N/A-- | Pretty printing for process profiles
1N/Ainstance Pretty ProcProfile where
1N/A pretty = printProcProfile
1N/A
1N/AprintProcProfile :: ProcProfile -> Doc
1N/AprintProcProfile (ProcProfile sorts commAlpha) =
1N/A printArgs sorts <+> colon <+> (ppWithCommas $ Set.toList commAlpha)
1N/A where printArgs [] = empty
1N/A printArgs args = parens $ ppWithCommas args
1N/A
1N/A-- | Pretty printing for Csp morphisms
1N/Ainstance Pretty CspAddMorphism where
1N/A pretty = text . show
1N/A
1N/A-- Sentences
1N/A
1N/A-- | A CspCASl senetence is either a CASL formula or a Procsses
1N/A-- equation. A process equation has on the LHS a process name, a
1N/A-- list of parameters which are qualified variables (which are
1N/A-- terms), a constituent( or is it permitted ?) communication alphabet and
1N/A-- finally on the RHS a fully qualified process.
1N/Adata CspCASLSen = CASLSen (FORMULA ())
1N/A | ProcessEq PROCESS_NAME ProcVarList CommAlpha PROCESS
1N/A deriving (Show, Eq, Ord)
1N/A
1N/Ainstance Pretty CspCASLSen where
1N/A -- Not implemented yet - the pretty printing of the casl sentences
1N/A pretty(CASLSen f) = pretty f
1N/A pretty(ProcessEq pn varList alpha proc) =
1N/A let varDoc = if (null varList)
1N/A then empty
1N/A else parens $ sepByCommas $ map pretty (map fst varList)
1N/A in pretty pn <+> varDoc <+> equals <+> pretty proc
1N/A
1N/AemptyCCSen :: CspCASLSen
1N/AemptyCCSen =
1N/A let emptyProcName = mkSimpleId "empty"
1N/A emptyVarList = []
1N/A emptyAlphabet = Set.empty
1N/A emptyProc = Skip nullRange
1N/A in ProcessEq emptyProcName emptyVarList emptyAlphabet emptyProc
1N/A
1N/AisCASLSen :: CspCASLSen -> Bool
1N/AisCASLSen (CASLSen _) = True
1N/AisCASLSen _ = False
1N/A
1N/AisProcessEq :: CspCASLSen -> Bool
1N/AisProcessEq (ProcessEq _ _ _ _) = True
1N/AisProcessEq _ = False
1N/A
1N/A