8a77240a809197c92c0736c431b4b88947a7bac1Christian Maeder{- |

8a77240a809197c92c0736c431b4b88947a7bac1Christian MaederModule : $Header$

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaederDescription : morphisms implementation

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2006

3a6c7a7ff823616f56cd3d205fc44664a683effdChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : Christian.Maeder@dfki.de

2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederStability : provisional

306763c67bb99228487345b32ab8c5c6cd41f23cChristian MaederPortability : portable

306763c67bb99228487345b32ab8c5c6cd41f23cChristian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maedermapping entities of morphisms

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder

44fb55f639914f4f531641f32dd4904f15c510a4Till Mossakowski-}

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskimodule HasCASL.Morphism where

af0cbe339851fc558d2b18cde3666981325e667cTill Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.Le

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowskiimport HasCASL.As

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.FoldType

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport HasCASL.TypeAna

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.AsUtils

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.AsToLe

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.MapTerm

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport HasCASL.Merge

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.DocUtils

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederimport Common.Doc

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Id

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport Common.Result

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Set as Set

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederimport qualified Data.Map as Map

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maederinstance Eq Morphism where

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder m1 == m2 = (msource m1, mtarget m1, typeIdMap m1, classIdMap m1, funMap m1)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder == (msource m2, mtarget m2, typeIdMap m2, classIdMap m2, funMap m2)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaederdisjointKeys :: (Ord a, Pretty a, Monad m) => Map.Map a b -> Map.Map a c

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder -> m ()

1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederdisjointKeys m1 m2 = let d = Map.keysSet $ Map.intersection m1 m2 in

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski if Set.null d then return () else

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fail $ show

922819b1c2d383a0fa5d70e1c4aa76667e2f1ca3Christian Maeder (sep [ text "overlapping identifiers for types and classes:"

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder , pretty d])

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder-- | map a kind along an identifier map

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian MaedermapKindI :: IdMap -> Kind -> Kind

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKindI jm = mapKind $ (\ a -> Map.findWithDefault a a jm)

24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder-- | map a kind along a signature morphism (variance is preserved)

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds :: Morphism -> Kind -> Kind

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaedermapKinds mor = mapKindI $ classIdMap mor

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder-- | only rename the kinds in a type

63324a97283728a30932828a612c7b0b0f687624Christian MaedermapKindsOfType :: IdMap -> TypeMap -> IdMap -> Type -> Type

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapKindsOfType jm tm im = foldType mapTypeRec

59fa9b1349ae1e001d996da732c4ac805c2938e2Christian Maeder { foldTypeAbs = \ _ a t p -> TypeAbs (mapTypeArg jm tm im a) t p

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski , foldKindedType = \ _ t ks p -> KindedType t

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (Set.map (mapKindI jm) ks) p }

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map type, expand it, and also adjust the kinds

53310804002cd9e3c9c5844db3b984abcf001788Christian MaedermapTypeE :: IdMap -> TypeMap -> IdMap -> Type -> Type

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeE jm tm im =

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski mapKindsOfType jm tm im . expandAliases tm . mapType im

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski-- | map a kind along a signature morphism (variance is preserved)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind :: IdMap -> TypeMap -> IdMap -> VarKind -> VarKind

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapVarKind jm tm im vk = case vk of

3a87487c048b275c56e502c4a933273788e8d0bbChristian Maeder VarKind k -> VarKind $ mapKindI jm k

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu Downset ty -> Downset $ mapTypeE jm tm im ty

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu _ -> vk

2b565fe5cfb9f99857fd25b52304758d8544e266Mihai Codescu

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskimapTypeArg :: IdMap -> TypeMap -> IdMap -> TypeArg -> TypeArg

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapTypeArg jm tm im (TypeArg i v vk rk c s r) =

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder TypeArg i v (mapVarKind jm tm im vk) rk c s r

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till Mossakowski

8731f7b93b26083dc34a2c0937cd6493b42f2c2cTill MossakowskimapTypeScheme :: IdMap -> TypeMap -> IdMap -> TypeScheme -> TypeScheme

d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian MaedermapTypeScheme jm tm im (TypeScheme args ty ps) =

24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder TypeScheme (map (mapTypeArg jm tm im) args) (mapTypeE jm tm im ty) ps

24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder

4184cb191a9081cb2a9cf3ef5f060f56f0ca5922Till MossakowskimapSen :: IdMap -> TypeMap -> IdMap -> FunMap -> Term -> Term

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapSen jm tm im fm = mapTerm (mapFunSym jm tm im fm, mapTypeE jm tm im)

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder

bba825b39570777866d560bfde3807731131097eKlaus LuettichsetToMap :: Ord a => Set.Set a -> Map.Map a a

