Morphism.hs revision cdee35b1b16886e4f341e2a2a69fa0e6be30b3fa
1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Christian Maeder and Uni Bremen 2002-2003
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : hets@tzi.de
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : portable
1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskithe symbol and morphism stuff for a logic
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Map as Map
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Common.Lib.Set as Set
f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maederimport qualified Common.Lib.Rel as Rel
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata SymbType = OpAsItemType OpType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder | PredAsItemType PredType
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski | SortAsItemType
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Show, Eq, Ord)
9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowskidata Symbol = Symbol {symName :: Id, symbType :: SymbType}
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder deriving (Show, Eq, Ord)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Show, Eq, Ord)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederdata Kind = SortKind | FunKind | PredKind
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder deriving (Show, Eq, Ord)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype Sort_map = Map.Map SORT SORT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype Fun_map = Map.Map (Id,OpType) (Id, FunKind)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskitype Pred_map = Map.Map (Id,PredType) Id
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskidata Morphism = Morphism {msource,mtarget :: Sign,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sort_map :: Sort_map,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski fun_map :: Fun_map,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski pred_map :: Pred_map}
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski deriving (Eq, Show)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapSort :: Sort_map -> SORT -> SORT
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapSort sorts s = Map.findWithDefault s s sorts
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapOpType :: Sort_map -> OpType -> OpType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapOpType sorts t = t { opArgs = map (mapSort sorts) $ opArgs t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , opRes = mapSort sorts $ opRes t }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimakeTotal :: FunKind -> OpType -> OpType
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermakeTotal Total t = t { opKind = Total }
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedermakeTotal _ t = t
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapPredType :: Sort_map -> PredType -> PredType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapPredType sorts t = t { predArgs = map (mapSort sorts) $ predArgs t }
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederembedMorphism :: Sign -> Sign -> Morphism
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederembedMorphism a b =
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder { msource = a
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , mtarget = b
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski , sort_map = Set.fold (\x -> Map.insert x x) Map.empty
b1caf27fb0c879dd39600d09d501074a2dfd865aChristian Maeder (\t -> Map.insert (i,t) (i, opKind t)) m ts)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (\t -> Map.insert (i,t) i) m ts)
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- Typeable instance
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersentenceTc, signTc, morphismTc, symbolTc, rawSymbolTc
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedersentenceTc = mkTyCon "CASL.Morphism.Sentence"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedersignTc = mkTyCon "CASL.Morphism.Sign"
5e46b572ed576c0494768998b043d9d340594122Till MossakowskimorphismTc = mkTyCon "CASL.Morphism.Morphism"
5e46b572ed576c0494768998b043d9d340594122Till MossakowskisymbolTc = mkTyCon "CASL.Morphism.Symbol"
5e46b572ed576c0494768998b043d9d340594122Till MossakowskirawSymbolTc = mkTyCon "CASL.Morphism.RawSymbol"
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederinstance Typeable Sentence where
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder typeOf _ = mkAppTy sentenceTc []
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maederinstance Typeable Sign where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder typeOf _ = mkAppTy signTc []
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Typeable Morphism where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typeOf _ = mkAppTy morphismTc []
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Typeable Symbol where
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder typeOf _ = mkAppTy symbolTc []
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maederinstance Typeable RawSymbol where
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski typeOf _ = mkAppTy rawSymbolTc []
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidToSortSymbol :: Id -> Symbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskiidToSortSymbol idt = Symbol idt SortAsItemType
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederidToOpSymbol :: Id -> OpType -> Symbol
4fc727afa544a757d1959ce77c02208f8bf330dcChristian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaederidToPredSymbol :: Id -> PredType -> Symbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedersymbTypeToKind :: SymbType -> Kind
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedersymbTypeToKind (OpAsItemType _) = FunKind
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedersymbTypeToKind (PredAsItemType _) = PredKind
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaedersymbTypeToKind SortAsItemType = SortKind
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbolToRaw :: Symbol -> RawSymbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbolToRaw (Symbol idt typ) = AKindedId (symbTypeToKind typ) idt
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederidToRaw :: Id -> RawSymbol
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederidToRaw x = AnID x
4601edb679f0ba530bbb085b25d82a411cd070aaChristian MaederrawSymName :: RawSymbol -> SORT
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederrawSymName (ASymbol sym) = symName sym
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederrawSymName (AnID id) = id
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederrawSymName (AKindedId _ id) = id
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymOf :: Sign -> Set.Set Symbol
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let sorts = Set.image idToSortSymbol $ sortSet sigma
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder Map.toList $ predMap sigma
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder in Set.unions [sorts, ops, preds]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskistatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result (Map.Map RawSymbol RawSymbol)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederstatSymbMapItems sl = return (Map.fromList $ concat $ map s1 sl)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder s1 (Symb_map_items kind l _) = map (symbOrMapToRaw kind) l
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedersymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> (RawSymbol,RawSymbol)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskisymbOrMapToRaw k (Symb s) = (symbToRaw k s,symbToRaw k s)
612749008484b6773aedf4d6bbc85b8d074d15c6Christian MaedersymbOrMapToRaw k (Symb_map s t _) = (symbToRaw k s,symbToRaw k t)
5e46b572ed576c0494768998b043d9d340594122Till MossakowskistatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian MaederstatSymbItems sl =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder return (concat (map s1 sl))
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder where s1 (Symb_items kind l _) = map (symbToRaw kind) l
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbToRaw :: SYMB_KIND -> SYMB -> RawSymbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbToRaw k (Symb_id idt) = symbKindToRaw k idt
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedersymbToRaw k (Qual_id idt _ _) = symbKindToRaw k idt
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbKindToRaw :: SYMB_KIND -> Id -> RawSymbol
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbKindToRaw Implicit idt = AnID idt
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian MaedersymbKindToRaw (Sorts_kind) idt = AKindedId SortKind idt
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedersymbKindToRaw (Ops_kind) idt = AKindedId FunKind idt
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedersymbKindToRaw (Preds_kind) idt = AKindedId PredKind idt
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymmapOf :: Morphism -> Map.Map Symbol Symbol
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskisymmapOf (Morphism src _ sorts ops preds) =
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ( \ s1 s2 -> Map.insert (idToSortSymbol s1) (idToSortSymbol s2))
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder ( \ (id1,t) (id2,k) ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Map.insert (idToOpSymbol id1 t)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (idToOpSymbol id2 $ mapOpTypeK sorts k t))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski ( \ (id1,t) id2 ->
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Map.insert (idToPredSymbol id1 t)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (idToPredSymbol id2 $ mapPredType sorts t))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder foldr Map.union sortSymMap [opSymMap,predSymMap]
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimatches :: Symbol -> RawSymbol -> Bool
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimatches x (ASymbol y) = x==y
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maedermatches (Symbol idt _) (AnID di) = idt==di
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimatches (Symbol idt SortAsItemType) (AKindedId SortKind di) = idt==di
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maedermatches (Symbol idt (OpAsItemType _)) (AKindedId FunKind di) = idt==di
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimatches (Symbol idt (PredAsItemType _)) (AKindedId PredKind di) = idt==di
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskimatches _ _ = False
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederidMor :: Sign -> Morphism
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder msource = sigma,
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mtarget = sigma,
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski sort_map = Set.fold (\s -> Map.insert s s) Map.empty (sortSet sigma),
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (\id ts m -> Set.fold (\t -> Map.insert (id,t) (id,opKind t)) m ts)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (\id ts m -> Set.fold (\t -> Map.insert (id,t) id) m ts)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Map.empty (predMap sigma)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedercompose :: Morphism -> Morphism -> Maybe Morphism
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maedercompose mor1 mor2 =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder if mtarget mor1 == msource mor2
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder then Just $ Morphism {
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder msource = msource mor1,
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mtarget = mtarget mor2,
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder sort_map = Map.map (mapSort (sort_map mor2)) (sort_map mor1),
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder fun_map = Map.mapWithKey mapOpId (fun_map mor1),
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder pred_map = Map.mapWithKey mapPredId (pred_map mor1)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapOpId :: (Id, OpType) -> (Id,FunKind) -> (Id,FunKind)
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder mapOpId (id,t) (id1,k1) =
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Map.find (id1,mapOpType (sort_map mor1) t) (fun_map mor2)
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski mapPredId :: (Id, PredType) -> Id -> Id
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mapPredId (id,t) id1 =
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Map.find (id1,mapPredType (sort_map mor1) t) (pred_map mor2)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder -- ??? dangerous use of Map.find here (may lead to call of error!)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederlegalSign sigma =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder Map.foldWithKey (\s sset b -> b && legalSort s && Set.all legalSort sset)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder True (Rel.toMap (sortRel sigma))
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder && Map.fold (\ts b -> b && Set.all legalOpType ts)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder True (opMap sigma)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder && Map.fold (\ts b -> b && Set.all legalPredType ts)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder True (predMap sigma)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder && Map.fold (\sset b -> b && Set.all legalSort sset)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder True (varMap sigma)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder where sorts = sortSet sigma
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder legalSort s = Set.member s sorts
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder legalOpType t = legalSort (opRes t)
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder && all legalSort (opArgs t)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder legalPredType t = all legalSort (predArgs t)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian MaederlegalMor mor =
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder legalSign sigma1
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder && legalSign sigma2
0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder (\s1 s2 b -> b && Set.member s1 (sortSet sigma1)
200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder && Set.member s2 (sortSet sigma2))
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (\(id1,t) (id2,k) b ->
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder Set.member t (Map.findWithDefault Set.empty id1 (opMap sigma1))
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Set.member (mapOpTypeK smap k t)
1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder (Map.findWithDefault Set.empty id2 (opMap sigma2))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder True (fun_map mor)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (\(id1,t) id2 b ->
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Set.member t (Map.findWithDefault Set.empty id1 (predMap sigma1))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder Set.member (mapPredType smap t)
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (Map.findWithDefault Set.empty id2 (predMap sigma2))
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder True (pred_map mor)
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder where sigma1 = msource mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder sigma2 = mtarget mor
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder smap = sort_map mor
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederinstance PrettyPrint Morphism where
7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder printText0 ga mor =
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (if null sorts then empty
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder else ptext "sorts" <+> (fsep $ punctuate comma sorts))
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (if null ops then empty
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else ptext "ops" <+> (fsep $ punctuate comma ops))
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (if null preds then empty
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder else ptext "preds" <+> (fsep $ punctuate comma preds))
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ptext " : " <+>
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ptext "{" <+> printText0 ga (msource mor) <+> ptext "}" <+>
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder ptext "->" <+>
b10d6cef708b7a659f2d3b367e8e0db0d03ae3f5Till Mossakowski ptext "{" <+> printText0 ga (mtarget mor) <+> ptext "}"
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder where sorts = map print_sort_map (Map.toList $ sort_map mor)
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder print_sort_map (s1,s2) =
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski printText0 ga s1 <+> ptext "|->" <+> printText0 ga s2
4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder ops = map print_op_map (Map.toList $ fun_map mor)
578b677874296e4ba48e57b5e4b4b0270d995603Christian Maeder print_op_map ((id1,ot),(id2,kind)) =
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder printText0 ga (Qual_op_name id1 (toOP_TYPE ot) [])
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> ptext "|->" <+>
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder printText0 ga id2
d79a4d0d842c212f82f9507fff178ffe4ba2e214Christian Maeder preds = map print_pred_map (Map.toList $ pred_map mor)
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder print_pred_map ((id1,pt),id2) =
68138d26bcddf5e89c30206aa83ab5ec006d170dChristian Maeder printText0 ga (Qual_pred_name id1 (toPRED_TYPE pt) [])
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder <+> ptext "|->" <+>
e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder printText0 ga id2