Copyright : (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005
Maintainer : Christian.Maeder@dfki.de
Symbol map analysis for the CASL logic.
Follows Sect. III:4.1 of the CASL Reference Manual.
, inducedFromToMorphismExt
inducedFromMorphism :: RawSymbolMap -> sign -> Result morphism
Here is Bartek Klin's algorithm that has benn used for CATS.
Our algorithm deviates from it. The exact details need to be checked.
Inducing morphism from raw symbol map and signature
Input: raw symbol map "Rsm"
Output: morphims "Mrph": Sigma1 -> "Sigma2".
1. let "Ssm" be an empty list of pairs (symbol, raw symbol).
2. for each pair "Rsym1,Rsym2" in Rsm do:
2.1. if there is no symbol in Sigma1 matching Rsym1, return error.
2.2. for each symbol "Sym" from Sigma1 matching Rsym1
2.2.1. add a pair "Sym,Rsym2" to Ssm.
//computing the "sort part" of the morphism
3. let Sigma2 be an empty signature.
4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.
5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol
5.1. if Rsym2 is not a sort raw symbol, return error.
5.2. if in Mrph there is a mapping of sort in Sym to sort with
name other than that in Rsym2, return error.
5.3. if in Mrph there is no mappinh of sort in Sym
5.3.1. add sort from Rsym2 to Sigma2
5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.
6. for each sort symbol "S" in Sigma1
6.1. if S is not mapped by Mrph,
6.1.1. add sort S to Sigma2
6.1.2. add mapping from S to S to Mrph.
7.1. let "F" be name contained in Sym, let "Fprof" be the profile.
7.2. let "Fprof1" be the value of Fprof via Mrph
(it can be computed, as we already have the "sort" part of
7.3. if Rsym2 is not of appriopriate type, return error, otherwise
let "F2" be the name of the symbol.
7.4. if Rsym2 enforces the profile of the symbol (
i.e., it is not
an implicit symbol), compare the profile to Fprof1. If it is
7.5. if in Mrph there is a mapping of F1 with profile Fprof to
some name different than F2, return error.
Sigma2. If it is a partial function and if in Sigma2 there
exists a total function with the same name and profile, do not
add it. Otherwise if it is a total function and if in Sigma2
there exists a partial function with the same name and profile,
add the total function removing the partial one.
profile Fprof to name F2.
that is not mapped by Mrph,
8.2. as in 7.6, replacing F2 with F1.
8.3. as in 7.7, replacing F2 with F1.
9. for each sort relation "S1,S2" in Sigma1,
9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)
9.2. add sort relation "S3,S4" in Sigma2.
10. Compute transitive closure of subsorting relation in Sigma2.
type InducedMorphism e m = RawSymbolMap -> e -> Result m
constMorphExt :: m -> InducedMorphism e m
constMorphExt m _ _ = return m
inducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt
inducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e
-> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
inducedFromMorphismExt extInd extEm rmap sigma = do
-- ??? Missing: check preservation of overloading relation
-- compute the sort map (as a Map)
return $ if s' == s then m1 else
Map.insert s s' m1)
-- compute the op map (as a Map)
-- compute the pred map (as a Map)
em <- extEm rmap $ extendedInfo sigma
-- return assembled morphism
return (embedMorphism em sigma $ closeSortRel
$ inducedSignAux extInd sort_Map op_Map pred_Map em sigma)
-- the sorts of the source signature
-- sortFun is the sort map as a Haskell function
sortFun :: RawSymbolMap -> Id -> Result Id
-- rsys contains the raw symbols to which s is mapped to
if
Set.null rsys then return s -- use default = identity mapping
return $ rawSymName $
Set.findMin rsys -- take the unique rsy
else plain_error s -- ambiguity! generate an error
" is mapped ambiguously: " ++ showDoc rsys "")
-- get all raw symbols to which s is mapped to
[ ASymbol $ idToSortSymbol s
, AKindedSymb Implicit s ]
{- to a Op_map, add everything resulting from mapping (id, ots)
opFun :: RawSymbolMap -> Sort_map -> Id ->
Set.Set OpType
-> Result Op_map -> Result Op_map
opFun rmap sort_Map ide ots m =
-- first consider all directly mapped profiles
-- now try the remaining ones with (un)kinded raw symbol
in case (
Map.lookup (AKindedSymb Ops_kind ide) rmap,
(Just rsy1, Just rsy2) ->
("operation " ++ showId ide
++ showDoc (rsy1, rsy2) "")
$ appRange (getRange rsy1) $ getRange rsy2
Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1
Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1
-- Anything not mapped explicitly is left unchanged
-- try to map an operation symbol directly
-- collect all opTypes that cannot be mapped directly
directOpMap :: RawSymbolMap -> Sort_map -> Id -> OpType
directOpMap rmap sort_Map ide' ot (ots',m') =
case lookupOpSymbol rmap ide' ot of
Just rsy -> (ots', insertmapOpSym sort_Map ide' rsy ot m')
lookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol
lookupOpSymbol rmap ide' ot = let mkS = idToOpSymbol ide' in
case
Map.lookup (ASymbol (mkS $ mkPartial ot)) rmap of
(ASymbol (mkS $ mkTotal ot)) rmap
-- map op symbol (ide,ot) to raw symbol rsy
mappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)
mappedOpSym sort_Map ide ot rsy =
let opSym = "operation symbol " ++ showDoc (idToOpSymbol ide ot)
ASymbol (Symbol ide' (OpAsItemType ot')) ->
if compatibleOpTypes (mapOpType sort_Map ot) ot'
then return (ide', opKind ot')
else plain_error (ide, kind)
(opSym ++ "type " ++ showDoc ot'
" but should be mapped to type " ++
showDoc (mapOpType sort_Map ot)"") $ getRange rsy
AKindedSymb k ide' | elem k [Implicit, Ops_kind] -> return (ide', kind)
_ -> plain_error (ide, kind)
(opSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
-- insert mapping of op symbol (ide,ot) to raw symbol rsy into m
insertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType
-> Result Op_map -> Result Op_map
insertmapOpSym sort_Map ide rsy ot m = do
(ide', kind') <- mappedOpSym sort_Map ide ot rsy
return $ if ide == ide' && kind' == opKind ot then m1 else
-- insert mapping of op symbol (ide, ot) to itself into m
{- to a Pred_map, add evering resulting from mapping (ide,pts)
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)
-- now try the remaining ones with (un)kinded raw symbol
in case (
Map.lookup (AKindedSymb Preds_kind ide) rmap,
(Just rsy1, Just rsy2) ->
("predicate " ++ showId ide
$ appRange (getRange rsy1) $ getRange rsy2
Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1
Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1
-- Anything not mapped explicitly is left unchanged
-- 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
(pts,insertmapPredSym sort_Map ide rsy pt 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)
ASymbol (Symbol ide' (PredAsItemType pt')) ->
if mapPredType sort_Map pt == pt'
(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'
(predSym ++ "symbol of wrong kind: " ++ showDoc 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
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).
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
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
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol -> Result (Morphism f e m)
inducedFromToMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt
inducedFromToMorphismExt :: (Eq e, Show f, Pretty e, Pretty m)
-> InducedMorphism e m -- ^ compute extended morphism
-> (e -> e -> Bool) -- ^ subsignature test of extensions
-> (e -> e -> e) -- ^ difference of extensions
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol -> Result (Morphism f e m)
inducedFromToMorphismExt extInd extEm isSubExt diffExt rmap sig1@(ExtSign _ sy1)
let iftm rm = (inducedFromToMorphismAuxExt extInd extEm isSubExt diffExt
isOk = isJust . resultToMaybe
pos = concatMapRange getRange $
Map.keys rmap
in if isOk res then res else
compatibleSymbols True (s, s2)) sy2)
fcombs = filter (all compatibleRawSymbs) combs
in if null $ drop 170 combs then
[(r, m)] -> (if length fcombs > 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
else warning () "too many possibilities for symbol maps" pos >> res
compatibleSymbTypes :: (SymbType, SymbType) -> Bool
compatibleSymbTypes p = case p of
(SortAsItemType, SortAsItemType) -> True
(OtherTypeKind s1, OtherTypeKind s2) -> s1 == s2
(OpAsItemType t1, OpAsItemType t2) ->
length (opArgs t1) == length (opArgs t2)
(PredAsItemType p1, PredAsItemType p2) ->
length (predArgs p1) == length (predArgs p2)
compatibleSymbols :: Bool -> (Symbol, Symbol) -> Bool
compatibleSymbols alsoId (Symbol i1 k1, Symbol i2 k2) =
compatibleSymbTypes (k1, k2) && (not alsoId || i1 == i2)
compatibleRawSymbs :: (RawSymbol, RawSymbol) -> Bool
compatibleRawSymbs p = case p of
(ASymbol s1, ASymbol s2) -> compatibleSymbols False (s1, s2)
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)
-> InducedMorphism e m -- ^ compute extended morphism
-> (e -> e -> Bool) -- ^ subsignature test of extensions
-> (e -> e -> e) -- ^ difference of extensions
-> 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
then composeM (\ _ _ -> return em) mor1 $ idOrInclMorphism
$ embedMorphism em inducedSign sigma2
-- here the empty mapping should be used, but it will be overwritten
-- by the first argument of composeM
("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.
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.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
7. return the inclusion of sigma1 into sigma.
generatedSign :: m -> SymbolSet -> Sign f e
-> Result (Morphism f e m)
generatedSign extEm sys sigma =
then let diffsyms = sys Set.\\ symset in
fatal_error ("Revealing: The following symbols "
++ showDoc diffsyms " are not in the signature")
else return $ idOrInclMorphism $ embedMorphism extEm sigma2 sigma
symset = symOf sigma -- 1.
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)
PredAsItemType pt -> -- 4.1.4.
sigma1 { sortSet = foldr
Set.insert (sortSet sigma1) $ predArgs pt
_ -> sigma1 -- extend this for the type variable e
Computing signature co-generated by a raw symbol set.
Algorithm adapted from Bartek Klin's algorithm for CATS.
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.1.1. Remove S from Sigma_symbols
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 =
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")
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)
OpAsItemType _ -> -- 3.1.2
PredAsItemType _ -> -- 3.1.2
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 =
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
$ text ("(" ++ (if b then "left" else "right")
: map pretty l ++ [mapsto <+> pretty s]
prM str = ppMap ((text str <+>) . pretty)
(vcat . map prL) id vcat (\ v1 v2 -> sep [v1, v2])
else fail $ "illegal overload relation identifications for profiles of:\n"
++ show (prM "op" d2 $+$ prM "pred" e2)
listOfSetDiff b rl1 l2 = let
(\ l3 -> if null l3 then Nothing else Just l3)
(r1, r2) = partition sIn r in
[] -> case find sIn l2 of
Just s2 -> (if elem s2 $ map fst3 l then l else