cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

79834070d6d3c63a098e570b12fa3405c607dc70Kristina SojakovaCopyright : (c) Christian Maeder and Uni Bremen 2002-2003

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaMaintainer : maeder@tzi.de

94e2e03f6efde106de095ef4ea0ec87f74955a31Kristina SojakovaStability : provisional

211c5fb252e0a776baad9a4857ab198659289a4aKristina SojakovaPortability : portable

211c5fb252e0a776baad9a4857ab198659289a4aKristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaederMorphism on 'Env' (as for CASL)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder-}

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakovamodule HasCASL.Morphism where

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.Le

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport HasCASL.As

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maederimport HasCASL.AsToLe

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maederimport HasCASL.Unify

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maederimport HasCASL.Symbol

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport HasCASL.MapTerm

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederimport HasCASL.TypeDecl

f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maederimport HasCASL.DataAna

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maederimport Common.Id

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport Common.Keywords

feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzeimport Common.Result

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport Common.PrettyPrint

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport Common.Lib.Pretty

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovaimport qualified Common.Lib.Map as Map

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maedertype IdMap = Map.Map Id Id

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovatype FunMap = Map.Map (Id, TySc) (Id, TySc)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakovadata Morphism = Morphism { msource :: Env

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , mtarget :: Env

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova , classIdMap :: IdMap -- ignore

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova , typeIdMap :: IdMap

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova , funMap :: FunMap }

f30760456a3b6f7d4d54c65323dbc73cceca68fbChristian Maeder deriving (Eq, Show)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maederinstance PrettyPrint Morphism where

feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze printText0 ga m =

feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze let tm = typeIdMap m

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova fm = funMap m

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova ds = Map.foldWithKey ( \ (i, TySc s) (j, TySc t) l ->

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (printText0 ga i <+> colon <+> printText0 ga s

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova <+> text mapsTo <+>

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova printText0 ga j <+> colon <+> printText0 ga t) : l)

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova [] fm

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova in (if Map.isEmpty tm then empty

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova else text (typeS ++ sS) <+> printText0 ga tm)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova $$ (if Map.isEmpty fm then empty

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova else text (opS ++ sS) <+> fsep (punctuate comma ds))

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder $$ nest 1 colon <+> braces (printText0 ga (msource m))

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova $$ nest 1 (text mapsTo)

2ddc9d39235393dca2e40203dde20284db4c3deeKristina Sojakova <+> braces (printText0 ga (mtarget m))

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapType :: IdMap -> Type -> Type

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova-- include classIdMap later

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapType m ty = if Map.isEmpty m then ty else

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova rename ( \ i k n ->

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova let t = TypeName i k n in

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder if n == 0 then

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova case Map.lookup i m of

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova Just j -> TypeName j k 0

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian Maeder _ -> t

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova else t) ty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapTypeScheme :: IdMap -> TypeScheme -> TypeScheme

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova-- rename clashing type arguments later

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapTypeScheme = mapTypeOfScheme . mapType

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapTySc :: IdMap -> TySc -> TySc

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovamapTySc m (TySc s1) = TySc $ mapTypeScheme m s1

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapSen :: Morphism -> Term -> Term

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapSen m = let tm = typeIdMap m in

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova mapTerm (mapFunSym tm (funMap m), mapType tm)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapDatatypeDefn :: Morphism -> IdMap -> DatatypeDefn -> DatatypeDefn

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovamapDatatypeDefn m tm (DatatypeConstr i j k args alts) =

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova let tim = typeIdMap m

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova rtm = Map.difference tim tm

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova -- do not rename the types in the data type mapping

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova in DatatypeConstr i (Map.findWithDefault j j tim)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder k args $ map (mapAlt m tm rtm args $ TypeName j

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova (typeArgsListToKind args star) 0) alts

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapAlt :: Morphism -> IdMap -> IdMap -> [TypeArg] -> Type -> AltDefn -> AltDefn

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina SojakovamapAlt m tm rtm args dt (Construct i ts p sels) =

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova let sc = TypeScheme args

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova ([] :=> getConstrType dt p (map (mapType tm) ts)) []

