4169N/A{- |

1178N/AModule : $Header$

1178N/ADescription : Morphism of Common Logic

1178N/ACopyright : (c) Uni Bremen DFKI 2010

1178N/ALicense : GPLv2 or higher, see LICENSE.txt

1178N/A

1178N/AMaintainer : kluc@informatik.uni-bremen.de

1178N/AStability : experimental

1178N/APortability : non-portable (via Logic.Logic)

1178N/A

1178N/AMorphism of Common Logic

1178N/A

1178N/A-}

1178N/A

1178N/Amodule CommonLogic.Morphism

1178N/A ( Morphism (..)

1178N/A , pretty -- pretty printing

2362N/A , idMor -- identity morphism

2362N/A , isLegalMorphism -- check if morhpism is ok

2362N/A , composeMor -- composition

1178N/A , inclusionMap -- inclusion map

4169N/A , mkMorphism -- create Morphism

1178N/A , mapSentence -- map of sentences

1178N/A , mapSentenceH -- map of sentences, without Result type

4033N/A , applyMap -- application function for maps

4033N/A , applyMorphism -- application function for morphism

1178N/A , morphismUnion

1178N/A ) where

1178N/A

1178N/Aimport qualified Data.Map as Map

4033N/Aimport qualified Data.Set as Set

1178N/Aimport qualified Common.Result as Result

1178N/Aimport Common.Id as Id

4033N/Aimport Common.Result

1178N/Aimport Common.Doc

1178N/Aimport Common.DocUtils

4033N/A

1178N/Aimport CommonLogic.AS_CommonLogic as AS_BASIC

1178N/Aimport CommonLogic.Sign as Sign

4033N/A

1178N/A-- maps of sets

1178N/Adata Morphism = Morphism

4033N/A { source :: Sign

1178N/A , target :: Sign

1178N/A , propMap :: Map.Map Id Id

1178N/A } deriving (Eq, Ord, Show)

4033N/A

0N/Ainstance Pretty Morphism where

0N/A pretty = printMorphism

0N/A

0N/A-- | Constructs an id-morphism

0N/AidMor :: Sign -> Morphism

0N/AidMor a = inclusionMap a a

0N/A

0N/A-- | Determines whether a morphism is valid

0N/AisLegalMorphism :: Morphism -> Bool

0N/AisLegalMorphism pmor =

0N/A let psource = items $ source pmor

4033N/A ptarget = items $ target pmor

0N/A pdom = Map.keysSet $ propMap pmor

1178N/A pcodom = Set.map (applyMorphism pmor) psource

0N/A in Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource

1178N/A

4033N/A-- | Application funtion for morphisms

1178N/AapplyMorphism :: Morphism -> Id -> Id

0N/AapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor

1178N/A

4033N/A-- | Application function for propMaps

4033N/AapplyMap :: Map.Map Id Id -> Id -> Id

4033N/AapplyMap pmap idt = Map.findWithDefault idt idt pmap

0N/A

4033N/A-- | Composition of morphisms in propositional Logic

1178N/AcomposeMor :: Morphism -> Morphism -> Result Morphism

4033N/AcomposeMor f g =

4033N/A let fSource = source f

4033N/A gTarget = target g

4033N/A fMap = propMap f

1178N/A gMap = propMap g

4033N/A in return Morphism

0N/A { source = fSource

4033N/A , target = gTarget

4033N/A , propMap = if Map.null gMap then fMap else

4033N/A Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in

4033N/A if i == j then id else Map.insert i j)

0N/A Map.empty $ items fSource }

1178N/A

0N/A-- | Pretty printing for Morphisms

4033N/AprintMorphism :: Morphism -> Doc

1178N/AprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)

1178N/A <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","

1178N/A <> pretty y <> rparen) $ Map.assocs $ propMap m)

0N/A

4033N/A-- | Inclusion map of a subsig into a supersig

1178N/AinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism

1178N/AinclusionMap s1 s2 = Morphism

