Morphism.hs revision 3d3889e0cefcdce9b3f43c53aaa201943ac2e895
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterModule : $Header$
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterDescription : Definition of signature morphisms for
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster first-order logic with dependent types (DFOL)
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterCopyright : (c) Kristina Sojakova, DFKI Bremen 2009
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterLicense : GPLv2 or higher, see LICENSE.txt
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterMaintainer : k.sojakova@jacobs-university.de
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterStability : experimental
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterPortability : portable
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster ( Morphism (..)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , isValidMorph
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , applyMorph
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , inclusionMorph
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , morphUnion
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , inducedFromMorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , inducedFromToMorphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Common.Result as Result
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Data.Map as Map
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterimport qualified Data.Set as Set
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- morphisms for DFOL - maps of symbol names
8af80418ba1ec431c8027fa9668e5678658d3611Allan Fosterdata Morphism = Morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster { source :: Sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , target :: Sign
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster , symMap :: Map.Map NAME NAME
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster } deriving (Ord, Show)
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- constructs an identity morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosteridMorph :: Sign -> Morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosteridMorph sig = Morphism sig sig Map.empty
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- composes two morphisms
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercompMorph :: Morphism -> Morphism -> Result Morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercompMorph m1 m2 =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster if target m1 /= source m2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then Result.Result [incompatibleMorphsError m1 m2] Nothing
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster else return $ Morphism (source m1) (target m2) $
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Set.fold (\ sym1 -> let sym2 = mapSymbol m2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster $ mapSymbol m1 sym1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster getSymbols $ source m1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- determines whether a morphism is valid
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidMorph :: Morphism -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterisValidMorph m@(Morphism sig1 sig2 map1) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let sym1 = getSymbols sig1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster sym2 = getSymbols sig2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster checkDom = Set.isSubsetOf (Map.keysSet map1) sym1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster checkCod = Set.isSubsetOf (Set.map (mapSymbol m) sym1) sym2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster checkTypes = map (checkTypePres m) $ Set.toList sym1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in and $ [checkDom, checkCod] ++ checkTypes
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercheckTypePres :: Morphism -> NAME -> Bool
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercheckTypePres m n =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let Just type1 = getSymbolType n $ source m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster Just type2 = getSymbolType (mapSymbol m n) $ target m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in applyMorph m type1 == type2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster{- converts the morphism into its canonical form where the symbol map contains
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster no key/value pairs of the form (k,k) -}
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercanForm :: Morphism -> Morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FostercanForm (Morphism sig1 sig2 map1) =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let map2 = Map.fromList $ filter (uncurry (/=)) $ Map.toList map1
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in Morphism sig1 sig2 map2
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster-- constructs the inclusion morphism between signatures
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterinclusionMorph :: Sign -> Sign -> Result.Result Morphism
8af80418ba1ec431c8027fa9668e5678658d3611Allan FosterinclusionMorph sig1 sig2 =
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster let m = Morphism sig1 sig2 Map.empty
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster in if isValidMorph m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster then Result.Result [] $ Just m
8af80418ba1ec431c8027fa9668e5678658d3611Allan Foster else Result.Result [noSubsigError sig1 sig2] Nothing
4.2 : Get the set "vars" of free variables in t, i.e. the symbols of sig
4.2 : Get the set "vars" of free variables in t, i.e. the symbols
coGenSig :: Bool -> Set.Set Symbol -> Sign -> Result Morphism
let names = Set.map name syms
in if Set.isSubsetOf names (getSymbols sig)
else genSig names Set.empty names sig
$ filter (\ (n, _) -> Set.member n incl) ds1
else Result.Result [symsNotInSigError names sig] Nothing
if Set.null todo
else let n = Set.findMin todo
incl1 = Set.union incl ns
done1 = Set.insert n done
cogSig excl [] sig = Set.difference (getSymbols sig) excl
if Set.member n excl
else let ns = Set.toList $ getFreeVars t
depen = any (`Set.member` excl) ns
then let excl1 = Set.insert n excl
morphUnion :: Morphism -> Morphism -> Result.Result Morphism
let Result.Result diag1 sigDM = sigUnion sig1D sig2D
Result.Result diag2 sigCM = sigUnion sig1C sig2C
Result.Result diag3 map3M = combineMaps map1 map2
Nothing -> Result.Result diag1 Nothing
Nothing -> Result.Result diag2 Nothing
Nothing -> Result.Result diag3 Nothing
then Result.Result [] $ Just m
else Result.Result
combineMaps map1 map2 = combineMapsH map1 $ Map.toList map2
combineMapsH :: Map.Map NAME NAME -> [(NAME, NAME)] ->
combineMapsH map1 [] = Result.Result [] $ Just map1
if Map.member k map1
then let Just v1 = Map.lookup k map1
else Result.Result [incompatibleMapError k v v1] Nothing
else let map2 = Map.insert k v map1
mapSymbol m sym = Map.findWithDefault sym sym $ symMap m
toTermMap m = Map.fromList $ map (\ (k, a) -> (k, Identifier a))
$ Map.toList m
printSymMap :: Map.Map NAME NAME -> Doc
$ Map.toList m
Result.Result dgs sig2M = buildSig sig1 map2
Nothing -> Result.Result dgs Nothing
Just sig2 -> Result.Result [] $ Just $ Morphism sig1 sig2 map2
buildSigH [] sig _ = Result.Result [] $ Just sig
let n2 = Map.findWithDefault n1 n1 map1
else Result.Result [incompatibleViewError1 n2 t2 t3]
inducedFromToMorphism :: Map.Map Symbol Symbol -> ExtSign Sign Symbol ->
ExtSign Sign Symbol -> Result.Result Morphism
buildMorph :: [SDECL] -> Morphism -> Result.Result Morphism
buildMorph [] m = Result.Result [] $ Just m
if Map.member n1 map1
Result.Result [incompatibleViewError2 n2 t2 t3] Nothing
m {symMap = Map.insert n1 s $ symMap m}
[] -> Result.Result [noSymToMapError n1 t2] Nothing
_ -> Result.Result [manySymToMapError n1 t2 ss] Nothing
incompatibleMorphsError :: Morphism -> Morphism -> Result.Diagnosis
, Result.diagString = "Codomain of the morphism\n" ++ show (pretty m1)
, Result.diagPos = nullRange
incompatibleViewError1 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
, Result.diagString = "Symbol\n" ++ show (pretty n)
, Result.diagPos = nullRange
incompatibleViewError2 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
, Result.diagString = "Symbol\n" ++ show (pretty n)
, Result.diagPos = nullRange
noSymToMapError :: NAME -> TYPE -> Result.Diagnosis
, Result.diagString = "Symbol\n" ++ show (pretty n)
, Result.diagPos = nullRange
manySymToMapError :: NAME -> TYPE -> [NAME] -> Result.Diagnosis
, Result.diagString = "Symbol\n" ++ show (pretty n)
, Result.diagPos = nullRange
noSubsigError :: Sign -> Sign -> Result.Diagnosis
, Result.diagString = "Signature\n" ++ show (pretty sig1)
, Result.diagPos = nullRange
incompatibleMapError :: NAME -> NAME -> NAME -> Result.Diagnosis
, Result.diagString = "Symbol\n" ++ show (pretty n)
, Result.diagPos = nullRange
invalidMorphError :: Morphism -> Morphism -> Result.Diagnosis
, Result.diagString = "The combination of morphisms\n" ++ show (pretty m1)
, Result.diagPos = nullRange
, Result.diagString = "The symbols\n"
++ show (printNames $ Set.toList syms)
, Result.diagPos = nullRange