{-# 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 { Morphism -> Sign source :: Sign , Morphism -> Sign target :: Sign , Morphism -> Map Id Id operatorMap :: Map.Map Id Id } deriving (Int -> Morphism -> ShowS [Morphism] -> ShowS Morphism -> String (Int -> Morphism -> ShowS) -> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Morphism] -> ShowS $cshowList :: [Morphism] -> ShowS show :: Morphism -> String $cshow :: Morphism -> String showsPrec :: Int -> Morphism -> ShowS $cshowsPrec :: Int -> Morphism -> ShowS Show, Morphism -> Morphism -> Bool (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> Eq Morphism forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: Morphism -> Morphism -> Bool $c/= :: Morphism -> Morphism -> Bool == :: Morphism -> Morphism -> Bool $c== :: Morphism -> Morphism -> Bool Eq, Eq Morphism Eq Morphism => (Morphism -> Morphism -> Ordering) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Morphism) -> (Morphism -> Morphism -> Morphism) -> Ord Morphism Morphism -> Morphism -> Bool Morphism -> Morphism -> Ordering Morphism -> Morphism -> Morphism forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Morphism -> Morphism -> Morphism $cmin :: Morphism -> Morphism -> Morphism max :: Morphism -> Morphism -> Morphism $cmax :: Morphism -> Morphism -> Morphism >= :: Morphism -> Morphism -> Bool $c>= :: Morphism -> Morphism -> Bool > :: Morphism -> Morphism -> Bool $c> :: Morphism -> Morphism -> Bool <= :: Morphism -> Morphism -> Bool $c<= :: Morphism -> Morphism -> Bool < :: Morphism -> Morphism -> Bool $c< :: Morphism -> Morphism -> Bool compare :: Morphism -> Morphism -> Ordering $ccompare :: Morphism -> Morphism -> Ordering $cp1Ord :: Eq Morphism Ord, Typeable, Typeable Morphism Constr DataType Typeable Morphism => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism) -> (Morphism -> Constr) -> (Morphism -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Morphism)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism)) -> ((forall b. Data b => b -> b) -> Morphism -> Morphism) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r) -> (forall u. (forall d. Data d => d -> u) -> Morphism -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism) -> Data Morphism Morphism -> Constr Morphism -> DataType (forall b. Data b => b -> b) -> Morphism -> Morphism (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism forall a. Typeable a => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> a -> c a) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c a) -> (a -> Constr) -> (a -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c a)) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a)) -> ((forall b. Data b => b -> b) -> a -> a) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r) -> (forall u. (forall d. Data d => d -> u) -> a -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> a -> m a) -> Data a forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u forall u. (forall d. Data d => d -> u) -> Morphism -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Morphism) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism) $cMorphism :: Constr $tMorphism :: DataType gmapMo :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism $cgmapMo :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapMp :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism $cgmapMp :: forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapM :: (forall d. Data d => d -> m d) -> Morphism -> m Morphism $cgmapM :: forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> Morphism -> m Morphism gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism -> u $cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Morphism -> u gmapQ :: (forall d. Data d => d -> u) -> Morphism -> [u] $cgmapQ :: forall u. (forall d. Data d => d -> u) -> Morphism -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r $cgmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r $cgmapQl :: forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Morphism -> r gmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism $cgmapT :: (forall b. Data b => b -> b) -> Morphism -> Morphism dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism) $cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Morphism) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Morphism) $cdataCast1 :: forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Morphism) dataTypeOf :: Morphism -> DataType $cdataTypeOf :: Morphism -> DataType toConstr :: Morphism -> Constr $ctoConstr :: Morphism -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism $cgunfold :: forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Morphism gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism $cgfoldl :: forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Morphism -> c Morphism $cp1Data :: Typeable Morphism Data) instance Pretty Morphism where pretty :: Morphism -> Doc pretty = Morphism -> Doc printMorphism -- | pretty printer for morphisms printMorphism :: Morphism -> Doc printMorphism :: Morphism -> Doc printMorphism m :: Morphism m = Sign -> Doc forall a. Pretty a => a -> Doc pretty (Morphism -> Sign source Morphism m) Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> String -> Doc text "-->" Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> Sign -> Doc forall a. Pretty a => a -> Doc pretty (Morphism -> Sign target Morphism m) Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> [Doc] -> Doc vcat (((Id, Id) -> Doc) -> [(Id, Id)] -> [Doc] forall a b. (a -> b) -> [a] -> [b] map ( \ (x :: Id x, y :: Id y) -> Doc lparen Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> Id -> Doc forall a. Pretty a => a -> Doc pretty Id x Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> String -> Doc text "," Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> Id -> Doc forall a. Pretty a => a -> Doc pretty Id y Doc -> Doc -> Doc forall a. Semigroup a => a -> a -> a <> Doc rparen) ([(Id, Id)] -> [Doc]) -> [(Id, Id)] -> [Doc] forall a b. (a -> b) -> a -> b $ Map Id Id -> [(Id, Id)] forall k a. Map k a -> [(k, a)] Map.assocs (Map Id Id -> [(Id, Id)]) -> Map Id Id -> [(Id, Id)] forall a b. (a -> b) -> a -> b $ Morphism -> Map Id Id operatorMap Morphism m) -- | Constructs an id-morphism idMor :: Sign -> Morphism idMor :: Sign -> Morphism idMor a :: Sign a = Sign -> Sign -> Morphism inclusionMap Sign a Sign a -- | calculates the composition of two morhpisms f:X->Y, g:Y->Z composeMor :: Morphism -> Morphism -> Result Morphism composeMor :: Morphism -> Morphism -> Result Morphism composeMor f :: Morphism f g :: Morphism g = let fSource :: Sign fSource = Morphism -> Sign source Morphism f gTarget :: Sign gTarget = Morphism -> Sign target Morphism g fMap :: Map Id Id fMap = Morphism -> Map Id Id operatorMap Morphism f gMap :: Map Id Id gMap = Morphism -> Map Id Id operatorMap Morphism g in Morphism -> Result Morphism forall (m :: * -> *) a. Monad m => a -> m a return Morphism :: Sign -> Sign -> Map Id Id -> Morphism Morphism { source :: Sign source = Sign fSource , target :: Sign target = Sign gTarget , operatorMap :: Map Id Id operatorMap = if Map Id Id -> Bool forall k a. Map k a -> Bool Map.null Map Id Id gMap then Map Id Id fMap else (Id -> Map Id Id -> Map Id Id) -> Map Id Id -> Set Id -> Map Id Id forall a b. (a -> b -> b) -> b -> Set a -> b Set.fold ( \ i :: Id i -> let j :: Id j = Map Id Id -> Id -> Id applyMap Map Id Id gMap (Map Id Id -> Id -> Id applyMap Map Id Id fMap Id i) in if Id i Id -> Id -> Bool forall a. Eq a => a -> a -> Bool == Id j then Map Id Id -> Map Id Id forall a. a -> a id else Id -> Id -> Map Id Id -> Map Id Id forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Id i Id j) Map Id Id forall k a. Map k a Map.empty (Set Id -> Map Id Id) -> Set Id -> Map Id Id forall a b. (a -> b) -> a -> b $ Sign -> Set Id opIds Sign fSource } -- | constructs the inclusion map for a given signature inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism inclusionMap :: Sign -> Sign -> Morphism inclusionMap s1 :: Sign s1 s2 :: Sign s2 = Morphism :: Sign -> Sign -> Map Id Id -> Morphism Morphism { source :: Sign source = Sign s1 , target :: Sign target = Sign s2 , operatorMap :: Map Id Id operatorMap = Map Id Id forall k a. Map k a Map.empty } -- | Application function for propMaps applyMap :: Map.Map Id Id -> Id -> Id applyMap :: Map Id Id -> Id -> Id applyMap operatormap :: Map Id Id operatormap idt :: Id idt = Id -> Id -> Map Id Id -> Id forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault Id idt Id idt Map Id Id operatormap -- | Application funtion for morphisms applyMorphism :: Morphism -> Id -> Id applyMorphism :: Morphism -> Id -> Id applyMorphism mor :: Morphism mor idt :: Id idt = Id -> Id -> Map Id Id -> Id forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault Id idt Id idt (Map Id Id -> Id) -> Map Id Id -> Id forall a b. (a -> b) -> a -> b $ Morphism -> Map Id Id operatorMap Morphism mor {- | sentence translation along signature morphism here just the renaming of formulae -} mapSentence :: Morphism -> CMD -> Result.Result CMD mapSentence :: Morphism -> CMD -> Result CMD mapSentence mor :: Morphism mor = CMD -> Result CMD forall (m :: * -> *) a. Monad m => a -> m a return (CMD -> Result CMD) -> (CMD -> CMD) -> CMD -> Result CMD forall b c a. (b -> c) -> (a -> b) -> a -> c . Morphism -> CMD -> CMD mapSentenceH Morphism mor mapSentenceH :: Morphism -> CMD -> CMD mapSentenceH :: Morphism -> CMD -> CMD mapSentenceH _ frm :: CMD frm = CMD frm morphismUnion :: Morphism -> Morphism -> Result.Result Morphism morphismUnion :: Morphism -> Morphism -> Result Morphism morphismUnion mor1 :: Morphism mor1 mor2 :: Morphism mor2 = let pmap1 :: Map Id Id pmap1 = Morphism -> Map Id Id operatorMap Morphism mor1 pmap2 :: Map Id Id pmap2 = Morphism -> Map Id Id operatorMap Morphism mor2 p1 :: Sign p1 = Morphism -> Sign source Morphism mor1 p2 :: Sign p2 = Morphism -> Sign source Morphism mor2 up1 :: Set Id up1 = Set Id -> Set Id -> Set Id forall a. Ord a => Set a -> Set a -> Set a Set.difference (Sign -> Set Id opIds Sign p1) (Set Id -> Set Id) -> Set Id -> Set Id forall a b. (a -> b) -> a -> b $ Map Id Id -> Set Id forall k a. Map k a -> Set k Map.keysSet Map Id Id pmap1 up2 :: Set Id up2 = Set Id -> Set Id -> Set Id forall a. Ord a => Set a -> Set a -> Set a Set.difference (Sign -> Set Id opIds Sign p2) (Set Id -> Set Id) -> Set Id -> Set Id forall a b. (a -> b) -> a -> b $ Map Id Id -> Set Id forall k a. Map k a -> Set k Map.keysSet Map Id Id pmap2 (pds :: [Diagnosis] pds, pmap :: Map Id Id pmap) = ((Id, Id) -> ([Diagnosis], Map Id Id) -> ([Diagnosis], Map Id Id)) -> ([Diagnosis], Map Id Id) -> [(Id, Id)] -> ([Diagnosis], Map Id Id) forall (t :: * -> *) a b. Foldable t => (a -> b -> b) -> b -> t a -> b foldr ( \ (i :: Id i, j :: Id j) (ds :: [Diagnosis] ds, m :: Map Id Id m) -> case Id -> Map Id Id -> Maybe Id forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup Id i Map Id Id m of Nothing -> ([Diagnosis] ds, Id -> Id -> Map Id Id -> Map Id Id forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Id i Id j Map Id Id m) Just k :: Id k -> if Id j Id -> Id -> Bool forall a. Eq a => a -> a -> Bool == Id k then ([Diagnosis] ds, Map Id Id m) else (DiagKind -> String -> Range -> Diagnosis Diag DiagKind Error ("incompatible mapping of prop " String -> ShowS forall a. [a] -> [a] -> [a] ++ Id -> ShowS showId Id i " to " String -> ShowS forall a. [a] -> [a] -> [a] ++ Id -> ShowS showId Id j " and " String -> ShowS forall a. [a] -> [a] -> [a] ++ Id -> ShowS showId Id k "") Range nullRange Diagnosis -> [Diagnosis] -> [Diagnosis] forall a. a -> [a] -> [a] : [Diagnosis] ds, Map Id Id m)) ([], Map Id Id pmap1) (Map Id Id -> [(Id, Id)] forall k a. Map k a -> [(k, a)] Map.toList Map Id Id pmap2 [(Id, Id)] -> [(Id, Id)] -> [(Id, Id)] forall a. [a] -> [a] -> [a] ++ (Id -> (Id, Id)) -> [Id] -> [(Id, Id)] forall a b. (a -> b) -> [a] -> [b] map (\ a :: Id a -> (Id a, Id a)) (Set Id -> [Id] forall a. Set a -> [a] Set.toList (Set Id -> [Id]) -> Set Id -> [Id] forall a b. (a -> b) -> a -> b $ Set Id -> Set Id -> Set Id forall a. Ord a => Set a -> Set a -> Set a Set.union Set Id up1 Set Id up2)) in if [Diagnosis] -> Bool forall (t :: * -> *) a. Foldable t => t a -> Bool null [Diagnosis] pds then Morphism -> Result Morphism forall (m :: * -> *) a. Monad m => a -> m a return Morphism :: Sign -> Sign -> Map Id Id -> Morphism Morphism { source :: Sign source = Sign -> Sign -> Sign unite Sign p1 Sign p2 , target :: Sign target = Sign -> Sign -> Sign unite (Morphism -> Sign target Morphism mor1) (Sign -> Sign) -> Sign -> Sign forall a b. (a -> b) -> a -> b $ Morphism -> Sign target Morphism mor2 , operatorMap :: Map Id Id operatorMap = Map Id Id pmap } else [Diagnosis] -> Maybe Morphism -> Result Morphism forall a. [Diagnosis] -> Maybe a -> Result a Result [Diagnosis] pds Maybe Morphism forall a. Maybe a Nothing