d97cb7d1c9beadc4d9102738da0a88c4efcf8fddChristian MaedersetToMap = Map.fromAscList . map ( \ a -> (a, a)) . Set.toList

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedergetDatatypeIds :: DataEntry -> Set.Set Id

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedergetDatatypeIds (DataEntry _ i _ _ _ alts) =

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder let getAltIds (Construct _ tys _ sels) = Set.union

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder (Set.unions $ map getTypeIds tys)

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder $ Set.unions $ concatMap (map getSelIds) sels

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder getSelIds (Select _ ty _) = getTypeIds ty

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder getTypeIds = idsOf (== 0)

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder in Set.insert i $ Set.unions $ map getAltIds $ Set.toList alts

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder

f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaedermapDataEntry :: IdMap -> TypeMap -> IdMap -> FunMap -> DataEntry -> DataEntry

f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaedermapDataEntry jm tm im fm de@(DataEntry dm i k args rk alts) =

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder let tim = Map.intersection (compIdMap dm im) $ setToMap $ getDatatypeIds de

3d86f079b07a6a058cdd6c112d287e01a69d9c0cChristian Maeder newargs = map (mapTypeArg jm tm im) args

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder in DataEntry tim i k newargs rk $ Set.map

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder (mapAlt jm tm tim fm newargs

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder $ patToType (Map.findWithDefault i i tim) args rk) alts

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaedermapAlt :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> AltDefn

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu -> AltDefn

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaedermapAlt jm tm im fm args dt c@(Construct mi ts p sels) =

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder case mi of

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder Just i ->

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder let sc = TypeScheme args

a975722baf6fee1ca3e67df170c732c4abd0a945Christian Maeder (getFunType dt p $ map (mapTypeE jm tm im) ts) nullRange

63324a97283728a30932828a612c7b0b0f687624Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder in Construct (Just j) ts (getPartiality ts ty) $

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu map (map (mapSel jm tm im fm args dt)) sels

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder Nothing -> c

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapSel :: IdMap -> TypeMap -> IdMap -> FunMap -> [TypeArg] -> Type -> Selector

b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder -> Selector

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapSel jm tm im fm args dt s@(Select mid t p) = case mid of

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu Nothing -> s

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder Just i -> let

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu sc = TypeScheme args (getSelType dt p $ mapTypeE jm tm im t) nullRange

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder (j, TypeScheme _ ty _) = mapFunSym jm tm im fm (i, sc)

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu in Select (Just j) t $ getPartiality [dt] ty

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski

0e51a998b1b213654c7a9eca451562041971f100Till Mossakowski-- | get the partiality from a constructor type

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder-- with a given number of curried arguments

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian MaedergetPartiality :: [a] -> Type -> Partiality

e9249d3ecd51a2b6a966a58669953e58d703adc6Till MossakowskigetPartiality args t = case getTypeAppl t of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (TypeName i _ _, [_, res]) | isArrow i -> case args of

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [] -> Total

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder [_] -> if isPartialArrow i then Partial else Total

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder _ : rs -> getPartiality rs res

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder (TypeName i _ _, [_]) | i == lazyTypeId ->

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if null args then Partial else error "getPartiality"

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder _ -> Total

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapSentence :: Morphism -> Sentence -> Result Sentence

f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaedermapSentence m s = let

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder tm = filterAliases $ typeMap $ mtarget m

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder im = typeIdMap m

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder jm = classIdMap m

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder fm = funMap m

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder f = mapFunSym jm tm im fm

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder in return $ case s of

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder Formula t -> Formula $ mapSen jm tm im fm t

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder DatatypeSen td -> DatatypeSen $ map (mapDataEntry jm tm im fm) td

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder ProgEqSen i sc pe ->

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let (ni, nsc) = f (i, sc)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder in ProgEqSen ni nsc $ mapEq (f, mapTypeE jm tm im) pe

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym :: IdMap -> TypeMap -> IdMap -> FunMap -> (Id, TypeScheme)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder -> (Id, TypeScheme)

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedermapFunSym jm tm im fm (i, sc) =

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder let msc = mapTypeScheme jm tm im sc

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder in Map.findWithDefault (i, msc) (i, msc) fm

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor :: Env -> Morphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaederideMor e = mkMorphism e e

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap :: IdMap -> IdMap -> IdMap

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompIdMap im1 im2 = Map.foldWithKey ( \ i j ->

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let k = Map.findWithDefault j j im2 in

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder if i == k then id else Map.insert i k) im2 im1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor :: Morphism -> Morphism -> Result Morphism

