57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , FlexibleInstances, DeriveDataTypeable #-}
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiDescription : Symbols and signature morphisms for the CASL logic
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian MaederPortability : non-portable (MPTC+FD)
e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiSymbols and signature morphisms for the CASL logic
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , RawSymbol (..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , Morphism (..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , DefMorExt (..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , emptyMorExt
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , MorphismExtension (..)
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , isInclusionMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , isSortInjective
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , isInjective
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , embedMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , sigInclusion
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , plainMorphismUnion
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , morphismUnion
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , morphismUnionM
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , idOrInclMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , morphismToSymbMap
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , typedSymbKindToRaw
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , symbolToRaw
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , mapPredType
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , compatibleOpTypes
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , imageOfMorphism
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , RawSymbolMap
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , InducedSign
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , inducedSignAux
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , inducedOpMap
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , inducedPredMap
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , statSymbMapItems
351391e0e3226210e7ffb183b334da9f96de36eaChristian Maeder , statSymbItems
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Set as Set
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maederimport qualified Common.Lib.MapSet as MapSet
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Common.Lib.Rel as Rel
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maederimport Common.Utils (composeMap)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype SymbolSet = Set.Set Symbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype SymbolMap = Map.Map Symbol Symbol
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maederdata RawSymbol = ASymbol Symbol | AKindedSymb SYMB_KIND Id
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder deriving (Show, Eq, Ord, Typeable, Data)
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maederinstance GetRange RawSymbol where
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder getRange rs = case rs of
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich ASymbol s -> getRange s
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb _ i -> getRange i
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedertype Sort_map = Map.Map SORT SORT
c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu-- always use the partial profile as key!
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maedertype Op_map = Map.Map (Id, OpType) (Id, OpKind)
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maedertype Pred_map = Map.Map (Id, PredType) Id
8e80792f474d154ff11762fac081a422e34f1accChristian Maederdata Morphism f e m = Morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { msource :: Sign f e
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , mtarget :: Sign f e
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , sort_map :: Sort_map
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder , op_map :: Op_map
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , pred_map :: Pred_map
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , extended_map :: m
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder } deriving (Show, Eq, Ord, Typeable, Data)
1a38107941725211e7c3f051f7a8f5e12199f03acmaederdata DefMorExt e = DefMorExt e deriving (Typeable, Data)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance Show (DefMorExt e) where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder show = const ""
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance Ord (DefMorExt e) where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder compare _ = const EQ
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maederinstance Eq (DefMorExt e) where
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder (==) e = (== EQ) . compare e
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian MaederemptyMorExt :: DefMorExt e
e6dccba746efe07338d3107fed512e713fd50b28Christian MaederemptyMorExt = DefMorExt $ error "emptyMorExt"
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Pretty (DefMorExt e) where
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder pretty _ = empty
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederclass (Pretty e, Pretty m) => MorphismExtension e m | m -> e where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder ideMorphismExtension :: e -> m
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder composeMorphismExtension :: Morphism f e m -> Morphism f e m -> Result m
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder inverseMorphismExtension :: Morphism f e m -> Result m
9a6779c8495854bdf36e4a87f98f095e8d0a6e45Christian Maeder inverseMorphismExtension = return . extended_map
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder isInclusionMorphismExtension :: m -> Bool
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder prettyMorphismExtension :: Morphism f e m -> Doc
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder prettyMorphismExtension = pretty . extended_map
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder legalMorphismExtension :: Morphism f e m -> Result ()
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder legalMorphismExtension _ = return ()
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maederinstance MorphismExtension () () where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder ideMorphismExtension _ = ()
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder composeMorphismExtension _ = return . extended_map
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder isInclusionMorphismExtension _ = True
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance Pretty e => MorphismExtension e (DefMorExt e) where
351145cfe8c03b4d47133c96b209f2bd6cfbf504Christian Maeder ideMorphismExtension _ = emptyMorExt
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder composeMorphismExtension _ = return . extended_map
81101b83a042f5a1bdeeef93b1b49aff05817e44Christian Maeder isInclusionMorphismExtension _ = True
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maedertype CASLMor = Morphism () () ()
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederisInclusionMorphism :: (m -> Bool) -> Morphism f e m -> Bool
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederisInclusionMorphism f m = f (extended_map m) && Map.null (sort_map m)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder && Map.null (pred_map m) && isInclOpMap (op_map m)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapSort :: Sort_map -> SORT -> SORT
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapSort sorts s = Map.findWithDefault s s sorts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapOpType :: Sort_map -> OpType -> OpType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapOpType sorts t = if Map.null sorts then t else
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder t { opArgs = map (mapSort sorts) $ opArgs t
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , opRes = mapSort sorts $ opRes t }
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermakeTotal :: OpKind -> OpType -> OpType
03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermakeTotal fk t = case fk of
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder Total -> mkTotal t
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermapOpSym :: Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermapOpSym sMap oMap (i, ot) = let mot = mapOpType sMap ot in
6a22b2854c3bc9cb4877cb7d29049d6559238639Christian Maeder case Map.lookup (i, mkPartial ot) oMap of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> (i, mot)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just (j, k) -> (j, makeTotal k mot)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder-- | Check if two OpTypes are equal modulo totality or partiality
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicompatibleOpTypes :: OpType -> OpType -> Bool
4e14c1bc2b97679b84c6ad996fa11c273b74ea02Christian MaedercompatibleOpTypes ot1 ot2 = opSorts ot1 == opSorts ot2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapPredType :: Sort_map -> PredType -> PredType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapPredType sorts t = if Map.null sorts then t else
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder t { predArgs = map (mapSort sorts) $ predArgs t }
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaedermapPredSym sMap oMap (i, pt) =
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder (Map.findWithDefault i (i, pt) oMap, mapPredType sMap pt)
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederembedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m
26d11a256b1433604a3dbc69913b520fff7586acChristian MaederembedMorphism extEm a b = Morphism
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { msource = a
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , mtarget = b
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , extended_map = extEm }
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder-- | given empty extensions convert a morphism
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapCASLMor :: e -> m -> Morphism f1 e1 m1 -> Morphism f e m
b5056cf24da461ee868c4be7b803a76b677fa21dChristian MaedermapCASLMor e me m =
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder (embedMorphism me (embedSign e $ msource m) $ embedSign e $ mtarget m)
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder { sort_map = sort_map m
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , op_map = op_map m
b5056cf24da461ee868c4be7b803a76b677fa21dChristian Maeder , pred_map = pred_map m }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbolToRaw :: Symbol -> RawSymbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedersymbolToRaw = ASymbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToRaw :: Id -> RawSymbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaederidToRaw = AKindedSymb Implicit
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrawSymName :: RawSymbol -> Id
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederrawSymName rs = case rs of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ASymbol sym -> symName sym
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb _ i -> i
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersortSyms :: Sign f e -> SymbolSet
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersortSyms = Set.map idToSortSymbol . sortSet
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederopSyms :: Sign f e -> [Symbol]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederopSyms = map (uncurry idToOpSymbol) . mapSetToList . opMap
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederpredSyms :: Sign f e -> [Symbol]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaederpredSyms = map (uncurry idToPredSymbol) . mapSetToList . predMap
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder{- | returns the symbol sets of the signature in the correct dependency order
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder, i.e., sorts first, then ops and predicates. Result list is of length two. -}
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzsymOf :: Sign f e -> [SymbolSet]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersymOf s = [ sortSyms s, Set.fromList $ predSyms s ++ opSyms s ]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersigSymsOf :: Sign f e -> [Symbol]
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian MaedersigSymsOf s = concat
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , map (\ (a, b) -> Symbol a $ SubsortAsItemType b)
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder . Rel.toList . Rel.transReduce . Rel.irreflex $ sortRel s
4e3c46a1ca40d50a045342c5fab25b5db4fa9a87Christian Maeder -- assume sort relation to be the transitive closure
ef60398f3b9f24614b074f8f0f1349ab527e1c77Christian Maeder , predSyms s ]
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst Schulz-- | set of symbols for a signature
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzsymsetOf :: Sign f e -> SymbolSet
bdf2e01977470bedcb4425e2dadabc9e9f6ba149Ewaryst SchulzsymsetOf = Set.unions . symOf
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercheckSymbList :: [SYMB_OR_MAP] -> [Diagnosis]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian MaedercheckSymbList l = case l of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder Symb (Symb_id a) : Symb (Qual_id b t _) : r -> mkDiag Warning
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ("profile '" ++ showDoc t "' does not apply to '"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ showId a "' but only to") b : checkSymbList r
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ : r -> checkSymbList r
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederinsertRsys :: (Pretty r, GetRange r, Ord r)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder => (r -> Id) -> (r -> Maybe Id) -> (Id -> r)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> (r -> Maybe Id) -> (Id -> r) -> Map.Map r r -> (r, r)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder -> Result (Map.Map r r)
8cceb39f451593f3904acbf9d64bea6af9860b57Christian MaederinsertRsys rawId getSort mkSort getImplicit mkImplicit m1 (rsy1, rsy2) =
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let m3 = Map.insert rsy1 rsy2 m1 in
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder case Map.lookup rsy1 m1 of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> case getSort rsy1 of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder case Map.lookup (mkImplicit i) m1 of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just r2 | Just (rawId rsy2) == getImplicit r2 ->
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder warning m1 ("ignoring separate mapping for sort " ++
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder show i) $ getRange i
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder _ -> return m3
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Nothing -> case getImplicit rsy1 of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just i -> let rsy3 = mkSort i in case Map.lookup rsy3 m1 of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder Just r2 | Just (rawId rsy2) == getSort r2 ->
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder warning (Map.delete rsy3 m3)
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder ("ignoring extra mapping of sort " ++
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder show i) $ getRange i
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder {- this case cannot occur, because unkinded names cannot
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder follow kinded ones:
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder in "sort s |-> t, o |-> q" "o" will be a sort, too. -}
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder _ -> return m3
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder _ -> return m3
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder Just rsy3 -> if rsy2 == rsy3 then
4e144aa4be1f50519f8fa377a7883edfbc76d406Christian Maeder hint m1 ("ignoring duplicate mapping of "
568da6120906d5283c4322114eee10f24ea8dd6dChristian Maeder ++ showDoc rsy1 "") $ getRange rsy1 else
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder plain_error m1 ("Symbol " ++ showDoc rsy1 " mapped twice to "
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederstatSymbMapItems :: Sign f e -> Maybe (Sign f e) -> [SYMB_MAP_ITEMS]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result RawSymbolMap
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederstatSymbMapItems sig msig sl = do
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder let st (Symb_map_items kind l _) = do
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder appendDiags $ checkSymbList l
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder fmap concat $ mapM (symbOrMapToRaw sig msig kind) l
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder getSort rsy = case rsy of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder ASymbol (Symbol i SortAsItemType) -> Just i
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder getImplicit rsy = case rsy of
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder AKindedSymb Implicit i -> Just i
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder mkSort i = ASymbol $ Symbol i SortAsItemType
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder mkImplicit = AKindedSymb Implicit
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder ls <- mapM st sl
8cceb39f451593f3904acbf9d64bea6af9860b57Christian Maeder foldM (insertRsys rawSymName getSort mkSort getImplicit mkImplicit)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedersymbOrMapToRaw :: Sign f e -> Maybe (Sign f e) -> SYMB_KIND -> SYMB_OR_MAP
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result [(RawSymbol, RawSymbol)]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedersymbOrMapToRaw sig msig k sm = case sm of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder v <- symbToRaw True sig k s
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return [(v, v)]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Symb_map s t _ -> do
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder appendDiags $ case (s, t) of
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder (Symb_id a, Symb_id b) | a == b ->
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder [mkDiag Hint "unneeded identical mapping of" a]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder w <- symbToRaw True sig k s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder x <- case msig of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Nothing -> symbToRaw False sig k t
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Just tsig -> symbToRaw True tsig k t
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder let mkS = ASymbol . idToSortSymbol
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder case (s, t) of
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (Qual_id _ t1 _, Qual_id _ t2 _) -> case (t1, t2) of
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (O_type (Op_type _ args1 res1 _), O_type (Op_type _ args2 res2 _))
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder | length args1 == length args2 -> -- ignore partiality
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return $ (w, x) : (mkS res1, mkS res2)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder : zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder (P_type (Pred_type args1 _), P_type (Pred_type args2 _))
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder | length args1 == length args2 ->
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return $ (w, x)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder : zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (O_type (Op_type _ [] res1 _), A_type s2) ->
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder return [(w, x), (mkS res1, mkS s2)]
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (A_type s1, O_type (Op_type _ [] res2 _)) ->
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder return [(w, x), (mkS s1, mkS res2)]
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder (A_type s1, A_type s2) ->
88124ca824f94153b0a2a24ea1e4b089fff7011fChristian Maeder return [(w, x), (mkS s1, mkS s2)]
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> fail $ "profiles '" ++ showDoc t1 "' and '"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder ++ showDoc t2 "' do not match"
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder _ -> return [(w, x)]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederstatSymbItems :: Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaederstatSymbItems sig sl =
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder let st (Symb_items kind l _) = do
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder appendDiags $ checkSymbList $ map Symb l
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder mapM (symbToRaw True sig kind) l
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder in fmap concat (mapM st sl)
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder-- | bool indicates if a deeper symbol check is possible for target symbols
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedersymbToRaw :: Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedersymbToRaw b sig k si = case si of
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Symb_id idt -> return $ case k of
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder Sorts_kind -> ASymbol $ idToSortSymbol idt
ee152ae82dc19d6415119c0019ae1bfa991b1f02Christian Maeder _ -> AKindedSymb k idt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Qual_id idt t _ -> typedSymbKindToRaw b sig k idt t
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedertypedSymbKindToRaw :: Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder -> Result RawSymbol
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian MaedertypedSymbKindToRaw b sig k idt t = let
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pm = predMap sig
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder om = opMap sig
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder err = plain_error (AKindedSymb Implicit idt)
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (showDoc idt ":" ++ showDoc t
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder "does not have kind" ++ showDoc k "") (getRange idt)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder aSymb = ASymbol $ case t of
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder O_type ot -> idToOpSymbol idt $ toOpType ot
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder P_type pt -> idToPredSymbol idt $ toPredType pt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder A_type s -> idToOpSymbol idt $ sortToOpType s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Error "unknown symbol" aSymb]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder Implicit -> case t of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder A_type s -> if b then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let pt = sortToPredType s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ot = sortToOpType s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pot = mkPartial ot
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder hasPred = Set.member pt $ getSet pm
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder hasOp = Set.member ot $ getSet om
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder hasPOp = Set.member pot $ getSet om
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder bothWarn = when hasPred $
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Warning "considering operation only" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if hasOp then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Hint "matched constant" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else if hasPOp then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Warning "constant is partial" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ ASymbol $ idToOpSymbol idt pot
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else if hasPred then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Hint "matched unary predicate" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ ASymbol $ idToPredSymbol idt pt
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder appendDiags [mkDiag Warning "qualify name as pred or op" idt]
99476ac2689c74251219db4782e57fe713a24a52Christian Maeder _ -> return aSymb
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Ops_kind -> case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder P_type _ -> err
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let ot = case t of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder O_type aot -> toOpType aot
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder A_type s -> sortToOpType s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder P_type _ -> error "CASL.typedSymbKindToRaw.Ops_kind"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pot = mkPartial ot
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder isMem aot = Set.member aot $ getSet om
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if isMem ot then return aSymb
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else if isMem pot then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Warning "operation is partial" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder return $ ASymbol $ idToOpSymbol idt pot
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else return aSymb
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Preds_kind -> case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder O_type _ -> err
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder let pt = case t of
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder A_type s -> sortToPredType s
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder P_type qt -> toPredType qt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder O_type _ -> error "CASL.typedSymbKindToRaw.Preds_kind"
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder pSymb = ASymbol $ idToPredSymbol idt pt
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder if Set.member pt $ getSet pm then do
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder appendDiags [mkDiag Hint "matched predicate" idt]
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder else return pSymb
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder Sorts_kind -> err
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedermorphismToSymbMap :: Morphism f e m -> SymbolMap
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedermorphismToSymbMap = morphismToSymbMapAux False
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedermorphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedermorphismToSymbMapAux b mor = let
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder src = msource mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sorts = sort_map mor
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ops = op_map mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder preds = pred_map mor
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder (\ s -> let t = mapSort sorts s in
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if b && s == t then id else
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Map.insert (idToSortSymbol s) $ idToSortSymbol t)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ i t -> let (j, k) = mapOpSym sorts ops (i, t) in
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if b && i == j && opKind k == opKind t then id else
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Map.insert (idToOpSymbol i t) $ idToOpSymbol j k)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ i t -> let (j, k) = mapPredSym sorts preds (i, t) in
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder if b && i == j then id else
e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder Map.insert (idToPredSymbol i t) $ idToPredSymbol j k)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder in foldr Map.union sortSymMap [opSymMap, predSymMap]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermatches :: Symbol -> RawSymbol -> Bool
fa167e362877db231378e17ba49c66fbb84862fcChristian Maedermatches (Symbol idt k) rs = case rs of
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder ASymbol (Symbol id2 k2) -> idt == id2 && case (k, k2) of
fa167e362877db231378e17ba49c66fbb84862fcChristian Maeder (OpAsItemType ot, OpAsItemType ot2) -> compatibleOpTypes ot ot2
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb rk di -> let res = idt == di in case (k, rk) of
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (_, Implicit) -> res
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (SortAsItemType, Sorts_kind) -> res
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (OpAsItemType _, Ops_kind) -> res
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder (PredAsItemType _, Preds_kind) -> res
03136b84a0c70d877e227444f0875e209506b9e4Christian MaederidMor :: m -> Sign f e -> Morphism f e m
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian MaederidMor extEm sigma = embedMorphism extEm sigma sigma
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian MaedercomposeM :: Eq e => (Morphism f e m -> Morphism f e m -> Result m)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian MaedercomposeM comp mor1 mor2 = do
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let sMap1 = sort_map mor1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder src = msource mor1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder tar = mtarget mor2
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder oMap1 = op_map mor1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder pMap1 = pred_map mor1
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sMap2 = sort_map mor2
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder oMap2 = op_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pMap2 = pred_map mor2
e0f1794e365dd347e97b37d7d22b2fce27296fa1Christian Maeder sMap = composeMap (MapSet.setToMap $ sortSet src) sMap1 sMap2
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder oMap = if Map.null oMap2 then oMap1 else
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder let (ni, nt) = mapOpSym sMap2 oMap2
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder $ mapOpSym sMap1 oMap1 (i, ot)
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder k = opKind nt
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder in if i == ni && opKind ot == k then id else
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder Map.insert (i, mkPartial ot) (ni, k))
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder pMap = if Map.null pMap2 then pMap1 else
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder let ni = fst $ mapPredSym sMap2 pMap2
4072adb8c5d2c86123e8e1c1918263968f187829Christian Maeder $ mapPredSym sMap1 pMap1 (i, pt)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder in if i == ni then id else Map.insert (i, pt) ni)
d5833d2ee7bafcbf2fdd2bdfd9a728c769b100c7Christian Maeder extComp <- comp mor1 mor2
d0c66a832d7b556e20ea4af4852cdc27a5463d51Christian Maeder let emb = embedMorphism extComp src tar
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder return $ cleanMorMaps emb
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder { sort_map = sMap
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder , op_map = oMap
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder , pred_map = pMap }
74d9a385499bf903b24848dff450a153f525bda7Christian MaederlegalSign :: Sign f e -> Bool
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian MaederlegalSign sigma =
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian Maeder MapSet.setAll legalSort (MapSet.setElems . Rel.toMap $ sortRel sigma)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder && MapSet.all legalOpType (opMap sigma)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder && MapSet.all legalPredType (predMap sigma)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski where sorts = sortSet sigma
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski legalSort s = Set.member s sorts
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian Maeder legalOpType t = -- omitted for VSE Boolean: legalSort (opRes t)
da5f197255c3e060416a2aa34cc94e7bf42365e3Christian Maeder all legalSort (opArgs t)
ebc51e8081f6f1fe2f3d39ceff81d8dd0169c0b0Christian Maeder legalPredType = all legalSort . predArgs
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder-- | the image of a signature morphism
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian MaederimageOfMorphism :: Morphism f e m -> Sign f e
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederimageOfMorphism m = imageOfMorphismAux (const $ extendedInfo $ mtarget m) m
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder-- | the generalized image of a signature morphism
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian MaederimageOfMorphismAux :: (Morphism f e m -> e) -> Morphism f e m -> Sign f e
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederimageOfMorphismAux fE m =
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder inducedSignAux (\ _ _ _ _ _ -> fE m)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder (sort_map m) (op_map m) (pred_map m) (extended_map m) (msource m)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maedertype InducedSign f e m r =
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder Sort_map -> Op_map -> Pred_map -> m -> Sign f e -> r
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder-- | the induced signature image of a signature morphism
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederinducedSignAux :: InducedSign f e m e -> InducedSign f e m (Sign f e)
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian MaederinducedSignAux f sm om pm em src =
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder let ms = mapSort sm
be98c516a8ff1d496fcdeb9b8be8c5f4b908ab95Christian Maeder in (emptySign $ f sm om pm em src)
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder { sortRel = Rel.transClosure . Rel.irreflex . Rel.map ms $ sortRel src
b2eb5854497af395cbf17a08c7ace5ab73e7eea2Christian Maeder -- sorts may fall together and need to be removed as trivial relation
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder , emptySortSet = msorts $ emptySortSet src
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder , opMap = inducedOpMap sm om $ opMap src
22eea35d0effc6582b2951a28b5240fa7a82f3dfChristian Maeder , assocOps = inducedOpMap sm om $ assocOps src
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder , predMap = inducedPredMap sm pm $ predMap src
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder , annoMap = inducedAnnoMap sm om pm $ annoMap src
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederinducedOpMap :: Sort_map -> Op_map -> OpMap -> OpMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederinducedOpMap sm fm = MapSet.foldWithKey
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (\ i ot -> let (j, nt) = mapOpSym sm fm (i, ot)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederinducedPredMap :: Sort_map -> Pred_map -> PredMap -> PredMap
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaederinducedPredMap sm pm = MapSet.foldWithKey
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ i pt -> let (j, nt) = mapPredSym sm pm (i, pt)
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian MaederinducedAnnoMap :: Sort_map -> Op_map -> Pred_map -> AnnoMap -> AnnoMap
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian MaederinducedAnnoMap sm om pm = MapSet.foldWithKey
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder ( \ sy s -> MapSet.insert (mapSymbol sm om pm sy) s) MapSet.empty
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian MaedermapSymbol :: Sort_map -> Op_map -> Pred_map -> Symbol -> Symbol
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian MaedermapSymbol sm om pm (Symbol i ty) = case ty of
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder SortAsItemType -> Symbol (mapSort sm i) SortAsItemType
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder SubsortAsItemType j ->
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder Symbol (mapSort sm i) $ SubsortAsItemType $ mapSort sm j
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder OpAsItemType ot -> let (j, nt) = mapOpSym sm om (i, ot) in
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder Symbol j $ OpAsItemType nt
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder PredAsItemType pt -> let (j, nt) = mapPredSym sm pm (i, pt) in
51659cc7b3c1e644d4969b8c5e987e61626500c0Christian Maeder Symbol j $ PredAsItemType nt
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian MaederlegalMor :: MorphismExtension e m => Morphism f e m -> Result ()
5e46b572ed576c0494768998b043d9d340594122Till MossakowskilegalMor mor =
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder let s1 = msource mor
329d1810c6d5a5a0827e1d07503d94431578d176Christian Maeder s2 = mtarget mor
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder sm = sort_map mor
d058429727dd696a0327cdc28cadd268c34c36baChristian Maeder msorts = Set.map $ mapSort sm
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder in if legalSign s1
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder && Set.isSubsetOf (msorts $ sortSet s1) (sortSet s2)
5a9a06d23910b9521e1d1cd39865ac7912ccee4bChristian Maeder && Set.isSubsetOf (msorts $ emptySortSet s1) (emptySortSet s2)
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder && isSubOpMap (inducedOpMap sm (op_map mor) $ opMap s1) (opMap s2)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder && isSubMap (inducedPredMap sm (pred_map mor) $ predMap s1) (predMap s2)
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder && legalSign s2
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder then legalMorphismExtension mor else fail "illegal CASL morphism"
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian MaederisInclOpMap :: Op_map -> Bool
2feea92963a4b1b7482a4b72ee85148d842d9ad6Christian MaederisInclOpMap = all (\ ((i, _), (j, _)) -> i == j) . Map.toList
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederidOrInclMorphism :: Morphism f e m -> Morphism f e m
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederidOrInclMorphism m =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder let src = opMap $ msource m
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tar = opMap $ mtarget m
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder in if isSubOpMap tar src then m
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder else let diffOpMap = MapSet.toMap $ MapSet.difference src tar in
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder m { op_map = Map.fromList $ concatMap (\ (i, s) ->
40d15f6c5f4d15866e085c588f8b5130dfd6cf63Christian Maeder map (\ t -> ((i, t), (i, Total)))
b0442fc87b3d8a47626543df44e4227d6933f8bdChristian MaedersigInclusion :: m -- ^ computed extended morphism
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> Sign f e -> Sign f e -> Result (Morphism f e m)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedersigInclusion extEm sigma1 =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder return . idOrInclMorphism . embedMorphism extEm sigma1
32562a567baac248a00782d2727716c13117dc4aChristian MaederaddSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
32562a567baac248a00782d2727716c13117dc4aChristian MaederaddSigM f a b = do
32562a567baac248a00782d2727716c13117dc4aChristian Maeder e <- f (extendedInfo a) $ extendedInfo b
32562a567baac248a00782d2727716c13117dc4aChristian Maeder return $ addSig (const $ const e) a b
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian MaederplainMorphismUnion :: (e -> e -> e) -- ^ join signature extensions
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
fa373bc327620e08861294716b4454be8d25669fChristian MaederplainMorphismUnion = morphismUnion retExtMap
fa373bc327620e08861294716b4454be8d25669fChristian MaederretExtMap :: b -> Morphism f e m -> Result m
fa373bc327620e08861294716b4454be8d25669fChristian MaederretExtMap = const $ return . extended_map
fa373bc327620e08861294716b4454be8d25669fChristian MaedermorphismUnion :: (Morphism f e m -> Morphism f e m -> Result m)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -- ^ join morphism extensions
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> (e -> e -> e) -- ^ join signature extensions
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
32562a567baac248a00782d2727716c13117dc4aChristian MaedermorphismUnion uniteM addSigExt =
32562a567baac248a00782d2727716c13117dc4aChristian Maeder morphismUnionM uniteM (\ e -> return . addSigExt e)
fa373bc327620e08861294716b4454be8d25669fChristian MaedermorphismUnionM :: (Morphism f e m -> Morphism f e m -> Result m)
fa373bc327620e08861294716b4454be8d25669fChristian Maeder -- ^ join morphism extensions
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> (e -> e -> Result e) -- ^ join signature extensions
7857a35e3af533dfbd0f0e18638ebd211e6358a0Christian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder-- consider identity mappings but filter them eventually
32562a567baac248a00782d2727716c13117dc4aChristian MaedermorphismUnionM uniteM addSigExt mor1 mor2 =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let smap1 = sort_map mor1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder smap2 = sort_map mor2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder s1 = msource mor1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder s2 = msource mor2
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder us1 = Set.difference (sortSet s1) $ Map.keysSet smap1
e68f45f355ed9d4026ee9baff5aa75aa7c911cc2Christian Maeder us2 = Set.difference (sortSet s2) $ Map.keysSet smap2
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder omap1 = op_map mor1
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder omap2 = op_map mor2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder uo1 = foldr delOp (opMap s1) $ Map.keys omap1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder uo2 = foldr delOp (opMap s2) $ Map.keys omap2
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder delOp (n, ot) m = diffOpMapSet m $ MapSet.fromList [(n, [mkTotal ot])]
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder uo = addOpMapSet uo1 uo2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder pmap1 = pred_map mor1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder pmap2 = pred_map mor2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder up1 = foldr delPred (predMap s1) $ Map.keys pmap1
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder up2 = foldr delPred (predMap s2) $ Map.keys pmap2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder up = addMapSet up1 up2
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder delPred (n, pt) = MapSet.delete n pt
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> (ds, Map.insert i j m)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Just k -> if j == k then (ds, m) else
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ("incompatible mapping of sort " ++ showId i " to "
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ++ showId j " and " ++ showId k "")
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder nullRange : ds, m)) ([], smap1)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (Map.toList smap2 ++ map (\ a -> (a, a))
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> (ds, Map.insert isc jsc m)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Just (k, p) -> if j == k then if p == t then (ds, m)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder else (ds, Map.insert isc (j, Total) m) else
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ("incompatible mapping of op " ++ showId i ":"
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder ++ showDoc (setOpKind t ot) " to "
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ++ showId j " and " ++ showId k "") nullRange : ds, m))
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (sds, omap1) (Map.toList omap2 ++ map
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder ( \ (a, ot) -> ((a, mkPartial ot), (a, opKind ot)))
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (mapSetToList uo))
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder (pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Nothing -> (ds, Map.insert isc j m)
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder Just k -> if j == k then (ds, m) else
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ("incompatible mapping of pred " ++ showId i ":"
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder ++ showDoc pt " to " ++ showId j " and "
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder ++ showId k "") nullRange : ds, m)) (ods, pmap1)
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder (Map.toList pmap2 ++ map ( \ (a, pt) -> ((a, pt), a))
e7ddd5495421698701a2bbc57a5b3390a11d12caChristian Maeder (mapSetToList up))
32562a567baac248a00782d2727716c13117dc4aChristian Maeder in if null pds then do
32562a567baac248a00782d2727716c13117dc4aChristian Maeder s3 <- addSigM addSigExt s1 s2
32562a567baac248a00782d2727716c13117dc4aChristian Maeder s4 <- addSigM addSigExt (mtarget mor1) $ mtarget mor2
fa373bc327620e08861294716b4454be8d25669fChristian Maeder extM <- uniteM mor1 mor2
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder return $ cleanMorMaps
fa373bc327620e08861294716b4454be8d25669fChristian Maeder (embedMorphism extM s3 s4)
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder { sort_map = smap
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder , op_map = omap
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder , pred_map = pmap }
32562a567baac248a00782d2727716c13117dc4aChristian Maeder else Result pds Nothing
3c8d067accf18572352351ec42ff905c7297a8a5Christian MaedercleanMorMaps :: Morphism f e m -> Morphism f e m
3c8d067accf18572352351ec42ff905c7297a8a5Christian MaedercleanMorMaps m = m
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder { sort_map = Map.filterWithKey (/=) $ sort_map m
3c8d067accf18572352351ec42ff905c7297a8a5Christian Maeder (\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian Maeder (MapSet.lookup i $ opMap $ msource m)) $ op_map m
812ee1f62e0e0e7235f3c05b41a0b173497b54ffChristian Maeder , pred_map = Map.filterWithKey ((/=) . fst) $ pred_map m }
3b70d8ee5c2927f843d5d907e6ef724f867f1b40Till MossakowskiisSortInjective :: Morphism f e m -> Bool
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederisSortInjective m =
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder let ss = sortSet $ msource m
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder in Set.size ss == Set.size (Set.map (mapSort $ sort_map m) ss)
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedersumSize :: MapSet.MapSet a b -> Int
2a5b885d9350ec6dd8bc4992ee91d2f68aa592f4Christian MaedersumSize = sum . map Set.size . Map.elems . MapSet.toMap
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder-- morphism extension m is not considered here
ca732bc259f74cb4f3f725daab7fe80fc7e1d9a0Till MossakowskiisInjective :: Morphism f e m -> Bool
2766ec926fcf3faf72248b10c3305b715b8c3249Christian MaederisInjective m = isSortInjective m && let
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder src = msource m
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder sm = sort_map m
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder os = opMap src
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder ps = predMap src
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder in sumSize os == sumSize (inducedOpMap sm (op_map m) os)
2766ec926fcf3faf72248b10c3305b715b8c3249Christian Maeder && sumSize ps == sumSize (inducedPredMap sm (pred_map m) ps)
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wanginstance Pretty RawSymbol where
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang pretty rsym = case rsym of
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ASymbol sy -> pretty sy
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder AKindedSymb k i -> pretty k <+> pretty i
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian MaederprintMorphism :: (e -> e -> Bool) -> (m -> Bool) -> (e -> Doc)
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder -> (Morphism f e m -> Doc) -> Morphism f e m -> Doc
fc033b8680245bf692c9c09723fd3046ff38971eChristian MaederprintMorphism isSubSigExt isInclMorExt fE fM mor =
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder let src = msource mor
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder tar = mtarget mor
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder ops = op_map mor
5824312cc0cfccce61f195fbe92307a21a467049Christian Maeder prSig s = specBraces (space <> printSign fE s)
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder srcD = prSig src
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in fsep $ if isInclusionMorphism isInclMorExt mor then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if isSubSig isSubSigExt tar src then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [text "identity morphism over", srcD]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [text "inclusion morphism of", srcD
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , if Map.null ops then empty
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [text "by totalizing",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pretty $ Set.map (uncurry idToOpSymbol) $ Map.keysSet ops]]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder [ braces $ printMap id sepByCommas pairElems
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder (morphismToSymbMapAux True mor) $+$ fM mor
2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder , colon <+> srcD, mapsto <+> prSig tar ]
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maederinstance (SignExtension e, Pretty e, Show f, MorphismExtension e m)
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder => Pretty (Morphism f e m) where
0ccfc8f86bd6518556ef09e367a0ce2bd1a69c91Christian Maeder pretty = printMorphism isSubSignExtension isInclusionMorphismExtension
7830e8fa7442fb7452af7ecdba102bc297ae367eChristian Maeder pretty prettyMorphismExtension