Morphism.hs revision 351145cfe8c03b4d47133c96b209f2bd6cfbf504
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer{- |
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerModule : $Header$
6b26240dca29e026900a83d51c75ca230a072a16Thiemo WiedemeyerDescription : Symbols and signature morphisms for the CspCASL logic
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerCopyright : (c) Liam O'Reilly, Markus Roggenbach, Swansea University 2008
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : csliam@swansea.ac.uk
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerStability : provisional
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerPortability : portable
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski
7520452bb30b5abbd471f82352fc4c1c937e02c5Till MossakowskiSymbols and signature morphisms for the CASL logic
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski-}
7520452bb30b5abbd471f82352fc4c1c937e02c5Till Mossakowski
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyermodule CspCASL.Morphism ( symOf,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer makeChannelNameSymbol,
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer makeProcNameSymbol
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer ) where
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport CASL.Sign
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified CASL.Morphism as CASL_Morphism
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport Common.Id(simpleIdToId)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport CspCASL.SignCSP
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport CspCASL.CspCASL_Keywords
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Map as Map
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyerimport qualified Data.Set as Set
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerchannelNameSymbType :: SymbType
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerchannelNameSymbType = OtherTypeKind channelS
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerprocessNameSymbType :: SymbType
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyerprocessNameSymbType = OtherTypeKind processS
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer-- | Calculate the set of symbols for a CspCASL signature
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyersymOf :: CspCASLSign -> Set.Set Symbol
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian MaedersymOf sigma =
521045d36343cd17dd217a81d4b9422ad6ab6a07Christian Maeder let caslSymbols = CASL_Morphism.symOf sigma -- Get CASL symbols
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer cspExt = extendedInfo sigma
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer chanNames = Map.keysSet (chans cspExt) -- Get the channel names
0193c86704431f83731015a77cb613d67ae4e3c2Thiemo Wiedemeyer procNames = Map.keysSet (procSet cspExt) -- Get the process names
109b67ffce2bad83667e2f4a319d2d7f380f91afThiemo Wiedemeyer -- Make channel symbols from names
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer chanNameSymbols = Set.map makeChannelNameSymbol chanNames
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer -- Make process name symbols from names
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer procNameSymbols = Set.map makeProcNameSymbol procNames
8836fa284a241af325aa6f41234b5130b26ec4f9Thiemo Wiedemeyer in Set.unions [caslSymbols, chanNameSymbols, procNameSymbols]
331603b37dec12e37e2e1df9634ef0f2c5c73ddfThiemo Wiedemeyer
7ae38566aaf40710cd83ffa3ba25655c4ad22741Thiemo WiedemeyermakeChannelNameSymbol :: CHANNEL_NAME -> Symbol
1a389234e68da7c3d087b038307ed8c66fc6dc32Thiemo WiedemeyermakeChannelNameSymbol c =
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer Symbol {symName = simpleIdToId c, symbType = channelNameSymbType}
66fd8f017efdb8a6c862c3f1856dfaef90865dd5Thiemo Wiedemeyer
38122cbf09ad3dcc31a826cc4093f630515a5cfcChristian MaedermakeProcNameSymbol :: PROCESS_NAME -> Symbol
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo WiedemeyermakeProcNameSymbol p =
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer Symbol {symName = simpleIdToId p, symbType = processNameSymbType}
53e76316f409f6b1b57ed3d2e5cb9cfe1cb511e5Thiemo Wiedemeyer