5c358300e78157f4bfaf5415c70e1096a9205b61Christian MaedercompMor m1 m2 = if mtarget m1 == msource m2 then

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder let tm1 = typeIdMap m1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder tm2 = typeIdMap m2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder im = compIdMap tm1 tm2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm1 = classIdMap m1

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder cm2 = classIdMap m2

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu cm = compIdMap cm1 cm2

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu fm2 = funMap m2

5c358300e78157f4bfaf5415c70e1096a9205b61Christian Maeder fm1 = funMap m1

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder tar = mtarget m2

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder src = msource m1

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder tm = filterAliases $ typeMap tar

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ctm = Map.intersection im $ typeMap src

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ccm = Map.intersection cm $ classMap src

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder emb = mkMorphism src tar

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder in if Map.null tm1 && Map.null tm2 && Map.null cm1 && Map.null cm2

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder && Map.null fm1 && Map.null fm2 then return emb else do

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder disjointKeys ctm ccm

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder return emb

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder { typeIdMap = ctm

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , classIdMap = ccm

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder , funMap = Map.intersection (Map.foldWithKey ( \ p1 p2 ->

255f43c567972176c2078e3de2fb7a2798bcfde0Christian Maeder let p3 = mapFunSym cm tm tm2 fm2 p2 in

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder if p1 == p3 then id else Map.insert p1 p3)

8c7aa750542dcadb94b971be712564a9a8f1d189Christian Maeder fm2 fm1) $ Map.fromList $

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder concatMap ( \ (k, os) ->

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder map ( \ o -> ((k, mapTypeScheme cm tm im

9f87aabedf02d74917d94fe1ac0300e07d3d4bc2Christian Maeder $ opType o), ())) $ Set.toList os)

24a0fbb77b860bc28d25be37ba555fd5746cb6d6Christian Maeder $ Map.toList $ assumps src }

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder else fail "intermediate signatures of morphisms do not match"

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaederinclusionMor :: Env -> Env -> Result Morphism

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian MaederinclusionMor e1 e2 =

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder if isSubEnv e1 e2

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder then return (mkMorphism e1 e2)

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder else Result [Diag Error

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder ("Attempt to construct inclusion between non-subsignatures:\n"

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian Maeder ++ showEnvDiff e1 e2) nullRange] Nothing

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder

6ea54752d184beb92c92fbae17ae9f7dd065d988Christian MaedershowEnvDiff :: Env -> Env -> String

b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedershowEnvDiff e1 e2 =

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder "Signature 1:\n" ++ showDoc e1 "\nSignature 2:\n"

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder ++ showDoc e2 "\nDifference\n" ++ showDoc

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder (diffEnv e1 e2) ""

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian MaederlegalEnv :: Env -> Bool

f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaederlegalEnv _ = True -- maybe a closure test?

f23641ce10de2d58493d41a4b39c64d904e5b534Christian Maeder

f23641ce10de2d58493d41a4b39c64d904e5b534Christian MaederlegalMor :: Morphism -> Bool

19298cbfd6ee2abd904f3181af7760b965b822c3Christian MaederlegalMor m = let

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder s = msource m

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder t = mtarget m

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ts = typeIdMap m

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder cs = classIdMap m

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder fs = funMap m in

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich all (`elem` Map.keys (typeMap s)) (Map.keys ts)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (typeMap t)) (Map.elems ts)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (classMap s)) (Map.keys cs)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all (`elem` Map.keys (classMap t)) (Map.elems cs)

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich && all ((`elem` Map.keys (assumps s)) . fst) (Map.keys fs)

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu && all ((`elem` Map.keys (assumps t)) . fst) (Map.elems fs)

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermorphismUnion :: Morphism -> Morphism -> Result Morphism

556f473448dfcceee22afaa89ed7a364489cdbbbChristian MaedermorphismUnion m1 m2 = do

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder let s1 = msource m1

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich s2 = msource m2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich s <- merge s1 s2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich t <- merge (mtarget m1) $ mtarget m2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich let tm1 = typeMap s1

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich tm2 = typeMap s2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich im1 = typeIdMap m1

da955132262baab309a50fdffe228c9efe68251dCui Jian im2 = typeIdMap m2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich -- unchanged types

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ut1 = Map.keysSet tm1 Set.\\ Map.keysSet im1

da955132262baab309a50fdffe228c9efe68251dCui Jian ut2 = Map.keysSet tm2 Set.\\ Map.keysSet im2

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder ima1 = Map.union im1 $ setToMap ut1

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder ima2 = Map.union im2 $ setToMap ut2

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder sAs = filterAliases $ typeMap s

556f473448dfcceee22afaa89ed7a364489cdbbbChristian Maeder tAs = filterAliases $ typeMap t

