SymbolMapAnalysis.hs revision d8f14f4b0bc8d94b61a10c1d268ac33c8e43cca0
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingModule : $Header$
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingDescription : symbol map analysis for the CASL logic.
cb3cb4d60ac28163d3159c7b26593413fad6cd3echuckCopyright : (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingMaintainer : Christian.Maeder@dfki.de
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingStability : provisional
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingPortability : portable
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingSymbol map analysis for the CASL logic.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding Follows Sect. III:4.1 of the CASL Reference Manual.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ( inducedFromMorphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , inducedFromToMorphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , cogeneratedSign
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding , generatedSign
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding , finalUnion
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Data.Map as Map
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Data.Set as Set
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Common.Lib.Rel as Rel
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldinginducedFromMorphism :: RawSymbolMap -> sign -> Result morphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingHere is Bartek Klin's algorithm that has benn used for CATS.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingOur algorithm deviates from it. The exact details need to be checked.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingInducing morphism from raw symbol map and signature
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingInput: raw symbol map "Rsm"
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding signature "Sigma1"
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingOutput: morphims "Mrph": Sigma1 -> "Sigma2".
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding//preparation
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding1. let "Ssm" be an empty list of pairs (symbol, raw symbol).
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding2. for each pair "Rsym1,Rsym2" in Rsm do:
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding 2.1. if there is no symbol in Sigma1 matching Rsym1, return error.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding 2.2. for each symbol "Sym" from Sigma1 matching Rsym1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 2.2.1. add a pair "Sym,Rsym2" to Ssm.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding//computing the "sort part" of the morphism
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding3. let Sigma2 be an empty signature.
ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.1. if Rsym2 is not a sort raw symbol, return error.
7708bd70088b64148d7d78fd84ede43ced63c713minfrin 5.2. if in Mrph there is a mapping of sort in Sym to sort with
7708bd70088b64148d7d78fd84ede43ced63c713minfrin name other than that in Rsym2, return error.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.3. if in Mrph there is no mappinh of sort in Sym
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.3.1. add sort from Rsym2 to Sigma2
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.
6335eb31f0f0ed54628a04ed32946360b8b77684minfrin6. for each sort symbol "S" in Sigma1
6335eb31f0f0ed54628a04ed32946360b8b77684minfrin 6.1. if S is not mapped by Mrph,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 6.1.1. add sort S to Sigma2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 6.1.2. add mapping from S to S to Mrph.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding//computing the "function/predicate part" of the morphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding7. for each pair "Sym,Rsym2" in Ssm such that Sym is a function/predicate
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe 7.2. let "Fprof1" be the value of Fprof via Mrph
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (it can be computed, as we already have the "sort" part of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 7.3. if Rsym2 is not of appriopriate type, return error, otherwise
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let "F2" be the name of the symbol.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding an implicit symbol), compare the profile to Fprof1. If it is
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding not equal, return error.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 7.5. if in Mrph there is a mapping of F1 with profile Fprof to
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding some name different than F2, return error.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 7.6. add an operation/predicate with name F2 and profile Fprof1 to
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Sigma2. If it is a partial function and if in Sigma2 there
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding exists a total function with the same name and profile, do not
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding add it. Otherwise if it is a total function and if in Sigma2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding there exists a partial function with the same name and profile,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding add the total function removing the partial one.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 7.7. add to Mrph a mapping from operation/predicate of name F1 and
11c3b5180e1de6776035320b012a28bb146e7b46chuck profile Fprof to name F2.
11c3b5180e1de6776035320b012a28bb146e7b46chuck8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1
11c3b5180e1de6776035320b012a28bb146e7b46chuck that is not mapped by Mrph,
11c3b5180e1de6776035320b012a28bb146e7b46chuck 8.1. as in 7.2
11c3b5180e1de6776035320b012a28bb146e7b46chuck 8.2. as in 7.6, replacing F2 with F1.
11c3b5180e1de6776035320b012a28bb146e7b46chuck 8.3. as in 7.7, replacing F2 with F1.
11c3b5180e1de6776035320b012a28bb146e7b46chuck9. for each sort relation "S1,S2" in Sigma1,
11c3b5180e1de6776035320b012a28bb146e7b46chuck 9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)
11c3b5180e1de6776035320b012a28bb146e7b46chuck 9.2. add sort relation "S3,S4" in Sigma2.
11c3b5180e1de6776035320b012a28bb146e7b46chuck10. Compute transitive closure of subsorting relation in Sigma2.
11c3b5180e1de6776035320b012a28bb146e7b46chuckinducedFromMorphism :: (Pretty e, Pretty f) =>
11c3b5180e1de6776035320b012a28bb146e7b46chuck m -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
11c3b5180e1de6776035320b012a28bb146e7b46chuckinducedFromMorphism extEm rmap sigma = do
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- ??? Missing: check preservation of overloading relation
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- first check: do all source raw symbols match with source signature?
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let syms = symOf sigma
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sortsSigma = sortSet sigma
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding incorrectRsyms = Map.foldWithKey
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (\rsy _ -> if any (matchesND rsy) $ Set.toList syms
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding matchesND rsy sy =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sy `matches` rsy &&
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding case rsy of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ASymbol _ -> True
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- unqualified raw symbols need some matching symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- that is not directly mapped
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding _ -> Map.lookup (ASymbol sy) rmap == Nothing
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- ... if not, generate an error
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if Set.null incorrectRsyms then return () else fatal_error
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ("the following symbols: "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc incorrectRsyms
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding "\nare already mapped directly or do not match with signature\n"
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc sigma "")
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ getRange incorrectRsyms
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- compute the sort map (as a Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (\s m -> do s' <- sortFun rmap s
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if s' == s then m else do
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding return $ Map.insert s s' m1)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (return Map.empty) sortsSigma
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- compute the op map (as a Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding op_Map <- Map.foldWithKey (opFun rmap sort_Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (return Map.empty) (opMap sigma)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- compute the pred map (as a Map)
11c3b5180e1de6776035320b012a28bb146e7b46chuck pred_Map <- Map.foldWithKey (predFun rmap sort_Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (return Map.empty) (predMap sigma)
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- compute target signature
11c3b5180e1de6776035320b012a28bb146e7b46chuck let sigma' =
1d7f1b96b49dafbd6cb414fb709cb85de2686a72chuck {sortSet = Set.map (mapSort sort_Map) sortsSigma,
11c3b5180e1de6776035320b012a28bb146e7b46chuck Rel.map (mapSort sort_Map) (sortRel sigma),
11c3b5180e1de6776035320b012a28bb146e7b46chuck opMap = Map.foldWithKey (mapOps sort_Map op_Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Map.empty (opMap sigma),
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding assocOps = Map.foldWithKey (mapOps sort_Map op_Map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Map.empty (assocOps sigma),
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding predMap = Map.foldWithKey (mapPreds sort_Map pred_Map)
11c3b5180e1de6776035320b012a28bb146e7b46chuck Map.empty (predMap sigma),
1d7f1b96b49dafbd6cb414fb709cb85de2686a72chuck -- return assembled morphism
11c3b5180e1de6776035320b012a28bb146e7b46chuck return (embedMorphism extEm sigma sigma')
11c3b5180e1de6776035320b012a28bb146e7b46chuck { sort_map = sort_Map
11c3b5180e1de6776035320b012a28bb146e7b46chuck , fun_map = op_Map
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , pred_map = pred_Map }
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- the sorts of the source signature
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- sortFun is the sort map as a Haskell function
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingsortFun :: RawSymbolMap -> Id -> Result Id
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingsortFun rmap s =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- rsys contains the raw symbols to which s is mapped to
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if Set.null rsys then return s -- use default = identity mapping
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding return $ rawSymName $ Set.findMin rsys -- take the unique rsy
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding else plain_error s -- ambiguity! generate an error
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ("Sort " ++ showId s
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding " is mapped ambiguously: " ++ showDoc rsys "")
11c3b5180e1de6776035320b012a28bb146e7b46chuck $ getRange rsys
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- get all raw symbols to which s is mapped to
11c3b5180e1de6776035320b012a28bb146e7b46chuck rsys = Set.unions $ map ( \ x -> case Map.lookup x rmap of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding [ASymbol $ idToSortSymbol s, AnID s, AKindedId SortKind s]
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding {- to a Fun_map, add everything resulting from mapping (id, ots)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding according to rmap -}
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingopFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> Result Fun_map -> Result Fun_map
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingopFun rmap sort_Map ide ots m =
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- first consider all directly mapped profiles
11c3b5180e1de6776035320b012a28bb146e7b46chuck let (ots1,m1) = Set.fold (directOpMap rmap sort_Map ide) (Set.empty,m) ots
1ccd992d37d62c8cb2056126f2234f64ec189bfddougm -- now try the remaining ones with (un)kinded raw symbol
2e7198b49257c8221f16c2b5db657ae6897b0992orlikowski in case (Map.lookup (AKindedId FunKind ide) rmap,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Map.lookup (AnID ide) rmap) of
1d7f1b96b49dafbd6cb414fb709cb85de2686a72chuck (Just rsy1, Just rsy2) ->
11c3b5180e1de6776035320b012a28bb146e7b46chuck plain_error m'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ("Operation " ++ showId ide
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding " is mapped twice: "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc (rsy1, rsy2) "")
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ appRange (getRange rsy1) $ getRange rsy2
9b3001f2097437c3c605d29e353fda5131b9952bminfrin (Just rsy, Nothing) ->
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (Nothing, Just rsy) ->
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- Anything not mapped explicitly is left unchanged
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (Nothing,Nothing) -> m1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- try to map an operation symbol directly
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- collect all opTypes that cannot be mapped directly
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowedirectOpMap :: RawSymbolMap -> Sort_map -> Id -> OpType
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -> (Set.Set OpType,Result Fun_map)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -> (Set.Set OpType,Result Fun_map)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowedirectOpMap rmap sort_Map ide' ot (ots',m') =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe case Map.lookup (ASymbol (idToOpSymbol ide' ot)) rmap of
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Just rsy ->
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (ots',insertmapOpSym sort_Map ide' rsy ot m')
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Nothing -> (Set.insert ot ots',m')
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- map op symbol (ide,ot) to raw symbol rsy
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowemappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id,FunKind)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowemappedOpSym sort_Map ide ot rsy =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe let opSym = "Operation symbol " ++ showDoc (idToOpSymbol ide ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe " is mapped to "
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe in case rsy of
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe ASymbol (Symbol ide' (OpAsItemType ot')) ->
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe if compatibleOpTypes (mapOpType sort_Map ot) ot'
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe then return (ide',opKind ot')
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe else plain_error (ide, opKind ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (opSym ++ "type " ++ showDoc ot'
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe " but should be mapped to type " ++
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe showDoc (mapOpType sort_Map ot)"") $ getRange rsy
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe AnID ide' -> return (ide',opKind ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe AKindedId FunKind ide' -> return (ide',opKind ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe _ -> plain_error (ide,opKind ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (opSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe $ getRange rsy
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- insert mapping of op symbol (ide,ot) to raw symbol rsy into m
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwroweinsertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -> Result Fun_map -> Result Fun_map
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwroweinsertmapOpSym sort_Map ide rsy ot m = do
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (ide',kind') <- mappedOpSym sort_Map ide ot rsy
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe return (Map.insert (ide, ot {opKind = Partial}) (ide',kind') m1)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- insert mapping of op symbol (ide,ot) to itself into m
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -- map the ops in the source signature
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowemapOps :: Sort_map -> Fun_map -> Id -> Set.Set OpType -> OpMap -> OpMap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowemapOps sort_Map op_Map ide ots m =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe mapOp ot m1 =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe let (ide',ot') = mapOpSym sort_Map op_Map (ide,ot)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe in Rel.setInsert ide' ot' m1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe {- to a Pred_map, add evering resulting from mapping (ide,pts)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe according to rmap -}
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowepredFun :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe -> Result Pred_map -> Result Pred_map
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingpredFun rmap sort_Map ide pts m =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- first consider all directly mapped profiles
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let (pts1,m1) = Set.fold (directPredMap rmap sort_Map ide)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- now try the remaining ones with (un)kinded raw symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding in case (Map.lookup (AKindedId PredKind ide) rmap,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Map.lookup (AnID ide) rmap) of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Just rsy1, Just rsy2) ->
68ce856106f153813339db8670f6cd0ab8dea484minfrin plain_error m'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ("Predicate " ++ showId ide
d7387fcd4969206172e3a2a8bbcd25a3d7011ac5rbb " is mapped twice: " ++
11c3b5180e1de6776035320b012a28bb146e7b46chuck showDoc (rsy1, rsy2) "")
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ appRange (getRange rsy1) $ getRange rsy2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe (Just rsy, Nothing) ->
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Nothing, Just rsy) ->
68ce856106f153813339db8670f6cd0ab8dea484minfrin Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts1
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin -- Anything not mapped explicitly is left unchanged
68ce856106f153813339db8670f6cd0ab8dea484minfrin (Nothing,Nothing) -> m1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- try to map a predicate symbol directly
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- collect all predTypes that cannot be mapped directly
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingdirectPredMap :: RawSymbolMap -> Sort_map -> Id -> PredType
11c3b5180e1de6776035320b012a28bb146e7b46chuck -> (Set.Set PredType,Result Pred_map)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> (Set.Set PredType,Result Pred_map)
11c3b5180e1de6776035320b012a28bb146e7b46chuckdirectPredMap rmap sort_Map ide pt (pts,m) =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding case Map.lookup (ASymbol (idToPredSymbol ide pt)) rmap of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just rsy ->
11c3b5180e1de6776035320b012a28bb146e7b46chuck (pts,insertmapPredSym sort_Map ide rsy pt m)
11c3b5180e1de6776035320b012a28bb146e7b46chuck Nothing -> (Set.insert pt pts,m)
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- map pred symbol (ide,pt) to raw symbol rsy
11c3b5180e1de6776035320b012a28bb146e7b46chuckmappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id
11c3b5180e1de6776035320b012a28bb146e7b46chuckmappedPredSym sort_Map ide pt rsy =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let predSym = "Predicate symbol " ++ showDoc (idToPredSymbol ide pt)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding " is mapped to "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding in case rsy of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ASymbol (Symbol ide' (PredAsItemType pt')) ->
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if mapPredType sort_Map pt == pt'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding then return ide'
d7387fcd4969206172e3a2a8bbcd25a3d7011ac5rbb else plain_error ide
11c3b5180e1de6776035320b012a28bb146e7b46chuck (predSym ++ "type " ++ showDoc pt'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding " but should be mapped to type " ++
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding showDoc (mapPredType sort_Map pt) "") $ getRange rsy
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding AnID ide' -> return ide'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding AKindedId PredKind ide' -> return ide'
11c3b5180e1de6776035320b012a28bb146e7b46chuck _ -> plain_error ide
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (predSym ++ "symbol of wrong kind: " ++ showDoc rsy "")
1ccd992d37d62c8cb2056126f2234f64ec189bfddougm $ getRange rsy
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- insert mapping of pred symbol (ide,pt) to raw symbol rsy into m
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldinginsertmapPredSym :: Sort_map -> Id -> RawSymbol -> PredType
1ccd992d37d62c8cb2056126f2234f64ec189bfddougm -> Result Pred_map -> Result Pred_map
11c3b5180e1de6776035320b012a28bb146e7b46chuckinsertmapPredSym sort_Map ide rsy pt m = do
11c3b5180e1de6776035320b012a28bb146e7b46chuck ide' <- mappedPredSym sort_Map ide pt rsy
b999f6ba2a266bf9a92687f31bb7e76021ac5891ianh return (Map.insert (ide, pt) ide' m1)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- insert mapping of pred symbol (ide,pt) to itself into m
5babe00918c88eda487771fa6d6d4a1a19c0ced0chuck -- map the preds in the source signature
11c3b5180e1de6776035320b012a28bb146e7b46chuckmapPreds :: Sort_map -> Pred_map -> Id -> Set.Set PredType
b999f6ba2a266bf9a92687f31bb7e76021ac5891ianh -> Map.Map Id (Set.Set PredType) -> Map.Map Id (Set.Set PredType)
b999f6ba2a266bf9a92687f31bb7e76021ac5891ianhmapPreds sort_Map pred_Map ide pts m =
11c3b5180e1de6776035320b012a28bb146e7b46chuck Set.fold mapPred m pts
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding mapPred pt m1 =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let (ide',pt') = mapPredSym sort_Map pred_Map (ide,pt)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding in Rel.setInsert ide' pt' m1
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldinginducedFromToMorphism :: RawSymbolMap -> sign -> sign -> Result morphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingAlgorithm adapted from Bartek Klin's algorithm for CATS.
a2f9f38db0931e6edf7b71378dd680c3c5fa5841rbbInducing morphisms from raw symbol map and source and target signature.
5babe00918c88eda487771fa6d6d4a1a19c0ced0chuckThis problem is NP-hard (The problem of 3-colouring can be reduced to it).
5babe00918c88eda487771fa6d6d4a1a19c0ced0chuckThis means that we have exponential runtime in the worst case.
1ccd992d37d62c8cb2056126f2234f64ec189bfddougmHowever, in many cases the runtime can be kept rather short by
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingusing some basic principles of constraint programming.
2e41eca72bcc4167d1871b0941ee79845540d58eminfrinWe use a depth-first search with some weak form of constraint
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingpropagation and MRV (minimum remaining values), see
35c9e4d2c0a6465746a98958ef756114834461e6minfrinStuart Russell and Peter Norvig:
35c9e4d2c0a6465746a98958ef756114834461e6minfrinArtificial Intelligence - A Modern Approach.
11c3b5180e1de6776035320b012a28bb146e7b46chuckPrentice Hall International
35c9e4d2c0a6465746a98958ef756114834461e6minfrinThe algorithm has additionally to take care of default values (i.e.
8a1e3e302a46f468054887a62abdbd9c98f3daa5rbbsymbol names are mapped identically be default, and the number of
11c3b5180e1de6776035320b012a28bb146e7b46chuckidentitically mapped names should be maximized). Moreover, it does
11c3b5180e1de6776035320b012a28bb146e7b46chucknot suffice to find just one solution, but also its uniqueness
35c9e4d2c0a6465746a98958ef756114834461e6minfrin(among those maximizing he number of identitically mapped names)
35c9e4d2c0a6465746a98958ef756114834461e6minfrinmust be checked (still, MRV is useful here).
11c3b5180e1de6776035320b012a28bb146e7b46chuckThe algorithm
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrinInput: raw symbol map "rmap"
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin signatures "sigma1,sigma2"
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrinOutput: morphism "mor": sigma1 -> sigma2
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin1. compute the morphism mor1 induced by rmap and sigma1 (i.e. the renaming)
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin1.1. if target mor1 is a subsignature of sigma2, return the composition
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin of this inclusion with mor1
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin (cf. Theorem 6 of Bartek Klin's Master's Thesis)
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin2. let "posmap" be a map, mapping each symbol "sym1" from sigma1 to a pair
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin of sets of symbols (symset1, symset2) from sigma2 such that sym1
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin can be mapped to each sym2 in symset1 union symset2 (i.e., they are
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin both sorts or operations/predicates of the same arity, and
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin moreover, if there is a pair (rsym1,rsym2) in rmap such that sym1
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin matches rsym1, then rsym2 must match rsym2). Moreover, symset1
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin contains only symbols with names equal to that of sym1,
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin whereas symset2 contains only symbols with names different from
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin that of sym1.
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin3. let "akmap" (from Actually Known Map) be an empty symbol map.
35c9e4d2c0a6465746a98958ef756114834461e6minfrin//DEPTH-FIRST MRV SEARCH
35c9e4d2c0a6465746a98958ef756114834461e6minfrin//recursively called procedure, returning a symbol map or a special
35c9e4d2c0a6465746a98958ef756114834461e6minfrin//"No_map" value. Parameters are: sigma1, sigma2, akmap, posmap.
35c9e4d2c0a6465746a98958ef756114834461e6minfrinGET MRV (minimun remaining values) "VARIABLE"
e2b2e15108eb7cb566b1d70ce4e479276d951de5minfrin4a. if posmap is empty
11c3b5180e1de6776035320b012a28bb146e7b46chuck 4a.1. check if akmap defines a mapping from every symbol in
35c9e4d2c0a6465746a98958ef756114834461e6minfrin source mor1. (this should be vacuously true - Bartek?)
35c9e4d2c0a6465746a98958ef756114834461e6minfrin 4a.2. if yes, return akmap, otherwise return "No_map".
35c9e4d2c0a6465746a98958ef756114834461e6minfrin4b. take a pair sym1 |-> (symset1,symset2) with MRV from posmap
35c9e4d2c0a6465746a98958ef756114834461e6minfrin (i.e. one with minimal cardinality of symset1 union symset2).
35c9e4d2c0a6465746a98958ef756114834461e6minfrin But: prefer those with non-empty symset1!
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Remove it from posmap.
35c9e4d2c0a6465746a98958ef756114834461e6minfrin (For efficiency reasons, we also carry around an indexing of posmap
35c9e4d2c0a6465746a98958ef756114834461e6minfrin according to the cardinalities. Hence, posmap really is a pair
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (posmap1,posmap2).)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding5. for each symbol "sym2" from symset1
11c3b5180e1de6776035320b012a28bb146e7b46chuck CONSISTENCY CHECK
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.1. check if mapping sym1 to sym2 clashes with akmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (it can clash if sym1 and sym2 are operations/predicates,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding and mapping on their profiles clashes with what is already
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding known in akmap)
11c3b5180e1de6776035320b012a28bb146e7b46chuck 5.2. if yes, proceed with the next sym2 in step 5.
5babe00918c88eda487771fa6d6d4a1a19c0ced0chuck 5.3. add mapping of sym1 to sym2 to akmap.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding CONSTRAINT PROPAGATION (forward checking)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.4. if sym1 and sym2 are sorts
11c3b5180e1de6776035320b012a28bb146e7b46chuck 5.5. for each sub/supersort s of sym1, restrict the possible
11c3b5180e1de6776035320b012a28bb146e7b46chuck mappings of s in posmap to sub/supersorts of sym2
11c3b5180e1de6776035320b012a28bb146e7b46chuck 5.6. for each operation/predicate f in dom(posmap) involving
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sym1 in its argument or result sorts, restrict the
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding possible mappings of f in posmap accordingly
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (5.6. can be omitted for the sake of simplicity,
1ccd992d37d62c8cb2056126f2234f64ec189bfddougm since 5.1. does the necessary check as well)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.7. if sym1 and sym2 are operations/predicates,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.8. For corresponding sorts in their profiles,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding remove incompatible mappings of the sorts from posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.9. For each sym in overloading relation with sym1,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding remove incompatible mappings of sym from posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding CONTINUE DEPTH FIRST SERACH
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 5.10. call recursively point 4.
11c3b5180e1de6776035320b012a28bb146e7b46chuck6. if for exactly one sym2 step 5 gave a map, return this map.
11c3b5180e1de6776035320b012a28bb146e7b46chuck7. if step 5 gave more than one map, raise an exception. Morphism is
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding not unique.
11c3b5180e1de6776035320b012a28bb146e7b46chuck8. (only) if for no sym2 step 5 gave a map,
11c3b5180e1de6776035320b012a28bb146e7b46chuck repeat steps 5-7 with symset2 instead of symset1
11c3b5180e1de6776035320b012a28bb146e7b46chuck if this does not give a map either, return "No_map".
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding//end of the recursive procedure
9453de6a918fa711e99072b0e7b7c72ef39ef457chuck9. if procedure returned "No_map" or raised an exception, return error
11c3b5180e1de6776035320b012a28bb146e7b46chuck10. otherwise, return computed morphism from target mor1 to sigma2
11c3b5180e1de6776035320b012a28bb146e7b46chuck composed with mor1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- Some auxiliary functions for inducedFromToMorphism
2e41eca72bcc4167d1871b0941ee79845540d58eminfrintestMatch :: RawSymbolMap -> Symbol -> Symbol -> Bool
2e41eca72bcc4167d1871b0941ee79845540d58eminfrintestMatch rmap sym1 sym2 =
11c3b5180e1de6776035320b012a28bb146e7b46chuck Map.foldWithKey match1 True rmap
11c3b5180e1de6776035320b012a28bb146e7b46chuck match1 rsy1 rsy2 b = b && ((sym1 `matches` rsy1) <= (sym2 `matches`rsy2))
11c3b5180e1de6776035320b012a28bb146e7b46chuckcanBeMapped :: RawSymbolMap -> Symbol -> Symbol -> Bool
2e41eca72bcc4167d1871b0941ee79845540d58eminfrincanBeMapped rmap sym1@(Symbol {symbType = SortAsItemType})
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin sym2@(Symbol {symbType = SortAsItemType}) =
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin testMatch rmap sym1 sym2
2e41eca72bcc4167d1871b0941ee79845540d58eminfrincanBeMapped rmap sym1@(Symbol {symbType = OpAsItemType ot1})
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin sym2@(Symbol {symbType = OpAsItemType ot2}) =
effec4f1cfb63d440447b9869712e45e7a25c91aminfrin length (opArgs ot1) == length (opArgs ot2) && -- same arity
11c3b5180e1de6776035320b012a28bb146e7b46chuck opKind ot1 >= opKind ot2 && -- preservation of totality
11c3b5180e1de6776035320b012a28bb146e7b46chuck testMatch rmap sym1 sym2
2e41eca72bcc4167d1871b0941ee79845540d58eminfrincanBeMapped rmap sym1@(Symbol {symbType = PredAsItemType pt1})
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin sym2@(Symbol {symbType = PredAsItemType pt2}) =
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin length (predArgs pt1) == length (predArgs pt2) && -- same arity
11c3b5180e1de6776035320b012a28bb146e7b46chuck testMatch rmap sym1 sym2
11c3b5180e1de6776035320b012a28bb146e7b46chuckcanBeMapped _ _ _ = False
2e41eca72bcc4167d1871b0941ee79845540d58eminfrinpreservesName :: Symbol -> Symbol -> Bool
2e41eca72bcc4167d1871b0941ee79845540d58eminfrinpreservesName sym1 sym2 = symName sym1 == symName sym2
2e41eca72bcc4167d1871b0941ee79845540d58eminfrincompatibleSorts :: SymbolMap -> (SORT, SORT) -> Bool
2e41eca72bcc4167d1871b0941ee79845540d58eminfrincompatibleSorts smap (s1,s2) =
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin case Map.lookup (idToSortSymbol s1) smap of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Nothing -> True
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just sym -> symName sym == s2
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin-- try to extend a symbol map with a yet unmapped symbol
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin-- (this can fail if sym1 and sym2 are operations/predicates,
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin-- and mapping on their profiles clashes with what is already
9865751743e928ea0a9ad83faa04a738001932deminfrin-- known in akmap)
9865751743e928ea0a9ad83faa04a738001932deminfrinextendSymbMap :: SymbolMap -> Symbol -> Symbol -> Maybe SymbolMap
9865751743e928ea0a9ad83faa04a738001932deminfrinextendSymbMap akmap sym1 sym2 =
11c3b5180e1de6776035320b012a28bb146e7b46chuck if case symbType sym1 of
9865751743e928ea0a9ad83faa04a738001932deminfrin SortAsItemType -> True
2e41eca72bcc4167d1871b0941ee79845540d58eminfrin OpAsItemType ot1 -> case symbType sym2 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding OpAsItemType ot2 -> all (compatibleSorts akmap)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ zip (opRes ot1:opArgs ot1) (opRes ot2:opArgs ot2)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding PredAsItemType pt1 -> case symbType sym2 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding PredAsItemType pt2 -> all (compatibleSorts akmap)
11c3b5180e1de6776035320b012a28bb146e7b46chuck $ zip (predArgs pt1) (predArgs pt2)
11c3b5180e1de6776035320b012a28bb146e7b46chuck then Just $ Map.insert sym1 sym2 akmap
11c3b5180e1de6776035320b012a28bb146e7b46chuck else Nothing
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- Type for posmap
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- Each symbol is mapped to the set symbols it possibly can be mapped to
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- Additionally, we store a flag meaning "no default map" and the
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- cardinality of the symobl set
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- For efficiency reasons, we also carry around an indexing of posmap
11c3b5180e1de6776035320b012a28bb146e7b46chuck-- according to the pairs (flag,cardinality). Since several symbols
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- may lead to the same pair, we have to associate a list of symbols
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- (and corresponding symbol sets) with each pair.
af952917c05e56874069e1e5f64e6473bb478b68minfrin-- Hence, PosMap really is a pair to two maps.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingtype PosMap = (Map.Map Symbol (SymbolSet,(Bool,Int)),
af952917c05e56874069e1e5f64e6473bb478b68minfrin Map.Map (Bool,Int) [(Symbol,SymbolSet)])
af952917c05e56874069e1e5f64e6473bb478b68minfrin-- Some basic operations on PosMap
35c9e4d2c0a6465746a98958ef756114834461e6minfrin-- postpone entries with no default mapping and size > 1
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianhpostponeEntry :: Symbol -> SymbolSet -> Bool
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingpostponeEntry sym symset =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Set.null (Set.filter (preservesName sym) symset) && Set.size symset > 1
af952917c05e56874069e1e5f64e6473bb478b68minfrinremoveFromPosmap :: Symbol -> (Bool,Int) -> PosMap -> PosMap
af952917c05e56874069e1e5f64e6473bb478b68minfrinremoveFromPosmap sym card (posmap1,posmap2) =
af952917c05e56874069e1e5f64e6473bb478b68minfrin (Map.delete sym posmap1,
af952917c05e56874069e1e5f64e6473bb478b68minfrin Map.update removeSym1 card posmap2)
af952917c05e56874069e1e5f64e6473bb478b68minfrin removeSym [] = []
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe removeSym ((x,y):l) = if x==sym then l else (x,y):removeSym l
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe removeSym1 l = case removeSym l of
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe [] -> Nothing
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe l1 -> Just l1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwroweaddToPosmap :: Symbol -> SymbolSet -> PosMap -> PosMap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwroweaddToPosmap sym symset (posmap1,posmap2) =
af952917c05e56874069e1e5f64e6473bb478b68minfrin (Map.insert sym (symset,card) posmap1,
af952917c05e56874069e1e5f64e6473bb478b68minfrin listInsert card (sym,symset) posmap2)
af952917c05e56874069e1e5f64e6473bb478b68minfrin where card = (postponeEntry sym symset,Set.size symset)
af952917c05e56874069e1e5f64e6473bb478b68minfrin-- restrict posmap such that each symbol from symset1 is only mapped
35c9e4d2c0a6465746a98958ef756114834461e6minfrin-- to symbols from symset2
af952917c05e56874069e1e5f64e6473bb478b68minfrinrestrictPosMap :: SymbolSet -> SymbolSet -> PosMap -> PosMap
af952917c05e56874069e1e5f64e6473bb478b68minfrinrestrictPosMap symset1' symset2 posmap' =
af952917c05e56874069e1e5f64e6473bb478b68minfrin Set.fold restrictPosMap1 posmap' symset1'
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe restrictPosMap1 sym1 posmap@(posmap1,_posmap2) =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe case Map.lookup sym1 posmap1 of
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Nothing -> posmap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Just (symset1,card) ->
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe addToPosmap sym1 (symset1 `Set.intersection` symset2)
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe $ removeFromPosmap sym1 card posmap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe-- for each sub/supersort s of sym1 in sigma1, restrict the possible
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe-- mappings of s in posmap to sub/supersorts of sym2 in sigma2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowerestrictSorts ::
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe Symbol -> Symbol -> Sign f e -> Sign f e -> PosMap -> PosMap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowerestrictSorts sym1 sym2 sigma1 sigma2 posmap =
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe restrictPosMap subsyms1 subsyms2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe $ restrictPosMap supersyms1 supersyms2 posmap
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe s1 = symName sym1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe s2 = symName sym2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe sub1 = Set.insert s1 $ subsortsOf s1 sigma1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe sub2 = Set.insert s2 $ subsortsOf s2 sigma2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe subsyms1 = Set.map idToSortSymbol sub1
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe subsyms2 = Set.map idToSortSymbol sub2
2ceedfca3a2fdfdb5ff60ca17f030ce91f6331cbwrowe super1 = Set.insert s1 $ supersortsOf s1 sigma1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding super2 = Set.insert s2 $ supersortsOf s2 sigma2
11c3b5180e1de6776035320b012a28bb146e7b46chuck supersyms1 = Set.map idToSortSymbol super1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding supersyms2 = Set.map idToSortSymbol super2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- remove all sort mappings that map s1 to a sort different from s2
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingremoveIncompatibleSortMaps :: Maybe PosMap -> (SORT,SORT) -> Maybe PosMap
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingremoveIncompatibleSortMaps Nothing _ = Nothing
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingremoveIncompatibleSortMaps (Just posmap@(posmap1,_posmap2)) (s1,s2) =
3c59b18ce62f97468aaa5951d4e21a5478ef36ecminfrin case Map.lookup sym1 posmap1 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Nothing -> Just posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just (symset,card) ->
a2f9f38db0931e6edf7b71378dd680c3c5fa5841rbb -- is there some remaining possibility to map the sort?
3c59b18ce62f97468aaa5951d4e21a5478ef36ecminfrin if sym2 `Set.member` symset
a2f9f38db0931e6edf7b71378dd680c3c5fa5841rbb then Just $ addToPosmap sym1 (Set.singleton sym2)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ removeFromPosmap sym1 card posmap
3c59b18ce62f97468aaa5951d4e21a5478ef36ecminfrin -- if not, there is no map!
11c3b5180e1de6776035320b012a28bb146e7b46chuck else Nothing
3c59b18ce62f97468aaa5951d4e21a5478ef36ecminfrin sym1 = idToSortSymbol s1
3c59b18ce62f97468aaa5951d4e21a5478ef36ecminfrin sym2 = idToSortSymbol s2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- For corresponding sorts in profiles of sym1 and sym2,
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- remove incompatible mappings of the sorts from posmap
11c3b5180e1de6776035320b012a28bb146e7b46chuckrestrictOps :: Symbol -> Symbol -> PosMap -> Maybe PosMap
11c3b5180e1de6776035320b012a28bb146e7b46chuckrestrictOps sym1 sym2 posmap =
11c3b5180e1de6776035320b012a28bb146e7b46chuck foldl removeIncompatibleSortMaps (Just posmap) $ zip sort1 sorts2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (sort1,sorts2) = case (symbType sym1,symbType sym2) of
11c3b5180e1de6776035320b012a28bb146e7b46chuck (OpAsItemType ot1,OpAsItemType ot2) ->
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (opRes ot1:opArgs ot1,opRes ot2:opArgs ot2)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (PredAsItemType pt1,PredAsItemType pt2) ->
11c3b5180e1de6776035320b012a28bb146e7b46chuck (predArgs pt1,predArgs pt2)
11c3b5180e1de6776035320b012a28bb146e7b46chuck _ -> ([],[])
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- the main function
9c70fe7952482a4b0bae89806525243c63a28212orlikowskiinducedFromToMorphism :: (Pretty f, Pretty e, Pretty m)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding => m -- ^ extended morphism
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> (e -> e -> Bool) -- ^ subsignature test of extensions
066877f1a045103acfdd376d48cdd473c33f409bdougm -> RawSymbolMap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> ExtSign (Sign f e) Symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> ExtSign (Sign f e) Symbol -> Result (Morphism f e m)
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldinginducedFromToMorphism extEm isSubExt rmap (ExtSign sigma1 sy1)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (ExtSign sigma2 sy2) = do
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let symset1 = symOf sigma1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding symset2 = symOf sigma2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 1. use rmap to get a renaming...
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding mor1 <- inducedFromMorphism extEm rmap sigma1
11c3b5180e1de6776035320b012a28bb146e7b46chuck -- 1.1 ... is the renamed source signature contained in the target signature?
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if isSubSig isSubExt (mtarget mor1) sigma2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- yes => we are done
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding then return (mor1 {mtarget = sigma2})
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- no => OK, we've to take the hard way
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding else let so1 = Set.findMin sy1
529005244758297d4415aa912c67a67f805349bcianh so2 = Set.findMin sy2 in
529005244758297d4415aa912c67a67f805349bcianh if Map.null rmap && Set.size sy1 == 1 && Set.size sy2 == 1
529005244758297d4415aa912c67a67f805349bcianh && symbType so1 == SortAsItemType && symbType so1 == SortAsItemType
529005244758297d4415aa912c67a67f805349bcianh then return mor1
529005244758297d4415aa912c67a67f805349bcianh { mtarget = sigma2
529005244758297d4415aa912c67a67f805349bcianh , sort_map = Map.singleton (symName so1)
529005244758297d4415aa912c67a67f805349bcianh $ symName so2 }
529005244758297d4415aa912c67a67f805349bcianh else do -- 2. Compute initial posmap, using all possible mappings of symbols
529005244758297d4415aa912c67a67f805349bcianh let addCard sym s = (s,(postponeEntry sym s,Set.size s))
529005244758297d4415aa912c67a67f805349bcianh ins1 sym = Map.insert sym
529005244758297d4415aa912c67a67f805349bcianh (addCard sym $ Set.filter (canBeMapped rmap sym) symset2)
529005244758297d4415aa912c67a67f805349bcianh ins2 sym1a (symset,card) = listInsert card (sym1a,symset)
529005244758297d4415aa912c67a67f805349bcianh posmap = (posmap1,posmap2)
93aa7afe1af831ee8b23aa0d97323c388e3fb8d3ianh -- Are there symbols that cannot be mapped at all?
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- Then generate an error immediately
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding --trace ("posmap1= "++showDoc posmap1 "") (return ())
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding case Map.lookup (True,0) posmap2 of
a2f9f38db0931e6edf7b71378dd680c3c5fa5841rbb Nothing -> return ()
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just syms -> fail $ "No symbol mapping for "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc (map fst syms) ""
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 3. call recursive function with empty akmap and initial posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding smap <- tryToInduce sigma1 sigma2 Map.empty posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding smap1 <- case smap of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Nothing -> fatal_error
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding "No signature morphism for symbol map found"
529005244758297d4415aa912c67a67f805349bcianh $ concatMapRange getRange $ Map.keys rmap
529005244758297d4415aa912c67a67f805349bcianh Just x -> return x
529005244758297d4415aa912c67a67f805349bcianh -- 9./10. compute and return the resulting morphism
529005244758297d4415aa912c67a67f805349bcianh symbMapToMorphism extEm sigma1 sigma2 smap1
529005244758297d4415aa912c67a67f805349bcianh -- 4. recursive depth first function
529005244758297d4415aa912c67a67f805349bcianh -- ambiguous map leads to fatal error (similar to exception)
529005244758297d4415aa912c67a67f805349bcianhtryToInduce :: Sign f e -> Sign f e -> SymbolMap -> PosMap
529005244758297d4415aa912c67a67f805349bcianh -> Result (Maybe SymbolMap)
529005244758297d4415aa912c67a67f805349bcianhtryToInduce sigma1 sigma2 akmap (posmap1, posmap2) = do
529005244758297d4415aa912c67a67f805349bcianh --trace("akmap: "++showDoc akmap "") (return ())
529005244758297d4415aa912c67a67f805349bcianh if Map.null posmap2 then return $ Just akmap -- 4a.
529005244758297d4415aa912c67a67f805349bcianh --trace ("trying to map: "++showDoc sym1 "") (return ())
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding case akmap1 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 6. no map for symset1, hence try symset2
11c3b5180e1de6776035320b012a28bb146e7b46chuck Nothing -> tryToInduce1 sigma1 sigma2 akmap posmap' sym1 symset2
11c3b5180e1de6776035320b012a28bb146e7b46chuck Just _ -> return akmap1
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 4b. take symbol with minimal remaining values (MRV)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (card,(sym1,symset):_symsets) = Map.findMin posmap2
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (symset1,symset2) = Set.partition (preservesName sym1) symset
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding posmap' = removeFromPosmap sym1 card (posmap1,posmap2)
a6314dfa8dd8a0d69db16288581e4950a2dd3955minfrin -- 5. to 7.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingtryToInduce1 :: Sign f e -> Sign f e -> SymbolMap -> PosMap -> Symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> Set.Set Symbol -> Result (Maybe SymbolMap)
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingtryToInduce1 sigma1 sigma2 akmap posmap sym1 symset = do
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Set.fold (tryToInduce2 sigma1 sigma2 akmap posmap sym1)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (return Nothing) symset
11c3b5180e1de6776035320b012a28bb146e7b46chucktryToInduce2 :: Sign f e -> Sign f e -> SymbolMap -> PosMap -> Symbol
dd30db1d9a88526ceda100b61aad90168a2cb98cminfrin -> Symbol -> Result (Maybe SymbolMap)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -> Result (Maybe SymbolMap)
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingtryToInduce2 sigma1 sigma2 akmap posmap sym1 sym2 akmapSoFar = do
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 5.1. to 5.3. consistency check
066877f1a045103acfdd376d48cdd473c33f409bdougm akmapSoFar1 <- akmapSoFar
11c3b5180e1de6776035320b012a28bb146e7b46chuck {-(trace ("map "++(case akmapSoFar1 of
dd30db1d9a88526ceda100b61aad90168a2cb98cminfrin Just x -> showDoc x " + "
a6314dfa8dd8a0d69db16288581e4950a2dd3955minfrin Nothing -> "")
a6314dfa8dd8a0d69db16288581e4950a2dd3955minfrin ++showDoc sym1 " |-> " ++showDoc sym2 "; stopBackTrack: "
a6314dfa8dd8a0d69db16288581e4950a2dd3955minfrin ++show stopBackTrack) (return ())) -}
a6314dfa8dd8a0d69db16288581e4950a2dd3955minfrin case extendSymbMap akmap sym1 sym2 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Nothing -> return Nothing
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- constraint propagation
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just akmap1 -> do
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let posmap1 = case symbType sym1 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 5.4./5.5. constraint propagation for a sort symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding SortAsItemType ->
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just $ restrictSorts sym1 sym2 sigma1 sigma2 posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 5.6. omitted so far (not really necessary)
a2f9f38db0931e6edf7b71378dd680c3c5fa5841rbb -- 5.7./5.8. constraint propagation
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- for an operation/predicate symbol
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding _ -> restrictOps sym1 sym2 posmap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 5.9. omitted until overload relation will be available !!??
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding case posmap1 of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Just posmap2 -> do
10a4cdd68ef1ca0e54af296fe1d08ac00150c90bwrowe tryToInduce sigma1 sigma2 akmap1 posmap2
11c3b5180e1de6776035320b012a28bb146e7b46chuck _ -> return Nothing
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- 6./7. uniqueness check
066877f1a045103acfdd376d48cdd473c33f409bdougm case (akmap',akmapSoFar1) of
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding -- stop backtracking next time if there haven't been new sort maps
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Nothing,Nothing) -> return Nothing
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Just smap,Nothing) -> return $ Just smap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Nothing,Just smap) -> return $ Just smap
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Just smap1, Just smap2) ->
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding let shorten = Map.filterWithKey (/=) in
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding fatal_error (shows
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (text "Ambiguous symbol map" $+$
11c3b5180e1de6776035320b012a28bb146e7b46chuck text "Map1" <+> pretty (shorten smap1) $+$
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding text "Map2" <+> pretty (shorten smap2) $+$
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding text "Please, supply a unique fitting morphism")
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding "") $ concatMapRange getRange $ Map.elems $ shorten smap1
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingComputing signature generated by a symbol set.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingAlgorithm adapted from Bartek Klin's algorithm for CATS.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingInput: symbol set "Syms"
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding signature "Sigma"
11c3b5180e1de6776035320b012a28bb146e7b46chuckOutput: signature "Sigma1"<=Sigma.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding1. get a set "Sigma_symbols" of symbols in Sigma.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding2. if Syms is not a subset of Sigma_symbols, return error.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding3. let Sigma1 be an empty signature.
066877f1a045103acfdd376d48cdd473c33f409bdougm4. for each symbol "Sym" in Syms do:
11c3b5180e1de6776035320b012a28bb146e7b46chuck 4.1. if Sym is a:
acb685561ae13c9216c96383ce260ed88ea663b2orlikowski 4.1.1. sort "S": add sort S to Sigma1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 4.1.2. total function "F" with profile "Fargs,Fres":
11c3b5180e1de6776035320b012a28bb146e7b46chuck 4.1.2.1. add all sorts from Fargs to Sigma1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 4.1.2.2. add sort Fres to Sigma1.
11c3b5180e1de6776035320b012a28bb146e7b46chuck 4.1.2.3. add F with the needed profile to Sigma1.
407cde44becba3694e7c3d81ac99b5d86f4b03a9rbb 4.1.3. partial function: as in 4.1.2.
11c3b5180e1de6776035320b012a28bb146e7b46chuck 4.1.4. predicate: as in 4.1.2., except that Fres is omitted.
407cde44becba3694e7c3d81ac99b5d86f4b03a9rbb5. get a list "Sig_sub" of subsort relations in Sigma.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding6. for each pair "S1,S2" in Sig_sub do:
11c3b5180e1de6776035320b012a28bb146e7b46chuck 6.1. if S1,S2 are sorts in Sigma1, add "S1,S2" to sort relations in
11c3b5180e1de6776035320b012a28bb146e7b46chuck7. return the inclusion of sigma1 into sigma.
407cde44becba3694e7c3d81ac99b5d86f4b03a9rbbgeneratedSign :: m -> SymbolSet -> Sign f e -> Result (Morphism f e m)
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldinggeneratedSign extEm sys sigma =
11c3b5180e1de6776035320b012a28bb146e7b46chuck if not (sys `Set.isSubsetOf` symset) -- 2.
11c3b5180e1de6776035320b012a28bb146e7b46chuck then let diffsyms = sys Set.\\ symset in
11c3b5180e1de6776035320b012a28bb146e7b46chuck fatal_error ("Revealing: The following symbols "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc diffsyms " are not in the signature")
11c3b5180e1de6776035320b012a28bb146e7b46chuck $ getRange diffsyms
407cde44becba3694e7c3d81ac99b5d86f4b03a9rbb else return $ embedMorphism extEm sigma2 sigma -- 7.
11c3b5180e1de6776035320b012a28bb146e7b46chuck symset = symOf sigma -- 1.
11c3b5180e1de6776035320b012a28bb146e7b46chuck sigma1 = Set.fold revealSym (sigma { sortSet = Set.empty
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , predMap = Map.empty }) sys -- 4.
11c3b5180e1de6776035320b012a28bb146e7b46chuck sigma2 = sigma1 {sortRel = sortRel sigma `Rel.restrict` sortSet sigma1}
11c3b5180e1de6776035320b012a28bb146e7b46chuckrevealSym :: Symbol -> Sign f e -> Sign f e
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingrevealSym sy sigma1 = case symbType sy of -- 4.1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding SortAsItemType -> -- 4.1.1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sigma1 {sortSet = Set.insert (symName sy) $ sortSet sigma1}
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding OpAsItemType ot -> -- 4.1.2./4.1.3.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sigma1 {sortSet = foldr Set.insert (sortSet sigma1) (opRes ot:opArgs ot),
11c3b5180e1de6776035320b012a28bb146e7b46chuck opMap = Rel.setInsert (symName sy) ot $ opMap sigma1}
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding PredAsItemType pt -> -- 4.1.4.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sigma1 {sortSet = foldr Set.insert (sortSet sigma1) (predArgs pt),
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding predMap = Rel.setInsert (symName sy) pt $ predMap sigma1}
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingComputing signature co-generated by a raw symbol set.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingAlgorithm adapted from Bartek Klin's algorithm for CATS.
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingInput: symbol set "Syms"
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding signature "Sigma"
11c3b5180e1de6776035320b012a28bb146e7b46chuckOutput: signature "Sigma1"<=Sigma.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding1. get a set "Sigma_symbols" of symbols in Sigma.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding2. if Syms is not a subset of Sigma_symbols, return error.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding3. for each symbol "Sym" in Syms do:
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 3.1. if Sym is a:
af952917c05e56874069e1e5f64e6473bb478b68minfrin 3.1.1. sort "S":
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 3.1.1.1. Remove S from Sigma_symbols
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding 3.1.1.2. For each function/predicate symbol in
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh Sigma_symbols, if its profile contains S
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh remove it from Sigma_symbols.
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh 3.1.2. any other symbol: remove if from Sigma_symbols.
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh4. let Sigma1 be a signature generated by Sigma_symbols in Sigma.
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh5. return the inclusion of sigma1 into sigma.
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianhcogeneratedSign :: m -> SymbolSet -> Sign f e
ff1234e45aca1b8171d711ecb87f58b9d9100a99ianh -> Result (Morphism f e m)
0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingcogeneratedSign extEm symset sigma =
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding if {-trace ("symset "++show symset++"\nsymset0 "++show symset0)-}
11c3b5180e1de6776035320b012a28bb146e7b46chuck (not (symset `Set.isSubsetOf` symset0)) -- 2.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding then let diffsyms = symset Set.\\ symset0 in
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding fatal_error ("Hiding: The following symbols "
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding ++ showDoc diffsyms " are not in the signature")
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ getRange diffsyms
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding else generatedSign extEm symset1 sigma -- 4./5.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding symset0 = symOf sigma -- 1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding symset1 = Set.fold revealSym' symset0 symset -- 3.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding revealSym' sy symset1' = case symbType sy of -- 3.1.
af952917c05e56874069e1e5f64e6473bb478b68minfrin SortAsItemType -> -- 3.1.1.
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding Set.filter (not . profileContains (symName sy) . symbType)
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding $ Set.delete sy symset1'
0f081398cf0eef8cc7c66a535d450110a92dc8aefielding OpAsItemType _ -> -- 3.1.2
35c9e4d2c0a6465746a98958ef756114834461e6minfrin PredAsItemType _ -> -- 3.1.2
35c9e4d2c0a6465746a98958ef756114834461e6minfrin profileContains _ SortAsItemType = False
35c9e4d2c0a6465746a98958ef756114834461e6minfrin profileContains s (OpAsItemType ot) = s `elem` (opRes ot:opArgs ot)
35c9e4d2c0a6465746a98958ef756114834461e6minfrin profileContains s (PredAsItemType pt) = s `elem` (predArgs pt)
35c9e4d2c0a6465746a98958ef756114834461e6minfrinfinalUnion :: (e -> e -> e) -- ^ join signature extensions
35c9e4d2c0a6465746a98958ef756114834461e6minfrin -> Sign f e -> Sign f e -> Result (Sign f e)
35c9e4d2c0a6465746a98958ef756114834461e6minfrinfinalUnion addSigExt sigma1 sigma2 = return $ addSig addSigExt sigma1 sigma2
35c9e4d2c0a6465746a98958ef756114834461e6minfrin -- ??? Finality check not yet implemented
35c9e4d2c0a6465746a98958ef756114834461e6minfrin-- | Insert into a list of values
35c9e4d2c0a6465746a98958ef756114834461e6minfrinlistInsert :: Ord k => k -> a -> Map.Map k [a] -> Map.Map k [a]
35c9e4d2c0a6465746a98958ef756114834461e6minfrinlistInsert kx x t = Map.insert kx (x : Map.findWithDefault [] kx t) t