Morphism.hs revision 26d11a256b1433604a3dbc69913b520fff7586ac
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichMaintainer : maeder@tzi.de
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichStability : provisional
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichPortability : portable
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik DietrichSymbols and signature morphisms for the CASL logic
9378a7d0065818b541d989837dae2d9a89154007Dominik Dietrichissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichthe qualification only applies to __+__ !
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichpossibly reuse SYMB_KIND for Kind
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichimport qualified Common.Lib.Map as Map
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichimport qualified Common.Lib.Set as Set
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichimport qualified Common.Lib.Rel as Rel
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichtype SymbolSet = Set.Set Symbol
eb8b603d56ab4beb9a66d186c430a66383588de3Dominik Dietrichtype SymbolMap = Map.Map Symbol Symbol
type RawSymbolSet = Set.Set RawSymbol
type RawSymbolMap = Map.Map RawSymbol RawSymbol
type Sort_map = Map.Map SORT SORT
type Fun_map = Map.Map (Id,OpType) (Id, FunKind)
type Pred_map = Map.Map (Id,PredType) Id
mapSort sorts s = Map.findWithDefault s s sorts
mapOpType sorts t = if Map.null sorts then t else
case Map.lookup (i, ot {opKind = Partial} ) fMap of
mapPredType sorts t = if Map.null sorts then t else
(Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)
, sort_map = Map.empty
, fun_map = Map.empty
, pred_map = Map.empty
let sorts = Set.map idToSortSymbol $ sortSet sigma
ops = Set.fromList $
$ Set.toList ts) $
Map.toList $ opMap sigma
preds = Set.fromList $
$ Set.toList ts) $
Map.toList $ predMap sigma
in Set.unions [sorts, ops, preds]
foldl insertRsys (return Map.empty) (concat ls)
case Map.lookup rsy1 m1 of
Nothing -> return $ Map.insert rsy1 rsy2 m1
case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap
Map.insert s t m
mapFun i ots m = Set.fold (insFun i) m ots
case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap
else Map.insert (i, ot {opKind = Partial}) (j, k) m
mapPred i pts m = Set.fold (insPred i) m pts
case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap
PredAsItemType _ -> if i == j then m else Map.insert (i, pt) j m
Map.empty $ sortSet src
opSymMap = Map.foldWithKey
( \ i s m -> Set.fold
( \ t -> Map.insert (idToOpSymbol i t)
Map.empty $ opMap src
predSymMap = Map.foldWithKey
( \ i s m -> Set.fold
( \ t -> Map.insert (idToPredSymbol i t)
Map.empty $ predMap src
foldr Map.union sortSymMap [opSymMap,predSymMap]
sMap = if Map.null sMap2 then sMap1 else
Set.fold ( \ i ->
if i == j then id else Map.insert i j)
Map.empty $ sortSet src
fun_map = if Map.null fMap2 then fMap1 else
Map.foldWithKey ( \ i t m ->
Set.fold ( \ ot ->
Map.insert (i, ot {opKind = Partial }) (ni, k)) m t)
Map.empty $ opMap src,
pred_map = if Map.null pMap2 then pMap1 else
Map.foldWithKey ( \ i t m ->
Set.fold ( \ pt ->
if i == ni then id else Map.insert (i, pt) ni) m t)
Map.empty $ predMap src,
Map.foldWithKey (\s sset b -> b && legalSort s && all legalSort
(Set.toList sset))
True (Rel.toMap (sortRel sigma))
legalSort s = Set.member s sorts
msorts = Set.map (mapSort smap) $ sortSet s1
mops = Map.foldWithKey ( \ i ->
flip $ Set.fold ( \ ot ->
mpreds = Map.foldWithKey ( \ i ->
flip $ Set.fold ( \ pt ->
&& Set.isSubsetOf msorts (sortSet s2)
uo1 = foldr delOp (opMap s1) $ Map.keys omap1
uo2 = foldr delOp (opMap s2) $ Map.keys omap2
delOp (n, ot) m = diffMapSet m $ Map.singleton n $
Set.fromList [ot {opKind = Partial}, ot {opKind =Total}]
up1 = foldr delPred (predMap s1) $ Map.keys pmap1
up2 = foldr delPred (predMap s2) $ Map.keys pmap2
(sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
Nothing -> (ds, Map.insert i j m)
(Map.toList smap2 ++ map (\ a -> (a, a))
case Map.lookup isc m of
Nothing -> (ds, Map.insert isc jsc m)
else (ds, Map.insert isc (j, Total) m) else
(sds, omap1) (Map.toList omap2 ++ concatMap
case Map.lookup isc m of
Nothing -> (ds, Map.insert isc j m)
(Map.toList pmap2 ++ concatMap ( \ (a, s) -> map
sort_map = Map.filterWithKey (/=) smap,
fun_map = Map.filterWithKey
(\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot
pred_map = Map.filterWithKey (\ (i, _) j -> i /= j) pmap,
src = Map.keys sm
where src = Map.keys symmap
pretty (Map.filterWithKey (/=) $ morphismToSymbMap mor)