89dbd1f57ed4195123cdd086f14e0413c2ffac68Kristina Sojakova (j, _) = mapFunSym (typeIdMap m) (funMap m) (i, sc)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder in Construct j (map (mapType rtm) ts) p sels

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova -- not change (unused) selectors and (alas) partiality

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovagetDTMap :: [DatatypeDefn] -> IdMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetDTMap = foldr ( \ (DatatypeConstr i j _ _ _) m ->

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if i == j then m else

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.insert i j m) Map.empty

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian MaedermapSentence :: Morphism -> Sentence -> Result Sentence

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapSentence m s = return $ case s of

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova Formula t -> Formula $ mapSen m t

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova DatatypeSen td -> DatatypeSen $ map (mapDatatypeDefn m $ getDTMap td) td

10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder ProgEqSen i sc pe ->

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova let tm = typeIdMap m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova fm = funMap m

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder f = mapFunSym tm fm

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (ni, nsc) = f (i, sc)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova in ProgEqSen ni nsc $ mapEq (f, mapType tm) pe

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermapFunSym :: IdMap -> FunMap -> (Id, TypeScheme) -> (Id, TypeScheme)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapFunSym tm fm (i, sc) =

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova let (j, TySc s) = mapFunEntry tm fm (i, TySc sc) in (j, s)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapFunEntry :: IdMap -> FunMap -> (Id, TySc) -> (Id, TySc)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamapFunEntry tm fm p@(i, sc) = if Map.isEmpty tm && Map.isEmpty fm then p else

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova Map.findWithDefault (i, mapTySc tm sc) (i, sc) fm

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedermkMorphism :: Env -> Env -> Morphism

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamkMorphism e1 e2 = Morphism e1 e2 Map.empty Map.empty Map.empty

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovaembedMorphism :: Env -> Env -> Morphism

