Morphism.hs revision 68138d26bcddf5e89c30206aa83ab5ec006d170d
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederModule : $Header$
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : maeder@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederPortability : portable
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiSymbols and signature morphisms for the CASL logic
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskithe qualification only applies to __+__ !
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set
5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport qualified Common.Lib.Rel as Rel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata SymbType = OpAsItemType OpType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- since symbols do not speak about totality, the totality
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -- information in OpType has to be ignored
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder | PredAsItemType PredType
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder | SortAsItemType
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder deriving (Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski-- Ordering and equality of symbol types has to ingore totality information
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Ord SymbType where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (OpAsItemType ot1) (OpAsItemType ot2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (opArgs ot1,opRes ot1) (opArgs ot2,opRes ot2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (OpAsItemType _) _ = LT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType pt1) (PredAsItemType pt2) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare pt1 pt2
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType _) (OpAsItemType _) = GT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare (PredAsItemType _) SortAsItemType = LT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare SortAsItemType SortAsItemType = EQ
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski compare SortAsItemType _ = GT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance Eq SymbType where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski t1 == t2 = compare t1 t2 == EQ
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Symbol = Symbol {symName :: Id, symbType :: SymbType}
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype SymbolSet = Set.Set Symbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedertype SymbolMap = Map.Map Symbol Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype RawSymbolSet = Set.Set RawSymbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata Kind = SortKind | FunKind | PredKind
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Show, Eq, Ord)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maedertype Sort_map = Map.Map SORT SORT
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- allways use the partial profile as key!
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskitype Fun_map = Map.Map (Id,OpType) (Id, FunKind)
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowskitype Pred_map = Map.Map (Id,PredType) Id
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maederdata Morphism f e m = Morphism {msource :: Sign f e,
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder mtarget :: Sign f e,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sort_map :: Sort_map,
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder fun_map :: Fun_map,
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder pred_map :: Pred_map,
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder extended_map :: m}
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder deriving (Eq, Show)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapSort :: Sort_map -> SORT -> SORT
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapSort sorts s = Map.findWithDefault s s sorts
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapOpType :: Sort_map -> OpType -> OpType
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapOpType sorts t = t { opArgs = map (mapSort sorts) $ opArgs t
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , opRes = mapSort sorts $ opRes t }
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermakeTotal :: FunKind -> OpType -> OpType
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermakeTotal Total t = t { opKind = Total }
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermakeTotal _ t = t
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapOpSym sMap fMap (i, ot) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let mot = mapOpType sMap ot in
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder case Map.lookup (i, ot {opKind = Partial} ) fMap of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Nothing -> (i, mot)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Just (j, k) -> (j, makeTotal k mot)
10a2cf8d9887524acde19d4ea59f8fea3a7f3258Till Mossakowski-- | Check if two OpTypes are equal except from totality or partiality
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicompatibleOpTypes :: OpType -> OpType -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskicompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapPredType :: Sort_map -> PredType -> PredType
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapPredType sorts t = t { predArgs = map (mapSort sorts) $ predArgs t }
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedermapPredSym sMap fMap (i, pt) =
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maedertype Ext f e m = Sign f e -> Sign f e -> m
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederembedMorphism :: Ext f e m -> Sign f e -> Sign f e -> Morphism f e m
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederembedMorphism extEm a b =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder { msource = a
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder , mtarget = b
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder , extended_map = extEm a b
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToSortSymbol :: Id -> Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToSortSymbol idt = Symbol idt SortAsItemType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToOpSymbol :: Id -> OpType -> Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToPredSymbol :: Id -> PredType -> Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbTypeToKind :: SymbType -> Kind
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbTypeToKind (OpAsItemType _) = FunKind
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbTypeToKind (PredAsItemType _) = PredKind
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbTypeToKind SortAsItemType = SortKind
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbolToRaw :: Symbol -> RawSymbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbolToRaw sym = ASymbol sym
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToRaw :: Id -> RawSymbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederidToRaw x = AnID x
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederrawSymName :: RawSymbol -> Id
5e46b572ed576c0494768998b043d9d340594122Till MossakowskirawSymName (ASymbol sym) = symName sym
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaederrawSymName (AnID i) = i
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaederrawSymName (AKindedId _ i) = i
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaedersymOf :: Sign f e -> SymbolSet
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder let sorts = Set.map idToSortSymbol $ sortSet sigma
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Map.toList $ predMap sigma
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder in Set.unions [sorts, ops, preds]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskistatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskistatSymbMapItems sl = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ls <- sequence $ map s1 sl
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski foldl insertRsys (return Map.empty) (concat ls)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski insertRsys m (rsy1,rsy2) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski case Map.lookup rsy1 m1 of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Nothing -> return $ Map.insert rsy1 rsy2 m1
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski plain_error m1 ("Symbol "++showPretty rsy1 " mapped twice to "
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ++showPretty rsy2 " and "++showPretty rsy3 "") nullRange
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskipairM :: Monad m => (m a,m b) -> m (a,b)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskipairM (x,y) = do
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol,RawSymbol)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbOrMapToRaw k (Symb s) = pairM (symbToRaw k s,symbToRaw k s)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbOrMapToRaw k (Symb_map s t _) = pairM (symbToRaw k s,symbToRaw k t)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederstatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederstatSymbItems sl =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fmap concat (sequence (map s1 sl))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersymbToRaw k (Symb_id idt) = return $ symbKindToRaw k idt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymbToRaw k (Qual_id idt t _) = typedSymbKindToRaw k idt t
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersymbKindToRaw :: SYMB_KIND -> Id -> RawSymbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedersymbKindToRaw sk idt = case sk of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Implicit -> AnID idt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder _ -> AKindedId (case sk of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Sorts_kind -> SortKind
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Preds_kind -> PredKind
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder _ -> FunKind) idt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitypedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitypedSymbKindToRaw k idt t =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let err = plain_error (AnID idt)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (showPretty idt ":" ++ showPretty t
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski "does not have kind" ++showPretty k "") nullRange
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder aSymb = ASymbol $ case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder O_type ot -> idToOpSymbol idt $ toOpType ot
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder P_type pt -> idToPredSymbol idt $ toPredType pt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- in case of ambiguity, return a constant function type
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder -- this deviates from the CASL summary !!!
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let ot = OpType {opKind = Total, opArgs = [], opRes = s}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in idToOpSymbol idt ot
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Implicit -> return aSymb
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Sorts_kind -> return $ AKindedId SortKind idt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Ops_kind -> case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder P_type _ -> err
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder _ -> return aSymb
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Preds_kind -> case t of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder O_type _ -> err
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder A_type s -> return $ ASymbol $
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder let pt = PredType {predArgs = [s]}
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in idToPredSymbol idt pt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder P_type _ -> return aSymb
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedersymbMapToMorphism :: Ext f e m -> Sign f e -> Sign f e
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> SymbolMap -> Result (Morphism f e m)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaedersymbMapToMorphism extEm sigma1 sigma2 smap = let
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder sort_map1 = Set.fold mapMSort Map.empty (sortSet sigma1)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mapMSort s m =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder of Just sym -> let t = symName sym in if s == t then m else
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mapFun i ots m = Set.fold (insFun i) m ots
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder insFun i ot m =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder of Just sym -> let j = symName sym in case symbType sym of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder OpAsItemType oty -> let k = opKind oty in
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder if j == i && opKind ot == k then m
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder else Map.insert (i, oty {opKind = Partial}) (j, k) m
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mapPred i pts m = Set.fold (insPred i) m pts
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder insPred i pt m =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder of Just sym -> let j = symName sym in case symbType sym of
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder PredAsItemType pty -> if i == j then m else Map.insert (i, pty) j m
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder in return (Morphism { msource = sigma1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mtarget = sigma2,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sort_map = sort_map1,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fun_map = fun_map1,
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder pred_map = pred_map1,
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder extended_map = extEm sigma1 sigma2})
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaedermorphismToSymbMap :: Morphism f e m -> SymbolMap
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermorphismToSymbMap mor =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder src = msource mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sorts = sort_map mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder ops = fun_map mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder preds = pred_map mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sortSymMap = Set.fold ( \ s -> Map.insert (idToSortSymbol s) $
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder idToSortSymbol $ mapSort sorts s)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ( \ t -> Map.insert (idToOpSymbol i t)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ uncurry idToOpSymbol $ mapOpSym sorts ops (i, t)) m s)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder ( \ t -> Map.insert (idToPredSymbol i t)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder $ uncurry idToPredSymbol $ mapPredSym sorts preds (i, t)) m s)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder foldr Map.union sortSymMap [opSymMap,predSymMap]
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermatches :: Symbol -> RawSymbol -> Bool
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedermatches x@(Symbol idt k) rs = case rs of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ASymbol y -> x == y
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder AnID di -> idt == di
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder AKindedId rk di -> let res = idt == di in case (k, rk) of
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (SortAsItemType, SortKind) -> res
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (OpAsItemType _, FunKind) -> res
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (PredAsItemType _, PredKind) -> res
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederidMor :: Ext f e m -> Sign f e -> Morphism f e m
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederidMor extEm sigma = embedMorphism extEm sigma sigma
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maedercompose :: (Eq e, Eq f) => (m -> m -> m)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maedercompose comp mor1 mor2 = if mtarget mor1 == msource mor2 then return $
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let sMap1 = sort_map mor1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder src = msource mor1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder fMap1 = fun_map mor1
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder pMap1 = pred_map mor1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sMap2 = sort_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fMap2 = fun_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pMap2 = pred_map mor2
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder sMap = Set.fold ( \ i ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let j = mapSort sMap2 (mapSort sMap1 i) in
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder if i == j then id else Map.insert i j)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder in Morphism {
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder msource = src,
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski mtarget = mtarget mor2,
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder sort_map = sMap,
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder fun_map = Map.foldWithKey ( \ i t m ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let (ni, nt) = mapOpSym sMap2 fMap2 $
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder mapOpSym sMap1 fMap1 (i, ot)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder k = opKind nt
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in assert (mapOpTypeK sMap k ot == nt) $
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder if i == ni && opKind ot == k then id else
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Map.insert (i, ot {opKind = Partial }) (ni, k)) m t)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder pred_map = Map.foldWithKey ( \ i t m ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder let (ni, nt) = mapPredSym sMap2 pMap2 $
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder mapPredSym sMap1 pMap1 (i, pt)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder in assert (mapPredType sMap pt == nt) $
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder if i == ni then id else Map.insert (i, pt) ni) m t)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder extended_map = comp (extended_map mor1) (extended_map mor2)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder else fail "target of first and source of second morphism are different"
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederlegalSign :: Sign f e -> Bool
5e46b572ed576c0494768998b043d9d340594122Till MossakowskilegalSign sigma =
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder Map.foldWithKey (\s sset b -> b && legalSort s && all legalSort
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True (Rel.toMap (sortRel sigma))
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder && Map.fold (\ts b -> b && all legalOpType (Set.toList ts))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True (opMap sigma)
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder && Map.fold (\ts b -> b && all legalPredType (Set.toList ts))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True (predMap sigma)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski where sorts = sortSet sigma
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski legalSort s = Set.member s sorts
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski legalOpType t = legalSort (opRes t)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski && all legalSort (opArgs t)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski legalPredType t = all legalSort (predArgs t)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederlegalMor :: Morphism f e m -> Bool
5e46b572ed576c0494768998b043d9d340594122Till MossakowskilegalMor mor =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski legalSign sigma1
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski && legalSign sigma2
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (\s1 s2 b -> b && Set.member s1 (sortSet sigma1)
a938729e277da5c7742bb88946ab2c150416fd5dTill Mossakowski && Set.member s2 (sortSet sigma2))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (\(id1,t) (id2,k) b ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Set.member t (Map.findWithDefault Set.empty id1 (opMap sigma1))
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Set.member (mapOpTypeK smap k t)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Map.findWithDefault Set.empty id2 (opMap sigma2))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True (fun_map mor)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (\(id1,t) id2 b ->
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Set.member t (Map.findWithDefault Set.empty id1 (predMap sigma1))
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder Set.member (mapPredType smap t)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski (Map.findWithDefault Set.empty id2 (predMap sigma2))
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski True (pred_map mor)
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski where sigma1 = msource mor
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski sigma2 = mtarget mor
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski smap = sort_map mor
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedersigInclusion :: (PrettyPrint e, PrettyPrint f)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder => Ext f e m -- ^ compute extended morphism
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> (e -> e -> Bool) -- ^ subsignature test of extensions
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> Sign f e -> Sign f e -> Result (Morphism f e m)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedersigInclusion extEm isSubExt sigma1 sigma2 =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder if isSubSig isSubExt sigma1 sigma2
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder then return (embedMorphism extEm sigma1 sigma2)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder else pfatal_error
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (text "Attempt to construct inclusion between non-subsignatures:"
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $$ text "Singature 1:" $$ printText sigma1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $$ text "Singature 2:" $$ printText sigma2)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedermorphismUnion :: (m -> m -> m) -- ^ join morphism extensions
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder -> (e -> e -> e) -- ^ join signature extensions
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder-- consider identity mappings but filter them eventually
746440cc1b984a852f5864235b8fa3930963a081Christian MaedermorphismUnion uniteM addSigExt mor1 mor2 =
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder let smap1 = sort_map mor1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder smap2 = sort_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder s1 = msource mor1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder s2 = msource mor2
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder us1 = Set.difference (sortSet s1) $ Rel.keysSet smap1
fcb1d8a27670f3206bd4ca28d77d4172619db602Christian Maeder us2 = Set.difference (sortSet s2) $ Rel.keysSet smap2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder omap1 = fun_map mor1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder omap2 = fun_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder uo1 = foldr delOp (opMap s1) $ Map.keys omap1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder uo2 = foldr delOp (opMap s2) $ Map.keys omap2
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder delOp (n, ot) m = diffMapSet m $ Map.singleton n $
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Set.fromList [ot {opKind = Partial}, ot {opKind =Total}]
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder uo = addMapSet uo1 uo2
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pmap1 = pred_map mor1
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder pmap2 = pred_map mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder up1 = foldr delPred (predMap s1) $ Map.keys pmap1
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder up2 = foldr delPred (predMap s2) $ Map.keys pmap2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder up = addMapSet up1 up2
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder delPred (n, pt) m = diffMapSet m $ Map.singleton n $ Set.singleton pt
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> (ds, Map.insert i j m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Just k -> if j == k then (ds, m) else
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ("incompatible mapping of sort " ++ showId i " to "
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ++ showId j " and " ++ showId k "")
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski nullRange : ds, m)) ([], smap1)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (Map.toList smap2 ++ map (\ a -> (a, a))
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> (ds, Map.insert isc jsc m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Just (k, p) -> if j == k then if p == t then (ds, m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder else (ds, Map.insert isc (j, Total) m) else
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ("incompatible mapping of op " ++ showId i ":"
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ++ showPretty ot { opKind = t } " to "
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ++ showId j " and " ++ showId k "") nullRange : ds, m))
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (sds, omap1) (Map.toList omap2 ++ concatMap
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ( \ (a, s) -> map ( \ ot -> ((a, ot {opKind = Partial}),
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (a, opKind ot)))
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Nothing -> (ds, Map.insert isc j m)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder Just k -> if j == k then (ds, m) else
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ("incompatible mapping of pred " ++ showId i ":"
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ++ showPretty pt " to " ++ showId j " and "
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ++ showId k "") nullRange : ds, m)) (ods, pmap1)
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (Map.toList pmap2 ++ concatMap ( \ (a, s) -> map
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder ( \ pt -> ((a, pt), a)) $ Set.toList s) (Map.toList up))
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder s3 = addSig addSigExt s1 s2
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder o3 = opMap s3 in
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder if null pds then Result [] $ Just Morphism
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder { msource = s3,
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder mtarget = addSig addSigExt (mtarget mor1) $ mtarget mor2,
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder sort_map = Map.filterWithKey (/=) smap,
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder (Map.findWithDefault Set.empty i o3)) omap,
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder pred_map = Map.filterWithKey (\ (i, _) j -> i /= j) pmap,
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder extended_map = uniteM (extended_map mor1) $ extended_map mor2 }
746440cc1b984a852f5864235b8fa3930963a081Christian Maeder else Result pds Nothing
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint Symbol where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga sy =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (symName sy) <>
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder case symbType sy of
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder SortAsItemType -> empty
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder st -> space <> colon <> printText0 ga st
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint SymbType where
239fe94380bba365636e6ac48e094fc92cae30c7Christian Maeder -- op types try to place a question mark immediately after a colon
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga (OpAsItemType ot) = printText0 ga ot
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder printText0 ga (PredAsItemType pt) = space <> printText0 ga pt
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder printText0 _ SortAsItemType = empty
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint Kind where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printText0 _ SortKind = text sortS
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printText0 _ FunKind = text opS
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printText0 _ PredKind = text predS
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiinstance PrettyPrint RawSymbol where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski printText0 ga rsym = case rsym of
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ASymbol sy -> printText0 ga sy
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder AnID i -> printText0 ga i
612749008484b6773aedf4d6bbc85b8d074d15c6Christian Maeder AKindedId k i -> printText0 ga k <+> printText0 ga i
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maederinstance (PrettyPrint e, PrettyPrint f, PrettyPrint m) =>
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder PrettyPrint (Morphism f e m) where
cdee35b1b16886e4f341e2a2a69fa0e6be30b3faTill Mossakowski printText0 ga mor =
8001ead00e2d306a1cf4735a3d2c1378fc8e3e31Christian Maeder printText0 ga (Map.filterWithKey (/=) $ morphismToSymbMap mor)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder $$ printText0 ga (extended_map mor)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $$ nest 1 colon $$
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder nest 3 (braces (space <> printText0 ga (msource mor) <> space))
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $$ nest 1 (text funS)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $$ nest 4 (braces (space <> printText0 ga (mtarget mor) <> space))