ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder{- |

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederModule : $Header$

81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : symbol map analysis for the CASL logic.

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

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian MaederStability : provisional

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPortability : portable

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederSymbol map analysis for the CASL logic.

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

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder-}

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maedermodule CASL.SymbolMapAnalysis

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder ( inducedFromMorphism

950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maeder , inducedFromToMorphism

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , inducedFromMorphismExt

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder , inducedFromToMorphismExt

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder , cogeneratedSign

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder , generatedSign

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder , finalUnion

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder ) where

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.Sign

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maederimport CASL.AS_Basic_CASL

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport CASL.Morphism

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport CASL.Overload (leqF, leqP)

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maeder

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maederimport qualified Data.Map as Map

fc7df539e6d41b050161ed8f9ae6e444b1b5ab14Christian Maederimport qualified Data.Set as Set

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian Maederimport qualified Common.Lib.Rel as Rel

2b9022bd5dfb351d1d80f61680336effeccfa23eChristian Maederimport Common.Doc

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maederimport Common.DocUtils

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.ExtSign

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport Common.Id

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederimport Common.Result

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maederimport Data.List (partition, find)

04dada28736b4a237745e92063d8bdd49a362debChristian Maederimport Data.Maybe (catMaybes, isJust)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder{-

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaederinducedFromMorphism :: RawSymbolMap -> sign -> Result morphism

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder

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

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

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederInducing morphism from raw symbol map and signature

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederInput: raw symbol map "Rsm"

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder signature "Sigma1"

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederOutput: morphims "Mrph": Sigma1 -> "Sigma2".

5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder

ce5ff829db5f0bb4f16ad4de150eed4401d6acd5Christian Maeder//preparation

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

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

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

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder 2.2.1. add a pair "Sym,Rsym2" to Ssm.

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder//computing the "sort part" of the morphism

cf5149eb4d0faef6272231879c04aa740f5abc2bChristian Maeder3. let Sigma2 be an empty signature.

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

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

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

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder name other than that in Rsym2, return error.

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

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder 5.3.1. add sort from Rsym2 to Sigma2

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

04dada28736b4a237745e92063d8bdd49a362debChristian Maeder6. for each sort symbol "S" in Sigma1

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder 6.1. if S is not mapped by Mrph,

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder 6.1.1. add sort S to Sigma2

ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder 6.1.2. add mapping from S to S to Mrph.

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder//computing the "function/predicate part" of the morphism

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

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder symbol

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder 7.2. let "Fprof1" be the value of Fprof via Mrph

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

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder morphism)

9ae2df7accdbf35839d56f90e1e8662be7112cdbChristian Maeder 7.3. if Rsym2 is not of appriopriate type, return error, otherwise

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder let "F2" be the name of the symbol.

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

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder not equal, return error.

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder some name different than F2, return error.

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder 7.6. add an operation/predicate with name F2 and profile Fprof1 to

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

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

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder add it. Otherwise if it is a total function and if in Sigma2

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder there exists a partial function with the same name and profile,

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder add the total function removing the partial one.

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

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder profile Fprof to name F2.

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

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder that is not mapped by Mrph,

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder 8.1. as in 7.2

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

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

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

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

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

ab0f35d8b9012e459417e086773049ce33dda2a0Christian Maeder10. Compute transitive closure of subsorting relation in Sigma2.

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-}

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaederinducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e

7dec34aee2b609b9535c48d060e0f7baf3536457Christian Maeder -> Result (Morphism f e m)

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederinducedFromMorphism = inducedFromMorphismExt $ \ _ _ _ _ -> extendedInfo

e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder

3f63b98c111e5e2bb2cf13795cf6e084a78b0a8dChristian MaederinducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e -> m

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

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian MaederinducedFromMorphismExt extInd extEm rmap sigma = do

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maeder -- ??? Missing: check preservation of overloading relation

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder -- compute the sort map (as a Map)

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

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder s' <- sortFun rmap s

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder m1 <- m

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder return $ if s' == s then m1 else Map.insert s s' m1)

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder (return Map.empty) (sortSet sigma)

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder -- compute the op map (as a Map)

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder op_Map <- Map.foldWithKey (opFun rmap sort_Map)

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder (return Map.empty) (opMap sigma)

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder -- compute the pred map (as a Map)

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (return Map.empty) (predMap sigma)

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder -- return assembled morphism

