4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederDescription : symbol map analysis for the CASL logic.

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederLicense : GPLv2 or higher, see LICENSE.txt

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederMaintainer : Christian.Maeder@dfki.de

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederSymbol map analysis for the CASL logic.

ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder Follows Sect. III:4.1 of the CASL Reference Manual.

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL.SymbolMapAnalysis

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder ( inducedFromMorphism

0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder , inducedFromToMorphism

0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder , inducedFromMorphismExt

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder , inducedFromToMorphismExt

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder , cogeneratedSign

dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder , generatedSign

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , finalUnion

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder , constMorphExt

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , revealSym

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder , hideSym

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , profileContainsSort

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder ) where

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport CASL.Sign

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport CASL.AS_Basic_CASL

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederimport CASL.Morphism

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport CASL.Overload (leqF, leqP)

0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport qualified Data.Map as Map

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport qualified Data.Set as Set

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport qualified Common.Lib.Rel as Rel

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Doc

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.DocUtils

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Common.ExtSign

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Id

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Common.Result

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Data.List (partition, find)

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport Data.Maybe

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder{-

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederinducedFromMorphism :: RawSymbolMap -> sign -> Result morphism

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederHere is Bartek Klin's algorithm that has benn used for CATS.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederOur algorithm deviates from it. The exact details need to be checked.

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederInducing morphism from raw symbol map and signature

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederInput: raw symbol map "Rsm"

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder signature "Sigma1"

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederOutput: morphims "Mrph": Sigma1 -> "Sigma2".

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder//preparation

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder1. let "Ssm" be an empty list of pairs (symbol, raw symbol).

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder2. for each pair "Rsym1,Rsym2" in Rsm do:

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder 2.1. if there is no symbol in Sigma1 matching Rsym1, return error.

cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder 2.2. for each symbol "Sym" from Sigma1 matching Rsym1

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 2.2.1. add a pair "Sym,Rsym2" to Ssm.

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder//computing the "sort part" of the morphism

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder3. let Sigma2 be an empty signature.

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder 5.1. if Rsym2 is not a sort raw symbol, return error.

e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder 5.2. if in Mrph there is a mapping of sort in Sym to sort with

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder name other than that in Rsym2, return error.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 5.3. if in Mrph there is no mappinh of sort in Sym

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 5.3.1. add sort from Rsym2 to Sigma2

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder6. for each sort symbol "S" in Sigma1

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder 6.1. if S is not mapped by Mrph,

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder 6.1.1. add sort S to Sigma2

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder 6.1.2. add mapping from S to S to Mrph.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder//computing the "function/predicate part" of the morphism

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder7. for each pair "Sym,Rsym2" in Ssm such that Sym is a function/predicate

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder symbol

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.2. let "Fprof1" be the value of Fprof via Mrph

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (it can be computed, as we already have the "sort" part of

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder morphism)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder 7.3. if Rsym2 is not of appriopriate type, return error, otherwise

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder let "F2" be the name of the symbol.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder an implicit symbol), compare the profile to Fprof1. If it is

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder not equal, return error.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.5. if in Mrph there is a mapping of F1 with profile Fprof to

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder some name different than F2, return error.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.6. add an operation/predicate with name F2 and profile Fprof1 to

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Sigma2. If it is a partial function and if in Sigma2 there

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder exists a total function with the same name and profile, do not

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder add it. Otherwise if it is a total function and if in Sigma2

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder there exists a partial function with the same name and profile,

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder add the total function removing the partial one.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder 7.7. add to Mrph a mapping from operation/predicate of name F1 and

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder profile Fprof to name F2.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder that is not mapped by Mrph,

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder 8.1. as in 7.2

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder 8.2. as in 7.6, replacing F2 with F1.

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder 8.3. as in 7.7, replacing F2 with F1.

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder9. for each sort relation "S1,S2" in Sigma1,

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder 9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder 9.2. add sort relation "S3,S4" in Sigma2.

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder10. Compute transitive closure of subsorting relation in Sigma2.

