{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./Common/DefaultMorphism.hs Description : supply a default morphism for a given signature type Copyright : (c) C. Maeder, and Uni Bremen 2002-2006 License : GPLv2 or higher, see LICENSE.txt Maintainer : Christian.Maeder@dfki.de Stability : provisional Portability : portable Supply a default morphism for a given signature type -} -- due to functional deps the instance for Logic.Category cannot be supplied module Common.DefaultMorphism ( DefaultMorphism (..) -- constructor is only exported for ATC , ideOfDefaultMorphism , compOfDefaultMorphism , defaultInclusion ) where import Common.Keywords import Common.Doc import Common.DocUtils import Data.Data data DefaultMorphism sign = MkMorphism { DefaultMorphism sign -> sign domOfDefaultMorphism :: sign , DefaultMorphism sign -> sign codOfDefaultMorphism :: sign } deriving (Int -> DefaultMorphism sign -> ShowS [DefaultMorphism sign] -> ShowS DefaultMorphism sign -> String (Int -> DefaultMorphism sign -> ShowS) -> (DefaultMorphism sign -> String) -> ([DefaultMorphism sign] -> ShowS) -> Show (DefaultMorphism sign) forall sign. Show sign => Int -> DefaultMorphism sign -> ShowS forall sign. Show sign => [DefaultMorphism sign] -> ShowS forall sign. Show sign => DefaultMorphism sign -> String forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [DefaultMorphism sign] -> ShowS $cshowList :: forall sign. Show sign => [DefaultMorphism sign] -> ShowS show :: DefaultMorphism sign -> String $cshow :: forall sign. Show sign => DefaultMorphism sign -> String showsPrec :: Int -> DefaultMorphism sign -> ShowS $cshowsPrec :: forall sign. Show sign => Int -> DefaultMorphism sign -> ShowS Show, DefaultMorphism sign -> DefaultMorphism sign -> Bool (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> Eq (DefaultMorphism sign) forall sign. Eq sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c/= :: forall sign. Eq sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool == :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c== :: forall sign. Eq sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool Eq, Eq (DefaultMorphism sign) Eq (DefaultMorphism sign) => (DefaultMorphism sign -> DefaultMorphism sign -> Ordering) -> (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> (DefaultMorphism sign -> DefaultMorphism sign -> Bool) -> (DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign) -> (DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign) -> Ord (DefaultMorphism sign) DefaultMorphism sign -> DefaultMorphism sign -> Bool DefaultMorphism sign -> DefaultMorphism sign -> Ordering DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign 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 forall sign. Ord sign => Eq (DefaultMorphism sign) forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Ordering forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign min :: DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign $cmin :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign max :: DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign $cmax :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> DefaultMorphism sign >= :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c>= :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool > :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c> :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool <= :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c<= :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool < :: DefaultMorphism sign -> DefaultMorphism sign -> Bool $c< :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Bool compare :: DefaultMorphism sign -> DefaultMorphism sign -> Ordering $ccompare :: forall sign. Ord sign => DefaultMorphism sign -> DefaultMorphism sign -> Ordering $cp1Ord :: forall sign. Ord sign => Eq (DefaultMorphism sign) Ord, Typeable, Typeable (DefaultMorphism sign) Constr DataType Typeable (DefaultMorphism sign) => (forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign)) -> (forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign)) -> (DefaultMorphism sign -> Constr) -> (DefaultMorphism sign -> DataType) -> (forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign))) -> (forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefaultMorphism sign))) -> ((forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign) -> (forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r) -> (forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r) -> (forall u. (forall d. Data d => d -> u) -> DefaultMorphism sign -> [u]) -> (forall u. Int -> (forall d. Data d => d -> u) -> DefaultMorphism sign -> u) -> (forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign)) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign)) -> (forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign)) -> Data (DefaultMorphism sign) DefaultMorphism sign -> Constr DefaultMorphism sign -> DataType (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign)) (forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign) (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign) forall sign. Data sign => Typeable (DefaultMorphism sign) forall sign. Data sign => DefaultMorphism sign -> Constr forall sign. Data sign => DefaultMorphism sign -> DataType forall sign. Data sign => (forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign forall sign u. Data sign => Int -> (forall d. Data d => d -> u) -> DefaultMorphism sign -> u forall sign u. Data sign => (forall d. Data d => d -> u) -> DefaultMorphism sign -> [u] forall sign r r'. Data sign => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r forall sign r r'. Data sign => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r forall sign (m :: * -> *). (Data sign, Monad m) => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) forall sign (m :: * -> *). (Data sign, MonadPlus m) => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) forall sign (c :: * -> *). Data sign => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign) forall sign (c :: * -> *). Data sign => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign) forall sign (t :: * -> *) (c :: * -> *). (Data sign, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign)) forall sign (t :: * -> * -> *) (c :: * -> *). (Data sign, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefaultMorphism sign)) 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) -> DefaultMorphism sign -> u forall u. (forall d. Data d => d -> u) -> DefaultMorphism sign -> [u] forall r r'. (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r forall (m :: * -> *). Monad m => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) forall (m :: * -> *). MonadPlus m => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) forall (c :: * -> *). (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign) forall (c :: * -> *). (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign) forall (t :: * -> *) (c :: * -> *). Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign)) forall (t :: * -> * -> *) (c :: * -> *). Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefaultMorphism sign)) $cMkMorphism :: Constr $tDefaultMorphism :: DataType gmapMo :: (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) $cgmapMo :: forall sign (m :: * -> *). (Data sign, MonadPlus m) => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) gmapMp :: (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) $cgmapMp :: forall sign (m :: * -> *). (Data sign, MonadPlus m) => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) gmapM :: (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) $cgmapM :: forall sign (m :: * -> *). (Data sign, Monad m) => (forall d. Data d => d -> m d) -> DefaultMorphism sign -> m (DefaultMorphism sign) gmapQi :: Int -> (forall d. Data d => d -> u) -> DefaultMorphism sign -> u $cgmapQi :: forall sign u. Data sign => Int -> (forall d. Data d => d -> u) -> DefaultMorphism sign -> u gmapQ :: (forall d. Data d => d -> u) -> DefaultMorphism sign -> [u] $cgmapQ :: forall sign u. Data sign => (forall d. Data d => d -> u) -> DefaultMorphism sign -> [u] gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r $cgmapQr :: forall sign r r'. Data sign => (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r $cgmapQl :: forall sign r r'. Data sign => (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DefaultMorphism sign -> r gmapT :: (forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign $cgmapT :: forall sign. Data sign => (forall b. Data b => b -> b) -> DefaultMorphism sign -> DefaultMorphism sign dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefaultMorphism sign)) $cdataCast2 :: forall sign (t :: * -> * -> *) (c :: * -> *). (Data sign, Typeable t) => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DefaultMorphism sign)) dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign)) $cdataCast1 :: forall sign (t :: * -> *) (c :: * -> *). (Data sign, Typeable t) => (forall d. Data d => c (t d)) -> Maybe (c (DefaultMorphism sign)) dataTypeOf :: DefaultMorphism sign -> DataType $cdataTypeOf :: forall sign. Data sign => DefaultMorphism sign -> DataType toConstr :: DefaultMorphism sign -> Constr $ctoConstr :: forall sign. Data sign => DefaultMorphism sign -> Constr gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign) $cgunfold :: forall sign (c :: * -> *). Data sign => (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DefaultMorphism sign) gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign) $cgfoldl :: forall sign (c :: * -> *). Data sign => (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DefaultMorphism sign -> c (DefaultMorphism sign) $cp1Data :: forall sign. Data sign => Typeable (DefaultMorphism sign) Data) instance Pretty a => Pretty (DefaultMorphism a) where pretty :: DefaultMorphism a -> Doc pretty = (a -> Doc) -> DefaultMorphism a -> Doc forall a. (a -> Doc) -> DefaultMorphism a -> Doc printDefaultMorphism a -> Doc forall a. Pretty a => a -> Doc pretty printDefaultMorphism :: (a -> Doc) -> DefaultMorphism a -> Doc printDefaultMorphism :: (a -> Doc) -> DefaultMorphism a -> Doc printDefaultMorphism fA :: a -> Doc fA (MkMorphism s :: a s t :: a t) = String -> Doc text "inclusion" Doc -> Doc -> Doc $+$ Doc -> Doc specBraces (a -> Doc fA a s) Doc -> Doc -> Doc $+$ String -> Doc text String mapsTo Doc -> Doc -> Doc <+> Doc -> Doc specBraces (a -> Doc fA a t) ideOfDefaultMorphism :: sign -> DefaultMorphism sign ideOfDefaultMorphism :: sign -> DefaultMorphism sign ideOfDefaultMorphism s :: sign s = sign -> sign -> DefaultMorphism sign forall sign. sign -> sign -> DefaultMorphism sign MkMorphism sign s sign s compOfDefaultMorphism :: Monad m => DefaultMorphism sign -> DefaultMorphism sign -> m (DefaultMorphism sign) compOfDefaultMorphism :: DefaultMorphism sign -> DefaultMorphism sign -> m (DefaultMorphism sign) compOfDefaultMorphism (MkMorphism s1 :: sign s1 _) (MkMorphism _ s3 :: sign s3) = DefaultMorphism sign -> m (DefaultMorphism sign) forall (m :: * -> *) a. Monad m => a -> m a return (DefaultMorphism sign -> m (DefaultMorphism sign)) -> DefaultMorphism sign -> m (DefaultMorphism sign) forall a b. (a -> b) -> a -> b $ sign -> sign -> DefaultMorphism sign forall sign. sign -> sign -> DefaultMorphism sign MkMorphism sign s1 sign s3 defaultInclusion :: Monad m => sign -> sign -> m (DefaultMorphism sign) defaultInclusion :: sign -> sign -> m (DefaultMorphism sign) defaultInclusion s :: sign s = DefaultMorphism sign -> m (DefaultMorphism sign) forall (m :: * -> *) a. Monad m => a -> m a return (DefaultMorphism sign -> m (DefaultMorphism sign)) -> (sign -> DefaultMorphism sign) -> sign -> m (DefaultMorphism sign) forall b c a. (b -> c) -> (a -> b) -> a -> c . sign -> sign -> DefaultMorphism sign forall sign. sign -> sign -> DefaultMorphism sign MkMorphism sign s