54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : symbol map analysis for the CASL logic.

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder

cfbd735270fe52115cef0508d265785efcb99cd7Christian MaederMaintainer : Christian.Maeder@dfki.de

120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederStability : provisional

120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederPortability : portable

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiSymbol map analysis for the CASL logic.

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

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder-}

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maedermodule CASL.SymbolMapAnalysis

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ( inducedFromMorphism

2ed75b9c0aced535e9bc446cd294fd0f530e7fe0Christian Maeder , inducedFromToMorphism

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder , cogeneratedSign

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder , generatedSign

c208973c890b8f993297720fd0247bc7481d4304Christian Maeder , finalUnion

55c5e901b5c3466300009135585bc70bd576dcb6Christian Maeder ) where

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport CASL.Sign

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maederimport CASL.AS_Basic_CASL

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maederimport CASL.Morphism

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maeder

54ea981a0503c396c2923a1c06421c6235baf27fChristian Maederimport qualified Data.Map as Map

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maederimport qualified Data.Set as Set

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maederimport qualified Common.Lib.Rel as Rel

a1c6679d00e15a949730ab640159e0adc5b0e3e7Christian Maederimport Common.Doc

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Common.DocUtils

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maederimport Common.Id

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maederimport Common.Result

cfbe82ead3f3127387072a21cc151e39f4fa51c6Christian Maeder

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder{-

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian MaederinducedFromMorphism :: RawSymbolMap -> sign -> Result morphism

54a0a1e10bd93721cf52dbd9b816c8f108997ec0Christian Maeder

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

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

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian MaederInducing morphism from raw symbol map and signature

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian MaederInput: raw symbol map "Rsm"

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder signature "Sigma1"

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian MaederOutput: morphims "Mrph": Sigma1 -> "Sigma2".

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder

cd9ca21a6446db25db7dca76a01c14231d4d48d5Cui Jian//preparation

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

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

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

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

94d9a4cf9aca9662f2a35f1d53170e86739baf24Cui Jian 2.2.1. add a pair "Sym,Rsym2" to Ssm.

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder//computing the "sort part" of the morphism

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder3. let Sigma2 be an empty signature.

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.

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

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

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

0d0278c34a374b29c2d6c58b39b8b56e283d48e8Christian Maeder name other than that in Rsym2, return error.

94d9a4cf9aca9662f2a35f1d53170e86739baf24Cui Jian 5.3. if in Mrph there is no mappinh of sort in Sym

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder 5.3.1. add sort from Rsym2 to Sigma2

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder6. for each sort symbol "S" in Sigma1

544b866d340cdef36332f59ecd899daa1807f6c7Cui Jian 6.1. if S is not mapped by Mrph,

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder 6.1.1. add sort S to Sigma2

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder 6.1.2. add mapping from S to S to Mrph.

da955132262baab309a50fdffe228c9efe68251dCui Jian//computing the "function/predicate part" of the morphism

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

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder symbol

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder 7.2. let "Fprof1" be the value of Fprof via Mrph

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

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder morphism)

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder 7.3. if Rsym2 is not of appriopriate type, return error, otherwise

2c81e2bd9f9dee247c74a642c03620a2f799d0a4Razvan Pascanu let "F2" be the name of the symbol.

31009d997a07e58087aa8acb84bc6ac90cb82942Till Mossakowski 7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not

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

6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder not equal, return error.

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

5129a6bc64bcdb44aa111adb7bd2d0683f452b7aChristian Maeder some name different than F2, return error.

c458c6f5a2ce173d8af7a7f5cb434813eb870937Jorina Freya Gerken 7.6. add an operation/predicate with name F2 and profile Fprof1 to

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder Sigma2. If it is a partial function and if in Sigma2 there

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

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder add it. Otherwise if it is a total function and if in Sigma2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder there exists a partial function with the same name and profile,

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder add the total function removing the partial one.

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder profile Fprof to name F2.

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder that is not mapped by Mrph,

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maeder 8.1. as in 7.2

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maeder 8.2. as in 7.6, replacing F2 with F1.

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder 8.3. as in 7.7, replacing F2 with F1.

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

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

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maeder 9.2. add sort relation "S3,S4" in Sigma2.

2ed75b9c0aced535e9bc446cd294fd0f530e7fe0Christian Maeder10. Compute transitive closure of subsorting relation in Sigma2.

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maeder-}

