Morphism.hs revision e82587ca2892d246aa4405c2f5b9f30f287f9ebf
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Symbols and signature morphisms for the CASL logic
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzCopyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzMaintainer : Christian.Maeder@dfki.de
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzStability : provisional
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzPortability : portable
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzSymbols and signature morphisms for the CASL logic
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzthe qualification only applies to __+__ !
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzpossibly reuse SYMB_KIND for Kind
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulzimport qualified Data.Map as Map
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzimport qualified Data.Set as Set
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzimport qualified Common.Lib.Rel as Rel
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype SymbolSet = Set.Set Symbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype SymbolMap = Map.Map Symbol Symbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz deriving (Show, Eq, Ord)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzinstance PosItem RawSymbol where
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz getRange rs = case rs of
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz ASymbol s -> getRange s
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz AnID i -> getRange i
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz AKindedId _ i -> getRange i
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype RawSymbolSet = Set.Set RawSymbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype RawSymbolMap = Map.Map RawSymbol RawSymbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzdata Kind = SortKind | FunKind | PredKind deriving (Show, Eq, Ord)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype Sort_map = Map.Map SORT SORT
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz-- always use the partial profile as key!
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulztype Fun_map = Map.Map (Id, OpType) (Id, FunKind)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulztype Pred_map = Map.Map (Id, PredType) Id
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulztype CASLMor = Morphism () () ()
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzdata MorKind = IdMor | InclMor | OtherMor deriving (Show, Eq, Ord)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzdata Morphism f e m = Morphism
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz { msource :: Sign f e
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , mtarget :: Sign f e
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , morKind :: MorKind
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , sort_map :: Sort_map
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , fun_map :: Fun_map
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , pred_map :: Pred_map
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , extended_map :: m
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz } deriving Show
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzisInclusionMorphism :: Morphism f e m -> Bool
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzisInclusionMorphism m = morKind m <= InclMor
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzinstance (Eq f, Eq e, Eq m) => Eq (Morphism f e m) where
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz m1 == m2 = msource m1 == msource m2 &&
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz (morKind m1 == IdMor && morKind m2 == IdMor
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz || mtarget m1 == mtarget m2) &&
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz sort_map m1 == sort_map m2 &&
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz fun_map m1 == fun_map m2 &&
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pred_map m1 == pred_map m2 &&
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder extended_map m1 == extended_map m2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapSort :: Sort_map -> SORT -> SORT
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapSort sorts s = Map.findWithDefault s s sorts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpType :: Sort_map -> OpType -> OpType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpType sorts t = if Map.null sorts then t else
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder t { opArgs = map (mapSort sorts) $ opArgs t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , opRes = mapSort sorts $ opRes t }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeTotal :: FunKind -> OpType -> OpType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeTotal fk t = case fk of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Total -> t { opKind = Total }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpSym sMap fMap (i, ot) = let mot = mapOpType sMap ot in
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case Map.lookup (i, ot {opKind = Partial} ) fMap of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> (i, mot)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just (j, k) -> (j, makeTotal k mot)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Check if two OpTypes are equal modulo totality or partiality
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercompatibleOpTypes :: OpType -> OpType -> Bool
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzcompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzmapPredType :: Sort_map -> PredType -> PredType
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzmapPredType sorts t = if Map.null sorts then t else
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz t { predArgs = map (mapSort sorts) $ predArgs t }
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzmapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzmapPredSym sMap fMap (i, pt) =
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzembedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzembedMorphism extEm a b = Morphism
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz { msource = a
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , mtarget = b
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , morKind = OtherMor -- unknown for most uses
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , extended_map = extEm }
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymbTypeToKind :: SymbType -> Kind
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymbTypeToKind st = case st of
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz OpAsItemType _ -> FunKind
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz PredAsItemType _ -> PredKind
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz SortAsItemType -> SortKind
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymbolToRaw :: Symbol -> RawSymbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymbolToRaw sym = ASymbol sym
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzidToRaw :: Id -> RawSymbol
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzidToRaw x = AnID x
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzrawSymName :: RawSymbol -> Id
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzrawSymName rs = case rs of
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz ASymbol sym -> symName sym
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz AKindedId _ i -> i
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymOf :: Sign f e -> SymbolSet
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzsymOf sigma = let
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz sorts = Set.map idToSortSymbol $ sortSet sigma
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t) $ Set.toList ts)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz $ Map.toList $ opMap sigma
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz $ Set.toList ts) $ Map.toList $ predMap sigma
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz in Set.unions [sorts, ops, preds]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzstatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzstatSymbMapItems sl = do
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz ls <- sequence $ map s1 sl
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz foldl insertRsys (return Map.empty) (concat ls)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz insertRsys m (rsy1,rsy2) = do
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz case Map.lookup rsy1 m1 of
f54cad0338da90c6789bb9baae1caec50d994b3aEwaryst Schulz Nothing -> return $ Map.insert rsy1 rsy2 m1
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz plain_error m1 ("Symbol " ++ showDoc rsy1 " mapped twice to "
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzsymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol, RawSymbol)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzsymbOrMapToRaw k sm = do
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let (u, v) = case sm of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Symb s -> (s, s)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Symb_map s t _ -> (s, t)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz w <- symbToRaw k u
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz x <- symbToRaw k v
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz return (w, x)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzstatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzstatSymbItems sl =
f54cad0338da90c6789bb9baae1caec50d994b3aEwaryst Schulz fmap concat (sequence (map s1 sl))
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzsymbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzsymbToRaw k si = case si of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Symb_id idt -> return $ symbKindToRaw k idt
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Qual_id idt t _ -> typedSymbKindToRaw k idt t
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzsymbKindToRaw :: SYMB_KIND -> Id -> RawSymbol
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzsymbKindToRaw sk idt = case sk of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Implicit -> AnID idt
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz _ -> AKindedId (case sk of
f54cad0338da90c6789bb9baae1caec50d994b3aEwaryst Schulz Sorts_kind -> SortKind
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Preds_kind -> PredKind
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz _ -> FunKind) idt
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulztypedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulztypedSymbKindToRaw k idt t = let
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz err = plain_error (AnID idt)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz (showDoc idt ":" ++ showDoc t
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz "does not have kind" ++ showDoc k "") nullRange
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz aSymb = ASymbol $ case t of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz O_type ot -> idToOpSymbol idt $ toOpType ot
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz P_type pt -> idToPredSymbol idt $ toPredType pt
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz -- in case of ambiguity, return a constant function type
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz -- this deviates from the CASL summary !!!
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let ot = OpType {opKind = Total, opArgs = [], opRes = s}
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in idToOpSymbol idt ot
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Implicit -> return aSymb
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Sorts_kind -> err
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Ops_kind -> case t of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz P_type _ -> err
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz _ -> return aSymb
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Preds_kind -> case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder O_type _ -> err
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz A_type s -> return $ ASymbol $
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz let pt = PredType {predArgs = [s]}
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in idToPredSymbol idt pt
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder P_type _ -> return aSymb
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzsymbMapToMorphism :: m -> Sign f e -> Sign f e
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz -> SymbolMap -> Result (Morphism f e m)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzsymbMapToMorphism extEm sigma1 sigma2 smap = let
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz sort_map1 = Set.fold mapMSort Map.empty (sortSet sigma1)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz mapMSort s m =
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz of Just sym -> let t = symName sym in if s == t then m else
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz mapFun i ots m = Set.fold (insFun i) m ots
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insFun i ot m =
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz of Just sym -> let j = symName sym in case symbType sym of
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz OpAsItemType oty -> let k = opKind oty in
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz if j == i && opKind ot == k then m
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz else Map.insert (i, ot {opKind = Partial}) (j, k) m
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz mapPred i pts m = Set.fold (insPred i) m pts
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz insPred i pt m =
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz of Just sym -> let j = symName sym in case symbType sym of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz PredAsItemType _ -> if i == j then m else Map.insert (i, pt) j m
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz in return (embedMorphism extEm sigma1 sigma2)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz { sort_map = sort_map1
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz , fun_map = fun_map1
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz , pred_map = pred_map1 }
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzmorphismToSymbMap :: Morphism f e m -> SymbolMap
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzmorphismToSymbMap = morphismToSymbMapAux False
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzmorphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzmorphismToSymbMapAux b mor = let
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder src = msource mor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorts = sort_map mor
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz ops = fun_map mor
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz preds = pred_map mor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (\ s -> let t = mapSort sorts s in
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz if b && s == t then id else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.insert (idToSortSymbol s) $ idToSortSymbol t)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz ( \ t -> let (j, k) = mapOpSym sorts ops (i, t) in
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz if b && i == j && opKind k == opKind t then id else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.insert (idToOpSymbol i t) $ idToOpSymbol j k)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz m s) Map.empty $ opMap src
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz ( \ t -> let (j, k) = mapPredSym sorts preds (i, t) in
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz if b && i == j then id else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.insert (idToPredSymbol i t) $ idToPredSymbol j k)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m s) Map.empty $ predMap src
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in foldr Map.union sortSymMap [opSymMap, predSymMap]
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzmatches :: Symbol -> RawSymbol -> Bool
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzmatches x@(Symbol idt k) rs = case rs of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz ASymbol y -> x == y
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz AnID di -> idt == di
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz AKindedId rk di -> let res = idt == di in case (k, rk) of
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz (SortAsItemType, SortKind) -> res
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz (OpAsItemType _, FunKind) -> res
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz (PredAsItemType _, PredKind) -> res
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederidMor :: m -> Sign f e -> Morphism f e m
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzidMor extEm sigma = (embedMorphism extEm sigma sigma) { morKind = IdMor }
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzcompose :: (Eq e, Eq f) => (m -> m -> m)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulzcompose comp mor1 mor2 = if mtarget mor1 == msource mor2 then
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let sMap1 = sort_map mor1
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz src = msource mor1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz tar = mtarget mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz fMap1 = fun_map mor1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz pMap1 = pred_map mor1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz sMap2 = sort_map mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz fMap2 = fun_map mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz pMap2 = pred_map mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz sMap = if Map.null sMap2 then sMap1 else
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let j = mapSort sMap2 (mapSort sMap1 i) in
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz if i == j then id else Map.insert i j)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz emb = (embedMorphism (comp (extended_map mor1) $ extended_map mor2)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz src tar) { morKind = max (morKind mor1) $ morKind mor2 }
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz if Map.null sMap1 && Map.null sMap2 && Map.null fMap1 && Map.null fMap2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz && Map.null pMap1 && Map.null pMap2 then emb else emb
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz { sort_map = sMap
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz , fun_map = if Map.null fMap2 then fMap1 else
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let (ni, nt) = mapOpSym sMap2 fMap2 $
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz mapOpSym sMap1 fMap1 (i, ot)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz k = opKind nt
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz in assert (mapOpTypeK sMap k ot == nt) $
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz if i == ni && opKind ot == k then id else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.insert (i, ot {opKind = Partial }) (ni, k)) m t)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz , pred_map = if Map.null pMap2 then pMap1 else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz let (ni, nt) = mapPredSym sMap2 pMap2 $
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz mapPredSym sMap1 pMap1 (i, pt)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz in assert (mapPredType sMap pt == nt) $
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz if i == ni then id else Map.insert (i, pt) ni) m t)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.empty $ predMap src }
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz else fail "target of first and source of second morphism are different"
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzlegalSign :: Sign f e -> Bool
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzlegalSign sigma =
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz Map.foldWithKey (\s sset b -> b && legalSort s && all legalSort
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz True (Rel.toMap (sortRel sigma))
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz && Map.fold (\ts b -> b && all legalOpType (Set.toList ts))
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz True (opMap sigma)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder && Map.fold (\ts b -> b && all legalPredType (Set.toList ts))
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz True (predMap sigma)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz where sorts = sortSet sigma
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder legalSort s = Set.member s sorts
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz legalOpType t = legalSort (opRes t)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz && all legalSort (opArgs t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder legalPredType t = all legalSort (predArgs t)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzlegalMor :: Morphism f e m -> Bool
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let s1 = msource mor
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz s2 = mtarget mor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder smap = sort_map mor
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz msorts = Set.map $ mapSort smap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder flip $ Set.fold ( \ ot ->
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let (j, nt) = mapOpSym smap (fun_map mor) (i, ot)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz flip $ Set.fold ( \ pt ->
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let (j, nt) = mapPredSym smap (pred_map mor) (i, pt)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in Rel.setInsert j nt)) Map.empty $ predMap s1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in legalSign s1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz && Set.isSubsetOf (msorts $ sortSet s1) (sortSet s2)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz && Set.isSubsetOf (msorts $ emptySortSet s1) (emptySortSet s2)
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz && isSubOpMap mops (opMap s2)
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz && isSubMapSet mpreds (predMap s2)
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz && legalSign s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederidOrInclMorphism :: (e -> e -> Bool) -> Morphism f e m -> Morphism f e m
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzidOrInclMorphism isSubExt m =
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz let src = msource m
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz tar = mtarget m
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz in if isSubSig isSubExt tar src then m { morKind = IdMor }
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz else let diffOpMap = diffMapSet (opMap src) $ opMap tar in
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m { morKind = InclMor
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , fun_map = Map.fromList $ concatMap (\ (i, s) ->
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz map (\ t -> ((i, t), (i, Total)))
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst SchulzsigInclusion :: (Pretty f, Pretty e)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz => m -- ^ compute extended morphism
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> (e -> e -> Bool) -- ^ subsignature test of extensions
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz -> (e -> e -> e) -- ^ difference of signature extensions
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz -> Sign f e -> Sign f e -> Result (Morphism f e m)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersigInclusion extEm isSubExt diffExt sigma1 sigma2 =
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz if isSubSig isSubExt sigma1 sigma2 then
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz return $ idOrInclMorphism isSubExt $ embedMorphism extEm sigma1 sigma2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz else Result [Diag Error
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ("Attempt to construct inclusion between non-subsignatures:\n"
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ++ showDoc (diffSig diffExt sigma1 sigma2) "") nullRange] Nothing
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermorphismUnion :: (m -> m -> m) -- ^ join morphism extensions
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz -> (e -> e -> e) -- ^ join signature extensions
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- consider identity mappings but filter them eventually
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermorphismUnion uniteM addSigExt mor1 mor2 =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let smap1 = sort_map mor1
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz smap2 = sort_map mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz s1 = msource mor1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder s2 = msource mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz us1 = Set.difference (sortSet s1) $ Map.keysSet smap1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz us2 = Set.difference (sortSet s2) $ Map.keysSet smap2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz omap1 = fun_map mor1
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder omap2 = fun_map mor2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz uo1 = foldr delOp (opMap s1) $ Map.keys omap1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz uo2 = foldr delOp (opMap s2) $ Map.keys omap2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz delOp (n, ot) m = diffMapSet m $ Map.singleton n $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Set.fromList [ot {opKind = Partial}, ot {opKind = Total}]
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz uo = addOpMapSet uo1 uo2
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz pmap1 = pred_map mor1
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz pmap2 = pred_map mor2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder up1 = foldr delPred (predMap s1) $ Map.keys pmap1
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz up2 = foldr delPred (predMap s2) $ Map.keys pmap2
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz up = addMapSet up1 up2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder delPred (n, pt) m = diffMapSet m $ Map.singleton n $ Set.singleton pt
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz (sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Nothing -> (ds, Map.insert i j m)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just k -> if j == k then (ds, m) else
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz ("incompatible mapping of sort " ++ showId i " to "
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ showId j " and " ++ showId k "")
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nullRange : ds, m)) ([], smap1)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Map.toList smap2 ++ map (\ a -> (a, a))
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz (ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> (ds, Map.insert isc jsc m)
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz Just (k, p) -> if j == k then if p == t then (ds, m)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else (ds, Map.insert isc (j, Total) m) else
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz ("incompatible mapping of op " ++ showId i ":"
e9f0cd6ee7be0336cfd071df0451d6282cf55d75Ewaryst Schulz ++ showDoc ot { opKind = t } " to "
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ++ showId j " and " ++ showId k "") nullRange : ds, m))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (sds, omap1) (Map.toList omap2 ++ concatMap
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ( \ (a, s) -> map ( \ ot -> ((a, ot {opKind = Partial}),
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz (a, opKind ot)))
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz (pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Nothing -> (ds, Map.insert isc j m)
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz Just k -> if j == k then (ds, m) else
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz ("incompatible mapping of pred " ++ showId i ":"
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ++ showDoc pt " to " ++ showId j " and "
a3b8d685ae08bf3f83a6c2930e872183c487c844Ewaryst Schulz ++ showId k "") nullRange : ds, m)) (ods, pmap1)
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz (Map.toList pmap2 ++ concatMap ( \ (a, s) -> map
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz ( \ pt -> ((a, pt), a)) $ Set.toList s) (Map.toList up))
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz s3 = addSig addSigExt s1 s2
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz o3 = opMap s3 in
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz if null pds then Result [] $ Just
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz (embedMorphism (uniteM (extended_map mor1) $ extended_map mor2)
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz s3 $ addSig addSigExt (mtarget mor1) $ mtarget mor2)
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz { morKind = max (morKind mor1) $ morKind mor2
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz , sort_map = Map.filterWithKey (/=) smap
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz (\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz , pred_map = Map.filterWithKey (\ (i, _) j -> i /= j) pmap }
7594b91154e299c9bcecd2bd62698705b55f99e8Ewaryst Schulz else Result pds Nothing
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst SchulzisSortInjective :: Morphism f e m -> Bool
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzisSortInjective m =
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz null [() | k1 <- src, k2 <- src, k1 /= k2,
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz (Map.lookup k1 sm :: Maybe SORT) == Map.lookup k2 sm]
67f09e0fddea50c48620c011b6d001cffe565de6Ewaryst Schulz where sm = sort_map m
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzisInjective :: Morphism f e m -> Bool
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzisInjective m =
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz null [() | k1 <- src, k2 <- src, k1 /= k2,
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz (Map.lookup k1 symmap :: Maybe Symbol) == Map.lookup k2 symmap]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz where src = Map.keys symmap
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz symmap = morphismToSymbMap m
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzinstance Pretty Kind where
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz pretty k = keyword $ case k of
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz SortKind -> sortS
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz FunKind -> opS
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz PredKind -> predS
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzinstance Pretty RawSymbol where
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz pretty rsym = case rsym of
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz ASymbol sy -> pretty sy
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz AnID i -> pretty i
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz AKindedId k i -> pretty k <+> pretty i
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzprintMorphism :: (f -> Doc) -> (e -> Doc) -> (m -> Doc) -> Morphism f e m
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst SchulzprintMorphism fF fE fM mor =
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz let src = msource mor
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz tar = mtarget mor
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz ops = fun_map mor
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz prSig s = specBraces (space <> printSign fF fE s)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz srcD = prSig src
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz in case morKind mor of
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz IdMor -> fsep [text "identity morphism over", srcD]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz InclMor -> fsep
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz [ text "inclusion morphism of", srcD
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , fsep $ if Map.null ops then
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz [ text "extended with"
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , pretty $ Set.difference (symOf tar) $ symOf src ]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz [ text "by totalizing"
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz , pretty $ Set.map (uncurry idToOpSymbol) $ Map.keysSet ops ]]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz OtherMor -> fsep
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz [ pretty (morphismToSymbMapAux True mor)
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz $+$ fM (extended_map mor)
dde363c92873e122a139e2db23862dfd7d265b73Ewaryst Schulz , colon <+> srcD, mapsto <+> prSig tar ]
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulzinstance (Pretty e, Pretty f, Pretty m) =>
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz Pretty (Morphism f e m) where
6c3ce177a0ad551edaae7daa17772b12f77a86daEwaryst Schulz pretty = printMorphism pretty pretty pretty