01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Till Mossakowski and Uni Bremen 2002-2003

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : hets@tzi.de

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski The symbol map analysis for the CASL logic.

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski Follows Sect. III:4.1 of the CASL Reference Manual.

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maedertodo:

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederremove identity subsort relations resulting from non-injective renaming

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder(or add them to ALL signatures)

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskioverloading stuff is missing (wait for Martin's implementation of leqF and leqP)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederintroduce symbol functor (additionally to signature symbol functor)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-}

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maedermodule CASL.SymbolMapAnalysis where

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport CASL.Sign

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.AS_Basic_CASL

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport CASL.Morphism

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport Common.Id

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport Common.Result

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport qualified Common.Lib.Map as Map

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set

90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maederimport qualified Common.Lib.Rel as Rel

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maederimport Common.PrettyPrint

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichimport Common.Lib.Pretty

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederimport Control.Monad

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichimport Data.Maybe

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder{-

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiinducedFromMorphism ::

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder RawSymbolMap -> Sign lid b s f e -> Result (Morphism lid b s f e)

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederHere is Bartek Klin's algorithm that has benn used for CATS.

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

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

8e80792f474d154ff11762fac081a422e34f1accChristian MaederInducing morphism from raw symbol map and signature

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederInput: raw symbol map "Rsm"

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder signature "Sigma1"

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederOutput: morphims "Mrph": Sigma1 -> "Sigma2".

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder//preparation

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

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

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder 2.1. if there is no symbol in Sigma1 matching Rsym1, return error.

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

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder 2.2.1. add a pair "Sym,Rsym2" to Ssm.

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder//computing the "sort part" of the morphism

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder3. let Sigma2 be an empty signature.

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.

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

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

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

9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder name other than that in Rsym2, return error.

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

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder 5.3.1. add sort from Rsym2 to Sigma2

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder6. for each sort symbol "S" in Sigma1

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 6.1. if S is not mapped by Mrph,

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 6.1.1. add sort S to Sigma2

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 6.1.2. add mapping from S to S to Mrph.

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder//computing the "function/predicate part" of the morphism

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

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder symbol

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 7.2. let "Fprof1" be the value of Fprof via Mrph

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

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder morphism)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski 7.3. if Rsym2 is not of appriopriate type, return error, otherwise

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let "F2" be the name of the symbol.

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

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

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder not equal, return error.

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

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder some name different than F2, return error.

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder 7.6. add an operation/predicate with name F2 and profile Fprof1 to

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder Sigma2. If it is a partial function and if in Sigma2 there

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

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder add it. Otherwise if it is a total function and if in Sigma2

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski there exists a partial function with the same name and profile,

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder add the total function removing the partial one.

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.7. add to Mrph a mapping from operation/predicate of name F1 and

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski profile Fprof to name F2.

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder that is not mapped by Mrph,

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder 8.1. as in 7.2

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder 8.2. as in 7.6, replacing F2 with F1.

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 8.3. as in 7.7, replacing F2 with F1.

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

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

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder 9.2. add sort relation "S3,S4" in Sigma2.

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder10. Compute transitive closure of subsorting relation in Sigma2.

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-}

