{-# 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