Morphism.hs revision 0e2ae85e2453466d03c1fc5884a3d693235bb9d9
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiModule : $Header$
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiMaintainer : hets@tzi.de
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiStability : provisional
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiPortability : portable
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiSymbols and signature morphisms for the CASL logic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaithe qualification only applies to __+__ !
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiimport qualified Common.Lib.Map as Map
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiimport qualified Common.Lib.Set as Set
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiimport qualified Common.Lib.Rel as Rel
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata SymbType = OpAsItemType OpType
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- since symbols do not speak about totality, the totality
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- information in OpType has to be ignored
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai | PredAsItemType PredType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi | SortAsItemType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi deriving (Show)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- Ordering and equality of symbol types has to ingore totality information
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Ord SymbType where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (OpAsItemType ot1) (OpAsItemType ot2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (opArgs ot1,opRes ot1) (opArgs ot2,opRes ot2)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (OpAsItemType _) _ = LT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (PredAsItemType pt1) (PredAsItemType pt2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare pt1 pt2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (PredAsItemType _) (OpAsItemType _) = GT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare (PredAsItemType _) SortAsItemType = LT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare SortAsItemType SortAsItemType = EQ
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi compare SortAsItemType _ = GT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Eq SymbType where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi t1 == t2 = compare t1 t2 == EQ
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata Symbol = Symbol {symName :: Id, symbType :: SymbType}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi deriving (Show, Eq, Ord)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype SymbolSet = Set.Set Symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype SymbolMap = Map.EndoMap Symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi deriving (Show, Eq, Ord)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype RawSymbolSet = Set.Set RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype RawSymbolMap = Map.EndoMap RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata Kind = SortKind | FunKind | PredKind
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi deriving (Show, Eq, Ord)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype Sort_map = Map.Map SORT SORT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype Fun_map = Map.Map (Id,OpType) (Id, FunKind)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype Pred_map = Map.Map (Id,PredType) Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Morphism f e m = Morphism {msource :: Sign f e,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mtarget :: Sign f e,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sort_map :: Sort_map,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fun_map :: Fun_map,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pred_map :: Pred_map,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi extended_map :: m}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi deriving (Eq, Show)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapSort :: Sort_map -> SORT -> SORT
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapSort sorts s = Map.findWithDefault s s sorts
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpType :: Sort_map -> OpType -> OpType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpType sorts t = t { opArgs = map (mapSort sorts) $ opArgs t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , opRes = mapSort sorts $ opRes t }
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimakeTotal :: FunKind -> OpType -> OpType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimakeTotal Total t = t { opKind = Total }
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimakeTotal _ t = t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapOpSym sMap fMap (i, ot) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi let mot = mapOpType sMap ot
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi val = (i, mot) in -- unchanged names need not be in Fun_map
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi case Map.lookup (i, ot) fMap of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Nothing -> case opKind ot of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Total -> case Map.lookup (i, ot {opKind = Partial}) fMap of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Nothing -> val
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Just (j, _) -> (j, mot) -- remains total
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Just (j, k) -> (j, makeTotal k mot)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Check if two OpTypes are equal except from totality or partiality
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchicompatibleOpTypes :: OpType -> OpType -> Bool
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchicompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapPredType :: Sort_map -> PredType -> PredType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapPredType sorts t = t { predArgs = map (mapSort sorts) $ predArgs t }
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchimapPredSym sMap fMap (i, pt) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchitype Ext f e m = Sign f e -> Sign f e -> m
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiembedMorphism :: Ext f e m -> Sign f e -> Sign f e -> Morphism f e m
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiembedMorphism extEm a b =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi { msource = a
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , mtarget = b
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , sort_map = Set.fold (\x -> Map.insert x x) Map.empty
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (\t -> Map.insert (i,t) (i, opKind t)) m ts)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (\t -> Map.insert (i,t) i) m ts)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , extended_map = extEm a b
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToSortSymbol :: Id -> Symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToSortSymbol idt = Symbol idt SortAsItemType
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToOpSymbol :: Id -> OpType -> Symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToPredSymbol :: Id -> PredType -> Symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbTypeToKind :: SymbType -> Kind
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbTypeToKind (OpAsItemType _) = FunKind
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbTypeToKind (PredAsItemType _) = PredKind
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbTypeToKind SortAsItemType = SortKind
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbolToRaw :: Symbol -> RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbolToRaw sym = ASymbol sym
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToRaw :: Id -> RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiidToRaw x = AnID x
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchirawSymName :: RawSymbol -> Id
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchirawSymName (ASymbol sym) = symName sym
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchirawSymName (AnID i) = i
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchirawSymName (AKindedId _ i) = i
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymOf :: Sign f e -> SymbolSet
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi let sorts = Set.image idToSortSymbol $ sortSet sigma
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Map.toList $ predMap sigma
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi in Set.unions [sorts, ops, preds]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchistatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchistatSymbMapItems sl = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ls <- sequence $ map s1 sl
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi foldl insertRsys (return Map.empty) (concat ls)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi insertRsys m (rsy1,rsy2) = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi case Map.lookup rsy1 m1 of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Nothing -> return $ Map.insert rsy1 rsy2 m1
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi plain_error m1 ("Symbol "++showPretty rsy1 " mapped twice to "
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ++showPretty rsy2 " and "++showPretty rsy3 "") nullPos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchipairM :: Monad m => (m a,m b) -> m (a,b)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchipairM (x,y) = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol,RawSymbol)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbOrMapToRaw k (Symb s) = pairM (symbToRaw k s,symbToRaw k s)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbOrMapToRaw k (Symb_map s t _) = pairM (symbToRaw k s,symbToRaw k t)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchistatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchistatSymbItems sl =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fmap concat (sequence (map s1 sl))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbToRaw k (Symb_id idt) = symbKindToRaw k idt
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbToRaw k (Qual_id idt t _) = typedSymbKindToRaw k idt t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbKindToRaw :: SYMB_KIND -> Id -> Result RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbKindToRaw Implicit idt = return (AnID idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbKindToRaw (Sorts_kind) idt = return (AKindedId SortKind idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbKindToRaw (Ops_kind) idt = return (AKindedId FunKind idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbKindToRaw (Preds_kind) idt = return (AKindedId PredKind idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw Implicit idt (O_type ot) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToOpSymbol idt (toOpType ot)))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw Implicit idt (P_type pt) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToPredSymbol idt (toPredType pt)))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- in case of ambiguity, return a constant function type
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- this deviates from the CASL summary !!!
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw Implicit idt (A_type s) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToOpSymbol idt ot))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi where ot = OpType {opKind = Total, opArgs = [], opRes = s}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw (Sorts_kind) idt _ = return (AKindedId SortKind idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw (Ops_kind) idt (O_type ot) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToOpSymbol idt (toOpType ot)))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw (Preds_kind) idt (P_type pt) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToPredSymbol idt (toPredType pt)))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw (Ops_kind) idt (A_type s) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToOpSymbol idt ot))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi where ot = OpType {opKind = Total, opArgs = [], opRes = s}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw (Preds_kind) idt (A_type s) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (ASymbol (idToPredSymbol idt pt))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi where pt = PredType {predArgs = [s]}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitypedSymbKindToRaw k idt t =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi plain_error (AnID idt)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (showPretty idt ":" ++ showPretty t
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi "does not have kind" ++showPretty k "") nullPos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbMapToMorphism :: Ext f e m -> Sign f e -> Sign f e
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi -> SymbolMap -> Result (Morphism f e m)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchisymbMapToMorphism extEm sigma1 sigma2 smap = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sort_map1 <- Set.fold mapMSort (return Map.empty) (sortSet sigma1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fun_map1 <- Map.foldWithKey mapFun (return Map.empty) (opMap sigma1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pred_map1 <- Map.foldWithKey mapPred (return Map.empty) (predMap sigma1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (Morphism { msource = sigma1,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mtarget = sigma2,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sort_map = sort_map1,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fun_map = fun_map1,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pred_map = pred_map1,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi extended_map = extEm sigma1 sigma2})
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mapMSort s m = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sym <- maybeToResult nullPos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ("symbMapToMorphism - Could not map sort "++showPretty s "")
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi $ Map.lookup (Symbol {symName = s,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi symbType = SortAsItemType}) smap
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (Map.insert s (symName sym) m1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mapFun i ots m = Set.fold (insFun i) m ots
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi insFun i ot m = do
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sym <- maybeToResult nullPos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ("symbMapToMorphism - Could not map op "++showPretty i "")
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi $ Map.lookup (Symbol {symName = i,
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi symbType = OpAsItemType ot}) smap
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi k <- case symbType sym of
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi OpAsItemType oty -> return $ opKind oty
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi _ -> plain_error Total
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ("symbMapToMorphism - Wrong result symbol type for op"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi ++showPretty i "") nullPos
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (Map.insert (i, ot) (symName sym,k) m1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi mapPred i pts m = Set.fold (insPred i) m pts
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai insPred i pt m = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sym <- maybeToResult nullPos
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ("symbMapToMorphism - Could not map pred "++showPretty i "")
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt})
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case symbType sym of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai PredAsItemType _ot -> return ()
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> plain_error ()
aa59c4cb15a6ac5d4e585dadf7a055b580abf579rsb ("symbMapToMorphism - Wrong result symbol type for pred"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ++showPretty i "") nullPos
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return (Map.insert (i, pt) (symName sym) m1)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimorphismToSymbMap :: Morphism f e m -> SymbolMap
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimorphismToSymbMap mor =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai src = msource mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sorts = sort_map mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ops = fun_map mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai preds = pred_map mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sortSymMap = Set.fold ( \ s -> Map.insert (idToSortSymbol s) $
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai idToSortSymbol $ mapSort sorts s)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Map.empty $ sortSet src
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ( \ i s m -> Set.fold
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ( \ t -> Map.insert (idToOpSymbol i t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ uncurry idToOpSymbol $ mapOpSym sorts ops (i, t)) m s)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ( \ i s m -> Set.fold
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ( \ t -> Map.insert (idToPredSymbol i t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ uncurry idToPredSymbol $ mapPredSym sorts preds (i, t)) m s)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Map.empty $ predMap src
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai foldr Map.union sortSymMap [opSymMap,predSymMap]
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches :: Symbol -> RawSymbol -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches x (ASymbol y) = x==y
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwmatches (Symbol idt _) (AnID di) = idt==di
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches (Symbol idt SortAsItemType) (AKindedId SortKind di) = idt==di
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches (Symbol idt (OpAsItemType _)) (AKindedId FunKind di) = idt==di
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches (Symbol idt (PredAsItemType _)) (AKindedId PredKind di) = idt==di
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimatches _ _ = False
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiidMor :: Ext f e m -> Sign f e -> Morphism f e m
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiidMor extEm sigma = embedMorphism extEm sigma sigma
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompose :: (Eq e, Eq f) => (m -> m -> m)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> Morphism f e m -> Morphism f e m -> Maybe (Morphism f e m)
681d9761e8516a7dc5ab6589e2dfe717777e1123Eric Taylorcompose comp mor1 mor2 = if mtarget mor1 == msource mor2 then Just $
681d9761e8516a7dc5ab6589e2dfe717777e1123Eric Taylor let sMap1 = sort_map mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sMap2 = sort_map mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in Morphism {
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai msource = msource mor1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mtarget = mtarget mor2,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sort_map = Map.map ( \ s -> mapSort sMap2 s) sMap1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai fun_map = Map.mapWithKey ( \ (_, ot) (j, k) ->
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let (ni, nt) = mapOpSym sMap2 (fun_map mor2) (j,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mapOpTypeK sMap1 k ot)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in (ni, opKind nt)) $ fun_map mor1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pred_map = Map.mapWithKey ( \ (_, ot) j ->
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw fst $ mapPredSym sMap2 (pred_map mor2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (j, mapPredType sMap1 ot)) $ pred_map mor1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai extended_map = comp (extended_map mor1) (extended_map mor2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else Nothing
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailegalSign :: Sign f e -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailegalSign sigma =
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Map.foldWithKey (\s sset b -> b && legalSort s && Set.all legalSort sset)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (Rel.toMap (sortRel sigma))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (opMap sigma)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (predMap sigma)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (varMap sigma)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai where sorts = sortSet sigma
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legalSort s = Set.member s sorts
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legalOpType t = legalSort (opRes t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && all legalSort (opArgs t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legalPredType t = all legalSort (predArgs t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailegalMor :: Morphism f e m -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailegalMor mor =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legalSign sigma1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && legalSign sigma2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (\s1 s2 b -> b && Set.member s1 (sortSet sigma1)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && Set.member s2 (sortSet sigma2))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (\(id1,t) (id2,k) b ->
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Set.member t (Map.findWithDefault Set.empty id1 (opMap sigma1))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Set.member (mapOpTypeK smap k t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (fun_map mor)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (\(id1,t) id2 b ->
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Set.member t (Map.findWithDefault Set.empty id1 (predMap sigma1))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Set.member (mapPredType smap t)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True (pred_map mor)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw where sigma1 = msource mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma2 = mtarget mor
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw smap = sort_map mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaisigInclusion :: (PrettyPrint e, PrettyPrint f)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai => Ext f e m -- ^ compute extended morphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> (e -> e -> Bool) -- ^ subsignature test of extensions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> Sign f e -> Sign f e -> Result (Morphism f e m)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaisigInclusion extEm isSubExt sigma1 sigma2 =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if isSubSig isSubExt sigma1 sigma2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then return (embedMorphism extEm sigma1 sigma2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else pfatal_error
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (text "Attempt to construct inclusion between non-subsignatures:"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ text "Singature 1:" $$ printText sigma1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ text "Singature 2:" $$ printText sigma2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimorphismUnion :: (m -> m -> m) -- ^ join morphism extensions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> (e -> e -> e) -- ^ join signature extensions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaimorphismUnion uniteM addSigExt mor1 mor2 = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let smap1 = sort_map mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai smap2 = sort_map mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai omap1 = fun_map mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai omap2 = fun_map mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pmap1 = pred_map mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pmap2 = pred_map mor2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw smap = smap1 `Map.union` smap2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (omap, omap3) = Map.foldWithKey ( \ p@(i, ot) v m@(m1, m2) ->
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw if Map.member p omap1 then m
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else let oty = ot { opKind = case opKind ot of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Total -> Partial
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Partial -> Total }
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in case Map.lookup (i, oty) omap1 of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just v2 -> let m3 = Map.delete p m2 in
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if v == v2 then (m1, m3)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else (m1, Map.insert (i, oty) v m3)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- re-add with same opKind
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> (Map.insert p v m1, m2)) (omap1, omap2) omap2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pmap = pmap1 `Map.union` pmap2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ( \x y -> if x==y then Nothing else Just x) m
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai when (not (smap2 `Map.subset` smap))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (pplain_error ()
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (text "Incompatible signature morphisms."
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ text "The following sorts are mapped differently"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <+> printText (Set.fromList $ diffKeys smap2 smap))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai when (not (omap3 `Map.subset` omap))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (pplain_error ()
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (text "Incompatible signature morphisms."
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ text "The following operations are mapped differently"
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw <+> printText (Set.fromList
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ map ( \ (i, ot) -> idToOpSymbol i ot)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ diffKeys omap3 omap))
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw when (not (pmap2 `Map.subset` pmap))
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (pplain_error ()
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (text "Incompatible signature morphisms."
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ text "The following predicates are mapped differently"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <+> printText (Set.fromList
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ map (\ (i, pt) -> idToPredSymbol i pt)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ diffKeys pmap2 pmap))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return $ Morphism { msource = addSig addSigExt (msource mor1) $ msource mor2,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mtarget = addSig addSigExt (mtarget mor1) $ mtarget mor2,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sort_map = smap,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai fun_map = omap,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pred_map = pmap,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai extended_map = uniteM (extended_map mor1) $
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai extended_map mor2}
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance PrettyPrint Symbol where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga sy =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga (symName sy) <>
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw case symbType sy of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai SortAsItemType -> empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai st -> space <> colon <> printText0 ga st
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance PrettyPrint SymbType where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- op types try to place a question mark immediately after a colon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga (OpAsItemType ot) = printText0 ga ot
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga (PredAsItemType pt) = space <> printText0 ga pt
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 _ SortAsItemType = empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance PrettyPrint Kind where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 _ SortKind = text sortS
cbcfaf83d8f1bf6aa00c793903a55685cac2c548jg printText0 _ FunKind = text opS
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 _ PredKind = text predS
cbcfaf83d8f1bf6aa00c793903a55685cac2c548jginstance PrettyPrint RawSymbol where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga rsym = case rsym of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ASymbol sy -> printText0 ga sy
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai AnID i -> printText0 ga i
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai AKindedId k i -> printText0 ga k <+> printText0 ga i
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance (PrettyPrint e, PrettyPrint f, PrettyPrint m) =>
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw PrettyPrint (Morphism f e m) where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga mor =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (if null sorts then empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else text (sortS ++ sS) <+> (fsep $ punctuate comma sorts))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (if null ops then empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else text (opS ++ sS) <+> (fsep $ punctuate comma ops))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (if null preds then empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else text (predS ++ sS) <+> (fsep $ punctuate comma preds))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ printText0 ga (extended_map mor)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ nest 1 colon $$
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw nest 3 (braces (space <> printText0 ga (msource mor) <> space))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ nest 1 (text funS)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $$ nest 4 (braces (space <> printText0 ga (mtarget mor) <> space))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai where sMap = sort_map mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sorts = map print_sort_map (Map.toList sMap)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw print_sort_map (s1,s2) =
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw printText0 ga s1 <+> text mapsTo <+> printText0 ga s2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ops = map print_op_map (Map.toList $ fun_map mor)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai print_op_map ((id1,ot),(id2, kind)) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga id1 <+> colon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <> printText0 ga (toOP_TYPE ot)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <+> text mapsTo <+>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga id2 <+> colon <>
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (printText0 ga $ toOP_TYPE $ mapOpTypeK sMap kind ot)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai preds = map print_pred_map (Map.toList $ pred_map mor)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai print_pred_map ((id1,pt),id2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga id1 <+> colon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <+> printText0 ga (toPRED_TYPE pt)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <+> text mapsTo <+>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai printText0 ga id2 <+> colon <+>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (printText0 ga $ toPRED_TYPE $ mapPredType sMap pt)