10e12ec6ab28a40706609341c727422a0cd8d34dChristian Maeder

31009d997a07e58087aa8acb84bc6ac90cb82942Till MossakowskiinducedFromMorphism :: (Pretty e, Pretty f) =>

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

120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaederinducedFromMorphism extEm rmap sigma = do

e953bea49e7f0e1a43bccf2a66c5e2a2b50848e0Christian Maeder -- ??? Missing: check preservation of overloading relation

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder -- first check: do all source raw symbols match with source signature?

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder let syms = symOf sigma

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder sortsSigma = sortSet sigma

31009d997a07e58087aa8acb84bc6ac90cb82942Till Mossakowski incorrectRsyms = Map.foldWithKey

b73d620aafdd5aef1d6dfbc5adc2060aa38818a9Christian Maeder (\rsy _ -> if any (matchesND rsy) $ Set.toList syms

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder then id

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder else Set.insert rsy)

edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian Set.empty

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder rmap

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder matchesND rsy sy =

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder sy `matches` rsy &&

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder case rsy of

62e5d73e5f0b5b4df9999aa4e523ed8f54cc24a6Christian Maeder ASymbol _ -> True

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder -- unqualified raw symbols need some matching symbol

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- that is not directly mapped

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

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- ... if not, generate an error

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder if Set.null incorrectRsyms then return () else fatal_error

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder ("the following symbols: "

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder ++ showDoc incorrectRsyms

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maeder "\nare already mapped directly or do not match with signature\n"

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maeder ++ showDoc sigma "")

6948b7295a0521212803f15cf919395d2073e2c9Christian Maeder $ getSetRange incorrectRsyms

b73d620aafdd5aef1d6dfbc5adc2060aa38818a9Christian Maeder

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- compute the sort map (as a Map)