26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederinducedFromMorphism :: (PrettyPrint e, PrettyPrint f) =>

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Ext f e m -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederinducedFromMorphism extEm rmap sigma = do

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- ??? Missing: check preservation of overloading relation

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- first check: do all source raw symbols match with source signature?

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let syms = symOf sigma

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder incorrectRsyms = Map.foldWithKey

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (\rsy _ -> if Set.any (matchesND rsy) syms

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder then id

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder else Set.insert rsy)

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Set.empty

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder rmap

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder matchesND rsy sy =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sy `matches` rsy &&

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder case rsy of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ASymbol _ -> True

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- unqualified raw symbols need some matching symbol

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- that is not directly mapped

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> Map.lookup (ASymbol sy) rmap == Nothing

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- ... if not, generate an error

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder when (not (Set.isEmpty incorrectRsyms))

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (pfatal_error

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ptext "the following symbols:"

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder <+> printText incorrectRsyms

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski $$ ptext "are already mapped directly or do not match with signature"

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder $$ printText sigma)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder nullPos)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- compute the sort map (as a Map)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sort_Map <- Set.fold

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (\s m -> do s' <- sortFun s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder m1 <- m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder return $ Map.insert s s' m1)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (return Map.empty) sortsSigma

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- compute the op map (as a Map)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder op_Map <- Map.foldWithKey (opFun sort_Map)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (return Map.empty) (opMap sigma)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- compute the pred map (as a Map)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder pred_Map <- Map.foldWithKey (predFun sort_Map)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (return Map.empty) (predMap sigma)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- compute target signature

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let sigma' =

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder sigma

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder {sortSet = Set.image (mapSort sort_Map) sortsSigma,

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder sortRel = Rel.transClosure $

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Rel.image (mapSort sort_Map) (sortRel sigma),

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski opMap = Map.foldWithKey (mapOps sort_Map op_Map)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Map.empty (opMap sigma),

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder assocOps = Map.foldWithKey (mapOps sort_Map op_Map)

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Map.empty (assocOps sigma),

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder predMap = Map.foldWithKey (mapPreds sort_Map pred_Map)

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Map.empty (predMap sigma),

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder varMap = Map.empty}

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -- return assembled morphism

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder return (Morphism { msource = sigma,

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder mtarget = sigma',

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder sort_map = sort_Map,

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder fun_map = op_Map,

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pred_map = pred_Map,

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder extended_map = extEm sigma sigma' })

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder where

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -- the sorts of the source signature

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder sortsSigma = sortSet sigma

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder -- sortFun is the sort map as a Haskell function

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder sortFun s =

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -- rsys contains the raw symbols to which s is mapped to

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder case Set.size rsys of

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder 0 -> return s -- use default = identity mapping

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder 1 -> return $ rawSymName $ Set.findMin rsys -- take the unique rsy

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski _ -> pplain_error s -- ambiguity! generate an error

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (ptext "Sort" <+> printText s

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> ptext "mapped ambiguously:" <+> printText rsys)

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder nullPos

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder where

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- get all raw symbols to which s is mapped to

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder rsys = Set.unions $ map (Set.maybeToSet . (\x -> Map.lookup x rmap))

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder [ASymbol $ idToSortSymbol s, AnID s, AKindedId SortKind s]

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- to a Fun_map, add evering resulting from mapping (id,ots) according to rmap

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder opFun :: Sort_map -> Id -> Set.Set OpType -> Result Fun_map -> Result Fun_map

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder opFun sort_Map ident ots m =

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- first consider all directly mapped profiles

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder let (ots1,m1) = Set.fold (directOpMap ident) (Set.empty,m) ots

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

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in case (Map.lookup (AKindedId FunKind ident) rmap,Map.lookup (AnID ident) rmap) of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (Just rsy1, Just rsy2) ->

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder do m' <- m

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder pplain_error m'

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (ptext "Operation" <+> printText ident

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <+> ptext "is mapped twice:"

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder <+> printText rsy1 <+> ptext "," <+> printText rsy2

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder )

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder nullPos

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (Just rsy, Nothing) ->

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder Set.fold (insertmapOpSym ident rsy) m1 ots1

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (Nothing, Just rsy) ->

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder Set.fold (insertmapOpSym ident rsy) m1 ots1

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder -- Anything not mapped explicitly is left unchanged

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (Nothing,Nothing) -> Set.fold (unchangedOpSym ident) m1 ots1

88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder where

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- try to map an operation symbol directly

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder -- collect all opTypes that cannot be mapped directly

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder directOpMap :: Id -> OpType -> (Set.Set OpType,Result Fun_map)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> (Set.Set OpType,Result Fun_map)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder directOpMap ident' ot (ots',m') =

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder case Map.lookup (ASymbol (idToOpSymbol ident' ot)) rmap of

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Just rsy ->

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (ots',insertmapOpSym ident' rsy ot m')

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder Nothing -> (Set.insert ot ots',m')

8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder -- map op symbol (ident,ot) to raw symbol rsy

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapOpSym :: Id -> OpType -> RawSymbol -> Result (Id,FunKind)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapOpSym ident ot rsy = case rsy of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ASymbol (Symbol ident' (OpAsItemType ot')) ->

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder if compatibleOpTypes (mapOpType sort_Map ot) ot'

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder then return (ident',opKind ot')

ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder else pplain_error (ident,opKind ot)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ptext "Operation symbol " <+> printText (idToOpSymbol ident ot)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> ptext "is mapped to type" <+> printText ot'

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> ptext "but should be mapped to type" <+>

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText (mapOpType sort_Map ot)

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder )

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder nullPos

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder AnID ident' -> return (ident',opKind ot)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder AKindedId FunKind ident' -> return (ident',opKind ot)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder rsy -> pplain_error (ident,opKind ot)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ptext "Operation symbol " <+> printText (idToOpSymbol ident ot)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder <+> ptext" is mapped to symbol of wrong kind:"

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder <+> printText rsy)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder nullPos

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- insert mapping of op symbol (ident,ot) to raw symbol rsy into m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder insertmapOpSym ident rsy ot m = do

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder m1 <- m

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (ident',kind') <- mapOpSym ident ot rsy

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder return (Map.insert (ident,ot) (ident',kind') m1)

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder -- insert mapping of op symbol (ident,ot) to itself into m

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder unchangedOpSym ident ot m = do

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder m1 <- m

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder return (Map.insert (ident,ot) (ident,opKind ot) m1)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- map the ops in the source signature

