Morphism.hs revision 59917a4f0a6a20f5a20bcab1f2a0a0774db56807
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederModule : $Header$
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederDescription : Instance of class Logic for propositional logic
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederMaintainer : luecke@tzi.de
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederStability : experimental
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederPortability : portable
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederDefinition of morphisms for propositional logic
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder What is a Logic?.
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder Morphism (..) -- datatype for Morphisms
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder ,pretty -- pretty printing
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder ,idMor -- identity morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder ,isLegalMorphism -- check if morhpism is ok
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder ,composeMor -- composition
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport qualified Data.Map as Map
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederimport qualified Data.Set as Set
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- Maps are simple maps between elements of sets
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- By the definition of maps in Common.Lib.Map
bcd232120234d3cbbfd730b64a5a165f5c16e2a9Christian Maeder-- these maps are injective
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maedertype PropMap = Map.Map Id Id
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | The datatype for morphisms in propositional logic as
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- | simple injective maps of sets
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederdata Morphism = Morphism
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder source :: Sign
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder , target :: Sign
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder , propMap :: PropMap
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder } deriving (Eq, Show)
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederinstance Pretty Morphism where
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder pretty = printMorphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederinstance Typeable Morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederinstance ShATermConvertible Morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- | Constructs an id-morphism as the diagonal
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederidMor :: Sign -> Morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederidMor a = Morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder , propMap = makeIdMor $ items a
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder makeIdMor :: (Ord b) => Set.Set b -> Map.Map b b
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder makeIdMor b = Set.fold (\x -> Map.insert x x) Map.empty b
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- | Determines whether a morphism is valid
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- since all maps from sets to sets are ok,
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- this value is glued to true
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederisLegalMorphism :: Morphism -> Bool
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederisLegalMorphism _ = True
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- | Composition of morphisms in propositional Logic
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- possibly there are far better way to solve this,
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder-- but I am jsut a n00b :)
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaedercomposeMor :: Morphism -> Morphism -> Result Morphism
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaedercomposeMor f g
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder | fTarget /= gSource = fail "Morphisms are not composable"
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder | otherwise = return Morphism
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder source = fSource
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , target = gTarget
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder , propMap = composeHelper fassoc gMap Map.empty
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder fSource = source f
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder fTarget = target f
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder gSource = source g
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder gTarget = target g
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder fMap = propMap f
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder gMap = propMap g
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder composeHelper :: (Ord a, Ord k, Ord b) => [(k, a)] -> Map.Map a b
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder composeHelper [] _ newMor = newMor
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder composeHelper ((k, a):xs) h newMor =
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Nothing -> composeHelper xs h newMor
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder Just v -> composeHelper xs h (Map.insert k v newMor)
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-- | Pretty printing for Morphisms
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian MaederprintMorphism :: Morphism -> Doc
9eaf4ea0944f7c5a1773c5f3c066f0117ece22dbChristian MaederprintMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder <> vcat (map ( \ (x, y) -> lparen <> idDoc x <> text ","
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder <> idDoc y <> rparen) $ Map.assocs $ propMap m)