SymbolMapAnalysis.hs revision e1839fb37a3a2ccd457464cb0dcc5efd466dbe22
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Till Mossakowski, Christian Maeder and Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : hets@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskisymbol map analysis for the HasCASL logic
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski ( inducedFromMorphism
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski , inducedFromToMorphism
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski , cogeneratedSign
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , generatedSign
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified Common.Lib.Map as Map
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Common.Lib.Set as Set
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaederinducedFromMorphism rmap sigma = do
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- first check: do all source raw symbols match with source signature?
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich let syms = symOf sigma
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder srcTypeMap = typeMap sigma
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich incorrectRsyms = Map.foldWithKey
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich (\rsy _ -> if Set.any (matchesND rsy) syms
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski matchesND rsy sy =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sy `matchSymb` rsy &&
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder AQualId _ _ -> True
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu -- unqualified raw symbols need some matching symbol
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder -- that is not directly mapped
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder _ -> Map.lookup (AQualId (symName sy) $ symType sy) rmap == Nothing
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder -- ... if not, generate an error
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if Set.isEmpty incorrectRsyms then return () else
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder pplain_error ()
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder (text "the following symbols:"
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder <+> printText incorrectRsyms
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $$ text "are already mapped directly or do not match with signature"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $$ printText sigma) nullPos
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder -- compute the sort map (as a Map)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder myTypeIdMap <- foldr
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (\ (s, ti) m ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder do s' <- typeFun rmap s (typeKind ti)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder return $ Map.insert s s' m1)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder -- compute the op map (as a Map)
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder let tarTypeMap = addUnit $ Map.foldWithKey ( \ i k m ->
4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder Map.insert (Map.findWithDefault i i myTypeIdMap)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder (mapTypeInfo myTypeIdMap k) m)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder op_Map <- Map.foldWithKey (opFun rmap sigma tarTypeMap myTypeIdMap)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder (return Map.empty) (assumps sigma)
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder -- compute target signature
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder let sigma' = Map.foldWithKey (mapOps myTypeIdMap op_Map) sigma
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder { typeMap = tarTypeMap, assumps = Map.empty }
d79e02625778d20a5458078f979ff74aac67db61Christian Maeder $ assumps sigma
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- return assembled morphism
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Result (envDiags sigma') $ Just ()
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder return $ (mkMorphism sigma (diffEnv sigma' preEnv))
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder { typeIdMap = myTypeIdMap
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder , funMap = op_Map }
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapTypeInfo :: IdMap -> TypeInfo -> TypeInfo
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapTypeInfo im ti =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder ti { superTypes = map (mapType im) $ superTypes ti
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski , typeDefn = mapTypeDefn im $ typeDefn ti }
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimapTypeDefn :: IdMap -> TypeDefn -> TypeDefn
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapTypeDefn im td =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder DatatypeDefn (DataEntry tm i k args alts) ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder DatatypeDefn (DataEntry (compIdMap tm im) i k args alts)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder AliasTypeDefn sc -> AliasTypeDefn $ mapTypeScheme im sc
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Supertype vs sc t ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Supertype vs (mapTypeScheme im sc)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ mapTerm (id, mapType im) t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | compute type mapping
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitypeFun :: RawSymbolMap -> Id -> Kind -> Result Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitypeFun rmap s k = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let rsys = Set.unions $ map (Set.maybeToSet . (\x -> Map.lookup x rmap))
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder [AQualId s $ TypeAsItemType k, AnID s, AKindedId SK_type s]
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- rsys contains the raw symbols to which s is mapped to
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder 0 -> return s -- use default = identity mapping
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder 1 -> return $ rawSymName $ Set.findMin rsys -- take the unique rsy
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder _ -> pplain_error s -- ambiguity! generate an error
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (text "type: " <+> printText s
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder <+> text "mapped ambiguously:" <+> printText rsys)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- | compute mapping of functions
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederopFun :: RawSymbolMap -> Env -> TypeMap -> IdMap -> Id -> OpInfos
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder -> Result FunMap -> Result FunMap
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederopFun rmap e tm type_Map i ots m =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- first consider all directly mapped profiles
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let (ots1,m1) = foldr (directOpMap rmap e tm type_Map i)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Set.empty, m) $ opInfos ots
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -- now try the remaining ones with (un)kinded raw symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in case (Map.lookup (AKindedId SK_op i) rmap,Map.lookup (AnID i) rmap) of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Just rsy1, Just rsy2) ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder pplain_error m'
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (text "Operation" <+> printText i
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder <+> text "is mapped twice:"
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder <+> printText rsy1 <+> text "," <+> printText rsy2
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Just rsy, Nothing) ->
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Set.fold (insertmapOpSym e tm type_Map i rsy) m1 ots1
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Nothing, Just rsy) ->
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Set.fold (insertmapOpSym e tm type_Map i rsy) m1 ots1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- Anything not mapped explicitly is left unchanged
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (Nothing,Nothing) -> Set.fold (unchangedOpSym type_Map i) m1 ots1
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- try to map an operation symbol directly
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- collect all opTypes that cannot be mapped directly
5e46b572ed576c0494768998b043d9d340594122Till MossakowskidirectOpMap :: RawSymbolMap -> Env -> TypeMap -> IdMap -> Id -> OpInfo
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder -> (Set.Set TySc, Result FunMap) -> (Set.Set TySc, Result FunMap)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederdirectOpMap rmap e tm type_Map i oi (ots,m) = let ot = opType oi in
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case Map.lookup (AQualId i $ OpAsItemType ot) rmap of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (ots, insertmapOpSym e tm type_Map i rsy (TySc ot) m)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Nothing -> (Set.insert (TySc ot) ots, m)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- map op symbol (id,ot) to raw symbol rsy
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapOpSym :: Env -> TypeMap -> IdMap -> Id -> TySc -> RawSymbol
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -> Result (Id, TySc)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapOpSym e tm type_Map i ot rsy = let sc1@(TySc sc) = mapTySc type_Map ot in
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski AnID id' -> return (id', sc1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski AKindedId SK_op id' -> return (id', sc1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski AQualId id' (OpAsItemType ot') ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski let (mt, ds) = runState (anaTypeScheme ot') e
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder {typeMap = tm}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in case mt of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> Result (envDiags ds) $ Just (i, sc1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Just nt -> if isUnifiable (typeMap ds) 0 sc nt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski then return (id', TySc ot')
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski else pplain_error (i, sc1)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (text "Operation symbol "
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder <+> printText (AQualId i $ OpAsItemType sc)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder <+> text "is mapped to type" <+> printText ot'
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski <+> text "but should be mapped to type" <+>
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder printText sc) nullPos
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> pplain_error (i, sc1)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (text "Operation symbol "
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> printText (AQualId i $ OpAsItemType sc)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> text" is mapped to symbol of wrong kind:"
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder <+> printText rsy)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- insert mapping of op symbol (id, ot) to raw symbol rsy into m
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederinsertmapOpSym :: Env -> TypeMap -> IdMap -> Id -> RawSymbol -> TySc
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder -> Result FunMap -> Result FunMap
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederinsertmapOpSym e tm type_Map i rsy ot m = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (id',kind') <- mapOpSym e tm type_Map i ot rsy
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder return (Map.insert (i, ot) (id',kind') m1)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- insert mapping of op symbol (id,ot) to itself into m
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederunchangedOpSym :: IdMap -> Id -> TySc -> Result FunMap -> Result FunMap
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederunchangedOpSym type_Map i ot m = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski return (Map.insert (i, ot) (i, mapTySc type_Map ot) m1)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- map the ops in the source signature
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermapOps :: IdMap -> FunMap -> Id -> OpInfos -> Env -> Env
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedermapOps type_Map op_Map i ots e =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder foldr ( \ ot e' ->
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let sc = TySc $ opType ot
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (id', TySc sc') = Map.findWithDefault (i, mapTySc type_Map sc)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (i, sc) op_Map
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in execState (addOpId id' sc' (opAttrs ot)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (mapOpDefn type_Map $ opDefn ot)) e')
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- more things in opAttrs and opDefns need renaming
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder e $ opInfos ots
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian MaedermapOpDefn :: IdMap -> OpDefn -> OpDefn
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapOpDefn im d = case d of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ConstructData i -> ConstructData $ Map.findWithDefault i i im
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder SelectData cs i -> SelectData (map (mapConstrInfo im) cs)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapConstrInfo :: IdMap -> ConstrInfo -> ConstrInfo
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapConstrInfo im ci = ci { constrType = mapTypeScheme im $ constrType ci}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- Some auxiliary functions for inducedFromToMorphism
3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian MaedertestMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertestMatch rmap sym1 sym2 =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Map.foldWithKey match1 True rmap
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder match1 rsy1 rsy2 b = b && ((sym1 `matchSymb` rsy1) <= (sym2 `matchSymb`rsy2))
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedercanBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedercanBeMapped rmap sym1@(Symbol {symType = ClassAsItemType _k1})
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sym2@(Symbol {symType = ClassAsItemType _k2}) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder testMatch rmap sym1 sym2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicanBeMapped rmap sym1@(Symbol {symType = TypeAsItemType _k1})
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder sym2@(Symbol {symType = TypeAsItemType _k2}) =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder testMatch rmap sym1 sym2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedercanBeMapped rmap sym1@(Symbol {symType = OpAsItemType _ot1})
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder sym2@(Symbol {symType = OpAsItemType _ot2}) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder testMatch rmap sym1 sym2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedercanBeMapped _ _ _ = False
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederpreservesName :: Symbol -> Symbol -> Bool
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederpreservesName sym1 sym2 = symName sym1 == symName sym2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder-- try to extend a symbol map with a yet unmapped symbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederextendSymbMap :: TypeMap -> SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederextendSymbMap tm akmap sym1 sym2 =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder if case (symType sym1, symType sym2) of
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (ClassAsItemType k1, ClassAsItemType k2) -> rawKind k1 == rawKind k2
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (TypeAsItemType k1, TypeAsItemType k2) -> rawKind k1 == rawKind k2
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder (OpAsItemType ot1, OpAsItemType ot2) ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let TySc sc2 =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mapTySc (Map.foldWithKey ( \ s1 s2 m ->
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Map.insert (symName s1) (symName s2) m)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Map.empty akmap) $ TySc ot1
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder in isUnifiable tm 0 ot2 sc2
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder then Just $ Map.insert sym1 sym2 akmap
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- Type for posmap
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- Each symbol is mapped to the set symbols it possibly can be mapped to
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- Additionally, we store a flag meaning "no default map" and the
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder-- cardinality of the symobl set
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- For efficiency reasons, we also carry around an indexing of posmap
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- according to the pairs (flag,cardinality). Since several symbols
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- may lead to the same pair, we have to associate a list of symbols
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- (and corresponding symbol sets) with each pair.
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- Hence, PosMap really is a pair to two maps.
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maedertype PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Map.Map (Bool,Int) [(Symbol,SymbolSet)])
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder-- Some basic operations on PosMap
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- postpone entries with no default mapping and size > 1
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederpostponeEntry :: Symbol -> SymbolSet -> Bool
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederpostponeEntry sym symset =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder not $ Set.any (preservesName sym) symset && Set.size symset > 1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederremoveFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederremoveFromPosmap sym card (posmap1,posmap2) =
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Map.update removeSym1 card posmap2)
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder removeSym [] = []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder removeSym ((x,y):l) = if x==sym then l else (x,y):removeSym l
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder removeSym1 l = case removeSym l of
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder [] -> Nothing
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder l1 -> Just l1
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederaddToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederaddToPosmap sym symset (posmap1,posmap2) =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (Map.insert sym (symset,card) posmap1,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Map.listInsert card (sym,symset) posmap2)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder where card = (postponeEntry sym symset,Set.size symset)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- restrict posmap such that each symbol from symset1 is only mapped
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- to symbols from symset2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederrestrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederrestrictPosMap symset1 symset2 posmap =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Set.fold restrictPosMap1 posmap symset1
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski restrictPosMap1 sym1 pm@(posmap1,_) =
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder case Map.lookup sym1 posmap1 of
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder Nothing -> pm
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just (symset,card) ->
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder addToPosmap sym1 (symset `Set.intersection` symset2)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder $ removeFromPosmap sym1 card posmap
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- the main function
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederinducedFromToMorphism :: RawSymbolMap -> Env -> Env -> Result Morphism
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian MaederinducedFromToMorphism rmap sigma1 sigma2 = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder --debug 3 ("rmap",rmap)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -- 1. use rmap to get a renaming...
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mor1 <- inducedFromMorphism rmap sigma1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- 1.1 ... is the renamed source signature contained in the target signature?
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder --debug 3 ("mtarget mor1",mtarget mor1)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder --debug 3 ("sigma2",sigma2)
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder if isSubEnv (mtarget mor1) sigma2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- yes => we are done
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder then return (mor1 {mtarget = sigma2})
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -- no => OK, we've to take the hard way
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder else {- pfatal_error (text "No symbol mapping for "
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder $$ printText rmap
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder $$ text "sigma1" $$ printText sigma1
58b5ac21d1c88344246aaedab0c0bdc7b759d7c6Christian Maeder $$ text "inducedFromMorphism sigma1" $$ printText (mtarget mor1)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder $$ text "to sigma2" $$ printText sigma2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $$ text "difference" $$ printText (diffEnv (mtarget mor1) sigma2))
4fc727afa544a757d1959ce77c02208f8bf330dcChristian Maeder inducedFromToMorphism2 rmap sigma1 sigma2
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederinducedFromToMorphism2 :: RawSymbolMap -> Env -> Env -> Result Morphism
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaederinducedFromToMorphism2 rmap sigma1 sigma2 = do
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder -- 2. Compute initial posmap, using all possible mappings of symbols
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let symset1 = symOf sigma1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder symset2 = symOf sigma2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder addCard sym s = (s,(postponeEntry sym s,Set.size s))
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (addCard sym $ Set.filter (canBeMapped rmap sym) symset2)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ins2 sym1 (symset,card) = Map.listInsert card (sym1,symset)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder posmap2 = Map.foldWithKey ins2 Map.empty posmap1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder posmap = (posmap1,posmap2)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder case Map.lookup (True,0) posmap2 of
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Nothing -> return ()
0799c8f17cbd2d06d02fcbc36e2d253f8c52a760Christian Maeder Just syms -> pfatal_error
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder (text "No symbol mapping for "
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski <+> printText (Set.fromList $ map fst syms)) nullPos
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder -- 3. call recursive function with empty akmap and initial posmap
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski smap <- tryToInduce sigma1 sigma2 Map.empty posmap
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder smap1 <- case smap of
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Nothing -> pfatal_error
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (text "No signature morphism for symbol map"
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $$ text "rmap" $$ printText rmap
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski $$ text "sigma1" $$ printText sigma1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder $$ text "sigma2" $$ printText sigma2)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski Just x -> return x
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- 9./10. compute and return the resulting morphism
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder symbMapToMorphism sigma1 sigma2 smap1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- 4. recursive depth first function
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -- ambiguous map leads to fatal error (similar to exception)
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaedertryToInduce :: Env -> Env -> SymbolMap -> PosMap -> Result (Maybe SymbolMap)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskitryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder --debug 5 ("akmap",akmap)
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder --debug 6 ("posmap",(posmap1,posmap2))
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder if Map.isEmpty posmap2 then return $ Just akmap -- 4a.
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder --debug 7 ("posmap'",posmap')
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder --debug 8 ("sym1",sym1)
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder akmap1 <- tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder if isNothing akmap1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -- 6. no map for symset1, hence try symset2
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder then tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder else return akmap1 -- otherwise, use symset1 only
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder -- 4b. take symbol with minimal remaining values (MRV)
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder (card,(sym1,symset):_symsets) = Map.findMin posmap2
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder (symset1,symset2) = Set.partition (preservesName sym1) symset
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder posmap' = removeFromPosmap sym1 card (posmap1,posmap2)
329d1810c6d5a5a0827e1d07503d94431578d176Christian MaedertryToInduce1 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski -> SymbolSet -> Result (Maybe SymbolMap)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedertryToInduce1 sigma1 sigma2 akmap posmap sym1 symset =
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder (return Nothing) symset
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedertryToInduce2 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -> Symbol -> Result (Maybe SymbolMap) -> Result (Maybe SymbolMap)
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian MaedertryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -- 5.1. to 5.3. consistency check
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder akmapSoFar1 <- akmapSoFar
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder akmap' <- case extendSymbMap (typeMap sigma1) akmap sym1 sym2 of
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder Nothing -> return Nothing
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder -- constraint propagation
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder Just akmap1 -> tryToInduce sigma1 sigma2 akmap1 posmap
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder -- 6./7. uniqueness check
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder case (akmap',akmapSoFar1) of
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (Nothing,Nothing) -> return Nothing
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder (Just smap,Nothing) -> return (Just smap)
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (Nothing,Just smap) -> return (Just smap)
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (Just smap1,Just smap2) ->
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder (text "Ambiguous symbol map" $$
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder text "Map1" <+> printText smap1 $$
27b37f8e6b165f7abb653a54b45ffcdb81cec561Christian Maeder text "Map2" <+> printText smap2)
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- | reveal the symbols in the set
32562a567baac248a00782d2727716c13117dc4aChristian MaedergeneratedSign :: SymbolSet -> Env -> Result Morphism
32562a567baac248a00782d2727716c13117dc4aChristian MaedergeneratedSign syms sigma =
32562a567baac248a00782d2727716c13117dc4aChristian Maeder let signSyms = symOf sigma
32562a567baac248a00782d2727716c13117dc4aChristian Maeder closedSyms = closeSymbSet syms
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder subSigma = plainHide (signSyms Set.\\ closedSyms) sigma
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder in checkSymbols closedSyms signSyms $
32562a567baac248a00782d2727716c13117dc4aChristian Maeder return $ embedMorphism subSigma sigma
32562a567baac248a00782d2727716c13117dc4aChristian Maeder-- | hide the symbols in the set
32562a567baac248a00782d2727716c13117dc4aChristian MaedercogeneratedSign :: SymbolSet -> Env -> Result Morphism
32562a567baac248a00782d2727716c13117dc4aChristian MaedercogeneratedSign syms sigma =
32562a567baac248a00782d2727716c13117dc4aChristian Maeder let signSyms = symOf sigma
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder subSigma = Set.fold hideRelSymbol sigma syms
32562a567baac248a00782d2727716c13117dc4aChristian Maeder in checkSymbols syms signSyms $
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder return $ embedMorphism subSigma sigma