99476ac2689c74251219db4782e57fe713a24a52Christian Maeder mapOps sort_Map op_Map ident ots m =

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Set.fold mapOp m ots

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder where

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapOp ot m1 =

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let (ident',ot') = fromMaybe (ident,ot) $ mapOpSym sort_Map op_Map (ident,ot)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in Map.setInsert ident' ot' m1

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder -- to a Pred_map, add evering resulting from mapping (ident,pts) according to rmap

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski predFun :: Sort_map -> Id -> Set.Set PredType

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Result Pred_map -> Result Pred_map

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder predFun sort_Map ident pts m =

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -- first consider all directly mapped profiles

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let (pts1,m1) = Set.fold (directPredMap ident) (Set.empty,m) pts

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

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder in case (Map.lookup (AKindedId PredKind ident) rmap,Map.lookup (AnID ident) rmap) of

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (Just rsy1, Just rsy2) ->

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder do m' <- m

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pplain_error m'

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (ptext "Predicate" <+> printText ident

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder <+> ptext "is mapped twice:"

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <+> printText rsy1 <+> ptext "," <+> printText rsy2)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder nullPos

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (Just rsy, Nothing) ->

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.fold (insertmapPredSym ident rsy) m1 pts1

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (Nothing, Just rsy) ->

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Set.fold (insertmapPredSym ident rsy) m1 pts1

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder -- Anything not mapped explicitly is left unchanged

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (Nothing,Nothing) -> Set.fold (unchangedPredSym ident) m1 pts1

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder where

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -- try to map a predicate symbol directly

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -- collect all predTypes that cannot be mapped directly

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder directPredMap :: Id -> PredType -> (Set.Set PredType,Result Pred_map)

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -> (Set.Set PredType,Result Pred_map)

