1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederDescription : Morphisms in Temporal logic
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeCopyright : (c) Dominik Luecke, Uni Bremen 2007
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeMaintainer : luecke@informatik.uni-bremen.de
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability : experimental
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : portable
501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder Definition of morphisms for temporal logic
501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder What is a Logic?.
501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ( Morphism (..) -- datatype for Morphisms
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , pretty -- pretty printing
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , idMor -- identity morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , isLegalMorphism -- check if morhpism is ok
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , composeMor -- composition
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , inclusionMap -- inclusion map
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , mapSentence -- map of sentences
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , mapSentenceH -- map of sentences, without Result type
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , applyMap -- application function for maps
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , applyMorphism -- application function for morphism
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Data.Map as Map
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Data.Set as Set
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Temporal.AS_BASIC_Temporal as AS_BASIC
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Common.Result as Result
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | The datatype for morphisms in temporal logic as
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkedata Morphism = Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { source :: Sign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , target :: Sign
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , propMap :: Map.Map Id Id
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Eq, Ord, Show, Typeable)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeinstance Pretty Morphism where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke pretty = printMorphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | Constructs an id-morphism
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeidMor :: Sign -> Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederidMor a = inclusionMap a a
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | Determines whether a morphism is valid
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederisLegalMorphism :: Morphism -> Result ()
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeisLegalMorphism pmor =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder let psource = items $ source pmor
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ptarget = items $ target pmor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pdom = Map.keysSet $ propMap pmor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pcodom = Set.map (applyMorphism pmor) psource
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in unless (Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource) $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fail "illegal Temporal morphism"
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | Application funtion for morphisms
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeapplyMorphism :: Morphism -> Id -> Id
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | Application function for propMaps
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeapplyMap :: Map.Map Id Id -> Id -> Id
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeapplyMap pmap idt = Map.findWithDefault idt idt pmap
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder-- | Composition of morphisms in temporal Logic
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecomposeMor :: Morphism -> Morphism -> Result Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedercomposeMor f g =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder let fSource = source f
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke gTarget = target g
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder fMap = propMap f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder gMap = propMap g
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder in return Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { source = fSource
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , target = gTarget
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , propMap = if Map.null gMap then fMap else
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder if i == j then id else Map.insert i j)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Map.empty $ items fSource }
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | Pretty printing for Morphisms
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeprintMorphism :: Morphism -> Doc
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke <> pretty y <> rparen) $ Map.assocs $ propMap m)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke-- | Inclusion map of a subsig into a supersig
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederinclusionMap s1 s2 = Morphism
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { source = s1
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , target = s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- | sentence translation along signature morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederhere just the renaming of formulae -}
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkemapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedermapSentence mor = return . mapSentenceH mor
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkemapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA