Morphism.hs revision ac19f8695aa1b2d2d1cd1319da2530edd8f46a96
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
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : hets@tzi.de
967e5f3c25249c779575864692935627004d3f9eChristian MaederStability : provisional
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederPortability : portable
967e5f3c25249c779575864692935627004d3f9eChristian MaederMorphism on 'Env' (as for CASL)
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Common.Lib.Map as Map
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian 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
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , typeIdMap :: IdMap
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , funMap :: FunMap }
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder deriving (Eq, Show)
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederinstance PrettyPrint Morphism where
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder printText0 ga m = braces (printText0 ga (msource m))
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder $$ text mapsTo
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder <+> braces (printText0 ga (mtarget m))
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType :: IdMap -> Type -> Type
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- include classIdMap later
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapType m = rename ( \ i k n ->
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder let t = TypeName i k n in
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder if n == 0 then
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder Just j -> TypeName j k 0
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- rename clashing type arguments later
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapTypeScheme = mapTypeOfScheme . mapType
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTySc :: IdMap -> TySc -> TySc
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapTySc m (TySc s1) = TySc $ mapTypeScheme m s1
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapSen :: Morphism -> Term -> Result Term
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapSen m = let tm = typeIdMap m in
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder return . mapTerm (mapFunSym tm (funMap m), mapType tm)
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian MaedermapFunSym tm fm (i, sc) =
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder let (i2, TySc sc2) = Map.findWithDefault
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder (i, TySc $ mapTypeScheme tm sc)
ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maeder (i, TySc sc) fm
967e5f3c25249c779575864692935627004d3f9eChristian MaedermkMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism :: Env -> Env -> Morphism
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism a b =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (mkMorphism a b)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder { typeIdMap = foldr (\x -> Map.insert x x) Map.empty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ( \ i (OpInfos ts) m -> foldr
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (\ oi -> let v = (i, TySc $ opType oi) in
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederideMor e = embedMorphism e e
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder if isSubEnv (mtarget m1) (msource m2) then Just
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (mkMorphism (msource m1) (mtarget m2))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder { typeIdMap = Map.map ( \ i -> Map.findWithDefault i i $ typeIdMap m2)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder $ typeIdMap m1
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , funMap = Map.foldWithKey ( \ (i1, sc1) (i2, sc2) m ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (Map.findWithDefault (i2, sc2) (i2, sc2) $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder funMap m2) m) Map.empty $ funMap m1
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return (embedMorphism e1 e2)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder else pplain_error (ideMor initialEnv)
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (ptext "Attempt to construct inclusion between non-subsignatures:"
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder $$ ptext "Singature 1:" $$ printText e1
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder $$ ptext "Singature 2:" $$ printText e2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian 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)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder { typeIdMap = type_map1
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , funMap = fun_map1}
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myIdMap i k m = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map sort "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , symType = TypeAsItemType
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symEnv = sigma1 }) smap
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (Map.insert i (symName sym) m1)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder insFun i ot m = do
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder let osc = opType ot
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder sym <- maybeToResult nullPos
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Could not map op "++showId i "")
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ Map.lookup (Symbol { symName = i
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symType = OpAsItemType osc
e817ea5134dced9e0bcce1a9d6b8fe4f81d36e56Christian Maeder , symEnv = sigma1 }) smap
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder k <- case symType sym of
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder OpAsItemType sc -> return $ TySc sc
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder _ -> plain_error (TySc osc)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ("symbMapToMorphism - Wrong result symbol type for op"
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ++showId i "") nullPos
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder return (Map.insert (i, TySc osc) (symName sym, k) m1)
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederlegalMor m = let s = msource m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder t = mtarget m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ts = typeIdMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder fs = funMap m
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder all (`elem` (Map.keys $ typeMap s))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all (`elem` (Map.keys $ typeMap t))
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder do s <- merge (msource m1) $ msource m2
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder t <- merge (mtarget m1) $ mtarget m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian 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: "
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showId k "") $ posOfId i] $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fm <- foldr ( \ (isc@(i, _), jsc@(j, TySc sc1)) rm -> do
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Nothing -> return $ Map.insert isc jsc m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Just ksc@(k, TySc sc2) -> if j == k &&
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder isUnifiable (typeMap t) 0 sc1 sc2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder then return m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder Result [Diag Error
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ("incompatible mapping of op: " ++
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder showFun isc " to: " ++ showFun jsc " and: "
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder ++ showFun ksc "") $ posOfId i] $ Just ()
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (return $ funMap m1) $ Map.toList $ funMap m2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder return (mkMorphism s t)
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder { typeIdMap = tm
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , funMap = fm }
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedershowFun :: (Id, TySc) -> ShowS
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedershowFun (i, TySc ty) = showId i . (" : " ++) . showPretty ty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermorphismToSymbMap mor =
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder src = msource mor
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder tar = mtarget mor
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder tm = typeMap src
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder ( \ s1 s2 m -> let k = typeKind $
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Map.findWithDefault starTypeInfo s1 tm
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder in Map.insert (idToTypeSymbol src s1 k) (idToTypeSymbol tar s2 k) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder typeIdMap mor
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder ( \ (id1, TySc t1) (id2, TySc t2) m ->
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder Map.insert (idToOpSymbol src id1 t1)
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder (idToOpSymbol tar id2 t2) m)
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder typeSymMap $ funMap mor