0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder directPredMap ident pt (pts,m) =

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case Map.lookup (ASymbol (idToPredSymbol ident pt)) rmap of

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Just rsy ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (pts,insertmapPredSym ident rsy pt m)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> (Set.insert pt pts,m)

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -- map pred symbol (ident,pt) to raw symbol rsy

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapPredSym :: Id -> PredType -> RawSymbol -> Result Id

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapPredSym ident pt rsy = case rsy of

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ASymbol (Symbol ident' (PredAsItemType pt')) ->

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if (mapPredType sort_Map pt) == pt'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder then return ident'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder else pplain_error ident

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (ptext "Predicate symbol " <+> printText (idToPredSymbol ident pt)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> ptext "is mapped to type" <+> printText pt'

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder <+> ptext "but should be mapped to type"

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder <+> printText (mapPredType sort_Map pt)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder )

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder nullPos

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder AnID ident' -> return ident'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder AKindedId PredKind ident' -> return ident'

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder rsy -> pplain_error ident

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (ptext "Predicate symbol" <+> printText (idToPredSymbol ident pt)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder <+> ptext "is mapped to symbol of wrong kind: "

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder <+> printText rsy

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder )

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder nullPos

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- insert mapping of pred symbol (ident,pt) to raw symbol rsy into m

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder insertmapPredSym ident rsy pt m = do

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder m1 <- m

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ident' <- mapPredSym ident pt rsy

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder return (Map.insert (ident,pt) ident' m1)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder -- insert mapping of pred symbol (ident,pt) to itself into m

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder unchangedPredSym ident pt m = do

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder m1 <- m

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder return (Map.insert (ident,pt) ident m1)

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- map the preds in the source signature

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder mapPreds sort_Map pred_Map ident pts m =

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Set.fold mapPred m pts

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder where

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder mapPred pt m1 =

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder let (ident',pt') = fromMaybe (ident,pt) $ mapPredSym sort_Map pred_Map (ident,pt)

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder in Map.setInsert ident' pt' m1

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder

aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder{-

aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederinducedFromToMorphism ::

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

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder

b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till MossakowskiAlgorithm adapted from Bartek Klin's algorithm for CATS.

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederInducing morphisms from raw symbol map and source and target signature.

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder

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

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederThis means that we have exponential runtime in the worst case.

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

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederusing some basic principles of constraint programming.

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederWe use a depth-first search with some weak form of constraint

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maederpropagation and MRV (minimum remaining values), see

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederStuart Russell and Peter Norvig:

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederArtificial Intelligence - A Modern Approach.

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederPrentice Hall International

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederThe algorithm has additionally to take care of default values (i.e.

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedersymbol names are mapped identically be default, and the number of

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maederidentitically mapped names should be maximized). Moreover, it does

44d2a211a352759ee988ed8353026f5fa9511209Christian Maedernot suffice to find just one solution, but also its uniqueness

44d2a211a352759ee988ed8353026f5fa9511209Christian Maeder(among those maximizing he number of identitically mapped names)

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maedermust be checked (still, MRV is useful here).

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

4fc727afa544a757d1959ce77c02208f8bf330dcChristian MaederThe algorithm

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederInput: raw symbol map "rmap"

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder signatures "sigma1,sigma2"

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederOutput: morphism "mor": sigma1 -> sigma2

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

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

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder1.1. if target mor1 is a subsignature of sigma2, return the composition

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder of this inclusion with mor1

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

4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder2. let "posmap" be a map, mapping each symbol "sym1" from sigma1 to a pair

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder of sets of symbols (symset1, symset2) from sigma2 such that sym1

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder can be mapped to each sym2 in symset1 union symset2 (i.e., they are

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder both sorts or operations/predicates of the same arity, and

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder moreover, if there is a pair (rsym1,rsym2) in rmap such that sym1

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder matches rsym1, thenrsym2 must match rsym2). Moreover, symset1

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder contains only symbols with names different form that of sym1,

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder whereas symset2 contains only symbols with names different from

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder that of sym1.

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder3. let "akmap" (from Actually Known Map) be an empty symbol map.

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder//DEPTH-FIRST MRV SEARCH

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder//recursively called procedure, returning a symbol map or a special

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder//"No_map" value. Parameters are: sigma1, sigma2, akmap, posmap.

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaederGET MRV (minimun remaining values) "VARIABLE"

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski4a. if posmap is empty

74d9a385499bf903b24848dff450a153f525bda7Christian Maeder 4a.1. check if akmap defines a mapping from every symbol in target mor1.

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (this should be vacuously true - Bartek?)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder 4a.2. if yes, return akmap, otherwise return "No_map".

88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder4b. take a pair sym1 |-> (symset1,symset2) with MRV from posmap

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (i.e. one with minimal cardinality of symset1 union symset2).

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder But: prefer those with non-empty symset1!

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Remove it from posmap.

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (For efficiency reasons, we also carry around an indexing of posmap

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski according to the cardinalities. Hence, posmap really is a pair

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (posmap1,posmap2).)

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski5. for each symbol "sym2" from symset1

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder CONSISTENCY CHECK

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder 5.1. check if mapping sym1 to sym2 clashes with akmap

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (it can clash if sym1 and sym2 are operations/predicates,

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski and mapping on their profiles clashes with what is already

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder known in akmap)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.2. if yes, proceed with the next sym2 in step 5.

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.3. add mapping of sym1 to sym2 to akmap.

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder CONSTRAINT PROPAGATION (forward checking)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.4. if sym1 and sym2 are sorts

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.5. for each sub/supersort s of sym1, restrict the possible

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder mappings of s in posmap to sub/supersorts of sym2

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.6. for each operation/predicate f in dom(posmap) involving

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder sym1 in its argument or result sorts, restrict the

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder possible mappings of f in posmap accordingly

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder (5.6. can be omitted for the sake of simplicity,

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder since 5.1. does the necessary check as well)

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.7. if sym1 and sym2 are operations/predicates,

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.8. For corresponding sorts in their profiles,

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder remove incompatible mappings of the sorts from posmap

22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder 5.9. For each sym in overloading relation with sym1,

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder remove incompatible mappings of sym from posmap

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder CONTINUE DEPTH FIRST SERACH

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder 5.10. call recursively point 4.

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder6. if for exactly one sym2 step 5 gave a map, return this map.

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder7. if step 5 gave more than one map, raise an exception. Morphism is not unique.

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder8. (only) if for no sym2 step 5 gave a map,

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder repeat steps 5-7 with symset2 instead of symset1

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder if this does not give a map either, return "No_map".

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder//end of the recursive procedure

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder9. if procedure returned "No_map" or raised an exception, return error

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder10. otherwise, return computed morphism from target mor1 to sigma2

ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder composed with mor1.

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder-}

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski-- Some auxiliary functions for inducedFromToMorphism

329d1810c6d5a5a0827e1d07503d94431578d176Christian MaedertestMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool

329d1810c6d5a5a0827e1d07503d94431578d176Christian MaedertestMatch rmap sym1 sym2 =

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder Map.foldWithKey match1 True rmap

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder where

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder match1 rsy1 rsy2 b = b && ((sym1 `matches` rsy1) <= (sym2 `matches`rsy2))

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder

5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian MaedercanBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedercanBeMapped rmap sym1@(Symbol {symbType = SortAsItemType})

d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder sym2@(Symbol {symbType = SortAsItemType}) =

329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder testMatch rmap sym1 sym2

5e46b572ed576c0494768998b043d9d340594122Till MossakowskicanBeMapped rmap sym1@(Symbol {symbType = OpAsItemType ot1})

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sym2@(Symbol {symbType = OpAsItemType ot2}) =

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder length (opArgs ot1) == length (opArgs ot2) && -- same arity

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder opKind ot1 >= opKind ot2 && -- preservation of totality

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder testMatch rmap sym1 sym2

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedercanBeMapped rmap sym1@(Symbol {symbType = PredAsItemType pt1})

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder sym2@(Symbol {symbType = PredAsItemType pt2}) =

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder length (predArgs pt1) == length (predArgs pt2) && -- same arity

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder testMatch rmap sym1 sym2

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedercanBeMapped _ _ _ = False

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaederpreservesName :: Symbol -> Symbol -> Bool

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaederpreservesName sym1 sym2 = symName sym1 == symName sym2

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian MaedercompatibleSorts :: SymbolMap -> (SORT, SORT) -> Bool

86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian MaedercompatibleSorts smap (s1,s2) =

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case Map.lookup (idToSortSymbol s1) smap of

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder Nothing -> True

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Just sym -> symName sym == s2

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder-- try to extend a symbol map with a yet unmapped symbol

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder-- (this can fail if sym1 and sym2 are operations/predicates,

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder-- and mapping on their profiles clashes with what is already

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder-- known in akmap)

27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian MaederextendSymbMap :: SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiextendSymbMap akmap sym1 sym2 =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder if case symbType sym1 of

32562a567baac248a00782d2727716c13117dc4aChristian Maeder SortAsItemType -> True

32562a567baac248a00782d2727716c13117dc4aChristian Maeder OpAsItemType ot1 -> case symbType sym2 of

32562a567baac248a00782d2727716c13117dc4aChristian Maeder OpAsItemType ot2 -> all (compatibleSorts akmap)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder $ zip (opRes ot1:opArgs ot1) (opRes ot2:opArgs ot2)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder _ -> False

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder PredAsItemType pt1 -> case symbType sym2 of

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder PredAsItemType pt2 -> all (compatibleSorts akmap)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder $ zip (predArgs pt1) (predArgs pt2)

32562a567baac248a00782d2727716c13117dc4aChristian Maeder _ -> False

32562a567baac248a00782d2727716c13117dc4aChristian Maeder then Just $ Map.insert sym1 sym2 akmap

32562a567baac248a00782d2727716c13117dc4aChristian Maeder else Nothing

32562a567baac248a00782d2727716c13117dc4aChristian Maeder

32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- Type for posmap

746440cc1b984a852f5864235b8fa3930963a081Christian Maeder-- Each symbol is mapped to the set symbols it possibly can be mapped to

32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- Additionally, we store a flag meaning "no default map" and the

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- cardinality of the symobl set

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- For efficiency reasons, we also carry around an indexing of posmap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- according to the pairs (flag,cardinality). Since several symbols

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- may lead to the same pair, we have to associate a list of symbols

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder-- (and corresponding symbol sets) with each pair.

e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder-- Hence, PosMap really is a pair to two maps.

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maedertype PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder Map.Map (Bool,Int) [(Symbol,SymbolSet)])

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- Some basic operations on PosMap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder-- postpone entries with no default mapping and size > 1

