0N/A{- |

196N/AModule : $Header$

0N/ACopyright : (c) C. Maeder, and Uni Bremen 2002-2006

0N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

0N/A

0N/AMaintainer : maeder@tzi.de

0N/AStability : provisional

0N/APortability : portable

0N/A

0N/Asupply a default morphism for a given signature

0N/A-}

0N/A

0N/A-- due to functional deps the instance for Logic.Category cannot be supplied

0N/A

0N/Amodule Common.DefaultMorphism where

0N/A

0N/Aimport Common.Keywords

0N/Aimport Common.Doc

0N/A

0N/Adata DefaultMorphism sign = MkMorphism sign sign deriving (Show, Eq)

0N/A

0N/Ainstance Pretty a => Pretty (DefaultMorphism a) where

0N/A pretty = printDefaultMorphism pretty

0N/A

0N/AprintDefaultMorphism :: (a -> Doc) -> DefaultMorphism a -> Doc

0N/AprintDefaultMorphism fA (MkMorphism s t) =

0N/A specBraces (fA s) $+$ (text mapsTo) <+> specBraces (fA t)

0N/A

0N/AdomOfDefaultMorphism, codOfDefaultMorphism :: DefaultMorphism sign -> sign

0N/AdomOfDefaultMorphism (MkMorphism s _) = s

0N/AcodOfDefaultMorphism (MkMorphism _ s) = s

0N/A

0N/AideOfDefaultMorphism :: sign -> DefaultMorphism sign

38N/AideOfDefaultMorphism s = MkMorphism s s

0N/A

0N/AcompOfDefaultMorphism :: (Monad m, Eq sign) => DefaultMorphism sign

0N/A -> DefaultMorphism sign -> m (DefaultMorphism sign)

0N/AcompOfDefaultMorphism (MkMorphism s1 s) (MkMorphism s2 s3) =

0N/A if s == s2 then return $ MkMorphism s1 s3 else

0N/A fail "intermediate signatures are different"

0N/A

0N/AlegalDefaultMorphism :: (sign -> Bool) -> DefaultMorphism sign -> Bool

0N/AlegalDefaultMorphism legalSign (MkMorphism s t) =

0N/A legalSign s && legalSign t

0N/A

0N/AdefaultInclusion :: (Monad m) => (sign -> sign -> Bool) -> sign -> sign

0N/A -> m (DefaultMorphism sign)

0N/AdefaultInclusion isSubSig s1 s2 =

0N/A if isSubSig s1 s2 then return $ MkMorphism s1 s2 else

0N/A fail "non subsignatures for inclusion"

0N/A