2796N/A{- |

2796N/AModule : $Header$

2796N/ADescription : Abstract syntax for reduce

2796N/ACopyright : (c) Dominik Dietrich, DFKI Bremen 2010

2796N/ALicense : GPLv2 or higher

2796N/A

2796N/AMaintainer : dominik.dietrich@dfki.de

2796N/AStability : experimental

2796N/APortability : portable

2796N/A

2796N/Athis file defines morhpisms for the reduce logic. A morphism is a mapping of operator symbols

2796N/A-}

2796N/A

2796N/A

2796N/Amodule CSL.Morphism

2796N/A ( Morphism (..) -- datatype for Morphisms

2796N/A , pretty -- pretty printing

2796N/A , idMor -- identity morphism

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

2796N/A , composeMor -- composition

2796N/A , inclusionMap -- inclusion map

2796N/A , mapSentence -- map of sentences

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

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

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

2796N/A , morphismUnion

2796N/A ) where

2796N/A

2796N/Aimport qualified Data.Map as Map

2796N/Aimport qualified Data.Set as Set

2796N/Aimport CSL.Sign as Sign

2796N/Aimport qualified Common.Result as Result

2796N/Aimport CSL.AS_BASIC_CSL

2796N/Aimport Common.Id as Id

2796N/Aimport Common.Result

2796N/Aimport Common.Doc

2796N/Aimport Common.DocUtils

2796N/A

2796N/A-- | The datatype for morphisms in reduce logic as maps of sets

2796N/Adata Morphism = Morphism

2796N/A { source :: Sign

2796N/A , target :: Sign

2796N/A , operatorMap :: Map.Map Id Id

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

2796N/A

2796N/Ainstance Pretty Morphism where

2796N/A pretty = printMorphism

2796N/A

2796N/A-- | pretty printer for morphisms

2796N/AprintMorphism :: Morphism -> Doc

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

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

2796N/A <> pretty y <> rparen) $ Map.assocs $ operatorMap m)

2796N/A

2796N/A

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

2796N/AidMor :: Sign -> Morphism

2796N/AidMor a = inclusionMap a a

2796N/A

2796N/A-- | checks whether a given morphism is legal

2796N/AisLegalMorphism :: Morphism -> Bool

2796N/AisLegalMorphism _ = True

2796N/A

2796N/A-- | calculates the composition of two morhpisms f:X->Y, g:Y->Z

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

2796N/AcomposeMor f g =

2796N/A 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 $ items 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 (items p1) $ Map.keysSet pmap1

up2 = Set.difference (items 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