4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian MaederpostponeEntry :: Symbol -> SymbolSet -> Bool

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederpostponeEntry sym symset =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (not $ Set.any (preservesName sym) symset) && Set.size symset > 1

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederremoveFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederremoveFromPosmap sym card (posmap1,posmap2) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (Map.delete sym posmap1,

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Map.update removeSym1 card posmap2)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder where

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder removeSym [] = []

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder removeSym ((x,y):l) = if x==sym then l else (x,y):removeSym l

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder removeSym1 l = case removeSym l of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder [] -> Nothing

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder l1 -> Just l1

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederaddToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederaddToPosmap sym symset (posmap1,posmap2) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (Map.insert sym (symset,card) posmap1,

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Map.listInsert card (sym,symset) posmap2)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder where card = (postponeEntry sym symset,Set.size symset)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- restrict posmap such that each symbol from symset1 is only mapped

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- to symbols from symset2

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaederrestrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederrestrictPosMap symset1 symset2 posmap =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Set.fold restrictPosMap1 posmap symset1

6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder where

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder restrictPosMap1 sym1 posmap@(posmap1,posmap2) =

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder case Map.lookup sym1 posmap1 of

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> posmap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Just (symset1,card) ->

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder addToPosmap sym1 (symset1 `Set.intersection` symset2)

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder $ removeFromPosmap sym1 card posmap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder-- for each sub/supersort s of sym1 in sigma1, restrict the possible

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder-- mappings of s in posmap to sub/supersorts of sym2 in sigma2

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederrestrictSorts ::

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Symbol -> Symbol -> Sign f e -> Sign f e -> PosMap -> PosMap