96caff87d2db43ba90e69e5ac3adb24c9f88b3deChristian Maeder sort_Map <- Set.fold

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (\s m -> do s' <- sortFun rmap s

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maeder if s' == s then m else do

0ac3f139c8a076e5e517f79dbe67b579971d0eeaChristian Maeder m1 <- m

b2e92fd7a332d07a52e0284ea7a40618e0ff5656Christian Maeder return $ Map.insert s s' m1)

96caff87d2db43ba90e69e5ac3adb24c9f88b3deChristian Maeder (return Map.empty) sortsSigma

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder -- compute the op map (as a Map)

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder op_Map <- Map.foldWithKey (opFun rmap sort_Map)

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder (return Map.empty) (opMap sigma)

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

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder pred_Map <- Map.foldWithKey (predFun rmap sort_Map)

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

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder -- compute target signature

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder let sigma' =

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder sigma

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder {sortSet = Set.map (mapSort sort_Map) sortsSigma,

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder sortRel = Rel.transClosure $ Rel.irreflex $

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder Rel.map (mapSort sort_Map) (sortRel sigma),

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder opMap = Map.foldWithKey (mapOps sort_Map op_Map)

31009d997a07e58087aa8acb84bc6ac90cb82942Till Mossakowski Map.empty (opMap sigma),

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder assocOps = Map.foldWithKey (mapOps sort_Map op_Map)

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder Map.empty (assocOps sigma),

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder predMap = Map.foldWithKey (mapPreds sort_Map pred_Map)

f5002b03ad30aeef45e2c2254dd2ede20efbaa5eTill Mossakowski Map.empty (predMap sigma),

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder varMap = Map.empty}

cfbe82ead3f3127387072a21cc151e39f4fa51c6Christian Maeder -- return assembled morphism

cfbe82ead3f3127387072a21cc151e39f4fa51c6Christian Maeder return (embedMorphism extEm sigma sigma')

cfbe82ead3f3127387072a21cc151e39f4fa51c6Christian Maeder { sort_map = sort_Map

be5ff99194b2ba0a1a35093e0ea21d4da332b526Christian Maeder , fun_map = op_Map

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder , pred_map = pred_Map }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder -- the sorts of the source signature

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

cfbe82ead3f3127387072a21cc151e39f4fa51c6Christian MaedersortFun :: RawSymbolMap -> Id -> Result Id

120eec9ff1748e1ae786e2ab073234198bc0f701Christian MaedersortFun rmap s =

31009d997a07e58087aa8acb84bc6ac90cb82942Till Mossakowski -- rsys contains the raw symbols to which s is mapped to

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder if Set.null rsys then return s -- use default = identity mapping

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder else if Set.null $ Set.deleteMin rsys then

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder return $ rawSymName $ Set.findMin rsys -- take the unique rsy

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder else plain_error s -- ambiguity! generate an error

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder ("Sort " ++ showId s

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder " is mapped ambiguously: " ++ showDoc rsys "")

be5ff99194b2ba0a1a35093e0ea21d4da332b526Christian Maeder $ getSetRange rsys

eebfd27d0164fc09ff3ad8e178cc3614975ca5f1Christian Maeder where

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder -- get all raw symbols to which s is mapped to

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder rsys = Set.unions $ map ( \ x -> case Map.lookup x rmap of

31009d997a07e58087aa8acb84bc6ac90cb82942Till Mossakowski Nothing -> Set.empty

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski Just r -> Set.singleton r)

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski [ASymbol $ idToSortSymbol s, AnID s, AKindedId SortKind s]

57d320fc4d0fe1a1c08cfe6cd9ebec09b86c2cbfTill Mossakowski

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder {- to a Fun_map, add everything resulting from mapping (id, ots)

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder according to rmap -}

3fe83d4c932a8266edcf0304a97814c59821d91fChristian MaederopFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

f1b1b26670c370355bc36a27c99ed974ab223537Christian Maeder -> Result Fun_map -> Result Fun_map

f1b1b26670c370355bc36a27c99ed974ab223537Christian MaederopFun rmap sort_Map ide ots m =

3fe83d4c932a8266edcf0304a97814c59821d91fChristian Maeder -- first consider all directly mapped profiles

120eec9ff1748e1ae786e2ab073234198bc0f701Christian Maeder let (ots1,m1) = Set.fold (directOpMap rmap sort_Map ide) (Set.empty,m) ots

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

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder in case (Map.lookup (AKindedId FunKind ide) rmap,

fb88eac77c89b668f5c306173a6fbe2d513e4bccMarkus Gross Map.lookup (AnID ide) rmap) of

9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder (Just rsy1, Just rsy2) ->

9192fdd8f0e682ac0f0183dd854d5210fbfa4ec5Christian Maeder do m' <- m

fb88eac77c89b668f5c306173a6fbe2d513e4bccMarkus Gross plain_error m'

d24317c8197e565e60c8f41309de246249c1e57eChristian Maeder ("Operation " ++ showId ide

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder " is mapped twice: "

f45fad43ee1673ab280fbc700821d5d20a493eaaChristian Maeder ++ showDoc (rsy1, rsy2) "")

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder $ appRange (getRange rsy1) $ getRange rsy2

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder (Just rsy, Nothing) ->

b03274844ecd270f9e9331f51cc4236a33e2e671Christian Maeder Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder (Nothing, Just rsy) ->

edd35c6c970fa1707dc6ad7a3ba26119e0046223Cui Jian Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1

0ea3fd177b4e67c85346500a53cebe2f9fae4cb8Christian Maeder -- Anything not mapped explicitly is left unchanged

0ea3fd177b4e67c85346500a53cebe2f9fae4cb8Christian Maeder (Nothing,Nothing) -> m1

e89d9f79e335f5051eb8d8d913b0b2c716d4e57aChristian Maeder

e89d9f79e335f5051eb8d8d913b0b2c716d4e57aChristian Maeder -- try to map an operation symbol directly

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

e89d9f79e335f5051eb8d8d913b0b2c716d4e57aChristian MaederdirectOpMap :: RawSymbolMap -> Sort_map -> Id -> OpType

4b136ad539bd9f4e115dff4eee4d552a42d4437eChristian Maeder -> (Set.Set OpType,Result Fun_map)

709653bffee501341e2fdc55b9223e4921047c65Till Mossakowski -> (Set.Set OpType,Result Fun_map)

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian MaederdirectOpMap rmap sort_Map ide' ot (ots',m') =

e89d9f79e335f5051eb8d8d913b0b2c716d4e57aChristian Maeder case Map.lookup (ASymbol (idToOpSymbol ide' ot)) rmap of

95a43f69d0da78c0cb804b6ea6c907d6e831a203Christian Maeder Just rsy ->

b73d620aafdd5aef1d6dfbc5adc2060aa38818a9Christian Maeder (ots',insertmapOpSym sort_Map ide' rsy ot m')

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

e89d9f79e335f5051eb8d8d913b0b2c716d4e57aChristian Maeder

def1779795c7ca2a1ae420e43e90cbd66c438faaTill Mossakowski -- map op symbol (ide,ot) to raw symbol rsy

afddef51d985ac2ea76a6bd846f04cbbc4311305Razvan PascanumappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id,FunKind)

b1789f0752d87f0f0dac2b2427794d18d2a21b41Christian MaedermappedOpSym sort_Map ide ot rsy =

f4ae50539e67874b6162f8334f6782a0d66acefaCui Jian let opSym = "Operation symbol " ++ showDoc (idToOpSymbol ide ot)

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder " is mapped to "

b73d620aafdd5aef1d6dfbc5adc2060aa38818a9Christian Maeder in case rsy of

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder ASymbol (Symbol ide' (OpAsItemType ot')) ->

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder if compatibleOpTypes (mapOpType sort_Map ot) ot'

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

e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder else plain_error (ide, opKind ot)

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

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder " but should be mapped to type " ++

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder showDoc (mapOpType sort_Map ot)"") $ getRange rsy

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder AnID ide' -> return (ide',opKind ot)

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder AKindedId FunKind ide' -> return (ide',opKind ot)

