DefaultMorphism.hs revision d543cf2bb0c810781625c76fe135476d46270d88
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzCopyright : (c) C. Maeder, and Uni Bremen 2002-2006
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzMaintainer : maeder@tzi.de
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzStability : provisional
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzPortability : portable
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzDescription : supply a default morphism for a given signature type
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz-- due to functional deps the instance for Logic.Category cannot be supplied
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzdata DefaultMorphism sign = MkMorphism sign sign deriving (Show, Eq)
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulzinstance Pretty a => Pretty (DefaultMorphism a) where
634880196bffeea4cad99e081f0956886ab77124Ewaryst Schulz pretty = printDefaultMorphism pretty
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintDefaultMorphism :: (a -> Doc) -> DefaultMorphism a -> Doc
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederprintDefaultMorphism fA (MkMorphism s t) =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder specBraces (fA s) $+$ (text mapsTo) <+> specBraces (fA t)
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzdomOfDefaultMorphism, codOfDefaultMorphism :: DefaultMorphism sign -> sign
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzdomOfDefaultMorphism (MkMorphism s _) = s
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzcodOfDefaultMorphism (MkMorphism _ s) = s
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzideOfDefaultMorphism :: sign -> DefaultMorphism sign
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzideOfDefaultMorphism s = MkMorphism s s
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzcompOfDefaultMorphism :: (Monad m, Eq sign) => DefaultMorphism sign
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz -> DefaultMorphism sign -> m (DefaultMorphism sign)
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzcompOfDefaultMorphism (MkMorphism s1 s) (MkMorphism s2 s3) =
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz if s == s2 then return $ MkMorphism s1 s3 else
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz fail "intermediate signatures are different"
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzlegalDefaultMorphism :: (sign -> Bool) -> DefaultMorphism sign -> Bool
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzlegalDefaultMorphism legalSign (MkMorphism s t) =
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz legalSign s && legalSign t
634880196bffeea4cad99e081f0956886ab77124Ewaryst SchulzdefaultInclusion :: (Monad m) => (sign -> sign -> Bool) -> sign -> sign
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz -> m (DefaultMorphism sign)
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst SchulzdefaultInclusion isSubSig s1 s2 =
e49fd57c63845c7806860a9736ad09f6d44dbaedChristian Maeder if isSubSig s1 s2 then return $ MkMorphism s1 s2 else
96b4cc8ddfdb1e4671c1218a963715d424332d49Ewaryst Schulz fail "non subsignatures for inclusion"