SymbolMapAnalysis.hs revision 3e884f4e6e79aaf2c940c35109918fdc62861898
a530dde7009b0a808300c420def741354a4d13d2Martin KühlModule : $Header$
a530dde7009b0a808300c420def741354a4d13d2Martin KühlCopyright : (c) Till Mossakowski, Christian Maeder and Uni Bremen 2002-2004
a530dde7009b0a808300c420def741354a4d13d2Martin KühlLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
a530dde7009b0a808300c420def741354a4d13d2Martin KühlMaintainer : hets@tzi.de
a530dde7009b0a808300c420def741354a4d13d2Martin KühlStability : provisional
a530dde7009b0a808300c420def741354a4d13d2Martin KühlPortability : portable
a530dde7009b0a808300c420def741354a4d13d2Martin Kühlsymbol map analysis for the HasCASL logic
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco ( inducedFromMorphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , inducedFromToMorphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , cogeneratedSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco , generatedSign
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riescoimport qualified Common.Lib.Map as Map
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riescoimport qualified Common.Lib.Set as Set
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoinducedFromMorphism :: RawSymbolMap -> Env -> Result Morphism
223be434693e8c97e2522ac19155a284b3536035Adrián RiescoinducedFromMorphism rmap sigma = do
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco -- first check: do all source raw symbols match with source signature?
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco let syms = symOf sigma
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco srcTypeMap = typeMap sigma
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco incorrectRsyms = Map.foldWithKey
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco (\rsy _ -> if Set.any (matchesND rsy) syms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco matchesND rsy sy =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco sy `matchSymb` rsy &&
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco AQualId _ _ -> True
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- unqualified raw symbols need some matching symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- that is not directly mapped
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> Map.lookup (AQualId (symName sy) $ symType sy) rmap == Nothing
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- ... if not, generate an error
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco if Set.isEmpty incorrectRsyms then return () else
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pplain_error ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ptext "the following symbols:"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> printText incorrectRsyms
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco $$ ptext "are already mapped directly or do not match with signature"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco $$ printText sigma) nullPos
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- compute the sort map (as a Map)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco myTypeIdMap <- foldr
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (\ (s, ti) m ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco do s' <- typeFun rmap s (typeKind ti)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco return $ Map.insert s s' m1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- compute the op map (as a Map)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let tarTypeMap = addUnit $ Map.foldWithKey ( \ i k m ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Map.insert (Map.findWithDefault i i myTypeIdMap)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (mapTypeDefn myTypeIdMap k) m)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco op_Map <- Map.foldWithKey (opFun rmap sigma tarTypeMap myTypeIdMap)
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco (return Map.empty) (assumps sigma)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- compute target signature
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let sigma' = Map.foldWithKey (mapOps myTypeIdMap op_Map) sigma
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco { typeMap = tarTypeMap, assumps = Map.empty }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco $ assumps sigma
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- return assembled morphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Result (envDiags sigma') $ Just ()
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco return $ (mkMorphism sigma (diffEnv sigma' preEnv))
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco { typeIdMap = myTypeIdMap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco , funMap = op_Map }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapTypeDefn :: IdMap -> TypeInfo -> TypeInfo
7474965b2e6323002c96c0b39a59843cde201870Adrián RiescomapTypeDefn im ti =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco ti { superTypes = map (mapType im) $ superTypes ti }
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | compute type mapping
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotypeFun :: RawSymbolMap -> Id -> Kind -> Result Id
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotypeFun rmap s k = do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let rsys = Set.unions $ map (Set.maybeToSet . (\x -> Map.lookup x rmap))
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco [AQualId s $ TypeAsItemType k, AnID s, AKindedId SK_type s]
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- rsys contains the raw symbols to which s is mapped to
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco 0 -> return s -- use default = identity mapping
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco 1 -> return $ rawSymName $ Set.findMin rsys -- take the unique rsy
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> pplain_error s -- ambiguity! generate an error
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ptext "type: " <+> printText s
7474965b2e6323002c96c0b39a59843cde201870Adrián Riesco <+> ptext "mapped ambiguously:" <+> printText rsys)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- | compute mapping of functions
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoopFun :: RawSymbolMap -> Env -> TypeMap -> IdMap -> Id -> OpInfos
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result FunMap -> Result FunMap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoopFun rmap e tm type_Map i ots m =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- first consider all directly mapped profiles
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let (ots1,m1) = foldr (directOpMap rmap e tm type_Map i)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (Set.empty, m) $ opInfos ots
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- now try the remaining ones with (un)kinded raw symbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in case (Map.lookup (AKindedId SK_op i) rmap,Map.lookup (AnID i) rmap) of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (Just rsy1, Just rsy2) ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco pplain_error m'
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ptext "Operation" <+> printText i
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> ptext "is mapped twice:"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> printText rsy1 <+> ptext "," <+> printText rsy2
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (Just rsy, Nothing) ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Set.fold (insertmapOpSym e tm type_Map i rsy) m1 ots1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (Nothing, Just rsy) ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Set.fold (insertmapOpSym e tm type_Map i rsy) m1 ots1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- Anything not mapped explicitly is left unchanged
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (Nothing,Nothing) -> Set.fold (unchangedOpSym type_Map i) m1 ots1
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- try to map an operation symbol directly
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- collect all opTypes that cannot be mapped directly
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescodirectOpMap :: RawSymbolMap -> Env -> TypeMap -> IdMap -> Id -> OpInfo
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> (Set.Set TySc, Result FunMap) -> (Set.Set TySc, Result FunMap)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescodirectOpMap rmap e tm type_Map i oi (ots,m) = let ot = opType oi in
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco case Map.lookup (AQualId i $ OpAsItemType ot) rmap of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ots, insertmapOpSym e tm type_Map i rsy (TySc ot) m)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> (Set.insert (TySc ot) ots, m)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- map op symbol (id,ot) to raw symbol rsy
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapOpSym :: Env -> TypeMap -> IdMap -> Id -> TySc -> RawSymbol
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result (Id, TySc)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapOpSym e tm type_Map i ot rsy = let sc1@(TySc sc) = mapTySc type_Map ot in
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco AnID id' -> return (id', sc1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco AKindedId SK_op id' -> return (id', sc1)
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco AQualId id' (OpAsItemType ot') ->
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco let (mt, ds) = runState (anaTypeScheme ot') e
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco {typeMap = tm}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco in case mt of
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Nothing -> Result (envDiags ds) $ Just (i, sc1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Just nt -> if isUnifiable (typeMap ds) 0 sc nt
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco then return (id', TySc ot')
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco else pplain_error (i, sc1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ptext "Operation symbol "
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> printText (AQualId i $ OpAsItemType sc)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> ptext "is mapped to type" <+> printText ot'
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco <+> ptext "but should be mapped to type" <+>
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco printText sc) nullPos
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco _ -> pplain_error (i, sc1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (ptext "Operation symbol "
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> printText (AQualId i $ OpAsItemType sc)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco <+> ptext" is mapped to symbol of wrong kind:"
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco <+> printText rsy)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- insert mapping of op symbol (id, ot) to raw symbol rsy into m
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoinsertmapOpSym :: Env -> TypeMap -> IdMap -> Id -> RawSymbol -> TySc
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -> Result FunMap -> Result FunMap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescoinsertmapOpSym e tm type_Map i rsy ot m = do
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco (id',kind') <- mapOpSym e tm type_Map i ot rsy
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco return (Map.insert (i, ot) (id',kind') m1)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- insert mapping of op symbol (id,ot) to itself into m
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián RiescounchangedOpSym :: IdMap -> Id -> TySc -> Result FunMap -> Result FunMap
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescounchangedOpSym type_Map i ot m = do
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco return (Map.insert (i, ot) (i, mapTySc type_Map ot) m1)
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco -- map the ops in the source signature
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapOps :: IdMap -> FunMap -> Id -> OpInfos -> Env -> Env
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescomapOps type_Map op_Map i ots e =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco foldr ( \ ot e' ->
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco let sc = TySc $ opType ot
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco (id', TySc sc') = Map.findWithDefault (i, mapTySc type_Map sc)
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco (i, sc) op_Map
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco in execState (addOpId id' sc' (opAttrs ot)
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco (mapOpDefn type_Map $ opDefn ot)) e')
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco -- more things in opAttrs and opDefns need renaming
d72e314a1952b4418fb1c98b17dbab0d16bba585Adrián Riesco e $ opInfos ots
223be434693e8c97e2522ac19155a284b3536035Adrián RiescomapOpDefn :: IdMap -> OpDefn -> OpDefn
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescomapOpDefn im d = case d of
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco ConstructData i -> ConstructData $ Map.findWithDefault i i im
fecce42517d20490f893c4a9dee29b000e1653eaAdrián Riesco SelectData cs i -> SelectData (map (mapConstrInfo im) cs)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián RiescomapConstrInfo :: IdMap -> ConstrInfo -> ConstrInfo
3f8cdebaede9921402318d525b57a9af8f9279d3Adrián RiescomapConstrInfo im ci = ci { constrType = mapTypeScheme im $ constrType ci}
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco-- Some auxiliary functions for inducedFromToMorphism
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotestMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián RiescotestMatch rmap sym1 sym2 =
5318901bb69bf247e0f341312c800ba4ea87e46bAdrián Riesco Map.foldWithKey match1 True rmap
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco match1 rsy1 rsy2 b = b && ((sym1 `matchSymb` rsy1) <= (sym2 `matchSymb`rsy2))
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescocanBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescocanBeMapped rmap sym1@(Symbol {symType = ClassAsItemType _k1})
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco sym2@(Symbol {symType = ClassAsItemType _k2}) =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco testMatch rmap sym1 sym2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescocanBeMapped rmap sym1@(Symbol {symType = TypeAsItemType _k1})
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco sym2@(Symbol {symType = TypeAsItemType _k2}) =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco testMatch rmap sym1 sym2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescocanBeMapped rmap sym1@(Symbol {symType = OpAsItemType _ot1})
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco sym2@(Symbol {symType = OpAsItemType _ot2}) =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco testMatch rmap sym1 sym2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescocanBeMapped _ _ _ = False
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescopreservesName :: Symbol -> Symbol -> Bool
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescopreservesName sym1 sym2 = symName sym1 == symName sym2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- try to extend a symbol map with a yet unmapped symbol
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoextendSymbMap :: TypeMap -> SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián RiescoextendSymbMap tm akmap sym1 sym2 =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco if case (symType sym1, symType sym2) of
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco (ClassAsItemType k1, ClassAsItemType k2) -> rawKind k1 == rawKind k2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco (TypeAsItemType k1, TypeAsItemType k2) -> rawKind k1 == rawKind k2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco (OpAsItemType ot1, OpAsItemType ot2) ->
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco let TySc sc2 =
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco mapTySc (Map.foldWithKey ( \ s1 s2 m ->
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco Map.insert (symName s1) (symName s2) m)
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco Map.empty akmap) $ TySc ot1
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco in isUnifiable tm 0 ot2 sc2
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco then Just $ Map.insert sym1 sym2 akmap
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- Type for posmap
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- Each symbol is mapped to the set symbols it possibly can be mapped to
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- Additionally, we store a flag meaning "no default map" and the
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- cardinality of the symobl set
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- For efficiency reasons, we also carry around an indexing of posmap
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- according to the pairs (flag,cardinality). Since several symbols
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- may lead to the same pair, we have to associate a list of symbols
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- (and corresponding symbol sets) with each pair.
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- Hence, PosMap really is a pair to two maps.
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riescotype PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco Map.Map (Bool,Int) [(Symbol,SymbolSet)])
6b2e3d60f2e2c230c9637bf0701d7024d289764dAdrián Riesco-- Some basic operations on PosMap
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco-- postpone entries with no default mapping and size > 1
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescopostponeEntry :: Symbol -> SymbolSet -> Bool
223be434693e8c97e2522ac19155a284b3536035Adrián RiescopostponeEntry sym symset =
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco not $ Set.any (preservesName sym) symset && Set.size symset > 1
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoremoveFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoremoveFromPosmap sym card (posmap1,posmap2) =
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco Map.update removeSym1 card posmap2)
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco removeSym [] = []
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco removeSym ((x,y):l) = if x==sym then l else (x,y):removeSym l
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco removeSym1 l = case removeSym l of
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco [] -> Nothing
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco l1 -> Just l1
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoaddToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoaddToPosmap sym symset (posmap1,posmap2) =
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco (Map.insert sym (symset,card) posmap1,
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco Map.listInsert card (sym,symset) posmap2)
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco where card = (postponeEntry sym symset,Set.size symset)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- restrict posmap such that each symbol from symset1 is only mapped
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco-- to symbols from symset2
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescorestrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián RiescorestrictPosMap symset1 symset2 posmap =
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco Set.fold restrictPosMap1 posmap symset1
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco restrictPosMap1 sym1 pm@(posmap1,_) =
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco case Map.lookup sym1 posmap1 of
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco Nothing -> pm
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco Just (symset,card) ->
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco addToPosmap sym1 (symset `Set.intersection` symset2)
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco $ removeFromPosmap sym1 card posmap
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco-- the main function
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescoinducedFromToMorphism :: RawSymbolMap -> Env -> Env -> Result Morphism
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián RiescoinducedFromToMorphism rmap sigma1 sigma2 = do
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco --debug 3 ("rmap",rmap)
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco -- 1. use rmap to get a renaming...
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco mor1 <- inducedFromMorphism rmap sigma1
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco -- 1.1 ... is the renamed source signature contained in the target signature?
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco --debug 3 ("mtarget mor1",mtarget mor1)
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco --debug 3 ("sigma2",sigma2)
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco if isSubEnv (mtarget mor1) sigma2
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco -- yes => we are done
fe5611d78ea0648e8719cb004a6a26e9a033429aAdrián Riesco then return (mor1 {mtarget = sigma2})
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco -- no => OK, we've to take the hard way
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco else {- pfatal_error (ptext "No symbol mapping for "
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco $$ printText rmap
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco $$ ptext "sigma1" $$ printText sigma1
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco $$ ptext "inducedFromMorphism sigma1" $$ printText (mtarget mor1)
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco $$ ptext "to sigma2" $$ printText sigma2
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco $$ ptext "difference" $$ printText (diffEnv (mtarget mor1) sigma2))
b9840e4ee6fda6e42fa4ee9f337482ccc4839a39Adrián Riesco inducedFromToMorphism2 rmap sigma1 sigma2
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián RiescoinducedFromToMorphism2 :: RawSymbolMap -> Env -> Env -> Result Morphism
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián RiescoinducedFromToMorphism2 rmap sigma1 sigma2 = do
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco -- 2. Compute initial posmap, using all possible mappings of symbols
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco let symset1 = symOf sigma1
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco symset2 = symOf sigma2
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco addCard sym s = (s,(postponeEntry sym s,Set.size s))
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco ins1 sym = Map.insert sym
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco (addCard sym $ Set.filter (canBeMapped rmap sym) symset2)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco ins2 sym1 (symset,card) = Map.listInsert card (sym1,symset)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco posmap2 = Map.foldWithKey ins2 Map.empty posmap1
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco posmap = (posmap1,posmap2)
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco case Map.lookup (True,0) posmap2 of
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco Nothing -> return ()
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco Just syms -> pfatal_error
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (ptext "No symbol mapping for "
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco <+> printText (Set.fromList $ map fst syms)) nullPos
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- 3. call recursive function with empty akmap and initial posmap
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco smap <- tryToInduce sigma1 sigma2 Map.empty posmap
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco smap1 <- case smap of
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco Nothing -> pfatal_error
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco (ptext "No signature morphism for symbol map"
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco $$ text "rmap" $$ printText rmap
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco $$ text "sigma1" $$ printText sigma1
223be434693e8c97e2522ac19155a284b3536035Adrián Riesco $$ text "sigma2" $$ printText sigma2)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco Just x -> return x
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- 9./10. compute and return the resulting morphism
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco symbMapToMorphism sigma1 sigma2 smap1
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco -- 4. recursive depth first function
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- ambiguous map leads to fatal error (similar to exception)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce :: Env -> Env -> SymbolMap -> PosMap -> Result (Maybe SymbolMap)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco --debug 5 ("akmap",akmap)
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco --debug 6 ("posmap",(posmap1,posmap2))
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if Map.isEmpty posmap2 then return $ Just akmap -- 4a.
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco --debug 7 ("posmap'",posmap')
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco --debug 8 ("sym1",sym1)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco akmap1 <- tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco if isNothing akmap1
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco -- 6. no map for symset1, hence try symset2
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco then tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco else return akmap1 -- otherwise, use symset1 only
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- 4b. take symbol with minimal remaining values (MRV)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (card,(sym1,symset):_symsets) = Map.findMin posmap2
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (symset1,symset2) = Set.partition (preservesName sym1) symset
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco posmap' = removeFromPosmap sym1 card (posmap1,posmap2)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce1 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -> SymbolSet -> Result (Maybe SymbolMap)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce1 sigma1 sigma2 akmap posmap sym1 symset =
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (return Nothing) symset
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce2 :: Env -> Env -> SymbolMap -> PosMap -> Symbol
c1cf2f634a37116ff90e99ca710179a23115cbfbAdrián Riesco -> Symbol -> Result (Maybe SymbolMap) -> Result (Maybe SymbolMap)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescotryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- 5.1. to 5.3. consistency check
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco akmapSoFar1 <- akmapSoFar
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco akmap' <- case extendSymbMap (typeMap sigma1) akmap sym1 sym2 of
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco Nothing -> return Nothing
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco -- constraint propagation
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco Just akmap1 -> tryToInduce sigma1 sigma2 akmap1 posmap
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco -- 6./7. uniqueness check
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco case (akmap',akmapSoFar1) of
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (Nothing,Nothing) -> return Nothing
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (Just smap,Nothing) -> return (Just smap)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco (Nothing,Just smap) -> return (Just smap)
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco (Just smap1,Just smap2) ->
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco (ptext "Ambiguous symbol map" $$
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco ptext "Map1" <+> printText smap1 $$
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco ptext "Map2" <+> printText smap2)
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | reveal the symbols in the set
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogeneratedSign :: SymbolSet -> Env -> Result Morphism
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescogeneratedSign syms sigma =
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco let signSyms = symOf sigma
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco closedSyms = closeSymbSet syms
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco subSigma = plainHide (signSyms Set.\\ closedSyms) sigma
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco in checkSymbols closedSyms signSyms $
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco return $ embedMorphism subSigma sigma
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco-- | hide the symbols in the set
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescocogeneratedSign :: SymbolSet -> Env -> Result Morphism
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián RiescocogeneratedSign syms sigma =
aea9000fc94442cbfc92596f4264473c0fce51e4Adrián Riesco let signSyms = symOf sigma
7fc57d0f02d0fec1192376ccebe2be0224cb9a55Adrián Riesco subSigma = Set.fold hideRelSymbol sigma syms
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco in checkSymbols syms signSyms $
27aad79faa0eec8d0e7dda32bca710db95bd2d0aAdrián Riesco return $ embedMorphism subSigma sigma