{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : ./CSL/Morphism.hs
Description : Abstract syntax for reduce
Copyright : (c) Dominik Dietrich, DFKI Bremen 2010
License : GPLv2 or higher, see LICENSE.txt
Maintainer : dominik.dietrich@dfki.de
Stability : experimental
Portability : portable
this file defines morhpisms for the reduce logic. A morphism is a mapping of operator symbols
-}
module CSL.Morphism
( Morphism (..) -- datatype for Morphisms
, pretty -- pretty printing
, idMor -- identity morphism
, composeMor -- composition
, inclusionMap -- inclusion map
, mapSentence -- map of sentences
, mapSentenceH -- map of sentences, without Result type
, applyMap -- application function for maps
, applyMorphism -- application function for morphism
, morphismUnion
) where
import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set
import CSL.Sign as Sign
import CSL.AS_BASIC_CSL
import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils
import qualified Common.Result as Result
-- | The datatype for morphisms in reduce logic as maps of sets
data Morphism = Morphism
{ source :: Sign
, target :: Sign
, operatorMap :: Map.Map Id Id
} deriving (Show, Eq, Ord, Typeable, Data)
instance Pretty Morphism where
pretty = printMorphism
-- | pretty printer for morphisms
printMorphism :: Morphism -> Doc
printMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
<> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
<> pretty y <> rparen) $ Map.assocs $ operatorMap m)
-- | Constructs an id-morphism
idMor :: Sign -> Morphism
idMor a = inclusionMap a a
-- | calculates the composition of two morhpisms f:X->Y, g:Y->Z
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g =
let fSource = source f
gTarget = target g
fMap = operatorMap f
gMap = operatorMap g
in return Morphism
{ source = fSource
, target = gTarget
, operatorMap = if Map.null gMap then fMap else
Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
if i == j then id else Map.insert i j)
Map.empty $ opIds fSource }
-- | constructs the inclusion map for a given signature
inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
inclusionMap s1 s2 = Morphism
{ source = s1
, target = s2
, operatorMap = Map.empty }
-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap operatormap idt = Map.findWithDefault idt idt operatormap
-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor idt = Map.findWithDefault idt idt $ operatorMap mor
{- | sentence translation along signature morphism
here just the renaming of formulae -}
mapSentence :: Morphism -> CMD -> Result.Result CMD
mapSentence mor = return . mapSentenceH mor
mapSentenceH :: Morphism -> CMD -> CMD
mapSentenceH _ frm = frm
morphismUnion :: Morphism -> Morphism -> Result.Result Morphism
morphismUnion mor1 mor2 =
let pmap1 = operatorMap mor1
pmap2 = operatorMap mor2
p1 = source mor1
p2 = source mor2
up1 = Set.difference (opIds p1) $ Map.keysSet pmap1
up2 = Set.difference (opIds p2) $ Map.keysSet pmap2
(pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
Nothing -> (ds, Map.insert i j m)
Just k -> if j == k then (ds, m) else
(Diag Error
("incompatible mapping of prop " ++ showId i " to "
++ showId j " and " ++ showId k "")
nullRange : ds, m)) ([], pmap1)
(Map.toList pmap2 ++ map (\ a -> (a, a))
(Set.toList $ Set.union up1 up2))
in if null pds then return Morphism
{ source = unite p1 p2
, target = unite (target mor1) $ target mor2
, operatorMap = pmap } else Result pds Nothing