1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{-# LANGUAGE DeriveDataTypeable #-}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDescription : Morphisms in Propositional logic extended with QBFs
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederCopyright : (c) Jonathan von Schroeder, DFKI GmbH 2010
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederMaintainer : <jonathan.von_schroeder@dfki.de>
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederStability : experimental
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederPortability : portable
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederDefinition of morphisms for propositional logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder What is a Logic?.
654eedbcf7478c0d24ecba13325cf57ac2858071Christian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ( Morphism (..) -- datatype for Morphisms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , pretty -- pretty printing
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , idMor -- identity morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , isLegalMorphism -- check if morhpism is ok
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , composeMor -- composition
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , inclusionMap -- inclusion map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , mapSentence -- map of sentences
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , mapSentenceH -- map of sentences, without Result type
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , applyMap -- application function for maps
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , applyMorphism -- application function for morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , morphismUnion
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Map as Map
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified Data.Set as Set
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederimport qualified QBF.AS_BASIC_QBF as AS_BASIC
1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport qualified Common.Result as Result
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder{- | The datatype for morphisms in propositional logic as
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederdata Morphism = Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder { source :: Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , target :: Sign
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , propMap :: Map.Map Id Id
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroederinstance Pretty Morphism where
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder pretty = printMorphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Constructs an id-morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederidMor :: Sign -> Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederidMor a = inclusionMap a a
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Determines whether a morphism is valid
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederisLegalMorphism :: Morphism -> Result ()
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederisLegalMorphism pmor =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let psource = items $ source pmor
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ptarget = items $ target pmor
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder pdom = Map.keysSet $ propMap pmor
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder pcodom = Set.map (applyMorphism pmor) psource
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder in unless (Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource)
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder $ fail "illegal QBF morphism"
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Application funtion for morphisms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederapplyMorphism :: Morphism -> Id -> Id
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederapplyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Application function for propMaps
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederapplyMap :: Map.Map Id Id -> Id -> Id
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederapplyMap pmap idt = Map.findWithDefault idt idt pmap
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Composition of morphisms in propositional Logic
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedercomposeMor :: Morphism -> Morphism -> Result Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedercomposeMor f g =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let fSource = source f
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder gTarget = target g
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder fMap = propMap f
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder gMap = propMap g
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder in return Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder { source = fSource
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , target = gTarget
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , propMap = if Map.null gMap then fMap else
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder if i == j then id else Map.insert i j)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Map.empty $ items fSource }
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Pretty printing for Morphisms
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederprintMorphism :: Morphism -> Doc
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder <> pretty y <> rparen) $ Map.assocs $ propMap m)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder-- | Inclusion map of a subsig into a supersig
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroederinclusionMap s1 s2 = Morphism
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroeder{- | sentence translation along signature morphism
ba06b25b69be05a4733db7197940efd73976f215Jonathan von Schroederhere just the renaming of formulae -}
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermapSentence mor = return . mapSentenceH mor
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermapSentenceH mor frm = case frm of
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (mapSentenceH mor form1) (mapSentenceH mor form2) rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (mapSentenceH mor form1) (mapSentenceH mor form2) rn
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.TrueAtom rn -> AS_BASIC.TrueAtom rn
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.FalseAtom rn -> AS_BASIC.FalseAtom rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder AS_BASIC.Predication predH -> AS_BASIC.Predication
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.ForAll xs form rn -> AS_BASIC.ForAll (map
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (id2SimpleId . applyMorphism mor . Id.simpleIdToId) xs)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (mapSentenceH mor form) rn
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder AS_BASIC.Exists xs form rn -> AS_BASIC.Exists
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (map (id2SimpleId . applyMorphism mor . Id.simpleIdToId) xs)
ece3b1a5353a9af3c966a1d5453594ed35334f7bJonathan von Schroeder (mapSentenceH mor form) rn
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermorphismUnion :: Morphism -> Morphism -> Result.Result Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von SchroedermorphismUnion mor1 mor2 =
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder let pmap1 = propMap mor1
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder pmap2 = propMap mor2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder p1 = source mor1
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder p2 = source mor2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder up1 = Set.difference (items p1) $ Map.keysSet pmap1
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder up2 = Set.difference (items p2) $ Map.keysSet pmap2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Nothing -> (ds, Map.insert i j m)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder Just k -> if j == k then (ds, m) else
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ("incompatible mapping of prop " ++ showId i " to "
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder ++ showId j " and " ++ showId k "")
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder nullRange : ds, m)) ([], pmap1)
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder (Map.toList pmap2 ++ map (\ a -> (a, a))
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder in if null pds then return Morphism
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder { source = unite p1 p2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , target = unite (target mor1) $ target mor2
b35e053c2c5a5ea0f13decfd0303894861d82b4dJonathan von Schroeder , propMap = pmap } else Result pds Nothing