95cb954c00f873306bf1a60b62d3209d3cff4102Christian Maeder _ -> plain_error (ide,opKind ot)

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

e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder $ getRange rsy

e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder

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

e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian MaederinsertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType

e1c24b1dbf5cb1c9bb22b14a40167a4ba7806501Christian Maeder -> Result Fun_map -> Result Fun_map

insertmapOpSym sort_Map ide rsy ot m = do

m1 <- m

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

return (Map.insert (ide, ot {opKind = Partial}) (ide',kind') m1)

-- insert mapping of op symbol (ide,ot) to itself into m

-- map the ops in the source signature

mapOps :: Sort_map -> Fun_map -> Id -> Set.Set OpType -> OpMap -> OpMap

mapOps sort_Map op_Map ide ots m =

Set.fold mapOp m ots

where

mapOp ot m1 =

let (ide',ot') = mapOpSym sort_Map op_Map (ide,ot)

in Rel.setInsert ide' ot' m1

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

according to rmap -}

predFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

-> Result Pred_map -> Result Pred_map

predFun rmap sort_Map ide pts m =

-- first consider all directly mapped profiles

let (pts1,m1) = Set.fold (directPredMap rmap sort_Map ide)

(Set.empty,m) pts

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

in case (Map.lookup (AKindedId PredKind ide) rmap,

Map.lookup (AnID ide) rmap) of

(Just rsy1, Just rsy2) ->

do m' <- m

plain_error m'

("Predicate " ++ showId ide

" is mapped twice: " ++

showDoc (rsy1, rsy2) "")

$ appRange (getRange rsy1) $ getRange rsy2

(Just rsy, Nothing) ->

Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1

(Nothing, Just rsy) ->

Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1

-- Anything not mapped explicitly is left unchanged

(Nothing,Nothing) -> m1

-- try to map a predicate symbol directly

-- collect all predTypes that cannot be mapped directly

directPredMap :: RawSymbolMap -> Sort_map -> Id -> PredType

-> (Set.Set PredType,Result Pred_map)

-> (Set.Set PredType,Result Pred_map)

directPredMap rmap sort_Map ide pt (pts,m) =

case Map.lookup (ASymbol (idToPredSymbol ide pt)) rmap of

Just rsy ->

(pts,insertmapPredSym sort_Map ide rsy pt m)

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

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

mappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id

mappedPredSym sort_Map ide pt rsy =

let predSym = "Predicate symbol " ++ showDoc (idToPredSymbol ide pt)

" is mapped to "

in case rsy of

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

if mapPredType sort_Map pt == pt'

then return ide'

else plain_error ide

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

" but should be mapped to type " ++

showDoc (mapPredType sort_Map pt) "") $ getRange rsy

AnID ide' -> return ide'

AKindedId PredKind ide' -> 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