502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder-}

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maedertype InducedMorphism e m = RawSymbolMap -> e -> Result m

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederconstMorphExt :: m -> InducedMorphism e m

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederconstMorphExt m _ _ = return m

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder{- | function and preds in the overloading relation are mapped in the same way

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederthus preserving the overload-relation -}

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederinducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder -> Result (Morphism f e m)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederinducedFromMorphism =

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder inducedFromMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederinducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e

31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder -> InducedMorphism e m

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)

76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian MaederinducedFromMorphismExt extInd extEm rmap sigma = do

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- compute the sort map (as a Map)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sort_Map <- Set.fold (\ s m -> do

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder s' <- sortFun rmap s

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder m1 <- m

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder return $ if s' == s then m1 else Map.insert s s' m1)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (return Map.empty) (sortSet sigma)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- compute the op map (as a Map)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder op_Map <- Map.foldWithKey (opFun sigma rmap sort_Map)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (return Map.empty) (opMap sigma)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- compute the pred map (as a Map)

628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder pred_Map <- Map.foldWithKey (predFun sigma rmap sort_Map)

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (return Map.empty) (predMap sigma)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder em <- extEm rmap $ extendedInfo sigma

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder -- return assembled morphism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return (embedMorphism em sigma $ closeSortRel

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder $ inducedSignAux extInd sort_Map op_Map pred_Map em sigma)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder { sort_map = sort_Map

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder , op_map = op_Map

cbbb99ab370e6ad265b14a37e7d35b7f08a50d43Christian Maeder , pred_map = pred_Map }

ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder

0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder {- the sorts of the source signature

fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder sortFun is the sort map as a Haskell function -}

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedersortFun :: RawSymbolMap -> Id -> Result Id

c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian MaedersortFun rmap s

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- rsys contains the raw symbols to which s is mapped to

7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder | Set.null rsys = return s -- use default = identity mapping

ac07a6558423dae7adc488ed9092cd8e9450a29dChristian Maeder | Set.null $ Set.deleteMin rsys =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder return $ rawSymName $ Set.findMin rsys -- take the unique rsy

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | otherwise = plain_error s -- ambiguity! generate an error

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder ("sort " ++ showId s

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder " is mapped ambiguously: " ++ showDoc rsys "")

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder $ getRange rsys

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder where

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder -- get all raw symbols to which s is mapped to

154d4152b38c55c3c4ab8f35578669a65fc04df9Christian Maeder rsys = Set.fromList $ mapMaybe (`Map.lookup` rmap)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder [ ASymbol $ idToSortSymbol s

b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder , AKindedSymb Implicit s ]

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder {- to a Op_map, add everything resulting from mapping (id, ots)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder according to rmap -}

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederopFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder -> Result Op_map -> Result Op_map

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederopFun src rmap sort_Map ide ots m =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- first consider all directly mapped profiles

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let otls = Rel.partSet (leqF src) ots

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder m1 = foldr (directOpMap rmap sort_Map ide) m otls

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- now try the remaining ones with (un)kinded raw symbol

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder in case (Map.lookup (AKindedSymb Ops_kind ide) rmap,

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (Just rsy1, Just rsy2) -> let

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder m2 = Set.fold (insertmapOpSym sort_Map ide rsy1) m1 ots

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder in Set.fold (insertmapOpSym sort_Map ide rsy2) m2 ots

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (Just rsy, Nothing) ->

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (Nothing, Just rsy) ->

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -- Anything not mapped explicitly is left unchanged

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (Nothing, Nothing) -> m1

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder {- try to map an operation symbol directly

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder collect all opTypes that cannot be mapped directly -}

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederdirectOpMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -> Result Op_map -> Result Op_map

f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaederdirectOpMap rmap sort_Map ide ots m =

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let ol = Set.toList ots

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder rl = map (lookupOpSymbol rmap ide) ol

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (ms, os) = partition (isJust . fst) $ zip rl ol

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder in case ms of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder l@((Just rsy, _) : rs) ->

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder foldr (\ (_, ot) ->

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder insertmapOpSym sort_Map ide

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (ASymbol $ idToOpSymbol (rawSymName rsy)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder $ mapOpType sort_Map ot) ot)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (foldr (\ (rsy2, ot) ->

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder insertmapOpSym sort_Map ide (fromJust rsy2) ot) m l)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder $ rs ++ os

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder _ -> m

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederlookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederlookupOpSymbol rmap ide' ot = let mkS = idToOpSymbol ide' in

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder case Map.lookup (ASymbol (mkS $ mkPartial ot)) rmap of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> Map.lookup

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (ASymbol (mkS $ mkTotal ot)) rmap

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder res -> res

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- map op symbol (ide, ot) to raw symbol rsy

f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedermappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedermappedOpSym sort_Map ide ot rsy =

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let opSym = "operation symbol " ++ showDoc (idToOpSymbol ide ot)

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder " is mapped to "

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder kind = opKind ot

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder ot2 = mapOpType sort_Map ot

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder in case rsy of

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder ASymbol (Symbol ide' (OpAsItemType ot')) ->

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder if compatibleOpTypes ot2 ot'

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder then return (ide', opKind ot')

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else plain_error (ide, kind)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder (opSym ++ "type " ++ showDoc ot'

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder " but should be mapped to type " ++

f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder showDoc ot2 "") $ getRange rsy

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder AKindedSymb k ide' | elem k [Implicit, Ops_kind] -> return (ide', kind)

afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder _ -> plain_error (ide, kind)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (opSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder $ getRange rsy

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder -- insert mapping of op symbol (ide, ot) to raw symbol rsy into m

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederinsertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder -> Result Op_map -> Result Op_map

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederinsertmapOpSym sort_Map ide rsy ot m = do

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder m1 <- m

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (ide', kind') <- mappedOpSym sort_Map ide ot rsy

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder let otsy = Symbol ide $ OpAsItemType ot

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder pos = getRange rsy

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder m2 = Map.insert (ide, mkPartial ot) (ide', kind') m1

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder case Map.lookup (ide, mkPartial ot) m1 of

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Nothing -> if ide == ide' && kind' == opKind ot then

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder case rsy of

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ASymbol _ -> return m1

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ -> hint m1 ("identity mapping of "

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ++ showDoc otsy "") pos

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder else return m2

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder Just (ide'', kind'') -> if ide' == ide'' then

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder warning (if kind' < kind'' then m2 else m1)

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ("ignoring duplicate mapping of " ++ showDoc otsy "")

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder pos

9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else plain_error m1

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder ("conflicting mapping of " ++ showDoc otsy " to " ++

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder show ide' ++ " and " ++ show ide'') pos

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder {- to a Pred_map, add evering resulting from mapping (ide, pts)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder according to rmap -}

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederpredFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -> Result Pred_map -> Result Pred_map

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederpredFun src rmap sort_Map ide pts m =

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -- first consider all directly mapped profiles

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let ptls = Rel.partSet (leqP src) pts

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder m1 = foldr (directPredMap rmap sort_Map ide) m ptls

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -- now try the remaining ones with (un)kinded raw symbol

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder in case (Map.lookup (AKindedSymb Preds_kind ide) rmap,

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (Just rsy1, Just rsy2) -> let

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder m2 = Set.fold (insertmapPredSym sort_Map ide rsy1) m1 pts

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder in Set.fold (insertmapPredSym sort_Map ide rsy2) m2 pts

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (Just rsy, Nothing) ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (Nothing, Just rsy) ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder -- Anything not mapped explicitly is left unchanged

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (Nothing, Nothing) -> m1

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder {- try to map a predicate symbol directly

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder collect all predTypes that cannot be mapped directly -}

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederdirectPredMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -> Result Pred_map -> Result Pred_map

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederdirectPredMap rmap sort_Map ide pts m =

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let pl = Set.toList pts

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder rl = map (\ pt -> Map.lookup (ASymbol $ idToPredSymbol ide pt) rmap) pl

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (ms, ps) = partition (isJust . fst) $ zip rl pl

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder in case ms of

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder l@((Just rsy, _) : rs) ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder foldr (\ (_, pt) ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder insertmapPredSym sort_Map ide

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder (ASymbol $ idToPredSymbol (rawSymName rsy)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder $ mapPredType sort_Map pt) pt)

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (foldr (\ (rsy2, pt) ->

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder insertmapPredSym sort_Map ide (fromJust rsy2) pt) m l)

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder $ rs ++ ps

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ -> m

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -- map pred symbol (ide, pt) to raw symbol rsy

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedermappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedermappedPredSym sort_Map ide pt rsy =

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder let predSym = "predicate symbol " ++ showDoc (idToPredSymbol ide pt)

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder " is mapped to "

4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder pt2 = mapPredType sort_Map pt

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder in case rsy of

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ASymbol (Symbol ide' (PredAsItemType pt')) ->

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder if pt2 == pt'

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder then return ide'

else plain_error ide

(predSym ++ "type " ++ showDoc pt'

" but should be mapped to type " ++

showDoc pt2 "") $ getRange rsy

AKindedSymb k ide' | elem k [Implicit, Preds_kind] -> return ide'

_ -> plain_error ide

(predSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

$ getRange rsy

-- insert mapping of pred symbol (ide, pt) to raw symbol rsy into m

insertmapPredSym :: Sort_map -> Id -> RawSymbol -> PredType

-> Result Pred_map -> Result Pred_map

insertmapPredSym sort_Map ide rsy pt m = do

m1 <- m

ide' <- mappedPredSym sort_Map ide pt rsy

let ptsy = Symbol ide $ PredAsItemType pt

pos = getRange rsy

m2 = Map.insert (ide, pt) ide' m1

case Map.lookup (ide, pt) m1 of

Nothing -> if ide == ide' then

case rsy of

ASymbol _ -> return m1

_ -> hint m1 ("identity mapping of "

++ showDoc ptsy "") pos

else return m2

Just ide'' -> if ide' == ide'' then

warning m1

("ignoring duplicate mapping of " ++ showDoc ptsy "") pos

else plain_error m1

("conflicting mapping of " ++ showDoc ptsy " to " ++

show ide' ++ " and " ++ show ide'') pos

{-

inducedFromToMorphism :: RawSymbolMap -> sign -> sign -> Result morphism

Algorithm adapted from Bartek Klin's algorithm for CATS.

Inducing morphisms from raw symbol map and source and target signature.

This problem is NP-hard (The problem of 3-colouring can be reduced to it).

This means that we have exponential runtime in the worst case.

However, in many cases the runtime can be kept rather short by

using some basic principles of constraint programming.

We use a depth-first search with some weak form of constraint

propagation and MRV (minimum remaining values), see

Stuart Russell and Peter Norvig:

Artificial Intelligence - A Modern Approach.

Prentice Hall International

The algorithm has additionally to take care of default values (i.e.

symbol names are mapped identically be default, and the number of

identitically mapped names should be maximized). Moreover, it does

not suffice to find just one solution, but also its uniqueness

(among those maximizing he number of identitically mapped names)

must be checked (still, MRV is useful here).

The algorithm

Input: raw symbol map "rmap"

signatures "sigma1,sigma2"

Output: morphism "mor": sigma1 -> sigma2

1. compute the morphism mor1 induced by rmap and sigma1 (i.e. the renaming)

1.1. if target mor1 is a subsignature of sigma2, return the composition

of this inclusion with mor1

(cf. Theorem 6 of Bartek Klin's Master's Thesis)

otherwise some heuristics is needed, because merely forgetting one renaming

may lead to unacceptable run-time for signatures with just about 10 symbols

-}

-- the main function

inducedFromToMorphism :: (Eq e, Show f, Pretty e, Pretty m)

=> m -- ^ extended morphism

-> (e -> e -> Bool) -- ^ subsignature test of extensions

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

-> ExtSign (Sign f e) Symbol -> Result (Morphism f e m)

inducedFromToMorphism m =

inducedFromToMorphismExt (\ _ _ _ _ -> extendedInfo) (constMorphExt m)

(\ _ _ -> return m)

inducedFromToMorphismExt

:: (Eq e, Show f, Pretty e, Pretty m)

=> InducedSign f e m e

-> InducedMorphism e m -- ^ compute extended morphism

-> (Morphism f e m -> Morphism f e m -> Result m)

-- ^ composition of extensions

-> (e -> e -> Bool) -- ^ subsignature test of extensions

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

-> ExtSign (Sign f e) Symbol

-> Result (Morphism f e m)

inducedFromToMorphismExt extInd extEm compM isSubExt diffExt rmap

sig1@(ExtSign _ sy1) sig2@(ExtSign _ sy2) =

let iftm rm = (inducedFromToMorphismAuxExt extInd extEm compM isSubExt

diffExt rm sig1 sig2, rm)

isOk = isJust . resultToMaybe

res = fst $ iftm rmap

pos = concatMapRange getRange $ Map.keys rmap

in if isOk res then res else

let ss1 = Set.filter (\ s -> Set.null $ Set.filter

(compatibleSymbols True s) sy2)

$ Set.filter (\ s -> not $ any (matches s) $ Map.keys rmap)

sy1

fcombs = filteredPairs compatibleRawSymbs

(map ASymbol $ Set.toList ss1)

$ map ASymbol $ Set.toList sy2

in if null (drop 20 fcombs) then

case filter (isOk . fst) $ map (iftm . Map.union rmap . Map.fromList)

fcombs of

[] -> res

[(r, m)] -> (if length fcombs > 1 then warning else hint)

() ("derived symbol map:\n" ++ showDoc m "") pos >> r

l -> fatal_error

("ambiguous symbol maps:\n" ++ show

(vcat $ map (pretty . snd) l)) pos

else warning () "too many possibilities for symbol maps" pos >> res

compatibleSymbTypes :: SymbType -> SymbType -> Bool

compatibleSymbTypes s1 s2 = case (s1, s2) of

(SortAsItemType, SortAsItemType) -> True

(OpAsItemType t1, OpAsItemType t2) ->

length (opArgs t1) == length (opArgs t2)

(PredAsItemType p1, PredAsItemType p2) ->

length (predArgs p1) == length (predArgs p2)

_ -> False

compatibleSymbols :: Bool -> Symbol -> Symbol -> Bool

compatibleSymbols alsoId (Symbol i1 k1) (Symbol i2 k2) =

compatibleSymbTypes k1 k2 && (not alsoId || i1 == i2)

compatibleRawSymbs :: RawSymbol -> RawSymbol -> Bool

compatibleRawSymbs r1 r2 = case (r1, r2) of

(ASymbol s1, ASymbol s2) -> compatibleSymbols False s1 s2

_ -> False -- irrelevant

filteredPairs :: (a -> b -> Bool) -> [a] -> [b] -> [[(a, b)]]

filteredPairs p s l = sequence [[(a, b) | b <- filter (p a) l] | a <- s]

-- http://www.haskell.org/pipermail/haskell-cafe/2009-December/069957.html

inducedFromToMorphismAuxExt

:: (Eq e, Show f, Pretty e, Pretty m)

=> InducedSign f e m e

-> InducedMorphism e m -- ^ compute extended morphism

-> (Morphism f e m -> Morphism f e m -> Result m)

-- ^ composition of extensions

-> (e -> e -> Bool) -- ^ subsignature test of extensions

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

-> ExtSign (Sign f e) Symbol

-> Result (Morphism f e m)

inducedFromToMorphismAuxExt extInd extEm compM isSubExt diffExt rmap

(ExtSign sigma1 _) (ExtSign sigma2 _) = do

-- 1. use rmap to get a renaming...

mor1 <- inducedFromMorphismExt extInd extEm rmap sigma1

-- 1.1 ... is the renamed source signature contained in the target signature?

let inducedSign = mtarget mor1

em = extended_map mor1

if isSubSig isSubExt inducedSign sigma2

-- yes => we are done

then composeM compM mor1 $ idOrInclMorphism

$ embedMorphism em inducedSign sigma2

{- here the empty mapping should be used, but it will be overwritten

by the first argument of composeM -}

else fatal_error

("No signature morphism for symbol map found.\n" ++

"The following mapped symbols are missing in the target signature:\n"

++ showDoc (diffSig diffExt inducedSign sigma2) "")

$ concatMapRange getRange $ Map.keys rmap

{-

Computing signature generated by a symbol set.

Algorithm adapted from Bartek Klin's algorithm for CATS.

Input: symbol set "Syms"

signature "Sigma"

Output: signature "Sigma1"<=Sigma.

1. get a set "Sigma_symbols" of symbols in Sigma.

2. if Syms is not a subset of Sigma_symbols, return error.

3. let Sigma1 be an empty signature.

4. for each symbol "Sym" in Syms do:

4.1. if Sym is a:

4.1.1. sort "S": add sort S to Sigma1.

4.1.2. total function "F" with profile "Fargs,Fres":

4.1.2.1. add all sorts from Fargs to Sigma1.

4.1.2.2. add sort Fres to Sigma1.

4.1.2.3. add F with the needed profile to Sigma1.

4.1.3. partial function: as in 4.1.2.

4.1.4. predicate: as in 4.1.2., except that Fres is omitted.

5. get a list "Sig_sub" of subsort relations in Sigma.

6. for each pair "S1,S2" in Sig_sub do:

6.1. if S1,S2 are sorts in Sigma1, add "S1,S2" to sort relations in

Sigma1.

7. return the inclusion of sigma1 into sigma.

-}

generatedSign :: m -> SymbolSet -> Sign f e -> Result (Morphism f e m)

generatedSign extEm sys sigma = let

symset = symsetOf sigma -- 1.

sigma1 = Set.fold revealSym sigma

{ sortSet = Set.empty

, opMap = Map.empty

, predMap = Map.empty } sys -- 4.

sigma2 = sigma1

{ sortRel = sortRel sigma `Rel.restrict` sortSet sigma1

, emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }

in if not $ Set.isSubsetOf sys symset -- 2.

then let diffsyms = sys Set.\\ symset in

fatal_error ("Revealing: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

else sigInclusion extEm sigma2 sigma -- 7.

revealSym :: Symbol -> Sign f e -> Sign f e

revealSym sy sigma1 = case symbType sy of

SortAsItemType -> -- 4.1.1.

sigma1 {sortSet = Set.insert (symName sy) $ sortSet sigma1}

OpAsItemType ot -> -- 4.1.2./4.1.3.

sigma1 { sortSet = foldr Set.insert (sortSet sigma1)

$ opRes ot : opArgs ot

, opMap = Rel.setInsert (symName sy) ot $ opMap sigma1 }

PredAsItemType pt -> -- 4.1.4.

sigma1 { sortSet = foldr Set.insert (sortSet sigma1) $ predArgs pt

, predMap = Rel.setInsert (symName sy) pt $ predMap sigma1 }

{-

Computing signature co-generated by a raw symbol set.

Algorithm adapted from Bartek Klin's algorithm for CATS.

Input: symbol set "Syms"

signature "Sigma"

Output: signature "Sigma1"<=Sigma.

1. get a set "Sigma_symbols" of symbols in Sigma.

2. if Syms is not a subset of Sigma_symbols, return error.

3. for each symbol "Sym" in Syms do:

3.1. if Sym is a:

3.1.1. sort "S":

3.1.1.1. Remove S from Sigma_symbols

3.1.1.2. For each function/predicate symbol in

Sigma_symbols, if its profile contains S

remove it from Sigma_symbols.

3.1.2. any other symbol: remove if from Sigma_symbols.

4. let Sigma1 be a signature generated by Sigma_symbols in Sigma.

5. return the inclusion of sigma1 into sigma.

-}

cogeneratedSign :: m -> SymbolSet -> Sign f e -> Result (Morphism f e m)

cogeneratedSign extEm symset sigma = let

symset0 = symsetOf sigma -- 1.

symset1 = Set.fold hideSym symset0 symset -- 3.

in if Set.isSubsetOf symset symset0 -- 2.

then generatedSign extEm symset1 sigma -- 4./5.

else let diffsyms = symset Set.\\ symset0 in

fatal_error ("Hiding: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

hideSym :: Symbol -> Set.Set Symbol -> Set.Set Symbol

hideSym sy symset1' = case symbType sy of

SortAsItemType -> -- 3.1.1.

Set.filter (not . profileContainsSort (symName sy) . symbType)

$ Set.delete sy symset1'

OpAsItemType _ -> -- 3.1.2

Set.delete sy symset1'

PredAsItemType _ -> -- 3.1.2

Set.delete sy symset1'

profileContainsSort :: SORT -> SymbType -> Bool

profileContainsSort s symbT = elem s $ case symbT of

OpAsItemType ot -> opRes ot : opArgs ot

PredAsItemType pt -> predArgs pt

SortAsItemType -> []

leCl :: Ord a => (a -> a -> Bool) -> Map.Map Id (Set.Set a)

-> Map.Map Id [Set.Set a]

leCl = Map.map . Rel.partSet

mkp :: Map.Map Id (Set.Set OpType) -> Map.Map Id (Set.Set OpType)

mkp = Map.map makePartial

finalUnion :: (e -> e -> e) -- ^ join signature extensions

-> Sign f e -> Sign f e -> Result (Sign f e)

finalUnion addSigExt s1 s2 =

let extP = Map.map (map $ \ s -> (s, [], False))

o1 = extP $ leCl (leqF s1) $ mkp $ opMap s1

o2 = extP $ leCl (leqF s2) $ mkp $ opMap s2

p1 = extP $ leCl (leqP s1) $ predMap s1

p2 = extP $ leCl (leqP s2) $ predMap s2

s3 = addSig addSigExt s1 s2

o3 = leCl (leqF s3) $ mkp $ opMap s3

p3 = leCl (leqP s3) $ predMap s3

d1 = Map.differenceWith (listOfSetDiff True) o1 o3

d2 = Map.union d1 $ Map.differenceWith (listOfSetDiff False) o2 o3

e1 = Map.differenceWith (listOfSetDiff True) p1 p3

e2 = Map.union e1 $ Map.differenceWith (listOfSetDiff False) p2 p3

prL (s, l, b) = fsep

$ text ("(" ++ (if b then "left" else "right")

++ " side of union)")

: map pretty l ++ [mapsto <+> pretty s]

prM str = ppMap ((text str <+>) . pretty)

(vcat . map prL) id vcat (\ v1 v2 -> sep [v1, v2])

in if Map.null d2 && Map.null e2 then return s3

else fail $ "illegal overload relation identifications for profiles of:\n"

++ show (prM "op" d2 $+$ prM "pred" e2)

listOfSetDiff :: Ord a => Bool -> [(Set.Set a, [Set.Set a], Bool)]

-> [Set.Set a] -> Maybe [(Set.Set a, [Set.Set a], Bool)]

listOfSetDiff b rl1 l2 = let

fst3 (s, _, _) = s

l1 = map fst3 rl1 in

(\ l3 -> if null l3 then Nothing else Just l3)

$ fst $ foldr

(\ s (l, r) ->

let sIn = Set.isSubsetOf s

(r1, r2) = partition sIn r in

case r1 of

[] -> case find sIn l2 of

Nothing -> error "CASL.finalUnion.listOfSetDiff1"

Just s2 -> (if elem s2 $ map fst3 l then l else

(s2, filter (`Set.isSubsetOf` s2) l1, b) : l, r)

[_] -> (l, r2)

_ -> error "CASL.finalUnion.listOfSetDiff2")

([], l2) l1