e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : symbol map analysis for the CASL logic.
980f1e5f03d0c0772698ebb372fc711431dd0114Christian MaederCopyright : (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill MossakowskiStability : provisional
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill MossakowskiPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiSymbol map analysis for the CASL logic.
679d3f541f7a9ede4079e045f7758873bb901872Till Mossakowski Follows Sect. III:4.1 of the CASL Reference Manual.
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder ( inducedFromMorphism
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder , inducedFromToMorphism
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder , inducedFromMorphismExt
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder , inducedFromToMorphismExt
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder , cogeneratedSign
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder , generatedSign
f203f0ce5b163f2c6131108033f40425e39f41aaChristian Maeder , constMorphExt
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder , profileContainsSort
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maederimport CASL.Overload (leqF, leqP)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
0c2a90cbfb63865ff485c3fbe20a14589a5914beTill Mossakowskiimport qualified Common.Lib.Rel as Rel
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maederimport Data.List (partition, find)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Map as Map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Data.Set as Set
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaederinducedFromMorphism :: RawSymbolMap -> sign -> Result morphism
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederHere is Bartek Klin's algorithm that has benn used for CATS.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiOur algorithm deviates from it. The exact details need to be checked.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInducing morphism from raw symbol map and signature
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInput: raw symbol map "Rsm"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski signature "Sigma1"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiOutput: morphims "Mrph": Sigma1 -> "Sigma2".
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski1. let "Ssm" be an empty list of pairs (symbol, raw symbol).
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski2. for each pair "Rsym1,Rsym2" in Rsm do:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 2.1. if there is no symbol in Sigma1 matching Rsym1, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 2.2. for each symbol "Sym" from Sigma1 matching Rsym1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 2.2.1. add a pair "Sym,Rsym2" to Ssm.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski//computing the "sort part" of the morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski3. let Sigma2 be an empty signature.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5.1. if Rsym2 is not a sort raw symbol, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5.2. if in Mrph there is a mapping of sort in Sym to sort with
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski name other than that in Rsym2, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5.3. if in Mrph there is no mappinh of sort in Sym
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5.3.1. add sort from Rsym2 to Sigma2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski6. for each sort symbol "S" in Sigma1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 6.1. if S is not mapped by Mrph,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 6.1.1. add sort S to Sigma2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 6.1.2. add mapping from S to S to Mrph.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski//computing the "function/predicate part" of the morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski7. for each pair "Sym,Rsym2" in Ssm such that Sym is a function/predicate
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.2. let "Fprof1" be the value of Fprof via Mrph
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (it can be computed, as we already have the "sort" part of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.3. if Rsym2 is not of appriopriate type, return error, otherwise
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let "F2" be the name of the symbol.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski an implicit symbol), compare the profile to Fprof1. If it is
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski not equal, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.5. if in Mrph there is a mapping of F1 with profile Fprof to
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski some name different than F2, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 7.6. add an operation/predicate with name F2 and profile Fprof1 to
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Sigma2. If it is a partial function and if in Sigma2 there
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski exists a total function with the same name and profile, do not
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 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,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 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
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski that is not mapped by Mrph,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 8.1. as in 7.2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 8.2. as in 7.6, replacing F2 with F1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 8.3. as in 7.7, replacing F2 with F1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski9. for each sort relation "S1,S2" in Sigma1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 9.2. add sort relation "S3,S4" in Sigma2.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski10. Compute transitive closure of subsorting relation in Sigma2.
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maedertype InducedMorphism e m = RawSymbolMap -> e -> Result m
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian MaederconstMorphExt :: m -> InducedMorphism e m
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian MaederconstMorphExt m _ _ = return m
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder{- | function and preds in the overloading relation are mapped in the same way
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maederthus preserving the overload-relation -}
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian MaederinducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder -> Result (Morphism f e m)
f203f0ce5b163f2c6131108033f40425e39f41aaChristian MaederinducedFromMorphism =
f203f0ce5b163f2c6131108033f40425e39f41aaChristian Maeder inducedFromMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt
f203f0ce5b163f2c6131108033f40425e39f41aaChristian MaederinducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maeder -> InducedMorphism e m
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian MaederinducedFromMorphismExt extInd extEm rmap sigma = do
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder -- compute the sort map (as a Map)
5f427cfb286859e5f450b2049f0e21008289c830Christian Maeder sort_Map <- Set.fold (\ s m -> do
5f427cfb286859e5f450b2049f0e21008289c830Christian Maeder s' <- sortFun rmap s
5f427cfb286859e5f450b2049f0e21008289c830Christian Maeder return $ if s' == s then m1 else Map.insert s s' m1)
ecf557c0b4f953106755a239da2c0b168064d3f4Christian Maeder (return Map.empty) (sortSet sigma)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- compute the op map (as a Map)
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder op_Map <- Map.foldWithKey (opFun sigma rmap sort_Map)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (return Map.empty) (MapSet.toMap $ opMap sigma)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- compute the pred map (as a Map)
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder pred_Map <- Map.foldWithKey (predFun sigma rmap sort_Map)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (return Map.empty) (MapSet.toMap $ predMap sigma)
036ecbd8f721096321f47cf6a354a9d1bf3d032fChristian Maeder em <- extEm rmap $ extendedInfo sigma
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- return assembled morphism
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder return (embedMorphism em sigma
f203f0ce5b163f2c6131108033f40425e39f41aaChristian Maeder $ inducedSignAux extInd sort_Map op_Map pred_Map em sigma)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { sort_map = sort_Map
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , op_map = op_Map
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder , pred_map = pred_Map }
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder {- the sorts of the source signature
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder sortFun is the sort map as a Haskell function -}
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaedersortFun :: RawSymbolMap -> Id -> Result Id
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian MaedersortFun rmap s
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- rsys contains the raw symbols to which s is mapped to
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder | Set.null rsys = return s -- use default = identity mapping
4705cb2fe71c52457c87a64d52a915337996dc23Christian Maeder return $ rawSymName $ Set.findMin rsys -- take the unique rsy
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder | otherwise = plain_error s -- ambiguity! generate an error
615967875347202454e75229d30b8db478ac508bChristian Maeder ("sort " ++ showId s
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder " is mapped ambiguously: " ++ showDoc rsys "")
d8f14f4b0bc8d94b61a10c1d268ac33c8e43cca0Christian Maeder $ getRange rsys
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- get all raw symbols to which s is mapped to
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder rsys = Set.fromList $ mapMaybe (`Map.lookup` rmap)
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder [ ASymbol $ idToSortSymbol s
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder , AKindedSymb Implicit s ]
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder {- to a Op_map, add everything resulting from mapping (id, ots)
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder according to rmap -}
4d16e663fab0891be3d790ec1e0290957a93e532Christian MaederopFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set OpType
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> Result Op_map -> Result Op_map
4d16e663fab0891be3d790ec1e0290957a93e532Christian MaederopFun src rmap sort_Map ide ots m =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- first consider all directly mapped profiles
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder let otls = Rel.partSet (leqF src) ots
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder m1 = foldr (directOpMap rmap sort_Map ide) m otls
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now try the remaining ones with (un)kinded raw symbol
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder in case (Map.lookup (AKindedSymb Ops_kind ide) rmap,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder (Just rsy1, Just rsy2) -> let
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder m2 = Set.fold (insertmapOpSym sort_Map ide rsy1) m1 ots
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder in Set.fold (insertmapOpSym sort_Map ide rsy2) m2 ots
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (Just rsy, Nothing) ->
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (Nothing, Just rsy) ->
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- Anything not mapped explicitly is left unchanged
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder (Nothing, Nothing) -> m1
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder {- try to map an operation symbol directly
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder collect all opTypes that cannot be mapped directly -}
4d16e663fab0891be3d790ec1e0290957a93e532Christian MaederdirectOpMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder -> Result Op_map -> Result Op_map
24dd53f70fcdb20410d6515642743b6265eb46e3Christian MaederdirectOpMap rmap sort_Map ide ots m =
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder rl = map (lookupOpSymbol rmap ide) ol
c74c2c0866974d72c50e10bc6ac5c7f7dfed894dChristian Maeder (ms, os) = partition (isJust . fst) $ zip rl ol
c74c2c0866974d72c50e10bc6ac5c7f7dfed894dChristian Maeder in case ms of
c74c2c0866974d72c50e10bc6ac5c7f7dfed894dChristian Maeder l@((Just rsy, _) : rs) ->
c74c2c0866974d72c50e10bc6ac5c7f7dfed894dChristian Maeder foldr (\ (_, ot) ->
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder insertmapOpSym sort_Map ide
6d2a698d6d7a4f2fd68cdc83c99d02363a7b3df6Christian Maeder (ASymbol $ idToOpSymbol (rawSymName rsy)
6d2a698d6d7a4f2fd68cdc83c99d02363a7b3df6Christian Maeder $ mapOpType sort_Map ot) ot)
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder (foldr (\ (rsy2, ot) ->
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder insertmapOpSym sort_Map ide (fromJust rsy2) ot) m l)
fa167e362877db231378e17ba49c66fbb84862fcChristian MaederlookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol
fa167e362877db231378e17ba49c66fbb84862fcChristian MaederlookupOpSymbol rmap ide' ot = let mkS = idToOpSymbol ide' in
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder case Map.lookup (ASymbol (mkS $ mkPartial ot)) rmap of
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder (ASymbol (mkS $ mkTotal ot)) rmap
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder -- map op symbol (ide, ot) to raw symbol rsy
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian MaedermappedOpSym sort_Map ide ot rsy =
615967875347202454e75229d30b8db478ac508bChristian Maeder let opSym = "operation symbol " ++ showDoc (idToOpSymbol ide ot)
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder " is mapped to "
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder kind = opKind ot
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder ot2 = mapOpType sort_Map ot
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder in case rsy of
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder ASymbol (Symbol ide' (OpAsItemType ot')) ->
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder if compatibleOpTypes ot2 ot'
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder then return (ide', opKind ot')
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder else plain_error (ide, kind)
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder (opSym ++ "type " ++ showDoc ot'
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder " but should be mapped to type " ++
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder showDoc ot2 "") $ getRange rsy
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb k ide' | elem k [Implicit, Ops_kind] -> return (ide', kind)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder _ -> plain_error (ide, kind)
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder (opSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
245e63ca4e8facdc267b6262e269ef3ac63b3c39Christian Maeder $ getRange rsy
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder -- insert mapping of op symbol (ide, ot) to raw symbol rsy into m
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaederinsertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder -> Result Op_map -> Result Op_map
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederinsertmapOpSym sort_Map ide rsy ot m = do
dd00735e659586abdebbb9442e4f44bf9eceedeeChristian Maeder (ide', kind') <- mappedOpSym sort_Map ide ot rsy
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder let otsy = Symbol ide $ OpAsItemType ot
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder pos = getRange rsy
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder m2 = Map.insert (ide, mkPartial ot) (ide', kind') m1
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder case Map.lookup (ide, mkPartial ot) m1 of
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder Nothing -> if ide == ide' && kind' == opKind ot then
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder ASymbol _ -> return m1
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder _ -> hint m1 ("identity mapping of "
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder ++ showDoc otsy "") pos
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder else return m2
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder Just (ide'', kind'') -> if ide' == ide'' then
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder warning (if kind' < kind'' then m2 else m1)
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder ("ignoring duplicate mapping of " ++ showDoc otsy "")
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder else plain_error m1
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder ("conflicting mapping of " ++ showDoc otsy " to " ++
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder show ide' ++ " and " ++ show ide'') pos
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder {- to a Pred_map, add evering resulting from mapping (ide, pts)
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder according to rmap -}
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian MaederpredFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set PredType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> Result Pred_map -> Result Pred_map
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian MaederpredFun src rmap sort_Map ide pts m =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- first consider all directly mapped profiles
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder let ptls = Rel.partSet (leqP src) pts
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder m1 = foldr (directPredMap rmap sort_Map ide) m ptls
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- now try the remaining ones with (un)kinded raw symbol
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder in case (Map.lookup (AKindedSymb Preds_kind ide) rmap,
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder Map.lookup (AKindedSymb Implicit ide) rmap) of
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder (Just rsy1, Just rsy2) -> let
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder m2 = Set.fold (insertmapPredSym sort_Map ide rsy1) m1 pts
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder in Set.fold (insertmapPredSym sort_Map ide rsy2) m2 pts
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (Just rsy, Nothing) ->
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder (Nothing, Just rsy) ->
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- Anything not mapped explicitly is left unchanged
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder (Nothing, Nothing) -> m1
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder {- try to map a predicate symbol directly
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder collect all predTypes that cannot be mapped directly -}
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian MaederdirectPredMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder -> Result Pred_map -> Result Pred_map
24dd53f70fcdb20410d6515642743b6265eb46e3Christian MaederdirectPredMap rmap sort_Map ide pts m =
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder rl = map (\ pt -> Map.lookup (ASymbol $ idToPredSymbol ide pt) rmap) pl
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder (ms, ps) = partition (isJust . fst) $ zip rl pl
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder in case ms of
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder l@((Just rsy, _) : rs) ->
24dd53f70fcdb20410d6515642743b6265eb46e3Christian Maeder foldr (\ (_, pt) ->
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder insertmapPredSym sort_Map ide
6d2a698d6d7a4f2fd68cdc83c99d02363a7b3df6Christian Maeder (ASymbol $ idToPredSymbol (rawSymName rsy)
6d2a698d6d7a4f2fd68cdc83c99d02363a7b3df6Christian Maeder $ mapPredType sort_Map pt) pt)
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder (foldr (\ (rsy2, pt) ->
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder insertmapPredSym sort_Map ide (fromJust rsy2) pt) m l)
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder -- map pred symbol (ide, pt) to raw symbol rsy
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaedermappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian MaedermappedPredSym sort_Map ide pt rsy =
615967875347202454e75229d30b8db478ac508bChristian Maeder let predSym = "predicate symbol " ++ showDoc (idToPredSymbol ide pt)
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder " is mapped to "
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder pt2 = mapPredType sort_Map pt
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder in case rsy of
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder ASymbol (Symbol ide' (PredAsItemType pt')) ->
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder if pt2 == pt'
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder then return ide'
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder else plain_error ide
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder (predSym ++ "type " ++ showDoc pt'
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder " but should be mapped to type " ++
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder showDoc pt2 "") $ getRange rsy
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb k ide' | elem k [Implicit, Preds_kind] -> return ide'
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder _ -> plain_error ide
786f66a85ab6d4541c407d4ae0d71dc338494f67Christian Maeder (predSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
245e63ca4e8facdc267b6262e269ef3ac63b3c39Christian Maeder $ getRange rsy
b7a0d2f2495d3b6b37d3316fc345e0efbbc61747Christian Maeder -- insert mapping of pred symbol (ide, pt) to raw symbol rsy into m
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaederinsertmapPredSym :: Sort_map -> Id -> RawSymbol -> PredType
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder -> Result Pred_map -> Result Pred_map
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederinsertmapPredSym sort_Map ide rsy pt m = do
d7f3a1e900a30469268df8033b87b92d7e827e30Christian Maeder ide' <- mappedPredSym sort_Map ide pt rsy
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder let ptsy = Symbol ide $ PredAsItemType pt
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder pos = getRange rsy
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder m2 = Map.insert (ide, pt) ide' m1
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder case Map.lookup (ide, pt) m1 of
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder Nothing -> if ide == ide' then
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder ASymbol _ -> return m1
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder _ -> hint m1 ("identity mapping of "
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder ++ showDoc ptsy "") pos
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder else return m2
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder Just ide'' -> if ide' == ide'' then
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder ("ignoring duplicate mapping of " ++ showDoc ptsy "") pos
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder else plain_error m1
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder ("conflicting mapping of " ++ showDoc ptsy " to " ++
f6e50d86cf46a89fcda7f875277c2d62bd008732Christian Maeder show ide' ++ " and " ++ show ide'') pos
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaederinducedFromToMorphism :: RawSymbolMap -> sign -> sign -> Result morphism
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiAlgorithm adapted from Bartek Klin's algorithm for CATS.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInducing morphisms from raw symbol map and source and target signature.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiThis problem is NP-hard (The problem of 3-colouring can be reduced to it).
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiThis means that we have exponential runtime in the worst case.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiHowever, in many cases the runtime can be kept rather short by
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiusing some basic principles of constraint programming.
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederWe use a depth-first search with some weak form of constraint
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederpropagation and MRV (minimum remaining values), see
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederStuart Russell and Peter Norvig:
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederArtificial Intelligence - A Modern Approach.
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederPrentice Hall International
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiThe algorithm has additionally to take care of default values (i.e.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskisymbol names are mapped identically be default, and the number of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiidentitically mapped names should be maximized). Moreover, it does
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskinot suffice to find just one solution, but also its uniqueness
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski(among those maximizing he number of identitically mapped names)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimust be checked (still, MRV is useful here).
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInput: raw symbol map "rmap"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski signatures "sigma1,sigma2"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiOutput: morphism "mor": sigma1 -> sigma2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski1. compute the morphism mor1 induced by rmap and sigma1 (i.e. the renaming)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski1.1. if target mor1 is a subsignature of sigma2, return the composition
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski of this inclusion with mor1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (cf. Theorem 6 of Bartek Klin's Master's Thesis)
2f437335bbaac47acfa272cf5de3c781e08fc325Christian Maederotherwise some heuristics is needed, because merely forgetting one renaming
2f437335bbaac47acfa272cf5de3c781e08fc325Christian Maedermay lead to unacceptable run-time for signatures with just about 10 symbols
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- the main function
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian MaederinducedFromToMorphism :: (Eq e, Show f, Pretty e, Pretty m)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder => m -- ^ extended morphism
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> (e -> e -> Bool) -- ^ subsignature test of extensions
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder -> (e -> e -> e) -- ^ difference of extensions
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder -> RawSymbolMap
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder -> ExtSign (Sign f e) Symbol
67869d63d1725c79e4c07b51acd466a31932b275Christian Maeder -> ExtSign (Sign f e) Symbol -> Result (Morphism f e m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian MaederinducedFromToMorphism m =
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder inducedFromToMorphismExt (\ _ _ _ _ -> extendedInfo) (constMorphExt m)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder (\ _ _ -> return m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian MaederinducedFromToMorphismExt
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder :: (Eq e, Show f, Pretty e, Pretty m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder => InducedSign f e m e
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> InducedMorphism e m -- ^ compute extended morphism
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> (Morphism f e m -> Morphism f e m -> Result m)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -- ^ composition of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> (e -> e -> Bool) -- ^ subsignature test of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> (e -> e -> e) -- ^ difference of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> RawSymbolMap
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> ExtSign (Sign f e) Symbol
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> ExtSign (Sign f e) Symbol
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> Result (Morphism f e m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian MaederinducedFromToMorphismExt extInd extEm compM isSubExt diffExt rmap
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder sig1@(ExtSign _ sy1) sig2@(ExtSign _ sy2) =
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder let iftm rm = (inducedFromToMorphismAuxExt extInd extEm compM isSubExt
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder diffExt rm sig1 sig2, rm)
58ab88e9fa53620974ff94aad166988495a27dc4Christian Maeder isOk = isJust . resultToMaybe
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder res = fst $ iftm rmap
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder pos = concatMapRange getRange $ Map.keys rmap
58ab88e9fa53620974ff94aad166988495a27dc4Christian Maeder in if isOk res then res else
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder let ss1 = Set.filter (\ s -> Set.null $ Set.filter
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder (compatibleSymbols True s) sy2)
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder $ Set.filter (\ s -> not $ any (matches s) $ Map.keys rmap)
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder fcombs = filteredPairs compatibleRawSymbs
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder (map ASymbol $ Set.toList ss1)
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder $ map ASymbol $ Set.toList sy2
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder in if null (drop 20 fcombs) then
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder case filter (isOk . fst) $ map (iftm . Map.union rmap . Map.fromList)
2937d25c9a98c4c1c17df12cb1ac61f8ce638b21Christian Maeder [(r, m)] -> (if length fcombs > 1 then warning else hint)
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder () ("derived symbol map:\n" ++ showDoc m "") pos >> r
1d8222622f2b30747efa88a7047b827c5c5e2945Christian Maeder l -> fatal_error
1d8222622f2b30747efa88a7047b827c5c5e2945Christian Maeder ("ambiguous symbol maps:\n" ++ show
1d8222622f2b30747efa88a7047b827c5c5e2945Christian Maeder (vcat $ map (pretty . snd) l)) pos
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder else warning () "too many possibilities for symbol maps" pos >> res
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleSymbTypes :: SymbType -> SymbType -> Bool
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleSymbTypes s1 s2 = case (s1, s2) of
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder (SortAsItemType, SortAsItemType) -> True
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder (OpAsItemType t1, OpAsItemType t2) ->
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder length (opArgs t1) == length (opArgs t2)
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder (PredAsItemType p1, PredAsItemType p2) ->
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder length (predArgs p1) == length (predArgs p2)
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleSymbols :: Bool -> Symbol -> Symbol -> Bool
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleSymbols alsoId (Symbol i1 k1) (Symbol i2 k2) =
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder compatibleSymbTypes k1 k2 && (not alsoId || i1 == i2)
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleRawSymbs :: RawSymbol -> RawSymbol -> Bool
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaedercompatibleRawSymbs r1 r2 = case (r1, r2) of
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder (ASymbol s1, ASymbol s2) -> compatibleSymbols False s1 s2
63882297f7ed36f6fb296324634da37b9fa6f1f4Christian Maeder _ -> False -- irrelevant
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaederfilteredPairs :: (a -> b -> Bool) -> [a] -> [b] -> [[(a, b)]]
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian MaederfilteredPairs p s l = sequence [[(a, b) | b <- filter (p a) l] | a <- s]
99fb5b9bb5661a895179ccbe144acf3b36d7248bChristian Maeder-- http://www.haskell.org/pipermail/haskell-cafe/2009-December/069957.html
7d41a06add784ca68e6507ce832e621a1d2abf49Christian MaederinducedFromToMorphismAuxExt
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder :: (Eq e, Show f, Pretty e, Pretty m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder => InducedSign f e m e
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> InducedMorphism e m -- ^ compute extended morphism
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -> (Morphism f e m -> Morphism f e m -> Result m)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder -- ^ composition of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> (e -> e -> Bool) -- ^ subsignature test of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> (e -> e -> e) -- ^ difference of extensions
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> RawSymbolMap
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> ExtSign (Sign f e) Symbol
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> ExtSign (Sign f e) Symbol
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> Result (Morphism f e m)
7d41a06add784ca68e6507ce832e621a1d2abf49Christian MaederinducedFromToMorphismAuxExt extInd extEm compM isSubExt diffExt rmap
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder (ExtSign sigma1 _) (ExtSign sigma2 _) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- 1. use rmap to get a renaming...
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder mor1 <- inducedFromMorphismExt extInd extEm rmap sigma1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- 1.1 ... is the renamed source signature contained in the target signature?
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder let inducedSign = mtarget mor1
f203f0ce5b163f2c6131108033f40425e39f41aaChristian Maeder em = extended_map mor1
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder if isSubSig isSubExt inducedSign sigma2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- yes => we are done
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder then composeM compM mor1 $ idOrInclMorphism
f203f0ce5b163f2c6131108033f40425e39f41aaChristian Maeder $ embedMorphism em inducedSign sigma2
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder {- here the empty mapping should be used, but it will be overwritten
a252bbf38eecc7a78c3435b6fac13231fcb7a717Christian Maeder by the first argument of composeM -}
2f437335bbaac47acfa272cf5de3c781e08fc325Christian Maeder else fatal_error
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder ("No signature morphism for symbol map found.\n" ++
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder "The following mapped symbols are missing in the target signature:\n"
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder ++ showDoc (diffSig diffExt inducedSign sigma2) "")
df6f4a9e6b3d0542ecc181fbc1bcec2affca1d30Christian Maeder $ concatMapRange getRange $ Map.keys rmap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiComputing signature generated by a symbol set.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiAlgorithm adapted from Bartek Klin's algorithm for CATS.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInput: symbol set "Syms"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski signature "Sigma"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiOutput: signature "Sigma1"<=Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski1. get a set "Sigma_symbols" of symbols in Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski2. if Syms is not a subset of Sigma_symbols, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski3. let Sigma1 be an empty signature.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski4. for each symbol "Sym" in Syms do:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1. if Sym is a:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.1. sort "S": add sort S to Sigma1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.2. total function "F" with profile "Fargs,Fres":
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.2.1. add all sorts from Fargs to Sigma1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.2.2. add sort Fres to Sigma1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.2.3. add F with the needed profile to Sigma1.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.3. partial function: as in 4.1.2.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 4.1.4. predicate: as in 4.1.2., except that Fres is omitted.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski5. get a list "Sig_sub" of subsort relations in Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski6. for each pair "S1,S2" in Sig_sub do:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 6.1. if S1,S2 are sorts in Sigma1, add "S1,S2" to sort relations in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski7. return the inclusion of sigma1 into sigma.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaedergeneratedSign :: m -> SymbolSet -> Sign f e -> Result (Morphism f e m)
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaedergeneratedSign extEm sys sigma = let
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz symset = symsetOf sigma -- 1.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder sigma1 = Set.fold revealSym sigma
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder , predMap = MapSet.empty } sys -- 4.
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder sigma2 = sigma1
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder { sortRel = sortRel sigma `Rel.restrict` sortSet sigma1
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder , emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder in if not $ Set.isSubsetOf sys symset -- 2.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder then let diffsyms = sys Set.\\ symset in
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder fatal_error ("Revealing: The following symbols "
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder ++ showDoc diffsyms " are not in the signature")
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder $ getRange diffsyms
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder else sigInclusion extEm sigma2 sigma -- 7.
d7f3a1e900a30469268df8033b87b92d7e827e30Christian MaederrevealSym :: Symbol -> Sign f e -> Sign f e
dece9056c18ada64bcc8f2fba285270374139ee8Christian MaederrevealSym sy sigma1 = let
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder n = symName sy
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder in case symbType sy of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SortAsItemType -> -- 4.1.1.
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder sigma1 {sortRel = insSort n $ sortRel sigma1}
e3169ed5885bb0888d8366c0d31ce1682e0fae74Christian Maeder SubsortAsItemType _ -> sigma1 -- ignore
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski OpAsItemType ot -> -- 4.1.2./4.1.3.
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder sigma1 { sortRel = foldr insSort (sortRel sigma1)
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder , opMap = MapSet.insert n ot $ opMap sigma1 }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski PredAsItemType pt -> -- 4.1.4.
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder sigma1 { sortRel = foldr insSort (sortRel sigma1) $ predArgs pt
dece9056c18ada64bcc8f2fba285270374139ee8Christian Maeder , predMap = MapSet.insert n pt $ predMap sigma1 }
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiComputing signature co-generated by a raw symbol set.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiAlgorithm adapted from Bartek Klin's algorithm for CATS.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiInput: symbol set "Syms"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski signature "Sigma"
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiOutput: signature "Sigma1"<=Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski1. get a set "Sigma_symbols" of symbols in Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski2. if Syms is not a subset of Sigma_symbols, return error.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski3. for each symbol "Sym" in Syms do:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3.1. if Sym is a:
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3.1.1. sort "S":
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3.1.1.1. Remove S from Sigma_symbols
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3.1.1.2. For each function/predicate symbol in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Sigma_symbols, if its profile contains S
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski remove it from Sigma_symbols.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski 3.1.2. any other symbol: remove if from Sigma_symbols.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski4. let Sigma1 be a signature generated by Sigma_symbols in Sigma.
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski5. return the inclusion of sigma1 into sigma.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaedercogeneratedSign :: m -> SymbolSet -> Sign f e -> Result (Morphism f e m)
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaedercogeneratedSign extEm symset sigma = let
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder symset0 = symsetOf sigma -- 1.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder symset1 = Set.fold hideSym symset0 symset -- 3.
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder in if Set.isSubsetOf symset symset0 -- 2.
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder then generatedSign extEm symset1 sigma -- 4./5.
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder else let diffsyms = symset Set.\\ symset0 in
245e63ca4e8facdc267b6262e269ef3ac63b3c39Christian Maeder fatal_error ("Hiding: The following symbols "
245e63ca4e8facdc267b6262e269ef3ac63b3c39Christian Maeder ++ showDoc diffsyms " are not in the signature")
d8f14f4b0bc8d94b61a10c1d268ac33c8e43cca0Christian Maeder $ getRange diffsyms
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaederhideSym :: Symbol -> Set.Set Symbol -> Set.Set Symbol
e73f0b9e920ae9ddfdbfe786cfbc5eb71e43ff6eChristian MaederhideSym sy set1 = let set2 = Set.delete sy set1 in case symbType sy of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski SortAsItemType -> -- 3.1.1.
e73f0b9e920ae9ddfdbfe786cfbc5eb71e43ff6eChristian Maeder Set.filter (not . profileContainsSort (symName sy) . symbType) set2
e73f0b9e920ae9ddfdbfe786cfbc5eb71e43ff6eChristian Maeder _ -> set2 -- 3.1.2
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaederprofileContainsSort :: SORT -> SymbType -> Bool
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaederprofileContainsSort s symbT = elem s $ case symbT of
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian Maeder OpAsItemType ot -> opSorts ot
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder PredAsItemType pt -> predArgs pt
e3169ed5885bb0888d8366c0d31ce1682e0fae74Christian Maeder SubsortAsItemType t -> [t]
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian Maeder SortAsItemType -> []
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederleCl :: Ord a => (a -> a -> Bool) -> MapSet.MapSet Id a
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederleCl f = Map.map (Rel.partSet f) . MapSet.toMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maedermkp :: OpMap -> OpMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maedermkp = MapSet.mapSet makePartial
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederfinalUnion :: (e -> e -> e) -- ^ join signature extensions
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> Sign f e -> Sign f e -> Result (Sign f e)
a0ac3ce207826aaccfdd220ac72cd49924660038Christian MaederfinalUnion addSigExt s1 s2 =
4d16e663fab0891be3d790ec1e0290957a93e532Christian Maeder let extP = Map.map (map $ \ s -> (s, [], False))
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder o1 = extP $ leCl (leqF s1) $ mkp $ opMap s1
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder o2 = extP $ leCl (leqF s2) $ mkp $ opMap s2
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder p1 = extP $ leCl (leqP s1) $ predMap s1
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder p2 = extP $ leCl (leqP s2) $ predMap s2
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder s3 = addSig addSigExt s1 s2
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder o3 = leCl (leqF s3) $ mkp $ opMap s3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder p3 = leCl (leqP s3) $ predMap s3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder d1 = Map.differenceWith (listOfSetDiff True) o1 o3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder d2 = Map.union d1 $ Map.differenceWith (listOfSetDiff False) o2 o3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder e1 = Map.differenceWith (listOfSetDiff True) p1 p3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder e2 = Map.union e1 $ Map.differenceWith (listOfSetDiff False) p2 p3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder prL (s, l, b) = fsep
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder $ text ("(" ++ (if b then "left" else "right")
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder ++ " side of union)")
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder : map pretty l ++ [mapsto <+> pretty s]
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder prM str = ppMap ((text str <+>) . pretty)
833d97d43e5f22c70c8abd79d344bc93a8ded319Christian Maeder (vcat . map prL) (const id) vcat (\ v1 v2 -> sep [v1, v2])
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder in if Map.null d2 && Map.null e2 then return s3
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder else fail $ "illegal overload relation identifications for profiles of:\n"
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder ++ show (prM "op" d2 $+$ prM "pred" e2)
a0ac3ce207826aaccfdd220ac72cd49924660038Christian MaederlistOfSetDiff :: Ord a => Bool -> [(Set.Set a, [Set.Set a], Bool)]
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder -> [Set.Set a] -> Maybe [(Set.Set a, [Set.Set a], Bool)]
a0ac3ce207826aaccfdd220ac72cd49924660038Christian MaederlistOfSetDiff b rl1 l2 = let
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder fst3 (s, _, _) = s
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder l1 = map fst3 rl1 in
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder (\ l3 -> if null l3 then Nothing else Just l3)
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder $ fst $ foldr
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder (\ s (l, r) ->
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder (r1, r2) = partition sIn r in
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder [] -> case find sIn l2 of
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder Nothing -> error "CASL.finalUnion.listOfSetDiff1"
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder Just s2 -> (if elem s2 $ map fst3 l then l else
7d41a06add784ca68e6507ce832e621a1d2abf49Christian Maeder (s2, filter (`Set.isSubsetOf` s2) l1, b) : l, r)
a0ac3ce207826aaccfdd220ac72cd49924660038Christian Maeder [_] -> (l, r2)