Morphism.hs revision 97ee7048e63953c5617342ce38c30cbcb35cc0be
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
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maederimport Data.List(partition)
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapType m t = case t of
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeName i k n ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder if n == 0 then
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder Just j -> TypeName j k 0
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeAppl t1 t2 ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeAppl (mapType m t1) (mapType m t2)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeToken _ -> t
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder BracketType b l ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder BracketType b (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder KindedType tk k ps ->
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder KindedType (mapType m tk) k ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder MixfixType l -> MixfixType $ map (mapType m) l
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder LazyType tl ps -> LazyType (mapType m tl) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder ProductType l ps -> ProductType (map (mapType m) l) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder FunType t1 a t2 ps -> FunType (mapType m t1) a (mapType m t2) ps
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder-- rename clashing type arguments later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme m (TypeScheme args (q :=> t) ps) =
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder TypeScheme args (q :=> mapType m t) ps
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTySc :: IdMap -> TySc -> TySc
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTySc m (TySc s1) = TySc (mapTypeScheme m s1)
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TySc) -> Maybe (Id, TySc)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapFunSym tm fm (i, sc) = do
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder (newI, _sc1) <- Map.lookup (i, sc) fm
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder let sc2 = mapTySc tm sc
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder -- unify sc2 with sc1 later
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder return (newI, sc2)
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeOpInfos :: TypeMap -> Int -> OpInfos -> OpInfos -> Result OpInfos
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOpInfos tm c (OpInfos l1) (OpInfos l2) =
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder do l <- mergeOps tm c l1 l2
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return $ OpInfos l
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder-- trace (showPretty l1 "\n+ " ++ showPretty l2 "\n 0" ++ showPretty l "") l
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps :: TypeMap -> Int -> [OpInfo] -> [OpInfo] -> Result [OpInfo]
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps _ _ [] l = return l
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermergeOps tm c (o:os) l2 = do
34c05dd06c937d85e7f552e4ff0d36ca0393daeaChristian Maeder let (es, us) = partition (isUnifiable (addUnit tm) c
34c05dd06c937d85e7f552e4ff0d36ca0393daeaChristian Maeder (opType o) . opType) l2
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder l1 <- mergeOps tm c os us
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder if null es then return (o : l1)
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder else do r <- mergeOpInfo tm c o $ head es
7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder return (r : l1)
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeEnv :: Env -> Env -> Result Env
09eef8548cd62d787cf3a6535f9eae10592eec89Christian MaedermergeEnv e1 e2 =
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder do cMap <- merge (classMap e1) $ classMap e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder let m = max (counter e1) $ counter e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder tMap <- mergeMap (mergeTypeInfo Map.empty 0)
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder (typeMap e1) $ typeMap e2
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian Maeder as <- mergeMap (mergeOpInfos tMap m)
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder (assumps e1) $ assumps e2
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder return initialEnv { classMap = cMap
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder , typeMap = tMap
adee28c3eb7bb0b9bb045d26ee6d35e19cf39053Christian Maeder , assumps = as }
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
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder $ typeKind k}) 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
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , symType = OpAsItemType osc}) 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 =
09eef8548cd62d787cf3a6535f9eae10592eec89Christian Maeder do s <- mergeEnv (msource m1) $ msource m2
09eef8548cd62d787cf3a6535f9eae10592eec89Christian Maeder t <- mergeEnv (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