Morphism.hs revision 242397ba0f1cc490e892130bf0df239deeecf5da
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederModule : $Header$
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederDescription : morphisms implementation
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian MaederMaintainer : Christian.Maeder@dfki.de
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maedermapping entities of morphisms
3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederimport qualified Data.Map as Map
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maederinstance Eq Morphism where
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, funMap m1) ==
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (msource m2, mtarget m2, typeIdMap m2, funMap m2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | map type and expand it
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeE :: TypeMap -> IdMap -> Type -> Type
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeE tm im = expandAliases tm . mapType im
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeScheme :: TypeMap -> IdMap -> TypeScheme -> TypeScheme
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapTypeScheme tm im = mapTypeOfScheme $ mapTypeE tm im
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapSen :: TypeMap -> IdMap -> FunMap -> Term -> Term
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapSen tm im fm = mapTerm (mapFunSym tm im fm, mapTypeE tm im)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapDataEntry :: TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapDataEntry tm im fm (DataEntry dm i k args rk alts) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let tim = compIdMap dm im
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in DataEntry tim i k args rk $ map
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder (mapAlt tm tim fm args $ patToType (Map.findWithDefault i i tim)
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder args rk) alts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapAlt :: TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermapAlt tm im fm args dt c@(Construct mi ts p sels) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let sc = TypeScheme args
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (getFunType dt p (map (mapTypeE tm im) ts)) nullRange
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (j, TypeScheme _ ty _) = mapFunSym tm im fm (i, sc)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in Construct (Just j) ts (getPartiality ts ty) sels
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- do not change (unused) selectors
abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- | get the partiality from a constructor type
c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder-- with a given number of curried arguments
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetPartiality :: [a] -> Type -> Partiality
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedergetPartiality args t = case getTypeAppl t of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [_] -> if isPartialArrow i then Partial else Total
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder _ : rs -> getPartiality rs res
92aa1b88f02d2a413da60dba78acd34312e6f29aChristian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if null args then Partial else error "getPartiality"
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermapSentence m s = let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm = filterAliases $ typeMap $ mtarget m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder im = typeIdMap m
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder fm = funMap m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder f = mapFunSym tm im fm
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in return $ case s of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Formula t -> Formula $ mapSen tm im fm t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry tm im fm) td
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder ProgEqSen i sc pe ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder let (ni, nsc) = f (i, sc)
d48085f765fca838c1d972d2123601997174583dChristian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE tm im) pe
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedermapFunSym :: TypeMap -> IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
d48085f765fca838c1d972d2123601997174583dChristian MaedermapFunSym tm im fm (i, sc) =
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder let msc = mapTypeScheme tm im sc
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederembedMorphism :: Env -> Env -> Morphism
d48085f765fca838c1d972d2123601997174583dChristian MaederembedMorphism = mkMorphism
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederideMor :: Env -> Morphism
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederideMor e = embedMorphism e e
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder let k = Map.findWithDefault j j im2 in
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder if i == k then id else Map.insert i k)
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
d48085f765fca838c1d972d2123601997174583dChristian MaedercompMor m1 m2 =
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder if mtarget m1 == msource m2 then
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder let tm2 = typeIdMap m2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder fm2 = funMap m2
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder tar = mtarget m2
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder tm = filterAliases $ typeMap tar
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder in return (mkMorphism (msource m1) tar)
d48085f765fca838c1d972d2123601997174583dChristian Maeder { typeIdMap = compIdMap (typeIdMap m1) tm2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->
d48085f765fca838c1d972d2123601997174583dChristian Maeder let p3 = mapFunSym tm tm2 fm2 p2 in
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder if p1 == p3 then id else Map.insert p1 p3)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder fm2 $ funMap m1
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder else fail "intermediate signatures of morphisms do not match"
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaederinclusionMor :: Env -> Env -> Result Morphism
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaederinclusionMor e1 e2 =
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder if isSubEnv e1 e2
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder then return (embedMorphism e1 e2)
d48085f765fca838c1d972d2123601997174583dChristian Maeder else Result [Diag Error
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedershowEnvDiff :: Env -> Env -> String
d48085f765fca838c1d972d2123601997174583dChristian MaedershowEnvDiff e1 e2 =
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
d48085f765fca838c1d972d2123601997174583dChristian Maeder (diffEnv e1 e2) ""
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlegalEnv :: Env -> Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlegalEnv _ = True -- maybe a closure test?
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederlegalMor :: Morphism -> Bool
2986838ec286d67e7c199e7ea81e7364ca36ad25Christian MaederlegalMor m = let s = msource m
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder t = mtarget m
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder ts = typeIdMap m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fs = funMap m
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder all (`elem` (Map.keys $ typeMap s))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder && all (`elem` (Map.keys $ typeMap t))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
413db961f13e112716509b6d61d7a7bbf50c98b2Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermorphismUnion m1 m2 =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do let s1 = msource m1
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder s2 = msource m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm1 = Map.toList $ typeIdMap m1
48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder tm2 = Map.toList $ typeIdMap m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- unchanged types
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ut1 = Map.keys (typeMap s1) \\ map fst tm1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ut2 = Map.keys (typeMap s2) \\ map fst tm2
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder mkP = map ( \ a -> (a, a))
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder tml = tm1 ++ tm2 ++ mkP (ut1 ++ ut2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fm1 = Map.toList $ funMap m1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fm2 = Map.toList $ funMap m2
37354e3ed68875fb527338105a610df481f98cb0Christian Maeder -- all functions
413db961f13e112716509b6d61d7a7bbf50c98b2Christian Maeder af = concatMap ( \ (i, os) ->
d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder map ( \ o -> (i, opType o)) $ opInfos os) . Map.toList
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- unchanged functions
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder uf1 = af (assumps s1) \\ map fst fm1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder uf2 = af (assumps s2) \\ map fst fm2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fml = fm1 ++ fm2 ++ mkP (uf1 ++ uf2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder s <- merge s1 s2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t <- merge (mtarget m1) $ mtarget m2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let sAs = filterAliases $ typeMap s
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tAs = filterAliases $ typeMap t
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tm <- foldr ( \ (i, j) rm ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> return $ Map.insert i j m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just k -> if j == k then return m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else fail ("incompatible mapping of type id: " ++
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder showId i " to: " ++ showId j " and: "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ showId k ""))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder fm <- foldr ( \ (isc@(i, sc), jsc@(j, sc1)) rm -> do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let nsc = expand sAs sc1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder nisc = (i, expand tAs sc)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> return $ Map.insert nisc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just ksc@(k, sc2) -> if j == k &&
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then return m
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else fail ("incompatible mapping of op: " ++
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder showFun isc " to: " ++ showFun jsc " and: "
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ++ showFun ksc ""))
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder return (mkMorphism s t)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder { typeIdMap = Map.filterWithKey (/=) tm
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder , funMap = Map.filterWithKey (/=) fm }
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedershowFun :: (Id, TypeScheme) -> ShowS
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedershowFun (i, ty) = showId i . (" : " ++) . showDoc ty
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermorphismToSymbMap :: Morphism -> SymbolMap
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian MaedermorphismToSymbMap mor =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder src = msource mor
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder tar = mtarget mor
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder im = typeIdMap mor
68485f7bfab1b4c6f963ce6837cba5fb148ed625Christian Maeder tm = filterAliases $ typeMap tar
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder k = typeKind ti
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in Map.insert (idToTypeSymbol src i k)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ idToTypeSymbol tar j k) Map.empty $ typeMap src
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ( \ i (OpInfos l) m ->
f875f7eebac7f69bf9da98c93479a542d0a8056fChristian Maeder foldr ( \ oi ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ty = opType oi
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (j, t2) = mapFunSym tm im (funMap mor) (i, ty)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in Map.insert (idToOpSymbol src i ty)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (idToOpSymbol tar j t2)) m l)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder typeSymMap $ assumps src