0330f0fab04797f8c41bd12691825032731798a2Kristina SojakovaembedMorphism a b =

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (mkMorphism a b)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova { typeIdMap = foldr (\x -> Map.insert x x) Map.empty

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova $ Map.keys $ typeMap a

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , funMap = Map.foldWithKey

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova ( \ i (OpInfos ts) m -> foldr

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian Maeder (\ oi -> let v = (i, TySc $ opType oi) in

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova Map.insert v v) m ts)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova Map.empty $ assumps a

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederideMor :: Env -> Morphism

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovaideMor e = embedMorphism e e

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedercompMor :: Morphism -> Morphism -> Maybe Morphism

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovacompMor m1 m2 =

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova if isSubEnv (mtarget m1) (msource m2) then

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova let tm2 = typeIdMap m2 in Just

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (mkMorphism (msource m1) (mtarget m2))

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { typeIdMap = Map.map ( \ i -> Map.findWithDefault i i tm2)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder $ typeIdMap m1

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian Maeder , funMap = Map.foldWithKey ( \ p1 p2 ->

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova Map.insert p1

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova $ mapFunEntry tm2 (funMap m2) p2) Map.empty $ funMap m1

0330f0fab04797f8c41bd12691825032731798a2Kristina Sojakova }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else Nothing

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian MaederinclusionMor :: Env -> Env -> Result Morphism

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina SojakovainclusionMor e1 e2 =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if isSubEnv e1 e2

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova then return (embedMorphism e1 e2)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova else pplain_error (ideMor initialEnv)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (ptext "Attempt to construct inclusion between non-subsignatures:"

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian Maeder $$ ptext "Singature 1:" $$ printText e1

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova $$ ptext "Singature 2:" $$ printText e2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullPos

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

cff5f538e6bb82f17567dcdff93291d39d74133dChristian MaedersymbMapToMorphism :: Env -> Env -> SymbolMap -> Result Morphism

034867cd56c1b4a67fddc607eb315d8f2b1933fbChristian MaedersymbMapToMorphism sigma1 sigma2 smap = do

097b7fb3f8f90e87120d30bf37a1d89fe0ddfaf0Kristina Sojakova type_map1 <- Map.foldWithKey myIdMap (return Map.empty) $ typeMap sigma1

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder fun_map1 <- Map.foldWithKey myAsMap (return Map.empty) $ assumps sigma1

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder return (mkMorphism sigma1 sigma2)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova { typeIdMap = type_map1

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , funMap = fun_map1}

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova where

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova myIdMap i k m = do

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova m1 <- m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova sym <- maybeToResult nullPos

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova ("symbMapToMorphism - Could not map sort "++showId i "")

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder $ Map.lookup (Symbol { symName = i

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , symType = TypeAsItemType

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova $ typeKind k

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder , symEnv = sigma1 }) smap

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova return (Map.insert i (symName sym) m1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder myAsMap i (OpInfos ots) m = foldr (insFun i) m ots

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insFun i ot m = do

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova let osc = opType ot

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m1 <- m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova sym <- maybeToResult nullPos

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder ("symbMapToMorphism - Could not map op "++showId i "")

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ Map.lookup (Symbol { symName = i

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , symType = OpAsItemType osc

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova , symEnv = sigma1 }) smap

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova k <- case symType sym of

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova OpAsItemType sc -> return $ TySc sc

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova _ -> plain_error (TySc osc)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova ("symbMapToMorphism - Wrong result symbol type for op"

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder ++showId i "") nullPos

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova return (Map.insert (i, TySc osc) (symName sym, k) m1)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovalegalEnv :: Env -> Bool

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovalegalEnv _ = True -- maybe a closure test?

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovalegalMor :: Morphism -> Bool

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovalegalMor m = let s = msource m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova t = mtarget m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova ts = typeIdMap m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova fs = funMap m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova in

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova all (`elem` (Map.keys $ typeMap s))

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (Map.keys ts)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova && all (`elem` (Map.keys $ typeMap t))

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (Map.elems ts)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder && all ((`elem` (Map.keys $ assumps s)) . fst)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova (Map.keys fs)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova && all ((`elem` (Map.keys $ assumps t)) . fst)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder (Map.elems fs)

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamorphismUnion :: Morphism -> Morphism -> Result Morphism

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina SojakovamorphismUnion m1 m2 =

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova do s <- merge (msource m1) $ msource m2

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova t <- merge (mtarget m1) $ mtarget m2

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova tm <- foldr ( \ (i, j) rm ->

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova do m <- rm

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova case Map.lookup i m of

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova Nothing -> return $ Map.insert i j m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova Just k -> if j == k then return m

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova else do

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova Result [Diag Error

9f8b6c20948cc102562f8ad0c39a4b5e3855b02fKristina Sojakova ("incompatible mapping of type id: " ++

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova showId i " to: " ++ showId j " and: "

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova ++ showId k "") $ posOfId i] $ Just ()

63dbf3642c023a8bebbc8ca0d56f698114551c8cKristina Sojakova return m)

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder (return $ typeIdMap m1) $ Map.toList $ typeIdMap m2

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova fm <- foldr ( \ (isc@(i, _), jsc@(j, TySc sc1)) rm -> do

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova m <- rm

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova case Map.lookup isc m of

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova Nothing -> return $ Map.insert isc jsc m

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova Just ksc@(k, TySc sc2) -> if j == k &&

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova asSchemes 0 (equalSubs $ typeMap t) sc1 sc2

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova then return m

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova else do

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova Result [Diag Error

150dbefbeef7403ab31ecbf9c3bb56515be67cdfKristina Sojakova ("incompatible mapping of op: " ++

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showFun isc " to: " ++ showFun jsc " and: "

cff5f538e6bb82f17567dcdff93291d39d74133dChristian Maeder ++ showFun ksc "") $ posOfId i] $ Just ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return m)

(return $ funMap m1) $ Map.toList $ funMap m2

return (mkMorphism s t)

{ typeIdMap = tm

, funMap = fm }

showFun :: (Id, TySc) -> ShowS

showFun (i, TySc ty) = showId i . (" : " ++) . showPretty ty

morphismToSymbMap :: Morphism -> SymbolMap

morphismToSymbMap mor =

let

src = msource mor

tar = mtarget mor

tm = typeIdMap mor

typeSymMap = Map.foldWithKey ( \ i ti ->

let j = Map.findWithDefault i i tm

k = typeKind ti

in Map.insert (idToTypeSymbol src i k)

$ idToTypeSymbol tar j k) Map.empty $ typeMap src

in Map.foldWithKey

( \ i (OpInfos l) m ->

foldr ( \ oi ->

let ty = opType oi

(j, TySc t2) = mapFunEntry tm (funMap mor) (i, TySc ty)

in Map.insert (idToOpSymbol src i ty)

(idToOpSymbol tar j t2)) m l)

typeSymMap $ assumps src