Morphism.hs revision c7e03d0708369f944b6f235057b39142a21599f2
967e5f3c25249c779575864692935627004d3f9eChristian MaederModule : $Header$
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian MaederDescription : morphisms implementation
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006
967e5f3c25249c779575864692935627004d3f9eChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
967e5f3c25249c779575864692935627004d3f9eChristian MaederMaintainer : Christian.Maeder@dfki.de
89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maedermapping entities of morphisms
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederimport qualified Data.Set as Set
fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Data.Map as Map
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederinstance Eq Morphism where
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, funMap m1) ==
967e5f3c25249c779575864692935627004d3f9eChristian Maeder (msource m2, mtarget m2, typeIdMap m2, funMap m2)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- | map type and expand it
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTypeE :: TypeMap -> IdMap -> Type -> Type
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapTypeE tm im = expandAliases tm . mapType im
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermapTypeScheme :: TypeMap -> IdMap -> TypeScheme -> TypeScheme
7a879b08ae0ca30006f9be887a73212b07f10204Christian MaedermapTypeScheme tm im = mapTypeOfScheme $ mapTypeE tm im
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedermapSen :: TypeMap -> IdMap -> FunMap -> Term -> Term
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapSen tm im fm = mapTerm (mapFunSym tm im fm, mapTypeE tm im)
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedersetToMap :: Ord a => Set.Set a -> Map.Map a a
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian MaedersetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaedergetDatatypeIds :: DataEntry -> Set.Set Id
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder let getAltIds (Construct _ tys _ sels) = Set.union
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder (Set.unions $ map getTypeIds tys)
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder $ Set.unions $ concatMap (map getSelIds) sels
d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder getTypeIds = idsOf (== 0)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapDataEntry :: TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedermapDataEntry tm im fm de@(DataEntry dm i k args rk alts) =
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in DataEntry tim i k args rk $ Set.map
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (mapAlt tm tim fm args $ patToType (Map.findWithDefault i i tim)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder args rk) alts
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapAlt :: TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn
717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapAlt tm im fm args dt c@(Construct mi ts p sels) =
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder let sc = TypeScheme args
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (getFunType dt p $ map (mapTypeE tm im) ts) nullRange
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (j, TypeScheme _ ty _) = mapFunSym tm im fm (i, sc)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in Construct (Just j) ts (getPartiality ts ty) $
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder map (map (mapSel tm im fm args dt)) sels
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedermapSel :: TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian MaedermapSel tm im fm args dt s@(Select mid t p) = case mid of
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Just i -> let
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder sc = TypeScheme args (getSelType dt p $ mapTypeE tm im t) nullRange
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (j, TypeScheme _ ty _) = mapFunSym tm im fm (i, sc)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Select (Just j) t $ getPartiality [dt] ty
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-- | get the partiality from a constructor type
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder-- with a given number of curried arguments
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedergetPartiality :: [a] -> Type -> Partiality
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian MaedergetPartiality args t = case getTypeAppl t of
c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder [_] -> if isPartialArrow i then Partial else Total
0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder _ : rs -> getPartiality rs res
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder if null args then Partial else error "getPartiality"
83814002b4922114cbe7e9ba728472a0bf44aac5Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermapSentence m s = let
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder tm = filterAliases $ typeMap $ mtarget m
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder im = typeIdMap m
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fm = funMap m
20e16bdd7481741d0b6b14f952aea42ee7a65efbChristian Maeder f = mapFunSym tm im fm
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder in return $ case s of
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder Formula t -> Formula $ mapSen tm im fm t
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry tm im fm) td
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ProgEqSen i sc pe ->
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let (ni, nsc) = f (i, sc)
a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE tm im) pe
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaedermapFunSym :: TypeMap -> IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)
650bafe7709533bc5f82bb9daf8fa06f431cd963Christian MaedermapFunSym tm im fm (i, sc) =
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder let msc = mapTypeScheme tm im sc
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian MaederembedMorphism :: Env -> Env -> Morphism
a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian MaederembedMorphism = mkMorphism
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till MossakowskiideMor :: Env -> Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederideMor e = embedMorphism e e
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedercompIdMap :: IdMap -> IdMap -> IdMap
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder let k = Map.findWithDefault j j im2 in
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski if i == k then id else Map.insert i k)
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism
842eedc62639561781b6c33533d1949693ef6cc5Christian MaedercompMor m1 m2 =
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder if mtarget m1 == msource m2 then
842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder let tm2 = typeIdMap m2
bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski im = compIdMap (typeIdMap m1) tm2
967e5f3c25249c779575864692935627004d3f9eChristian Maeder fm2 = funMap m2
967e5f3c25249c779575864692935627004d3f9eChristian Maeder tar = mtarget m2
967e5f3c25249c779575864692935627004d3f9eChristian Maeder src = msource m1
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder tm = filterAliases $ typeMap tar
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in return (mkMorphism src tar)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder { typeIdMap = Map.intersection im $ typeMap src
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let p3 = mapFunSym tm tm2 fm2 p2 in
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder if p1 == p3 then id else Map.insert p1 p3)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fm2 $ funMap m1) $ Map.fromList $
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder concatMap ( \ (k, os) ->
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder map ( \ o -> ((k, mapTypeScheme tm im
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder $ opType o), ())) $ Set.toList os)
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder $ Map.toList $ assumps src
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else fail "intermediate signatures of morphisms do not match"
967e5f3c25249c779575864692935627004d3f9eChristian MaederinclusionMor :: Env -> Env -> Result Morphism
7221c71b38c871ce66eee4537cb681d468308dfbChristian MaederinclusionMor e1 e2 =
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder if isSubEnv e1 e2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder then return (embedMorphism e1 e2)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder else Result [Diag Error
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedershowEnvDiff :: Env -> Env -> String
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedershowEnvDiff e1 e2 =
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (diffEnv e1 e2) ""
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederlegalEnv :: Env -> Bool
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederlegalEnv _ = True -- maybe a closure test?
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederlegalMor :: Morphism -> Bool
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederlegalMor m = let s = msource m
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder t = mtarget m
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ts = typeIdMap m
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder fs = funMap m
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder all (`elem` (Map.keys $ typeMap s))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder && all (`elem` (Map.keys $ typeMap t))
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder && all ((`elem` (Map.keys $ assumps t)) . fst)
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedermorphismUnion m1 m2 = do
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder let s1 = msource m1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder s2 = msource m2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder s <- merge s1 s2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder t <- merge (mtarget m1) $ mtarget m2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let tm1 = typeMap s1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder tm2 = typeMap s2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder im1 = typeIdMap m1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder im2 = typeIdMap m2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder -- unchanged types
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder ima1 = Map.union im1 $ setToMap ut1
7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder ima2 = Map.union im2 $ setToMap ut2
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder sAs = filterAliases $ typeMap s
deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder tAs = filterAliases $ typeMap t
967e5f3c25249c779575864692935627004d3f9eChristian Maeder expP = Map.fromList . map ( \ ((i, o), (j, p)) ->
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder ((i, expand tAs o), (j, expand tAs p)))
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fm1 = expP $ funMap m1
83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder fm2 = expP $ funMap m2
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder af im = Set.unions . map ( \ (i, os) ->
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Set.map ( \ o -> (i, mapTypeScheme tAs im
97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder $ expand sAs $ opType o)) os)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder -- unchanged functions
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder uf1 = af im1 (assumps s1) Set.\\ Map.keysSet fm1
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder uf2 = af im2 (assumps s2) Set.\\ Map.keysSet fm2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fma1 = Map.union fm1 $ setToMap uf1
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fma2 = Map.union fm2 $ setToMap uf2
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty
dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder fail $ "incompatible type mapping to `"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder fail $ "incompatible mapping to '"
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2
2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder return (mkMorphism s t)
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder { typeIdMap = tma
07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder , funMap = fma }
typeSymMap = Map.foldWithKey ( \ i ti ->
let j = Map.findWithDefault i i im
in Map.insert (idToTypeSymbol src i k)
$ idToTypeSymbol tar j k) Map.empty $ typeMap src
Set.fold ( \ oi ->
in Map.insert (idToOpSymbol src i ty)