Morphism.hs revision 8b054cade993ef373d564b2d74c9c5a2da48f8b7
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerModule : $Header$
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederDescription : Definition of signature morphisms for first-order logic with dependent types (DFOL)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner-- morphisms for DFOL - so far just the identity morphisms
f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maederdata Morphism = Morphism {object :: Sign} deriving (Show, Eq, Ord)
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElkneridMorph :: Sign -> Morphism
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElkneridMorph sig = Morphism {object = sig}
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknercompMorph :: Morphism -> Morphism -> Result Morphism
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknercompMorph m1 m2 = if object m1 == object m2
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner then return m1
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner else fail "Codomain of the first morphism must equal the domain of the second."
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerisValidMorph :: Morphism -> Bool
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerisValidMorph m = isValidSig $ object m
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner-- pretty printing
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elknerinstance Pretty Morphism where
a84a8d508a0778b13a4d097a6dd34b95feae78acJens Elkner pretty = printMorph
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerprintMorph :: Morphism -> Doc
a84a8d508a0778b13a4d097a6dd34b95feae78acJens ElknerprintMorph m = text "Identity on" <+> (pretty $ object m)