Morphism.hs revision 4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederModule : $Header$
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederDescription : Symbols and signature morphisms for the CASL logic
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederMaintainer : Christian.Maeder@dfki.de
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederStability : provisional
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederPortability : portable
ff9ef2b186549bc431f5d86b096575aa48963b01Christian MaederSymbols and signature morphisms for the CASL logic
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederthe qualification only applies to __+__ !
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederpossibly reuse SYMB_KIND for Kind
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederimport qualified Data.Map as Map
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederimport qualified Data.Set as Set
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederimport qualified Common.Lib.Rel as Rel
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maedertype SymbolSet = Set.Set Symbol
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maedertype SymbolMap = Map.Map Symbol Symbol
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maeder deriving (Show, Eq, Ord)
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maederinstance PosItem RawSymbol where
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maeder getRange rs =
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maeder ASymbol s -> getRange s
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maeder AnID i -> getRange i
ff9ef2b186549bc431f5d86b096575aa48963b01Christian Maeder AKindedId _ i -> getRange i
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
sorts = Set.map idToSortSymbol $ sortSet sigma
ops = Set.fromList $
concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t) $ Set.toList ts)
$ Map.toList $ opMap sigma
preds = Set.fromList $
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
mops = Map.foldWithKey ( \ i ->
flip $ Set.fold ( \ ot ->
mpreds = Map.foldWithKey ( \ i ->
flip $ Set.fold ( \ pt ->
&& Set.isSubsetOf (msorts $ sortSet s1) (sortSet s2)
&& Set.isSubsetOf (msorts $ emptySortSet s1) (emptySortSet 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 $ Set.difference (symOf tar) $ symOf src ]
[ pretty (Map.filterWithKey (/=) $ morphismToSymbMap mor)