return (Map.insert (ide, pt) ide' m1)

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

-- map the preds in the source signature

mapPreds :: Sort_map -> Pred_map -> Id -> Set.Set PredType

-> Map.Map Id (Set.Set PredType) -> Map.Map Id (Set.Set PredType)

mapPreds sort_Map pred_Map ide pts m =

Set.fold mapPred m pts

where

mapPred pt m1 =

let (ide',pt') = mapPredSym sort_Map pred_Map (ide,pt)

in Rel.setInsert ide' pt' m1

{-

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)

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

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

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

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

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

matches rsym1, then rsym2 must match rsym2). Moreover, symset1

contains only symbols with names equal to that of sym1,

whereas symset2 contains only symbols with names different from

that of sym1.

3. let "akmap" (from Actually Known Map) be an empty symbol map.

//DEPTH-FIRST MRV SEARCH

//recursively called procedure, returning a symbol map or a special

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

GET MRV (minimun remaining values) "VARIABLE"

4a. if posmap is empty

4a.1. check if akmap defines a mapping from every symbol in

source mor1. (this should be vacuously true - Bartek?)

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

4b. take a pair sym1 |-> (symset1,symset2) with MRV from posmap

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

But: prefer those with non-empty symset1!

Remove it from posmap.

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

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

(posmap1,posmap2).)

5. for each symbol "sym2" from symset1

CONSISTENCY CHECK

5.1. check if mapping sym1 to sym2 clashes with akmap

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

and mapping on their profiles clashes with what is already

known in akmap)

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

5.3. add mapping of sym1 to sym2 to akmap.

CONSTRAINT PROPAGATION (forward checking)

5.4. if sym1 and sym2 are sorts

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

mappings of s in posmap to sub/supersorts of sym2

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

sym1 in its argument or result sorts, restrict the

possible mappings of f in posmap accordingly

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

since 5.1. does the necessary check as well)

5.7. if sym1 and sym2 are operations/predicates,

5.8. For corresponding sorts in their profiles,

remove incompatible mappings of the sorts from posmap

5.9. For each sym in overloading relation with sym1,

remove incompatible mappings of sym from posmap

CONTINUE DEPTH FIRST SERACH

5.10. call recursively point 4.

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

7. if step 5 gave more than one map, raise an exception. Morphism is

not unique.

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

repeat steps 5-7 with symset2 instead of symset1

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

//end of the recursive procedure

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

10. otherwise, return computed morphism from target mor1 to sigma2

composed with mor1.

-}

-- Some auxiliary functions for inducedFromToMorphism

testMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool

testMatch rmap sym1 sym2 =

Map.foldWithKey match1 True rmap

where

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

canBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool

canBeMapped rmap sym1@(Symbol {symbType = SortAsItemType})

sym2@(Symbol {symbType = SortAsItemType}) =

testMatch rmap sym1 sym2

canBeMapped rmap sym1@(Symbol {symbType = OpAsItemType ot1})

sym2@(Symbol {symbType = OpAsItemType ot2}) =

length (opArgs ot1) == length (opArgs ot2) && -- same arity

opKind ot1 >= opKind ot2 && -- preservation of totality

testMatch rmap sym1 sym2

canBeMapped rmap sym1@(Symbol {symbType = PredAsItemType pt1})

sym2@(Symbol {symbType = PredAsItemType pt2}) =

length (predArgs pt1) == length (predArgs pt2) && -- same arity

testMatch rmap sym1 sym2

canBeMapped _ _ _ = False

preservesName :: Symbol -> Symbol -> Bool

preservesName sym1 sym2 = symName sym1 == symName sym2

compatibleSorts :: SymbolMap -> (SORT, SORT) -> Bool

compatibleSorts smap (s1,s2) =

case Map.lookup (idToSortSymbol s1) smap of

Nothing -> True

Just sym -> symName sym == s2

-- try to extend a symbol map with a yet unmapped symbol

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

-- and mapping on their profiles clashes with what is already

-- known in akmap)

extendSymbMap :: SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap

extendSymbMap akmap sym1 sym2 =

if case symbType sym1 of

SortAsItemType -> True

OpAsItemType ot1 -> case symbType sym2 of

OpAsItemType ot2 -> all (compatibleSorts akmap)

$ zip (opRes ot1:opArgs ot1) (opRes ot2:opArgs ot2)

_ -> False

