6133N/A{- |

6133N/AModule : $Header$

6133N/ADescription : Definition of signature morphisms for

6133N/A first-order logic with dependent types (DFOL)

6133N/A-}

6133N/A

6133N/Amodule DFOL.Morphism where

6133N/A

6133N/Aimport DFOL.AS_DFOL

6133N/Aimport DFOL.Sign

6133N/Aimport Common.Result

6133N/Aimport Common.Doc

6133N/Aimport Common.DocUtils

6133N/Aimport qualified Data.Map as Map

6133N/Aimport qualified Data.Set as Set

6133N/A

6133N/A-- morphisms for DFOL - maps of symbol names

6133N/Adata Morphism = Morphism

6133N/A { source :: Sign

6133N/A , target :: Sign

6133N/A , symMap :: Map.Map NAME NAME

6133N/A } deriving (Eq, Ord, Show)

6133N/A

6133N/A-- constructs an identity morphism

6133N/AidMorph :: Sign -> Morphism

6133N/AidMorph sig = Morphism sig sig Map.empty

6133N/A

6133N/A-- composes two morphisms

6133N/AcompMorph :: Morphism -> Morphism -> Result Morphism

6133N/AcompMorph m1 m2 =

6147N/A if target m1 /= source m2

6147N/A then fail $ "Codomain of the first morphism "

6147N/A ++ "must equal the domain of the second."

6147N/A else return $ Morphism (source m1) (target m2) $

6147N/A Set.fold (\ sym1 -> let sym2 = mapSymbol m2

6147N/A $ mapSymbol m1 sym1

6133N/A in if (sym1 == sym2)

6147N/A then id

6147N/A else Map.insert sym1 sym2)

6147N/A Map.empty $

6147N/A getSymbols $ source m1

6147N/A

6147N/A-- determines whether a morphism is valid

6133N/AisValidMorph :: Morphism -> Bool

6147N/AisValidMorph m@(Morphism sig1 sig2 map1) =

6147N/A let sym1 = getSymbols sig1

6147N/A sym2 = getSymbols sig2

6133N/A checkDom = Set.isSubsetOf (Map.keysSet map1) sym1

6147N/A checkCod = Set.isSubsetOf (Set.map (mapSymbol m) sym1) sym2

6147N/A checkTypes = map (checkTypePres m) $ Set.toList sym1

6147N/A in and $ [checkDom,checkCod] ++ checkTypes

6147N/A

6133N/AcheckTypePres:: Morphism -> NAME -> Bool

6133N/AcheckTypePres m n =

6133N/A let Just type1 = getSymbolType n $ source m

6133N/A Just type2 = getSymbolType (mapSymbol m n) $ target m

in (applyMorphism m type1) == type2

{- converts the morphism into its canonical form where the symbol map contains

no key/value pairs of the form (k,k) -}

morphCanForm :: Morphism -> Morphism

morphCanForm (Morphism sig1 sig2 map1) =

let map2 = Map.fromList $ filter (\ (k,a) -> k /= a) $ Map.toList map1

in Morphism sig1 sig2 map2

-- applies a morphism to a symbol

mapSymbol :: Morphism -> NAME -> NAME

mapSymbol m sym = Map.findWithDefault sym sym $ symMap m

-- translates a term, type or formula along the given morphism

applyMorphism :: Translatable a => Morphism -> a -> a

applyMorphism m t =

let syms = getSymbols (target m)

map1 = Map.fromList $ map (\ (k,a) -> (k, Identifier a))

$ Map.toList $ symMap m

in translate map1 syms t

-- pretty printing

instance Pretty Morphism where

pretty = printMorph

printMorph :: Morphism -> Doc

printMorph m =

if m == (idMorph $ source m)

then vcat [text "Identity morphism on:", pretty $ source m]

else vcat [text "Source signature:", pretty $ source m,

text "Target signature:", pretty $ target m,

text "Mapping:", printSymMap $ symMap m]

printSymMap :: Map.Map NAME NAME -> Doc

printSymMap m = vcat $ map (\ (k,a) -> pretty k <+> text "|->" <+> pretty a)

$ Map.toList m