4033N/A { source = s1

1178N/A , target = s2

1178N/A , propMap = Map.empty }

4033N/A

1178N/A-- | creates a Morphism

4033N/AmkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism

1178N/AmkMorphism s t p =

1178N/A Morphism { source = s

1178N/A , target = t

1178N/A , propMap = p }

4033N/A

1178N/A-- | sentence translation along signature morphism

4033N/A-- here just the renaming of formulae

4033N/AmapSentence :: Morphism -> AS_BASIC.SENTENCE -> Result.Result AS_BASIC.SENTENCE

0N/AmapSentence mor = return . mapSentenceH mor

4033N/A

4033N/AmapSentenceH :: Morphism -> AS_BASIC.SENTENCE -> AS_BASIC.SENTENCE

0N/AmapSentenceH mor frm = case frm of

0N/A AS_BASIC.Quant_sent qs rn -> case qs of

0N/A AS_BASIC.Universal xs sen -> AS_BASIC.Quant_sent

0N/A (AS_BASIC.Universal xs (mapSentenceH mor sen)) rn -- fix

0N/A AS_BASIC.Existential xs sen -> AS_BASIC.Quant_sent

0N/A (AS_BASIC.Existential xs (mapSentenceH mor sen)) rn -- fix

0N/A AS_BASIC.Bool_sent bs rn -> case bs of

0N/A AS_BASIC.Conjunction sens -> AS_BASIC.Bool_sent

0N/A (AS_BASIC.Conjunction (map (mapSentenceH mor) sens)) rn

4033N/A AS_BASIC.Disjunction sens -> AS_BASIC.Bool_sent

0N/A (AS_BASIC.Disjunction (map (mapSentenceH mor) sens)) rn

1178N/A AS_BASIC.Negation sen -> AS_BASIC.Bool_sent

0N/A (AS_BASIC.Negation (mapSentenceH mor sen)) rn

4033N/A AS_BASIC.Implication s1 s2 -> AS_BASIC.Bool_sent

1178N/A (AS_BASIC.Implication (mapSentenceH mor s1) (mapSentenceH mor s2)) rn

4033N/A AS_BASIC.Biconditional s1 s2 -> AS_BASIC.Bool_sent

4033N/A (AS_BASIC.Biconditional (mapSentenceH mor s1) (mapSentenceH mor s2))

1178N/A rn

4033N/A AS_BASIC.Atom_sent atom rn -> AS_BASIC.Atom_sent atom rn -- fix

4033N/A AS_BASIC.Comment_sent cm sen rn -> AS_BASIC.Comment_sent cm sen rn -- unused

0N/A AS_BASIC.Irregular_sent sen rn -> AS_BASIC.Irregular_sent sen rn -- unused

4033N/A

4033N/A{-

1178N/A AS_BASIC.Predication predH -> AS_BASIC.Predication

1178N/A $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH

0N/A-}

4033N/A

0N/AmorphismUnion :: Morphism -> Morphism -> Result.Result Morphism

0N/AmorphismUnion mor1 mor2 =

0N/A let pmap1 = propMap mor1

1178N/A pmap2 = propMap mor2

1178N/A p1 = source mor1

4033N/A p2 = source mor2

0N/A up1 = Set.difference (items p1) $ Map.keysSet pmap1

0N/A up2 = Set.difference (items p2) $ Map.keysSet pmap2

1178N/A (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of

1178N/A Nothing -> (ds, Map.insert i j m)

0N/A Just k -> if j == k then (ds, m) else

4033N/A (Diag Error

0N/A ("incompatible mapping of prop " ++ showId i " to "

0N/A ++ showId j " and " ++ showId k "")

0N/A nullRange : ds, m)) ([], pmap1)

0N/A (Map.toList pmap2 ++ map (\ a -> (a, a))

0N/A (Set.toList $ Set.union up1 up2))

0N/A in if null pds then return Morphism

{ source = unite p1 p2

, target = unite (target mor1) $ target mor2

, propMap = pmap } else Result pds Nothing