Morphism.hs revision deb7bff126ec547bd812d0c8683ad6e785a45abb
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
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maedertype FunMap = Map.Map (Id, TypeScheme) (Id, TypeScheme)
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederdata Morphism = Morphism { msource :: Env
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , mtarget :: Env
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , classIdMap :: IdMap -- ignore
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , typeIdMap :: IdMap
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder , funMap :: FunMap }
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maeder deriving (Eq, Show)
dea4c92f0c061d589c542d0640a18dab36dfbb46Christian Maederinstance PrettyPrint Morphism where
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder printText0 ga m =
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let tm = typeIdMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fm = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ds = Map.foldWithKey ( \ (i, s) (j, t) l ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (printText0 ga i <+> colon <+> printText0 ga s
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <+> text mapsTo <+>
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder printText0 ga j <+> colon <+> printText0 ga t) : l)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder in (if Map.isEmpty tm then empty
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else text (typeS ++ sS) <+> printText0 ga tm)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $$ (if Map.isEmpty fm then empty
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else text (opS ++ sS) <+> fsep (punctuate comma ds))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder $$ nest 1 colon <+> braces (printText0 ga $ msource m)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder $$ nest 1 (text mapsTo)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <+> braces (printText0 ga $ mtarget m)
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTypeScheme im = mapTypeOfScheme $ mapType im
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapSen :: Morphism -> Term -> Term
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian MaedermapSen m = let im = typeIdMap m in
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder mapTerm (mapFunSym im (funMap m), mapType im)
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapDataEntry :: Morphism -> DataEntry -> DataEntry
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapDataEntry m (DataEntry tm i k args alts) =
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder let tim = compIdMap tm $ typeIdMap m
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder in DataEntry tim i k args $ map
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (mapAlt m tim args (Map.findWithDefault i i tim, args, star)) alts
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaedermapAlt :: Morphism -> IdMap -> [TypeArg] -> DataPat -> AltDefn -> AltDefn
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapAlt m tm args dt c@(Construct mi ts p sels) =
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let sc = TypeScheme args
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (getConstrType dt p (map (mapType tm) ts)) []
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (j, TypeScheme _ ty _) =
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder mapFunSym (typeIdMap m) (funMap m) (i, sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Construct (Just j) ts (getPartiality ts ty) sels
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder -- do not change (unused) selectors
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapSentence m s = return $ case s of
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder Formula t -> Formula $ mapSen m t
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry m) td
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ProgEqSen i sc pe ->
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder let tm = typeIdMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fm = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder f = mapFunSym tm fm
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (ni, nsc) = f (i, sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapFunSym im fm (i, sc) =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let (j, sc2) = Map.findWithDefault (i, mapTypeScheme im sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (i, sc) fm in
967e5f3c25249c779575864692935627004d3f9eChristian MaedermkMorphism :: Env -> Env -> Morphism
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian MaedermkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederembedMorphism :: Env -> Env -> Morphism
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaederembedMorphism = mkMorphism
967e5f3c25249c779575864692935627004d3f9eChristian MaederideMor :: Env -> Morphism
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaederideMor e = embedMorphism e e
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Map.insert i $ Map.findWithDefault j j im2)
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedercompMor m1 m2 =
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder if isSubEnv (mtarget m1) (msource m2) &&
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder isSubEnv (msource m2) (mtarget m1) then
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder let tm2 = typeIdMap m2
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder fm2 = funMap m2 in return
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (mkMorphism (msource m1) (mtarget m2))
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder { classIdMap = compIdMap (classIdMap m1) $ classIdMap m2
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder , typeIdMap = compIdMap (typeIdMap m1) tm2
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder $ mapFunSym tm2 fm2 p2) fm2 $ funMap m1
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder else fail "intermediate signatures of morphisms do not match"
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder if isSubEnv e1 e2
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder then return (embedMorphism e1 e2)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else Result [Diag Error
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder ++ showEnvDiff e1 e2) nullPos] Nothing
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedershowEnvDiff :: Env -> Env -> String
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedershowEnvDiff e1 e2 =
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder "Signature 1:\n" ++ showPretty e1 "\nSignature 2:\n"
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder ++ showPretty e2 "\nDifference\n" ++ showPretty
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder (diffEnv e1 e2) ""
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv :: Env -> Bool
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalEnv _ = True -- maybe a closure test?
967e5f3c25249c779575864692935627004d3f9eChristian MaederlegalMor :: Morphism -> Bool
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederlegalMor m = let s = msource m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder t = mtarget m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ts = typeIdMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fs = funMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder all (`elem` (Map.keys $ typeMap s))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder && all (`elem` (Map.keys $ typeMap t))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
967e5f3c25249c779575864692935627004d3f9eChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedermorphismUnion m1 m2 =
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder do let s1 = msource m1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder s2 = msource m2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder tm1 = Map.toList $ typeIdMap m1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder tm2 = Map.toList $ typeIdMap m2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder -- unchanged types
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ut1 = Map.keys (typeMap s1) List.\\ map fst tm1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ut2 = Map.keys (typeMap s2) List.\\ map fst tm2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder mkP = map ( \ a -> (a, a))
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder tml = tm1 ++ tm2 ++ mkP (ut1 ++ ut2)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder fm1 = Map.toList $ funMap m1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder fm2 = Map.toList $ funMap m2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder -- all functions
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder af = concatMap ( \ (i, os) ->
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder map ( \ o -> (i, opType o)) $ opInfos os) . Map.toList
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder -- unchanged functions
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder uf1 = af (assumps s1) List.\\ map fst fm1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder uf2 = af (assumps s2) List.\\ map fst fm2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder fml = fm1 ++ fm2 ++ mkP (uf1 ++ uf2)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder s <- merge s1 s2
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder t <- merge (mtarget m1) $ mtarget m2
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder tm <- foldr ( \ (i, j) rm ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Nothing -> return $ Map.insert i j m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Just k -> if j == k then return m
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder else fail ("incompatible mapping of type id: " ++
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder showId i " to: " ++ showId j " and: "
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ++ showId k ""))
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let nsc = expand (typeMap t) sc1
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder nisc = (i, expand (typeMap s) sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Nothing -> return $ Map.insert nisc
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder Just ksc@(k, sc2) -> if j == k &&
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder then return m
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder else fail ("incompatible mapping of op: " ++
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder showFun isc " to: " ++ showFun jsc " and: "
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ++ showFun ksc ""))
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder return (mkMorphism s t)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder { typeIdMap = Map.filterWithKey (/=) tm
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder , funMap = Map.filterWithKey (/=) fm }
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedershowFun :: (Id, TypeScheme) -> ShowS
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedershowFun (i, ty) = showId i . (" : " ++) . showPretty ty
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermorphismToSymbMap :: Morphism -> SymbolMap
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermorphismToSymbMap mor =
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder src = msource mor
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder tar = mtarget mor
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder tm = typeIdMap mor
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder k = typeKind ti
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Map.insert (idToTypeSymbol src i k)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder $ idToTypeSymbol tar j k) Map.empty $ typeMap src
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder ( \ i (OpInfos l) m ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder foldr ( \ oi ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let ty = opType oi
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (j, t2) = mapFunSym
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder tm (funMap mor) (i, ty)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Map.insert (idToOpSymbol src i ty)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (idToOpSymbol tar j t2)) m l)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder typeSymMap $ assumps src