PredAsItemType pt1 -> case symbType sym2 of

PredAsItemType pt2 -> all (compatibleSorts akmap)

$ zip (predArgs pt1) (predArgs pt2)

_ -> False

then Just $ Map.insert sym1 sym2 akmap

else Nothing

-- Type for posmap

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

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

-- cardinality of the symobl set

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

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

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

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

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

type PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),

Map.Map (Bool,Int) [(Symbol,SymbolSet)])

-- Some basic operations on PosMap

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

postponeEntry :: Symbol -> SymbolSet -> Bool

postponeEntry sym symset =

Set.null (Set.filter (preservesName sym) symset) && Set.size symset > 1

removeFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap

removeFromPosmap sym card (posmap1,posmap2) =

(Map.delete sym posmap1,

Map.update removeSym1 card posmap2)

where

removeSym [] = []

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

removeSym1 l = case removeSym l of

[] -> Nothing

l1 -> Just l1

addToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap

addToPosmap sym symset (posmap1,posmap2) =

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

listInsert card (sym,symset) posmap2)

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

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

-- to symbols from symset2

restrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap

restrictPosMap symset1' symset2 posmap' =

Set.fold restrictPosMap1 posmap' symset1'

where

restrictPosMap1 sym1 posmap@(posmap1,_posmap2) =

case Map.lookup sym1 posmap1 of

Nothing -> posmap

Just (symset1,card) ->

addToPosmap sym1 (symset1 `Set.intersection` symset2)

$ removeFromPosmap sym1 card posmap

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

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

restrictSorts ::

Symbol -> Symbol -> Sign f e -> Sign f e -> PosMap -> PosMap

restrictSorts sym1 sym2 sigma1 sigma2 posmap =

restrictPosMap subsyms1 subsyms2

$ restrictPosMap supersyms1 supersyms2 posmap

where

s1 = symName sym1

s2 = symName sym2

sub1 = Set.insert s1 $ subsortsOf s1 sigma1

sub2 = Set.insert s2 $ subsortsOf s2 sigma2

subsyms1 = Set.map idToSortSymbol sub1

subsyms2 = Set.map idToSortSymbol sub2

super1 = Set.insert s1 $ supersortsOf s1 sigma1

super2 = Set.insert s2 $ supersortsOf s2 sigma2

supersyms1 = Set.map idToSortSymbol super1

supersyms2 = Set.map idToSortSymbol super2

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

removeIncompatibleSortMaps :: Maybe PosMap -> (SORT,SORT) -> Maybe PosMap

removeIncompatibleSortMaps Nothing _ = Nothing

removeIncompatibleSortMaps (Just posmap@(posmap1,_posmap2)) (s1,s2) =

case Map.lookup sym1 posmap1 of

Nothing -> Just posmap

Just (symset,card) ->

-- is there some remaining possibility to map the sort?

if sym2 `Set.member` symset

then Just $ addToPosmap sym1 (Set.singleton sym2)

$ removeFromPosmap sym1 card posmap

-- if not, there is no map!

else Nothing

where

sym1 = idToSortSymbol s1

sym2 = idToSortSymbol s2

-- For corresponding sorts in profiles of sym1 and sym2,

-- remove incompatible mappings of the sorts from posmap

restrictOps :: Symbol -> Symbol -> PosMap -> Maybe PosMap

restrictOps sym1 sym2 posmap =

foldl removeIncompatibleSortMaps (Just posmap) $ zip sort1 sorts2

where

(sort1,sorts2) = case (symbType sym1,symbType sym2) of

(OpAsItemType ot1,OpAsItemType ot2) ->

(opRes ot1:opArgs ot1,opRes ot2:opArgs ot2)

(PredAsItemType pt1,PredAsItemType pt2) ->

(predArgs pt1,predArgs pt2)

_ -> ([],[])

-- the main function

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

=> m -- ^ extended morphism

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

-> RawSymbolMap

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

inducedFromToMorphism extEm isSubExt rmap sigma1 sigma2 = do

let symset1 = symOf sigma1

symset2 = symOf sigma2

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

mor1 <- inducedFromMorphism extEm rmap sigma1

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

if isSubSig isSubExt (mtarget mor1) sigma2

-- yes => we are done

then return (mor1 {mtarget = sigma2})

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