d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederrestrictSorts sym1 sym2 sigma1 sigma2 posmap =

32562a567baac248a00782d2727716c13117dc4aChristian Maeder restrictPosMap subsyms1 subsyms2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder $ restrictPosMap supersyms1 supersyms2 posmap

32562a567baac248a00782d2727716c13117dc4aChristian Maeder where

32562a567baac248a00782d2727716c13117dc4aChristian Maeder s1 = symName sym1

32562a567baac248a00782d2727716c13117dc4aChristian Maeder s2 = symName sym2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder sub1 = subsortsOf s1 sigma1

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder sub2 = subsortsOf s2 sigma2

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder subsyms1 = Set.image idToSortSymbol sub1

32562a567baac248a00782d2727716c13117dc4aChristian Maeder subsyms2 = Set.image idToSortSymbol sub2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder super1 = supersortsOf s1 sigma1

32562a567baac248a00782d2727716c13117dc4aChristian Maeder super2 = supersortsOf s2 sigma2

32562a567baac248a00782d2727716c13117dc4aChristian Maeder supersyms1 = Set.image idToSortSymbol super1

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski supersyms2 = Set.image idToSortSymbol super2

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till Mossakowski

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- remove all sort mappings that map s1 to a sort different from s2

2766ec926fcf3faf72248b10c3305b715b8c3249Christian MaederremoveIncompatibleSortMaps :: Maybe PosMap -> (SORT,SORT) -> Maybe PosMap

2766ec926fcf3faf72248b10c3305b715b8c3249Christian MaederremoveIncompatibleSortMaps Nothing _ = Nothing

3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiremoveIncompatibleSortMaps (Just posmap@(posmap1,posmap2)) (s1,s2) =

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder case Map.lookup sym1 posmap1 of

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Nothing -> Just posmap

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder Just (symset,card) ->

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder -- is there some remaining possibility to map the sort?

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski if sym2 `Set.member` symset

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder then Just $ addToPosmap sym1 (Set.single sym2)

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder $ removeFromPosmap sym1 card posmap

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder -- if not, there is no map!

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder else Nothing

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder where

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder sym1 = idToSortSymbol s1

