hets/CspCASL/SignCSP.hs

	SignCSP.hs revision b4fbc96e05117839ca409f5f20f97b3ac872d1ed
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachModule      :  $Header$
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright   :  (c) Markus Roggenbach and Till Mossakowski and Uni Bremen 2004
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachLicence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer  :  M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability   :  provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability :  portable
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach  signatures for CSP-CASL
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski{- todo:  implement isInclusion, computeExt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachmodule CspCASL.SignCSP where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport CASL.AS_Basic_CASL
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport CASL.Sign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport CASL.Morphism
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport Common.Id
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Map as Map
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport qualified Common.Lib.Set as Set
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiimport Data.Dynamic
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiimport Common.DynamicUtils
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiimport Common.Lib.Pretty
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiimport Common.PrettyPrint
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiimport Common.PrintLaTeX
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata CSPAddSign = CSPAddSign { channelNames :: Map.Map Id SORT
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach                             , processNames :: Map.Map Id (Maybe SORT)}
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski                  deriving (Eq, Show)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype CSPSign = Sign () CSPAddSign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachemptyCSPAddSign :: CSPAddSign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachemptyCSPAddSign = CSPAddSign { channelNames = Map.empty
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach                       , processNames = Map.empty
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach                       }
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
e99df192a380bfa91e3261c911751bb034c09a17Till MossakowskidiffCSPAddSign :: CSPAddSign -> CSPAddSign -> CSPAddSign
e99df192a380bfa91e3261c911751bb034c09a17Till MossakowskidiffCSPAddSign a b =
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski    a { channelNames = channelNames a `Map.difference` channelNames b,
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski        processNames = processNames a `Map.difference` processNames b
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski      }
e99df192a380bfa91e3261c911751bb034c09a17Till Mossakowski
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskidiffCSPSign :: CSPSign -> CSPSign -> CSPSign
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskidiffCSPSign sig1 sig2 =
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski  diffSig sig1 sig2
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski     { extendedInfo = extendedInfo sig1 `diffCSPAddSign` extendedInfo sig2 }
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachemptyCSPSign :: CSPSign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachemptyCSPSign = emptySign emptyCSPAddSign
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion :: CSPAddSign -> CSPAddSign -> Bool
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskiisInclusion _ _ = True
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachdata CSPAddMorphism =
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach     CSPAddMorphism { channelMap :: Map.Map Id Id
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach                    , processMap :: Map.Map Id Id
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach                    }
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski     deriving (Eq, Show)
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachtype CSPMorphism = Morphism () CSPAddSign CSPAddMorphism
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
1df33829303cbf924aa018ac5ce9a28e69c17d22Till MossakowskicomputeExt :: Ext () CSPAddSign CSPAddMorphism
3c046d52053fee2b80b00b8236072a261b880d3eTill MossakowskicomputeExt _ _  =
3c046d52053fee2b80b00b8236072a261b880d3eTill Mossakowski  CSPAddMorphism { channelMap = Map.empty -- ???
3c046d52053fee2b80b00b8236072a261b880d3eTill Mossakowski                 , processMap = Map.empty -- ???
3c046d52053fee2b80b00b8236072a261b880d3eTill Mossakowski                 }
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till MossakowskisignTc      = mkTyCon "CspCASL.SignCSP.CSPAddSign"
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiinstance Typeable CSPAddSign where
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski  typeOf _ = mkTyConApp signTc []
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till MossakowskimorTc      = mkTyCon "CspCASL.SignCSP.CSPAddMorphism"
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowskiinstance Typeable CSPAddMorphism where
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski  typeOf _ = mkTyConApp morTc []
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski
b3dca469a9e267d6d71acfdeca7bf284d0581dc7Till Mossakowski-- dummy instances, need to be elaborated!
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiinstance PrettyPrint CSPAddSign where
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski  printText0 _ x = ptext $ show x
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiinstance PrettyPrint CSPAddMorphism where
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski  printText0 _ x = ptext $ show x
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiinstance PrintLaTeX CSPAddSign where
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski  printLatex0 _ x = ptext $ show x
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowskiinstance PrintLaTeX CSPAddMorphism where
1df33829303cbf924aa018ac5ce9a28e69c17d22Till Mossakowski  printLatex0 _ x = ptext $ show x