fd496ec12c6be2731410ea84111f1ff88d8b6384Christian Maeder cm1 = classMap s1

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cm2 = classMap s2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich jm1 = classIdMap m1

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder jm2 = classIdMap m2

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder -- unchanged classes

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cut1 = Map.keysSet cm1 Set.\\ Map.keysSet jm1

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cut2 = Map.keysSet cm2 Set.\\ Map.keysSet jm2

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cima1 = Map.union jm1 $ setToMap cut1

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder cima2 = Map.union jm2 $ setToMap cut2

3946c010d94321f14139e12061dd4261a3cc7295Christian Maeder expP = Map.fromList . map ( \ ((i, o), (j, p)) ->

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder ((i, expand tAs o), (j, expand tAs p)))

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder . Map.toList

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder fm1 = expP $ funMap m1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fm2 = expP $ funMap m2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski af jm im = Set.unions . map ( \ (i, os) ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski Set.map ( \ o -> (i, mapTypeScheme jm tAs im

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ expand sAs $ opType o)) os)

6ca6ffc92f5c0058ae4b92d46e4e8cbc7beb11fcMihai Codescu . Map.toList

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski -- unchanged functions

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski uf1 = af jm1 im1 (assumps s1) Set.\\ Map.keysSet fm1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski uf2 = af jm2 im2 (assumps s2) Set.\\ Map.keysSet fm2

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma1 = Map.union fm1 $ setToMap uf1

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski fma2 = Map.union fm2 $ setToMap uf2

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder showFun (i, ty) = showId i . (" : " ++) . showDoc ty

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski tma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fail $ "incompatible type mapping to `"

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich ++ showId t1 "' and '" ++ showId t2 "'") ima1 ima2

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich cma <- mergeMap ( \ t1 t2 -> if t1 == t2 then return t1 else

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder fail $ "incompatible class mapping to `"

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder ++ showId t1 "' and '" ++ showId t2 "'") cima1 cima2

3fb8a83c3c06671ee94fd12a1782b14563d09df1Christian Maeder fma <- mergeMap ( \ o1 o2 -> if o1 == o2 then return o1 else

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus Luettich fail $ "incompatible mapping to '"

19298cbfd6ee2abd904f3181af7760b965b822c3Christian Maeder ++ showFun o1 "' and '" ++ showFun o2 "'") fma1 fma2

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder disjointKeys tma cma

27166b063721ef1a2efd8f00ab3d9bc820b315fbChristian Maeder return (mkMorphism s t)

83b3260413a3b1b7dee1f9c4d3249dec994a875cMihai Codescu { typeIdMap = tma

da955132262baab309a50fdffe228c9efe68251dCui Jian , classIdMap = cma

da955132262baab309a50fdffe228c9efe68251dCui Jian , funMap = fma }

da955132262baab309a50fdffe228c9efe68251dCui Jian

eb0e19a83d8e3eaeb936c197555b20d37129022cKlaus LuettichmorphismToSymbMap :: Morphism -> SymbolMap

da955132262baab309a50fdffe228c9efe68251dCui JianmorphismToSymbMap mor = let

a98fd29a06e80e447af26d898044c23497adbc73Mihai Codescu src = msource mor

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu tar = mtarget mor

f2c050360525df494e6115073b0edc4c443a847cMihai Codescu im = typeIdMap mor

b60a22e76e983e8129c5dae4d713fe2794ed7054Christian Maeder jm = classIdMap mor

da955132262baab309a50fdffe228c9efe68251dCui Jian tm = filterAliases $ typeMap tar

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder classSymMap = Map.foldWithKey ( \ i ti ->

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder let j = Map.findWithDefault i i jm

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder k = rawKind ti

ca8550c6d47234042130bdc10a152806ecbc9832Christian Maeder in Map.insert (idToClassSymbol src i k)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder $ idToClassSymbol tar j k) Map.empty $ classMap src

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder typeSymMap = Map.foldWithKey ( \ i ti ->

4ef5e33657aae95850b7e6941f67ac1fb73cd13fChristian Maeder let j = Map.findWithDefault i i im

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski k = typeKind ti

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.insert (idToTypeSymbol src i k)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski $ idToTypeSymbol tar j k) classSymMap $ typeMap src

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski in Map.foldWithKey

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski ( \ i s m ->

53310804002cd9e3c9c5844db3b984abcf001788Christian Maeder Set.fold ( \ oi ->

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski let ty = opType oi

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder (j, t2) = mapFunSym jm tm im (funMap mor) (i, ty)

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder in Map.insert (idToOpSymbol src i ty)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski (idToOpSymbol tar j t2)) m s)

e9249d3ecd51a2b6a966a58669953e58d703adc6Till Mossakowski typeSymMap $ assumps src

d85e3f253f6af237c4b70bbfacb1bfecb5cfa678Christian Maeder