2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder sym2 = idToSortSymbol s2

ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till Mossakowski

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- For corresponding sorts in profiles of sym1 and sym2,

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang-- remove incompatible mappings of the sorts from posmap

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun WangrestrictOps :: Symbol -> Symbol -> PosMap -> Maybe PosMap

aea143fff7a50aceb809845fbc42698b0b3f545aChristian MaederrestrictOps sym1 sym2 posmap =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl removeIncompatibleSortMaps (Just posmap) $ zip sort1 sorts2

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder where

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder (sort1,sorts2) = case (symbType sym1,symbType sym2) of

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (OpAsItemType ot1,OpAsItemType ot2) ->

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (opRes ot1:opArgs ot1,opRes ot2:opArgs ot2)

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (PredAsItemType pt1,PredAsItemType pt2) ->

9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (predArgs pt1,predArgs pt2)

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder _ -> ([],[])

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder-- the main function

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederinducedFromToMorphism :: (PrettyPrint f, PrettyPrint e) =>

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder Ext f e m -> RawSymbolMap -> Sign f e -> Sign f e

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -> Result (Morphism f e m)

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian MaederinducedFromToMorphism extEm rmap sigma1 sigma2 = do

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -- 1. use rmap to get a renaming...

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder mor1 <- inducedFromMorphism extEm rmap sigma1

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

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder if isSubSig (mtarget mor1) sigma2

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -- yes => we are done

40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder then return (mor1 {mtarget = sigma2})

d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder -- no => OK, we've to take the hard way

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder else do -- 2. Compute initial posmap, using all possible mappings of symbols

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder let symset1 = symOf sigma1

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder symset2 = symOf sigma2

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang addCard sym s = (s,(postponeEntry sym s,Set.size s))

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ins1 sym = Map.insert sym

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang (addCard sym $ Set.filter (canBeMapped rmap sym) symset2)

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang posmap1 = Set.fold ins1 Map.empty symset1

ins2 sym1a (symset,card) = Map.listInsert card (sym1a,symset)

posmap2 = Map.foldWithKey ins2 Map.empty posmap1

posmap = (posmap1,posmap2)

-- Are there symbols that cannot be mapped at all?

-- Then generate an error immediately

--trace ("posmap1= "++showPretty posmap1 "") (return ())

case Map.lookup (True,0) posmap2 of

Nothing -> return ()

Just syms -> pfatal_error

(ptext "No symbol mapping for "

<+> printText (Set.fromList $ map fst syms)) nullPos

-- 3. call recursive function with empty akmap and initial posmap

smap <- tryToInduce sigma1 sigma2 Map.empty posmap

smap1 <- case smap of

Nothing -> fail "No signature morphism for symbol map\n(try with option -v3 to get some hints)"

Just x -> return x

-- 9./10. compute and return the resulting morphism

symbMapToMorphism extEm sigma1 sigma2 smap1

where

-- 4. recursive depth first function

-- ambiguous map leads to fatal error (similar to exception)

tryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do

--trace("akmap: "++showPretty akmap "") (return ())

if Map.isEmpty posmap2 then return $ Just akmap -- 4a.

else do

--trace ("trying to map: "++showPretty sym1 "") (return ())

(akmap1,stopBT,immF) <-

tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1

(akmap2,stopBT2,immF2) <-

if isNothing akmap1 && not stopBT

-- 6. no map for symset1, hence try symset2

then tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2

else return (akmap1,stopBT,immF) -- otherwise, use symset1 only

when ((akmap2,stopBT2)==(Nothing,False) && immF)

(phint () (ptext "Possibly no mapping for "<+>printText sym1) nullPos)

return akmap2

where

-- 4b. take symbol with minimal remaining values (MRV)

(card,(sym1,symset):symsets) = Map.findMin posmap2

(symset1,symset2) = Set.partition (preservesName sym1) symset

posmap' = removeFromPosmap sym1 card (posmap1,posmap2)

-- 5. to 7.

tryToInduce1 sigma1 sigma2 akmap posmap sym1 symset = do

Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)

(return (Nothing,False,False)) symset

tryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do

