SymbolMapAnalysis.hs revision df3b448cc91d371e6028a43bc63e53df4d7765c0
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbModule : $Header$
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbCopyright : (c) Till Mossakowski, Christian Maeder and Uni Bremen 2002-2004
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbMaintainer : hets@tzi.de
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbStability : provisional
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbPortability : portable
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbThe symbol map analysis for the HasCASL logic
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb(adapted from CASL version r1.8 of 24.1.2004)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ( inducedFromMorphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , inducedFromToMorphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , cogeneratedSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , generatedSign
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified Common.Lib.Map as Map
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbimport qualified Common.Lib.Set as Set
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbinducedFromMorphism rmap sigma = do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- first check: do all source raw symbols match with source signature?
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let syms = symOf sigma
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb srcTypeMap = typeMap sigma
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb incorrectRsyms = Map.foldWithKey
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (\rsy _ -> if Set.any (matchesND rsy) syms
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb matchesND rsy sy =
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sy `matchSymb` rsy &&
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case rsy of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ASymbol _ -> True
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- unqualified raw symbols need some matching symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- that is not directly mapped
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb _ -> Map.lookup (ASymbol sy) rmap == Nothing
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- ... if not, generate an error
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb if Set.isEmpty incorrectRsyms then return () else
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb pplain_error ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ptext "the following symbols:"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb <+> printText incorrectRsyms
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $$ ptext "are already mapped directly or do not match with signature"
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $$ printText sigma)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ posOfId $ rawSymName $ Set.findMin incorrectRsyms
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- compute the sort map (as a Map)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb myTypeIdMap <- foldr
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (\ (s, ti) m ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb do s' <- typeFun rmap s (typeKind ti)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return $ Map.insert s s' m1)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- compute the op map (as a Map)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb op_Map <- Map.foldWithKey (opFun rmap srcTypeMap myTypeIdMap)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (return Map.empty) (assumps sigma)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- compute target signature
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let tarTypeMap = Map.foldWithKey ( \ i k m ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (mapTypeDefn myTypeIdMap k) m)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb sigma' = Map.foldWithKey (mapOps myTypeIdMap op_Map) sigma
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb { typeMap = addUnit tarTypeMap, assumps = Map.empty }
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ assumps sigma
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- return assembled morphism
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Result (envDiags sigma') $ Just ()
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb return $ (mkMorphism sigma (diffEnv sigma' preEnv))
f888346b48f5e5b5e3f0a47dedb8cefd2759a4e2gregames { typeIdMap = myTypeIdMap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb , funMap = op_Map }
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbmapTypeDefn :: IdMap -> TypeInfo -> TypeInfo
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbmapTypeDefn im ti =
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ti { superTypes = map (mapType im) $ superTypes ti }
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | compute type mapping
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtypeFun :: RawSymbolMap -> Id -> Kind -> Result Id
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantztypeFun rmap s k = do
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz let rsys = Set.unions $ map (Set.maybeToSet . (\x -> Map.lookup x rmap))
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz [ASymbol $ idToTypeSymbol s k, AnID s, AKindedId SK_type s]
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz -- rsys contains the raw symbols to which s is mapped to
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz 0 -> return s -- use default = identity mapping
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz 1 -> return $ rawSymName $ Set.findMin rsys -- take the unique rsy
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz _ -> pplain_error s -- ambiguity! generate an error
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz (ptext "type: " <+> printText s
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb <+> ptext "mapped ambiguously:" <+> printText rsys)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb-- | compute mapping of functions
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwroweopFun :: RawSymbolMap -> TypeMap -> IdMap -> Id -> OpInfos
a2a0abd88b19e042a3eb2a9fa1702c25ad51303dwrowe -> Result FunMap -> Result FunMap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbopFun rmap tm type_Map i ots m =
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- first consider all directly mapped profiles
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let (ots1,m1) = foldr (directOpMap rmap tm type_Map i) (Set.empty,m)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb $ opInfos ots
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- now try the remaining ones with (un)kinded raw symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb in case (Map.lookup (AKindedId SK_op i) rmap,Map.lookup (AnID i) rmap) of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (Just rsy1, Just rsy2) ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb do m' <- m
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb pplain_error m'
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ptext "Operation" <+> printText i
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb <+> ptext "is mapped twice:"
c3e342e5b0b9fea6617ee16d2da02c3ef2108126dougm <+> printText rsy1 <+> ptext "," <+> printText rsy2
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (Just rsy, Nothing) ->
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Set.fold (insertmapOpSym tm type_Map i rsy) m1 ots1
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (Nothing, Just rsy) ->
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Set.fold (insertmapOpSym tm type_Map i rsy) m1 ots1
c2cf53a40a9814eb91db2cdf820f97d943f21628coar -- Anything not mapped explicitly is left unchanged
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (Nothing,Nothing) -> Set.fold (unchangedOpSym type_Map i) m1 ots1
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- try to map an operation symbol directly
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar -- collect all opTypes that cannot be mapped directly
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowedirectOpMap :: RawSymbolMap -> TypeMap -> IdMap -> Id -> OpInfo
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar -> (Set.Set TySc, Result FunMap) -> (Set.Set TySc, Result FunMap)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowedirectOpMap rmap tm type_Map i oi (ots,m) = let ot = TySc $ opType oi in
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe case Map.lookup (ASymbol (idToOpSymbol i ot)) rmap of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Just rsy ->
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (ots,insertmapOpSym tm type_Map i rsy ot m)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Nothing -> (Set.insert ot ots,m)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- map op symbol (id,ot) to raw symbol rsy
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowemapOpSym :: TypeMap -> IdMap -> Id -> TySc -> RawSymbol
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -> Result (Id, TySc)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowemapOpSym tm type_Map i ot rsy = let sc1@(TySc sc) = mapTySc type_Map ot in
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames case rsy of
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe ASymbol (Symbol id' (OpAsItemType sc2@(TySc ot'))) ->
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe if isUnifiable (addUnit tm) 0 sc ot'
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh then return (id', sc2)
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh else pplain_error (i, sc1)
9e2e5b9bccb45b4a1bb9b747f15c7355e43be916ianh (ptext "Operation symbol " <+> printText (idToOpSymbol i sc1)
cbd8d35ca8d9780f1081f30ebfe4abda44cab7ebianh <+> ptext "is mapped to type" <+> printText ot'
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh <+> ptext "but should be mapped to type" <+>
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh printText sc
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh AnID id' -> return (id', sc1)
ea512a4af20e6b6e6931de4929d54d93f03a0139ianh AKindedId SK_op id' -> return (id', sc1)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe _ -> pplain_error (i, sc1)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (ptext "Operation symbol " <+> printText (idToOpSymbol i sc1)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz <+> ptext" is mapped to symbol of wrong kind:"
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz <+> printText rsy)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz -- insert mapping of op symbol (id, ot) to raw symbol rsy into m
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinsertmapOpSym :: TypeMap -> IdMap -> Id -> RawSymbol -> TySc
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -> Result FunMap -> Result FunMap
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinsertmapOpSym tm type_Map i rsy ot m = do
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames (id',kind') <- mapOpSym tm type_Map i ot rsy
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames return (Map.insert (i, ot) (id',kind') m1)
3e392a5afd51526de3cb15d57ee46d8cb160ae65gregames -- insert mapping of op symbol (id,ot) to itself into m
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweunchangedOpSym :: IdMap -> Id -> TySc -> Result FunMap -> Result FunMap
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoarunchangedOpSym type_Map i ot m = do
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe return (Map.insert (i, ot) (i, mapTySc type_Map ot) m1)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe -- map the ops in the source signature
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowemapOps :: IdMap -> FunMap -> Id -> OpInfos -> Env -> Env
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowemapOps type_Map op_Map i ots e =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe foldr ( \ ot e' ->
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe let sc = TySc $ opType ot
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (id', TySc sc') = Map.findWithDefault (i, mapTySc type_Map sc)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe (i, sc) op_Map
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe in execState (addOpId id' sc' (opAttrs ot) (opDefn ot)) e')
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe -- things in opAttrs and opDefns need renaming too!
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe e $ opInfos ots
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- Some auxiliary functions for inducedFromToMorphism
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowetestMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool
4775dfc34c90fada8c7c4d6a57ed8a3114d55c2dtrawicktestMatch rmap sym1 sym2 =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Map.foldWithKey match1 True rmap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe match1 rsy1 rsy2 b = b && ((sym1 `matchSymb` rsy1) <= (sym2 `matchSymb`rsy2))
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoarcanBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowecanBeMapped rmap sym1@(Symbol {symbType = ClassAsItemType _k1})
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe sym2@(Symbol {symbType = ClassAsItemType _k2}) =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe testMatch rmap sym1 sym2
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowecanBeMapped rmap sym1@(Symbol {symbType = TypeAsItemType _k1})
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe sym2@(Symbol {symbType = TypeAsItemType _k2}) =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe testMatch rmap sym1 sym2
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowecanBeMapped rmap sym1@(Symbol {symbType = OpAsItemType _ot1})
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe sym2@(Symbol {symbType = OpAsItemType _ot2}) =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe testMatch rmap sym1 sym2
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowecanBeMapped _ _ _ = False
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowepreservesName :: Symbol -> Symbol -> Bool
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowepreservesName sym1 sym2 = symName sym1 == symName sym2
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- try to extend a symbol map with a yet unmapped symbol
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweextendSymbMap :: TypeMap -> SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweextendSymbMap tm akmap sym1 sym2 =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe if case (symbType sym1, symbType sym2) of
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe (ClassAsItemType k1, ClassAsItemType k2) -> rawKind k1 == rawKind k2
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz (TypeAsItemType k1, TypeAsItemType k2) -> rawKind k1 == rawKind k2
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe (OpAsItemType sc1@(TySc _), OpAsItemType (TySc ot2)) ->
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe let TySc sc2 =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe mapTySc (Map.foldWithKey ( \ s1 s2 m ->
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Map.insert (symName s1) (symName s2) m)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe in isUnifiable tm 0 ot2 sc2
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar _ -> False
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe then Just $ Map.insert sym1 sym2 akmap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe else Nothing
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- Type for posmap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- Each symbol is mapped to the set symbols it possibly can be mapped to
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe-- Additionally, we store a flag meaning "no default map" and the
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- cardinality of the symobl set
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- For efficiency reasons, we also carry around an indexing of posmap
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- according to the pairs (flag,cardinality). Since several symbols
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe-- may lead to the same pair, we have to associate a list of symbols
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- (and corresponding symbol sets) with each pair.
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- Hence, PosMap really is a pair to two maps.
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantztype PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Map.Map (Bool,Int) [(Symbol,SymbolSet)])
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- Some basic operations on PosMap
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz-- postpone entries with no default mapping and size > 1
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzpostponeEntry :: Symbol -> SymbolSet -> Bool
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzpostponeEntry sym symset =
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe not $ Set.any (preservesName sym) symset && Set.size symset > 1
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweremoveFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweremoveFromPosmap sym card (posmap1,posmap2) =
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Map.update removeSym1 card posmap2)
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe removeSym [] = []
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz removeSym ((x,y):l) = if x==sym then l else (x,y):removeSym l
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz removeSym1 l = case removeSym l of
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz [] -> Nothing
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe l1 -> Just l1
c2cf53a40a9814eb91db2cdf820f97d943f21628coaraddToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wroweaddToPosmap sym symset (posmap1,posmap2) =
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz (Map.insert sym (symset,card) posmap1,
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Map.listInsert card (sym,symset) posmap2)
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz where card = (postponeEntry sym symset,Set.size symset)
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- restrict posmap such that each symbol from symset1 is only mapped
c2cf53a40a9814eb91db2cdf820f97d943f21628coar-- to symbols from symset2
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowerestrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantzrestrictPosMap symset1 symset2 posmap =
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz Set.fold restrictPosMap1 posmap symset1
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe restrictPosMap1 sym1 pm@(posmap1,_) =
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe case Map.lookup sym1 posmap1 of
fa06de8a28a737e8fbaad76d7f3ff67aaa5e4a09wrowe Nothing -> pm
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe Just (symset,card) ->
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe addToPosmap sym1 (symset `Set.intersection` symset2)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe $ removeFromPosmap sym1 card posmap
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe-- the main function
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinducedFromToMorphism :: RawSymbolMap -> Env -> Env -> Result Morphism
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewroweinducedFromToMorphism rmap sigma1 sigma2 = do
d4abb06ac220bb280ae996b6d21bbd257db51bb1jerenkrantz --debug 3 ("rmap",rmap)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- 1. use rmap to get a renaming...
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe mor1 <- inducedFromMorphism rmap sigma1
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- 1.1 ... is the renamed source signature contained in the target signature?
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe --debug 3 ("mtarget mor1",mtarget mor1)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe --debug 3 ("sigma2",sigma2)
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe if isSubEnv (mtarget mor1) sigma2
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- yes => we are done
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe then return (mor1 {mtarget = sigma2})
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe -- no => OK, we've to take the hard way
83a8dc5a596a8a1b9d14f063268287d123b9ed7ewrowe else {- pfatal_error (ptext "No symbol mapping for "
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $$ printText rmap
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $$ ptext "sigma1" $$ printText sigma1
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $$ ptext "inducedFromMorphism sigma1" $$ printText (mtarget mor1)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $$ ptext "to sigma2" $$ printText sigma2
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe $$ ptext "difference" $$ printText (diffEnv (mtarget mor1) sigma2))
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe inducedFromToMorphism2 rmap sigma1 sigma2
cc9582e53aead2a044077c4a92f3dfc3605590b3wroweinducedFromToMorphism2 :: RawSymbolMap -> Env -> Env -> Result Morphism
cc9582e53aead2a044077c4a92f3dfc3605590b3wroweinducedFromToMorphism2 rmap sigma1 sigma2 = do
0540a0b469147b52e858587270dba31c2aaa9e09wrowe -- 2. Compute initial posmap, using all possible mappings of symbols
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe let symset1 = symOf sigma1
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe symset2 = symOf sigma2
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe addCard sym s = (s,(postponeEntry sym s,Set.size s))
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe ins1 sym = Map.insert sym
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (addCard sym $ Set.filter (canBeMapped rmap sym) symset2)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe ins2 sym1 (symset,card) = Map.listInsert card (sym1,symset)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe posmap = (posmap1,posmap2)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe case Map.lookup (True,0) posmap2 of
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Nothing -> return ()
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Just syms -> pfatal_error
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp (ptext "No symbol mapping for "
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe <+> printText (Set.fromList $ map fst syms)) nullPos
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -- 3. call recursive function with empty akmap and initial posmap
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp smap <- tryToInduce sigma1 sigma2 Map.empty posmap
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe smap1 <- case smap of
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Nothing -> fail "No signature morphism for symbol map"
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Just x -> return x
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -- 9./10. compute and return the resulting morphism
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe symbMapToMorphism sigma1 sigma2 smap1
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -- 4. recursive depth first function
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp -- ambiguous map leads to fatal error (similar to exception)
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianptryToInduce :: Env -> Env -> SymbolMap -> PosMap -> Result (Maybe SymbolMap)
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianptryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp --debug 5 ("akmap",akmap)
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp --debug 6 ("posmap",(posmap1,posmap2))
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp if Map.isEmpty posmap2 then return $ Just akmap -- 4a.
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp --debug 7 ("posmap'",posmap')
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp --debug 8 ("sym1",sym1)
7a2edaa0193cbb0d79a65a8461a609a9402aea49brianp akmap1 <- tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp if isNothing akmap1
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp -- 6. no map for symset1, hence try symset2
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianp then tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2
7a2edaa0193cbb0d79a65a8461a609a9402aea49brianp else return akmap1 -- otherwise, use symset1 only
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -- 4b. take symbol with minimal remaining values (MRV)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (card,(sym1,symset):_symsets) = Map.findMin posmap2
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (symset1,symset2) = Set.partition (preservesName sym1) symset
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe posmap' = removeFromPosmap sym1 card (posmap1,posmap2)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -- 5. to 7.
a2b181763cb35fd899feb4a436aeadaa80bf91eabrianptryToInduce1 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe -> SymbolSet -> Result (Maybe SymbolMap)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowetryToInduce1 sigma1 sigma2 akmap posmap sym1 symset =
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)
cc9582e53aead2a044077c4a92f3dfc3605590b3wrowe (return Nothing) symset
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtryToInduce2 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -> Symbol -> Result (Maybe SymbolMap) -> Result (Maybe SymbolMap)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbtryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- 5.1. to 5.3. consistency check
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb akmapSoFar1 <- akmapSoFar
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb akmap' <- case extendSymbMap (typeMap sigma1) akmap sym1 sym2 of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Nothing -> return Nothing
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- constraint propagation
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb Just akmap1 -> tryToInduce sigma1 sigma2 akmap1 posmap
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb -- 6./7. uniqueness check
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case (akmap',akmapSoFar1) of
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (Nothing,Nothing) -> return Nothing
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (Just smap,Nothing) -> return (Just smap)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (Nothing,Just smap) -> return (Just smap)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (Just smap1,Just smap2) ->
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb fail $ shows
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ptext "Ambiguous symbol map" $$
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ptext "Map1" <+> printText smap1 $$
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb ptext "Map2" <+> printText smap2)
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbcheckSymbols :: SymbolSet -> SymbolSet -> Result a -> Result a
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbcheckSymbols s1 s2 r =
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb let s = s1 Set.\\ s2 in
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb if Set.isEmpty s then r else
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb pfatal_error
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb (ptext "unknown symbols: "
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb <+> printText s) $ posOfId $ symName $ Set.findMin s
b38846b15c8891c6dec44dcc4f96ca40721bf663rbbhideSymbol :: Symbol -> Env -> Env
c2cf53a40a9814eb91db2cdf820f97d943f21628coarhideSymbol sym sig =
c2cf53a40a9814eb91db2cdf820f97d943f21628coar let i = symName sym
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb tm = typeMap sig
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb as = assumps sig in
b38846b15c8891c6dec44dcc4f96ca40721bf663rbb case symbType sym of
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe ClassAsItemType _ -> sig
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe TypeAsItemType _ -> sig { typeMap =
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe OpAsItemType (TySc ot) ->
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe let OpInfos os = Map.findWithDefault (OpInfos []) i as
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe rs = filter (not . isUnifiable tm 0 ot . opType) os
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe in sig { assumps = if null rs then Map.delete i as
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe else Map.insert i (OpInfos rs) as }
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweplainHide :: SymbolSet -> Env -> Env
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwroweplainHide syms sigma =
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe let (opSyms, otherSyms) = Set.partition (\ sy -> case symbType sy of
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe OpAsItemType _ -> True
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe _ -> False) syms
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe in Set.fold hideSymbol (Set.fold hideSymbol sigma otherSyms) opSyms
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowesubSymsOf :: Symbol -> SymbolSet
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowesubSymsOf sy = case symbType sy of
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe OpAsItemType (TySc (TypeScheme _ (_ :=> ty) _)) -> subSyms ty
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoarcloseSymbSet :: SymbolSet -> SymbolSet
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowecloseSymbSet s = Set.unions (s : map subSymsOf (Set.toList s))
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar-- | reveal the symbols in the set
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowegeneratedSign :: SymbolSet -> Env -> Result Morphism
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoargeneratedSign syms sigma =
11fb2f3611e6ff9a541e10b13e3108934f828141gregames let signSyms = symOf sigma
11fb2f3611e6ff9a541e10b13e3108934f828141gregames closedSyms = closeSymbSet syms
11fb2f3611e6ff9a541e10b13e3108934f828141gregames subSigma = plainHide (signSyms Set.\\ closedSyms) sigma
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe in checkSymbols closedSyms signSyms $
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe return $ embedMorphism subSigma sigma
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe-- | hide the symbols in the set
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowecogeneratedSign :: SymbolSet -> Env -> Result Morphism
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowecogeneratedSign syms sigma =
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe let signSyms = symOf sigma
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar allSyms = Set.fold ( \ sy se ->
2f1949bb0e3c209db94c8d521cba7380b9d11421trawick if Set.disjoint syms $ subSymsOf sy then
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar se else Set.insert sy se) syms signSyms
290ecc1ddceca1ed49bc1a5338921264b5c3e07cwrowe subSigma = plainHide allSyms sigma
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar in checkSymbols syms signSyms $
731344ed8f3677d1661c261ca5fcdd2ee3dbc74ccoar return $ embedMorphism subSigma sigma