9c03fbe72966fb21c99238c449efdb0126dae9deChristian Maeder return (embedMorphism extEm sigma $ closeSortRel

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder $ inducedSignAux extInd sort_Map op_Map pred_Map extEm sigma)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder { sort_map = sort_Map

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , op_map = op_Map

d48085f765fca838c1d972d2123601997174583dChristian Maeder , pred_map = pred_Map }

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -- the sorts of the source signature

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersortFun :: RawSymbolMap -> Id -> Result Id

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaedersortFun rmap s =

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

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder else if Set.null $ Set.deleteMin rsys then

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

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder else plain_error s -- ambiguity! generate an error

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder ("Sort " ++ showId s

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder " is mapped ambiguously: " ++ showDoc rsys "")

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder $ getRange rsys

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder where

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder rsys = Set.fromList $ catMaybes $ map (flip Map.lookup rmap)

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder [ ASymbol $ idToSortSymbol s

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder , AKindedSymb Implicit s ]

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder according to rmap -}

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederopFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> Result Op_map -> Result Op_map

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederopFun rmap sort_Map ide ots m =

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder -- first consider all directly mapped profiles

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

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

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

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (Just rsy1, Just rsy2) ->

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder do m' <- m

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder plain_error m'

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder ("Operation " ++ showId ide

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder " is mapped twice: "

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder ++ showDoc (rsy1, rsy2) "")

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder $ appRange (getRange rsy1) $ getRange rsy2

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder (Just rsy, Nothing) ->

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Nothing, Just rsy) ->

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

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

793945d4ac7c0f22760589c87af8e71427c76118Christian Maeder (Nothing,Nothing) -> m1

0f0aa53f11a0d1ab08c76428b9de73db5b17c977Christian Maeder

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder -- try to map an operation symbol directly

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

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

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian Maeder -> (Set.Set OpType, Result Op_map)

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder -> (Set.Set OpType, Result Op_map)

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaederdirectOpMap rmap sort_Map ide' ot (ots',m') =

15c12a3ac049a4528da05b1017b78145f308aeb0Christian Maeder case lookupOpSymbol rmap ide' ot of

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder Just rsy -> (ots', insertmapOpSym sort_Map ide' rsy ot m')

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

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederlookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederlookupOpSymbol rmap ide' ot = let mkS = idToOpSymbol ide' in

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

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder Nothing -> Map.lookup

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder (ASymbol (mkS $ mkTotal ot)) rmap

0b14ccc700093e203914052bf6aceda3164af730Christian Maeder res -> res

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder

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

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

f4741f6b7da52b5417899c8fcbe4349b920b006eChristian MaedermappedOpSym sort_Map ide ot rsy =

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder let opSym = "Operation symbol " ++ showDoc (idToOpSymbol ide ot)

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder " is mapped to "

cc8b603388a7deb7fb8045db0341f550f8be5844Christian Maeder kind = opKind ot

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian Maeder in case rsy of

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

1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder if compatibleOpTypes (mapOpType sort_Map ot) ot'

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

ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder else plain_error (ide, kind)

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder " but should be mapped to type " ++

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder showDoc (mapOpType sort_Map ot)"") $ getRange rsy

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder _ -> plain_error (ide, kind)

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder $ getRange rsy

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder

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

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

ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder -> Result Op_map -> Result Op_map

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederinsertmapOpSym sort_Map ide rsy ot m = do

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder m1 <- m

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

ad623ebb0fa505940a039fe967ecff8749719ac9Christian Maeder return $ if ide == ide' && kind' == opKind ot then m1 else

4ef2a978e66e2246ff0b7f00c77deb7aabb28b8eChristian Maeder Map.insert (ide, mkPartial ot) (ide', kind') m1

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder according to rmap -}

20fe556546c9277cf017931a07d90add61f199d9Christian Maeder

c2dead95fafd7ca36d06ddf07606a1292ead6d8aChristian MaederpredFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder -> Result Pred_map -> Result Pred_map

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian MaederpredFun rmap sort_Map ide pts m =

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder -- first consider all directly mapped profiles

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