-- 5.1. to 5.3. consistency check

(akmapSoFar1,stopBackTrack,_) <- akmapSoFar

--(trace ("map "++(case akmapSoFar1 of

-- Just x -> showPretty x " + "

-- Nothing -> "")

-- ++showPretty sym1 " |-> " ++showPretty sym2 "; stopBackTrack: "++show stopBackTrack) (return ()))

(akmap',stopBackTrack',immediateFailure) <-

case extendSymbMap akmap sym1 sym2 of

Nothing -> return (Nothing,stopBackTrack,True)

-- constraint propagation

Just akmap1 -> do

let posmap1 = case symbType sym1 of

-- 5.4./5.5. constraint propagation for a sort symbol

SortAsItemType ->

Just $ restrictSorts sym1 sym2 sigma1 sigma2 posmap

-- 5.6. omitted so far (not really necessary)

-- 5.7./5.8. constraint propagation

-- for an operation/predicate symbol

_ -> restrictOps sym1 sym2 posmap

-- 5.9. omitted until overload relation will be available !!!???

noNewSortMaps = posmap1==Just posmap

-- 5.10.

-- case posmap1 of

-- Just x -> trace ("posmap1: Something") (return ())

-- Nothing -> trace ("posmap1: Nothing") (return ())

case (posmap1,noNewSortMaps&&stopBackTrack) of

(Just posmap2,False) -> do

pm <- tryToInduce sigma1 sigma2 akmap1 posmap2

return (pm,noNewSortMaps,False)

-- if there is no posmap left, or

-- if there are no new sort maps and a similar tree already

-- has been searched (stopBackTrack), stop searching here

-- and keep the old stopBackTrack flag

_ -> return (Nothing,stopBackTrack,True)

-- 6./7. uniqueness check

case (akmap',akmapSoFar1) of

-- stop backtracking next time if there haven't been new sort maps

(Nothing,Nothing) -> return (Nothing,stopBackTrack',immediateFailure)

(Just smap,Nothing) -> return (Just smap,stopBackTrack',immediateFailure)

(Nothing,Just smap) -> return (Just smap,stopBackTrack',immediateFailure)

(Just smap1,Just smap2) ->

fail $ shows

(ptext "Ambiguous symbol map" $$

ptext "Map1" <+> printText smap1 $$

ptext "Map2" <+> printText smap2)

""

{-

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 :: Ext f e m -> SymbolSet -> Sign f e -> Result (Morphism f e m)

generatedSign extEm sys sigma = do

if not (sys `Set.subset` symset) -- 2.

then pfatal_error

(ptext "Revealing: The following symbols"

<+> printText(sys Set.\\ symset)

<+> ptext "are not in the signature") nullPos

else return $ embedMorphism extEm sigma2 sigma -- 7.

where

symset = symOf sigma -- 1.

sigma1 = Set.fold revealSym (sigma { sortSet = Set.empty

, opMap = Map.empty

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

revealSym sy sigma1 = case symbType sy of -- 4.1.

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 = Map.setInsert (symName sy) ot $ opMap sigma1}

PredAsItemType pt -> -- 4.1.4.

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

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

sigma2 = sigma1 {sortRel = sortRel sigma `Rel.restrict` sortSet sigma1} -- 5./6.

{-

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 :: Ext f e m -> SymbolSet -> Sign f e

-> Result (Morphism f e m)

cogeneratedSign extEm symset sigma = do

if not (symset `Set.subset` symset0) -- 2.

then pfatal_error

(ptext "Hiding: The following symbols"

<+> printText(symset Set.\\ symset0)

<+> ptext "are not in the signature") nullPos

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

where

symset0 = symOf sigma -- 1.

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

revealSym sy symset1 = case symbType sy of -- 3.1.

SortAsItemType -> -- 3.1.1.

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

$ Set.delete sy symset1

OpAsItemType _ -> -- 3.1.2

Set.delete sy symset1

PredAsItemType _ -> -- 3.1.2

Set.delete sy symset1

profileContains _ SortAsItemType = False

profileContains s (OpAsItemType ot) = s `elem` (opRes ot:opArgs ot)

profileContains s (PredAsItemType pt) = s `elem` (predArgs pt)

finalUnion ::

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

finalUnion sigma1 sigma2 = return $ addSig sigma1 sigma2

-- ??? Finality check not yet implemented