Morphism.hs revision 5096f518ac5380a0834a09b22a8b38fabe247bf5
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannModule : $Header$
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannDescription : Morphism of Common Logic
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannCopyright : (c) Uni Bremen DFKI 2010
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannLicense : similar to LGPL, see HetCATS/LICENSE.txt
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannMaintainer : kluc@informatik.uni-bremen.de
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannStability : experimental
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannPortability : non-portable (via Logic.Logic)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntemporary Dummy Morphism using Default Mprphism for Common Logic
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ( Morphism (..) -- datatype for Morphisms
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , pretty -- pretty printing
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , idMor -- identity morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , isLegalMorphism -- check if morhpism is ok
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , composeMor -- composition
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , inclusionMap -- inclusion map
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , mapSentence -- map of sentences
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , mapSentenceH -- map of sentences, without Result type
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , applyMap -- application function for maps
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , applyMorphism -- application function for morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , morphismUnion
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport qualified Data.Map as Map
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport qualified Data.Set as Set
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport qualified Common.Result as Result
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmannimport CommonLogic.AS_CommonLogic as AS_BASIC
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanntype Morphism = DefaultMorphism Sign
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | The datatype for morphisms in propositional logic as
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- maps of sets
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanndata Morphism = Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { source :: Sign
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , target :: Sign
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , propMap :: Map.Map Id Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann } deriving (Eq, Ord, Show)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmanninstance Pretty Morphism where
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann pretty = printMorphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Constructs an id-morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidMor :: Sign -> Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannidMor a = inclusionMap a a
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Determines whether a morphism is valid
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannisLegalMorphism :: Morphism -> Bool
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannisLegalMorphism pmor =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let psource = items $ source pmor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ptarget = items $ target pmor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann pdom = Map.keysSet $ propMap pmor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann pcodom = Set.map (applyMorphism pmor) psource
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann in Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Application funtion for morphisms
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannapplyMorphism :: Morphism -> Id -> Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Application function for propMaps
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannapplyMap :: Map.Map Id Id -> Id -> Id
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannapplyMap pmap idt = Map.findWithDefault idt idt pmap
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Composition of morphisms in propositional Logic
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncomposeMor :: Morphism -> Morphism -> Result Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanncomposeMor f g =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let fSource = source f
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann gTarget = target g
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann fMap = propMap f
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann gMap = propMap g
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann in return Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { source = fSource
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , target = gTarget
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , propMap = if Map.null gMap then fMap else
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann if i == j then id else Map.insert i j)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Map.empty $ items fSource }
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Pretty printing for Morphisms
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannprintMorphism :: Morphism -> Doc
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann <> pretty y <> rparen) $ Map.assocs $ propMap m)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | Inclusion map of a subsig into a supersig
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanninclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmanninclusionMap s1 s2 = Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { source = s1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , target = s2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- | sentence translation along signature morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann-- here just the renaming of formulae
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapSentence :: Morphism -> AS_BASIC.SENTENCE -> Result.Result AS_BASIC.SENTENCE
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapSentence mor = return . mapSentenceH mor
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapSentenceH :: Morphism -> AS_BASIC.SENTENCE -> AS_BASIC.SENTENCE
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmapSentenceH mor frm = case frm of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Quant_sent form rn -> case form of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (mapSentenceH mor form1) (mapSentenceH mor form2) rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (mapSentenceH mor form1) (mapSentenceH mor form2) rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.True_atom rn -> AS_BASIC.True_atom rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.False_atom rn -> AS_BASIC.False_atom rn
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann AS_BASIC.Predication predH -> AS_BASIC.Predication
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel HausmannmorphismUnion mor1 mor2 =
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann let pmap1 = propMap mor1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann pmap2 = propMap mor2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann p1 = source mor1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann p2 = source mor2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann up1 = Set.difference (items p1) $ Map.keysSet pmap1
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann up2 = Set.difference (items p2) $ Map.keysSet pmap2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Nothing -> (ds, Map.insert i j m)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann Just k -> if j == k then (ds, m) else
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ("incompatible mapping of prop " ++ showId i " to "
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann ++ showId j " and " ++ showId k "")
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann nullRange : ds, m)) ([], pmap1)
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann (Map.toList pmap2 ++ map (\ a -> (a, a))
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann in if null pds then return Morphism
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann { source = unite p1 p2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , target = unite (target mor1) $ target mor2
74dfa6bc521350525358340117512f8afe9fdd26Daniel Hausmann , propMap = pmap } else Result pds Nothing