Morphism.hs revision a578ec30cded5e396a7ce9a3b469e8cd3a88246a
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederMaintainer : maeder@tzi.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
967e5f3c25249c779575864692935627004d3f9eChristian MaederMorphism on 'Env' (as for CASL)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Common.Lib.Map as Map
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maedertype IdMap = Map.Map Id Id
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maedertype FunMap = Map.Map (Id, TySc) (Id, TySc)
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederdata Morphism = Morphism { msource :: Env
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , mtarget :: Env
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , classIdMap :: IdMap -- ignore
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , typeIdMap :: IdMap
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , funMap :: FunMap }
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder deriving (Eq, Show)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederinstance PrettyPrint Morphism where
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder printText0 ga m =
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let tm = typeIdMap m
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder fm = funMap m
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder ds = Map.foldWithKey ( \ (i, TySc s) (j, TySc t) l ->
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (printText0 ga i <+> colon <+> printText0 ga s
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder <+> text mapsTo <+>
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder printText0 ga j <+> colon <+> printText0 ga t) : l)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in (if Map.isEmpty tm then empty
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder else text (typeS ++ sS) <+> printText0 ga tm)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $$ (if Map.isEmpty fm then empty
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder else text (opS ++ sS) <+> fsep (punctuate comma ds))
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $$ nest 1 colon <+> braces (printText0 ga (msource m))
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $$ nest 1 (text mapsTo)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder <+> braces (printText0 ga (mtarget m))
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaedermapType :: IdMap -> Type -> Type
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- include classIdMap later
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapType m ty = if Map.isEmpty m then ty else
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder rename ( \ i k n ->
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let t = TypeName i k n in
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder if n == 0 then
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder Just j -> TypeName j k 0
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder-- rename clashing type arguments later
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapTypeScheme = mapTypeOfScheme . mapType
d17834302eaa101395b4b806cd73670fd864445fChristian MaedermapTySc :: IdMap -> TySc -> TySc
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTySc m (TySc s1) = TySc $ mapTypeScheme m s1
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapSen :: Morphism -> Term -> Term
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapSen m = let tm = typeIdMap m in
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder mapTerm (mapFunSym tm (funMap m), mapType tm)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapDatatypeDefn :: Morphism -> IdMap -> DatatypeDefn -> DatatypeDefn
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapDatatypeDefn m tm (DatatypeConstr i j k args alts) =
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let tim = typeIdMap m
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- do not rename the types in the data type mapping
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder in DatatypeConstr i (Map.findWithDefault j j tim)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder k args $ map (mapAlt m tm rtm args $ TypeName j
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder (typeArgsListToKind args star) 0) alts
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedermapAlt :: Morphism -> IdMap -> IdMap -> [TypeArg] -> Type -> AltDefn -> AltDefn
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapAlt m tm rtm args dt (Construct i ts p sels) =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let sc = TypeScheme args
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ([] :=> getConstrType dt p (map (mapType tm) ts)) []
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (j, _) = mapFunSym (typeIdMap m) (funMap m) (i, sc)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder in Construct j (map (mapType rtm) ts) p sels
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder -- not change (unused) selectors and (alas) partiality
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedergetDTMap :: [DatatypeDefn] -> IdMap
967e5f3c25249c779575864692935627004d3f9eChristian MaedergetDTMap = foldr ( \ (DatatypeConstr i j _ _ _) m ->
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder if i == j then m else
967e5f3c25249c779575864692935627004d3f9eChristian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermapSentence m s = return $ case s of
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Formula t -> Formula $ mapSen m t
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDatatypeDefn m $ getDTMap td) td
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder ProgEqSen i sc pe ->
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let tm = typeIdMap m
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder fm = funMap m
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder f = mapFunSym tm fm
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (ni, nsc) = f (i, sc)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaedermapFunSym tm fm (i, sc) =
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder let (j, TySc s) = mapFunEntry tm fm (i, TySc sc) in (j, s)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapFunEntry :: IdMap -> FunMap -> (Id, TySc) -> (Id, TySc)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapFunEntry tm fm p@(i, sc) = if Map.isEmpty tm && Map.isEmpty fm then p else
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Map.findWithDefault (i, mapTySc tm sc) (i, sc) fm
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermkMorphism :: Env -> Env -> Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederembedMorphism :: Env -> Env -> Morphism
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiembedMorphism = mkMorphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederideMor :: Env -> Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederideMor e = embedMorphism e e
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism
e76e6a43f51438215737d6fc176c89da05bb86daChristian MaedercompMor m1 m2 =
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder if isSubEnv (mtarget m1) (msource m2) then
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder let tm2 = typeIdMap m2
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski fm2 = funMap m2 in Just
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (mkMorphism (msource m1) (mtarget m2))
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder { typeIdMap = Map.foldWithKey ( \ i j ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder Map.insert i $ Map.findWithDefault j j tm2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder tm2 $ typeIdMap m1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ mapFunEntry tm2 fm2 p2) fm2 $ funMap m1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederinclusionMor :: Env -> Env -> Result Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaederinclusionMor e1 e2 =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if isSubEnv e1 e2
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder then return (embedMorphism e1 e2)
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder else pplain_error (ideMor initialEnv)
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder (ptext "Attempt to construct inclusion between non-subsignatures:"
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder $$ ptext "Singature 1:" $$ printText e1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $$ ptext "Singature 2:" $$ printText e2)
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedersymbMapToMorphism sigma1 sigma2 smap = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (mkMorphism sigma1 sigma2)
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder { typeIdMap = type_map1
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , funMap = fun_map1}
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder myIdMap i k m = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map sort "++showId i "")
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder $ Map.lookup (Symbol { symName = i
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , symType = TypeAsItemType
967e5f3c25249c779575864692935627004d3f9eChristian Maeder , symEnv = sigma1 }) smap
967e5f3c25249c779575864692935627004d3f9eChristian Maeder return (Map.insert i (symName sym) m1)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder insFun i ot m = do
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder let osc = opType ot
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder sym <- maybeToResult nullPos
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder $ Map.lookup (Symbol { symName = i
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , symType = OpAsItemType osc
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , symEnv = sigma1 }) smap
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder k <- case symType sym of
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder OpAsItemType sc -> return $ TySc sc
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder _ -> plain_error (TySc osc)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"
967e5f3c25249c779575864692935627004d3f9eChristian Maeder ++showId i "") nullPos
967e5f3c25249c779575864692935627004d3f9eChristian Maeder return (Map.insert (i, TySc osc) (symName sym, k) m1)
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederlegalEnv :: Env -> Bool
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederlegalEnv _ = True -- maybe a closure test?
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederlegalMor :: Morphism -> Bool
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederlegalMor m = let s = msource m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder t = mtarget m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ts = typeIdMap m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fs = funMap m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder all (`elem` (Map.keys $ typeMap s))
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder && all (`elem` (Map.keys $ typeMap t))
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermorphismUnion m1 m2 =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder do s <- merge (msource m1) $ msource m2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder t <- merge (mtarget m1) $ mtarget m2
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder tm <- foldr ( \ (i, j) rm ->
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ Map.insert i j m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just k -> if j == k then return m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of type id: " ++
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showId i " to: " ++ showId j " and: "
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ++ showId k "") $ posOfId i] $ Just ()
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fm <- foldr ( \ (isc@(i, _), jsc@(j, TySc sc1)) rm -> do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Nothing -> return $ Map.insert isc jsc m
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Just ksc@(k, TySc sc2) -> if j == k &&
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder asSchemes 0 (equalSubs $ typeMap t) sc1 sc2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder then return m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Result [Diag Error
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder ("incompatible mapping of op: " ++
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder showFun isc " to: " ++ showFun jsc " and: "
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder ++ showFun ksc "") $ posOfId i] $ Just ()
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (return $ funMap m1) $ Map.toList $ funMap m2
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder return (mkMorphism s t)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder { typeIdMap = tm
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , funMap = fm }
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedershowFun :: (Id, TySc) -> ShowS
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedershowFun (i, TySc ty) = showId i . (" : " ++) . showPretty ty
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermorphismToSymbMap mor =
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder src = msource mor
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder tar = mtarget mor
typeSymMap = Map.foldWithKey ( \ i ti ->
let j = Map.findWithDefault i i tm
in Map.insert (idToTypeSymbol src i k)
$ idToTypeSymbol tar j k) Map.empty $ typeMap src
in Map.insert (idToOpSymbol src i ty)