else let sortSet2 = sortSet sigma2 in

if Map.null rmap && Set.size symset1 == 1 && Set.size sortSet2 == 1

then return mor1

{ mtarget = sigma2

, sort_map = Map.singleton (symName $ Set.findMin symset1)

$ Set.findMin sortSet2 }

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

let addCard sym s = (s,(postponeEntry sym s,Set.size s))

ins1 sym = Map.insert sym

(addCard sym $ Set.filter (canBeMapped rmap sym) symset2)

posmap1 = Set.fold ins1 Map.empty symset1

ins2 sym1a (symset,card) = 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= "++showDoc posmap1 "") (return ())

case Map.lookup (True,0) posmap2 of

Nothing -> return ()

Just syms -> fatal_error ("No symbol mapping for "

++ showDoc (map fst syms) "")

$ concatMapRange getRange $ map fst syms

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

smap <- tryToInduce sigma1 sigma2 Map.empty posmap

smap1 <- case smap of

Nothing -> fatal_error

"No signature morphism for symbol map found"

$ concatMapRange getRange $ Map.keys rmap

Just x -> return x

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

symbMapToMorphism extEm sigma1 sigma2 smap1

-- 4. recursive depth first function

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

tryToInduce :: Sign f e -> Sign f e -> SymbolMap -> PosMap

-> Result (Maybe SymbolMap)

tryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do

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

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

else do

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

akmap1 <-

tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1

case akmap1 of

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

Nothing -> tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2

Just _ -> return akmap1

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 :: Sign f e -> Sign f e -> SymbolMap -> PosMap -> Symbol

-> Set.Set Symbol -> Result (Maybe SymbolMap)

tryToInduce1 sigma1 sigma2 akmap posmap sym1 symset = do

Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)

(return Nothing) symset

tryToInduce2 :: Sign f e -> Sign f e -> SymbolMap -> PosMap -> Symbol

-> Symbol -> Result (Maybe SymbolMap)

-> Result (Maybe SymbolMap)

tryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do

-- 5.1. to 5.3. consistency check

akmapSoFar1 <- akmapSoFar

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

Just x -> showDoc x " + "

Nothing -> "")

++showDoc sym1 " |-> " ++showDoc sym2 "; stopBackTrack: "

++show stopBackTrack) (return ())) -}

akmap' <-

case extendSymbMap akmap sym1 sym2 of

Nothing -> return Nothing

-- 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 !!??

-- 5.10.

case posmap1 of

Just posmap2 -> do

tryToInduce sigma1 sigma2 akmap1 posmap2

_ -> return Nothing

-- 6./7. uniqueness check

case (akmap',akmapSoFar1) of

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

(Nothing,Nothing) -> return Nothing

(Just smap,Nothing) -> return $ Just smap

(Nothing,Just smap) -> return $ Just smap

(Just smap1, Just smap2) ->

let shorten = Map.filterWithKey (/=) in

fatal_error (shows

(text "Ambiguous symbol map" $+$

text "Map1" <+> pretty (shorten smap1) $+$

text "Map2" <+> pretty (shorten smap2) $+$

text "Please, supply a unique fitting morphism")

"") $ concatMapRange getRange $ Map.elems $ shorten smap1

{-

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 =

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

then let diffsyms = sys Set.\\ symset in

fatal_error ("Revealing: The following symbols "

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

$ getSetRange diffsyms

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.

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

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

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 = 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}

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

-> Result (Morphism f e m)

cogeneratedSign extEm symset sigma =

if {-trace ("symset "++show symset++"\nsymset0 "++show symset0)-}

(not (symset `Set.isSubsetOf` symset0)) -- 2.

then let diffsyms = symset Set.\\ symset0 in

fatal_error ("Hiding: The following symbols "

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

$ getSetRange diffsyms

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 :: (e -> e -> e) -- ^ join signature extensions

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

finalUnion addSigExt sigma1 sigma2 = return $ addSig addSigExt sigma1 sigma2

-- ??? Finality check not yet implemented

-- | Insert into a list of values

listInsert :: Ord k => k -> a -> Map.Map k [a] -> Map.Map k [a]

listInsert kx x t = Map.insert kx (x : Map.findWithDefault [] kx t) t

getSetRange :: PosItem a => Set.Set a -> Range

getSetRange = concatMapRange getRange . Set.toList