c9b711a46e5138b2742727817c8071960e673073Christian Maeder (Set.empty,m) pts

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

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder in case (Map.lookup (AKindedSymb Preds_kind ide) rmap,

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of

10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maeder (Just rsy1, Just rsy2) ->

59c036af82aff7fbe074455dad50477b7878e2d8Christian Maeder do m' <- m

81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder plain_error m'

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder ("Predicate " ++ showId ide

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder " is mapped twice: " ++

6d96cc81e7926a65188fea5626e0e4e199f9d782Christian Maeder 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

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

_ -> plain_error ide

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

$ getRange rsy

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

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

-> Result Pred_map -> Result Pred_map

insertmapPredSym sort_Map ide rsy pt m = do

m1 <- m

ide' <- mappedPredSym sort_Map ide pt rsy

return $ if ide' == ide then m1 else Map.insert (ide, pt) ide' m1

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

{-

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

Algorithm adapted from Bartek Klin's algorithm for CATS.

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

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

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

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

using some basic principles of constraint programming.

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

propagation and MRV (minimum remaining values), see

Stuart Russell and Peter Norvig:

Artificial Intelligence - A Modern Approach.

Prentice Hall International

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

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

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

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

(among those maximizing he number of identitically mapped names)

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

The algorithm

Input: raw symbol map "rmap"

signatures "sigma1,sigma2"

Output: morphism "mor": sigma1 -> sigma2

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

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

of this inclusion with mor1

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

otherwise some heuristics is needed, because merely forgetting one renaming

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

-}

-- the main function

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

=> m -- ^ extended morphism

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

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

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphism = inducedFromToMorphismExt $ \ _ _ _ _ -> extendedInfo

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

=> InducedSign f e m e

-> m -- ^ extended morphism

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

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

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphismExt extInd extEm isSubExt diffExt rmap sig1@(ExtSign _ sy1)

sig2@(ExtSign _ sy2) =

let iftm rm = (inducedFromToMorphismAuxExt extInd extEm isSubExt diffExt

rm sig1 sig2, rm)

isOk = isJust . resultToMaybe

res = fst $ iftm rmap

pos = concatMapRange getRange $ Map.keys rmap

in if isOk res then res else

let filt = Set.filter $ (== SortAsItemType) . symbType

ss2 = filt sy2

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

$ Set.difference (filt sy1) ss2

prod = Set.size ss1 * Set.size ss2

in if prod < 19 then

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

$ combine (map ASymbol $ Set.toList ss1)

$ map ASymbol $ Set.toList ss2 of

[(r, m)] -> (if prod > 1 && Map.size m > 1 then warning else hint)

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

(_, m1) : (_, m2) : _ -> fatal_error

("ambiguous symbol map1:\n" ++ showDoc m1 "\n"

++ "ambiguous symbol map2:\n" ++ showDoc m2 "") pos

[] -> res

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

combine :: [a] -> [a] -> [[(a, a)]]

combine l1 = map (zip l1) . takeKFromN l1

takeKFromN :: [b] -> [a] -> [[a]]

takeKFromN s l = case s of

[] -> [[]]

_ : r -> [ a : b | a <- l, b <- takeKFromN r l]

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

=> InducedSign f e m e

-> m -- ^ extended morphism

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

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

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphismAuxExt extInd extEm isSubExt diffExt rmap

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

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

mor1 <- inducedFromMorphismExt extInd extEm rmap sigma1

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

let inducedSign = mtarget mor1

if isSubSig isSubExt inducedSign sigma2

-- yes => we are done

then composeM (\ _ _ -> return extEm) mor1

$ idOrInclMorphism $ embedMorphism extEm inducedSign sigma2

else fatal_error

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

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

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

$ concatMapRange getRange $ Map.keys rmap

{-

Computing signature generated by a symbol set.

Algorithm adapted from Bartek Klin's algorithm for CATS.

Input: symbol set "Syms"

signature "Sigma"

Output: signature "Sigma1"<=Sigma.

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

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

3. let Sigma1 be an empty signature.

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

4.1. if Sym is a:

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

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

4.1.2.1. add all sorts from Fargs to Sigma1.

4.1.2.2. add sort Fres to Sigma1.

4.1.2.3. add F with the needed profile to Sigma1.

4.1.3. partial function: as in 4.1.2.

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

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

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

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

Sigma1.

7. return the inclusion of sigma1 into sigma.

-}

generatedSign :: m -> SymbolSet -> Sign f e

-> Result (Morphism f e m)

generatedSign extEm sys sigma =

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")

$ getRange diffsyms

else return $ idOrInclMorphism $ 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

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

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 }

_ -> sigma1 -- extend this for the type variable e

-- 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 Set.isSubsetOf symset symset0 -- 2.

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

else let diffsyms = symset Set.\\ symset0 in

fatal_error ("Hiding: The following symbols "

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

$ getRange diffsyms

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'

_ -> symset1'

profileContains s symbT = elem s $ case symbT of

OpAsItemType ot -> opRes ot : opArgs ot

PredAsItemType pt -> predArgs pt

_ -> [] -- for other kinds the profiles need to be looked up

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

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

finalUnion addSigExt s1 s2 =

let leCl eq = Map.map (Rel.partSet eq)

mkp = Map.map makePartial

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

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

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

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

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

s3 = addSig addSigExt s1 s2

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

p3 = leCl (leqP s3) $ predMap s3

d1 = Map.differenceWith (listOfSetDiff True) o1 o3

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

e1 = Map.differenceWith (listOfSetDiff True) p1 p3

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

prL (s, l, b) = fsep

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

++ " side of union)")

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

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

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

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

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

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

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

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

listOfSetDiff b rl1 l2 = let

fst3 (s, _, _) = s

l1 = map fst3 rl1 in

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

$ fst $ foldr

(\ s (l, r) ->

let sIn = Set.isSubsetOf s

(r1, r2) = partition sIn r in

case r1 of

[] -> case find sIn l2 of

Nothing -> error "CASL.finalUnion.listOfSetDiff1"

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

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

[_] -> (l, r2)

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

([], l2) l1