{- |

Module : $Header$

Description : Symbols and signature morphisms for the CASL logic

Copyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : non-portable (MPTC+FD)

Symbols and signature morphisms for the CASL logic

-}

module CASL.Morphism where

import CASL.Sign

import CASL.AS_Basic_CASL

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Common.Lib.Rel as Rel

import Common.Doc

import Common.DocUtils

import Common.Id

import Common.Result

import Control.Exception (assert)

import Control.Monad

type SymbolSet = Set.Set Symbol

type SymbolMap = Map.Map Symbol Symbol

data RawSymbol = ASymbol Symbol | AKindedSymb SYMB_KIND Id

deriving (Show, Eq, Ord)

instance GetRange RawSymbol where

getRange rs = case rs of

ASymbol s -> getRange s

AKindedSymb _ i -> getRange i

type RawSymbolSet = Set.Set RawSymbol

type RawSymbolMap = Map.Map RawSymbol RawSymbol

type Sort_map = Map.Map SORT SORT

-- always use the partial profile as key!

type Op_map = Map.Map (Id, OpType) (Id, OpKind)

type Pred_map = Map.Map (Id, PredType) Id

data Morphism f e m = Morphism

{ msource :: Sign f e

, mtarget :: Sign f e

, sort_map :: Sort_map

, op_map :: Op_map

, pred_map :: Pred_map

, extended_map :: m

} deriving (Show, Eq, Ord)

data DefMorExt e = DefMorExt deriving (Show, Eq, Ord)

emptyMorExt :: DefMorExt e

emptyMorExt = DefMorExt

instance Pretty (DefMorExt e) where

pretty _ = empty

class MorphismExtension e m | m -> e where

ideMorphismExtension :: e -> m

composeMorphismExtension :: m -> m -> Result m

inverseMorphismExtension :: m -> Result m

isInclusionMorphismExtension :: m -> Bool

instance MorphismExtension () () where

ideMorphismExtension _ = ()

composeMorphismExtension _ = return

inverseMorphismExtension = return

isInclusionMorphismExtension _ = True

instance MorphismExtension e (DefMorExt e) where

ideMorphismExtension _ = emptyMorExt

composeMorphismExtension _ = return

inverseMorphismExtension = return

isInclusionMorphismExtension _ = True

type CASLMor = Morphism () () ()

isInclusionMorphism :: (m -> Bool) -> Morphism f e m -> Bool

isInclusionMorphism f m = f (extended_map m) && Map.null (sort_map m)

&& Map.null (pred_map m) && isInclOpMap (op_map m)

mapSort :: Sort_map -> SORT -> SORT

mapSort sorts s = Map.findWithDefault s s sorts

mapOpType :: Sort_map -> OpType -> OpType

mapOpType sorts t = if Map.null sorts then t else

t { opArgs = map (mapSort sorts) $ opArgs t

, opRes = mapSort sorts $ opRes t }

mapOpTypeK :: Sort_map -> OpKind -> OpType -> OpType

mapOpTypeK sorts k = makeTotal k . mapOpType sorts

makeTotal :: OpKind -> OpType -> OpType

makeTotal fk t = case fk of

Total -> mkTotal t

_ -> t

mapOpSym :: Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)

mapOpSym sMap oMap (i, ot) = let mot = mapOpType sMap ot in

case Map.lookup (i, mkPartial ot) oMap of

Nothing -> (i, mot)

Just (j, k) -> (j, makeTotal k mot)

-- | Check if two OpTypes are equal modulo totality or partiality

compatibleOpTypes :: OpType -> OpType -> Bool

compatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

mapPredType :: Sort_map -> PredType -> PredType

mapPredType sorts t = if Map.null sorts then t else

t { predArgs = map (mapSort sorts) $ predArgs t }

mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)

mapPredSym sMap oMap (i, pt) =

(Map.findWithDefault i (i, pt) oMap, mapPredType sMap pt)

embedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m

embedMorphism extEm a b = Morphism

{ msource = a

, mtarget = b

, sort_map = Map.empty

, op_map = Map.empty

, pred_map = Map.empty

, extended_map = extEm }

symbTypeToKind :: SymbType -> SYMB_KIND

symbTypeToKind st = case st of

OpAsItemType _ -> Ops_kind

PredAsItemType _ -> Preds_kind

SortAsItemType -> Sorts_kind

OtherTypeKind s -> OtherKinds s

symbolToRaw :: Symbol -> RawSymbol

symbolToRaw = ASymbol

idToRaw :: Id -> RawSymbol

idToRaw = AKindedSymb Implicit

rawSymName :: RawSymbol -> Id

rawSymName rs = case rs of

ASymbol sym -> symName sym

AKindedSymb _ i -> i

symOf :: Sign f e -> SymbolSet

symOf sigma = let

sorts = Set.map idToSortSymbol $ sortSet sigma

ops = Set.fromList $

concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t) $ Set.toList ts)

$ Map.toList $ opMap sigma

preds = Set.fromList $

concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)

$ Set.toList ts) $ Map.toList $ predMap sigma

in Set.unions [sorts, ops, preds]

checkSymbList :: [SYMB_OR_MAP] -> [Diagnosis]

checkSymbList l = case l of

Symb (Symb_id a) : Symb (Qual_id b t _) : r -> mkDiag Warning

("profile '" ++ showDoc t "' does not apply to '"

++ showId a "' but only to") b : checkSymbList r

_ : r -> checkSymbList r

[] -> []

statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

statSymbMapItems sl = do

let st (Symb_map_items kind l _) = do

appendDiags $ checkSymbList l

fmap concat $ mapM (symbOrMapToRaw kind) l

insertRsys m1 (rsy1, rsy2) = let m3 = Map.insert rsy1 rsy2 m1 in

case Map.lookup rsy1 m1 of

Nothing -> return $ case rsy1 of

ASymbol (Symbol i SortAsItemType) ->

case Map.lookup (AKindedSymb Implicit i) m1 of

Just (AKindedSymb Implicit j) | rawSymName rsy2 == j -> m1

_ -> m3

AKindedSymb Implicit i ->

let rsy3 = ASymbol (Symbol i SortAsItemType) in

case Map.lookup rsy3 m1 of

Just (ASymbol (Symbol j SortAsItemType))

| rawSymName rsy2 == j -> Map.delete rsy3 m3

_ -> m3

_ -> m3

Just rsy3 -> if rsy2 == rsy3 then return m1 else

plain_error m1 ("Symbol " ++ showDoc rsy1 " mapped twice to "

++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange

ls <- mapM st sl

foldM insertRsys Map.empty (concat ls)

symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result [(RawSymbol, RawSymbol)]

symbOrMapToRaw k sm = case sm of

Symb s -> do

v <- symbToRaw k s

return [(v, v)]

Symb_map s t _ -> do

appendDiags $ case (s, t) of

(Symb_id a, Symb_id b) | a == b ->

[mkDiag Hint "unneeded identical mapping of" a]

_ -> []

w <- symbToRaw k s

x <- symbToRaw k t

let mkS = ASymbol . idToSortSymbol

case (s, t) of

(Qual_id _ t1 _, Qual_id _ t2 _) -> case (t1, t2) of

(O_type (Op_type _ args1 res1 _), O_type (Op_type _ args2 res2 _))

| length args1 == length args2 -> -- ignore partiality

return $ (w, x) : (mkS res1, mkS res2)

: zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2

(P_type (Pred_type args1 _), P_type (Pred_type args2 _))

| length args1 == length args2 ->

return $ (w, x)

: zipWith (\ s1 s2 -> (mkS s1, mkS s2)) args1 args2

(O_type (Op_type _ [] res1 _), A_type s2) ->

return [(w, x), (mkS res1, mkS s2)]

(A_type s1, O_type (Op_type _ [] res2 _)) ->

return [(w, x), (mkS s1, mkS res2)]

(A_type s1, A_type s2) ->

return [(w, x), (mkS s1, mkS s2)]

_ -> fail $ "profiles '" ++ showDoc t1 "' and '"

++ showDoc t2 "' do not match"

_ -> return [(w, x)]

statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]

statSymbItems sl =

let st (Symb_items kind l _) = do

appendDiags $ checkSymbList $ map Symb l

mapM (symbToRaw kind) l

in fmap concat (mapM st sl)

symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol

symbToRaw k si = case si of

Symb_id idt -> return $ case k of

Sorts_kind -> ASymbol $ idToSortSymbol idt

_ -> AKindedSymb k idt

Qual_id idt t _ -> typedSymbKindToRaw k idt t

typedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol

typedSymbKindToRaw k idt t = let

err = plain_error (AKindedSymb Implicit idt)

(showDoc idt ":" ++ showDoc t

"does not have kind" ++ showDoc k "") nullRange

aSymb = ASymbol $ case t of

O_type ot -> idToOpSymbol idt $ toOpType ot

P_type pt -> idToPredSymbol idt $ toPredType pt

-- in case of ambiguity, return a constant function type

-- this deviates from the CASL summary !!!

A_type s ->

let ot = OpType {opKind = Total, opArgs = [], opRes = s}

in idToOpSymbol idt ot

in case k of

Implicit -> case t of

A_type _ -> do

appendDiags [mkDiag Warning "qualify name as pred or op" idt]

return aSymb

_ -> return aSymb

Ops_kind -> case t of

P_type _ -> err

_ -> return aSymb

Preds_kind -> case t of

O_type _ -> err

A_type s -> return $ ASymbol $

let pt = PredType {predArgs = [s]}

in idToPredSymbol idt pt

P_type _ -> return aSymb

_ -> err

symbMapToMorphism :: m -> Sign f e -> Sign f e

-> SymbolMap -> Result (Morphism f e m)

symbMapToMorphism extEm sigma1 sigma2 smap = let

sort_map1 = Set.fold mapMSort Map.empty (sortSet sigma1)

mapMSort s m =

case Map.lookup Symbol {symName = s, symbType = SortAsItemType} smap

of Just sym -> let t = symName sym in if s == t then m else

Map.insert s t m

Nothing -> m

op_map1 = Map.foldWithKey mapOp Map.empty (opMap sigma1)

pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)

mapOp i ots m = Set.fold (insOp i) m ots

insOp i ot m =

case Map.lookup Symbol {symName = i, symbType = OpAsItemType ot} smap

of Just sym -> let j = symName sym in case symbType sym of

OpAsItemType oty -> let k = opKind oty in

if j == i && opKind ot == k then m

else Map.insert (i, mkPartial ot) (j, k) m

_ -> m

_ -> m

mapPred i pts m = Set.fold (insPred i) m pts

insPred i pt m =

case Map.lookup Symbol {symName = i, symbType = PredAsItemType pt} smap

of Just sym -> let j = symName sym in case symbType sym of

PredAsItemType _ -> if i == j then m else Map.insert (i, pt) j m

_ -> m

_ -> m

in return (embedMorphism extEm sigma1 sigma2)

{ sort_map = sort_map1

, op_map = op_map1

, pred_map = pred_map1 }

morphismToSymbMap :: Morphism f e m -> SymbolMap

morphismToSymbMap = morphismToSymbMapAux False

morphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap

morphismToSymbMapAux b mor = let

src = msource mor

sorts = sort_map mor

ops = op_map mor

preds = pred_map mor

sortSymMap = Set.fold

(\ s -> let t = mapSort sorts s in

if b && s == t then id else

Map.insert (idToSortSymbol s) $ idToSortSymbol t)

Map.empty $ sortSet src

opSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> let (j, k) = mapOpSym sorts ops (i, t) in

if b && i == j && opKind k == opKind t then id else

Map.insert (idToOpSymbol i t) $ idToOpSymbol j k)

m s) Map.empty $ opMap src

predSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> let (j, k) = mapPredSym sorts preds (i, t) in

if b && i == j then id else

Map.insert (idToPredSymbol i t) $ idToPredSymbol j k)

m s) Map.empty $ predMap src

in foldr Map.union sortSymMap [opSymMap, predSymMap]

matches :: Symbol -> RawSymbol -> Bool

matches (Symbol idt k) rs = case rs of

ASymbol (Symbol id2 k2) -> idt == id2 && case (k, k2) of

(OpAsItemType ot, OpAsItemType ot2) -> compatibleOpTypes ot ot2

_ -> k == k2

AKindedSymb rk di -> let res = idt == di in case (k, rk) of

(_, Implicit) -> res

(SortAsItemType, Sorts_kind) -> res

(OpAsItemType _, Ops_kind) -> res

(PredAsItemType _, Preds_kind) -> res

(OtherTypeKind s, OtherKinds t) -> t == s && res

_ -> False

idMor :: m -> Sign f e -> Morphism f e m

idMor extEm sigma = embedMorphism extEm sigma sigma

composeM :: Eq e => (m -> m -> Result m)

-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)

composeM comp mor1 mor2 = if mtarget mor1 == msource mor2 then do

let sMap1 = sort_map mor1

src = msource mor1

tar = mtarget mor2

oMap1 = op_map mor1

pMap1 = pred_map mor1

sMap2 = sort_map mor2

oMap2 = op_map mor2

pMap2 = pred_map mor2

sMap = if Map.null sMap2 then sMap1 else Set.fold ( \ i ->

let j = mapSort sMap2 (mapSort sMap1 i) in

if i == j then id else Map.insert i j)

Map.empty $ sortSet src

oMap = if Map.null oMap2 then oMap1 else

Map.foldWithKey ( \ i t m ->

Set.fold ( \ ot ->

let (ni, nt) = mapOpSym sMap2 oMap2 $

mapOpSym sMap1 oMap1 (i, ot)

k = opKind nt

in assert (mapOpTypeK sMap k ot == nt) $

if i == ni && opKind ot == k then id else

Map.insert (i, mkPartial ot) (ni, k)) m t)

Map.empty $ opMap src

pMap = if Map.null pMap2 then pMap1 else

Map.foldWithKey ( \ i t m ->

Set.fold ( \ pt ->

let (ni, nt) = mapPredSym sMap2 pMap2 $

mapPredSym sMap1 pMap1 (i, pt)

in assert (mapPredType sMap pt == nt) $

if i == ni then id else Map.insert (i, pt) ni) m t)

Map.empty $ predMap src

extComp <- comp (extended_map mor1) $ extended_map mor2

let emb = embedMorphism extComp src tar

return $ emb

{ sort_map = sMap

, op_map = oMap

, pred_map = pMap }

else fail "target of first and source of second morphism are different"

legalSign :: Sign f e -> Bool

legalSign sigma =

Map.foldWithKey (\s sset b -> b && legalSort s && all legalSort

(Set.toList sset))

True (Rel.toMap (sortRel sigma))

&& Map.fold (\ts b -> b && all legalOpType (Set.toList ts))

True (opMap sigma)

&& Map.fold (\ts b -> b && all legalPredType (Set.toList ts))

True (predMap sigma)

where sorts = sortSet sigma

legalSort s = Set.member s sorts

legalOpType t = legalSort (opRes t)

&& all legalSort (opArgs t)

legalPredType = all legalSort . predArgs

-- | the image of a signature morphism

imageOfMorphism :: Morphism f e m -> Sign f e

imageOfMorphism m = imageOfMorphismAux (const $ extendedInfo $ mtarget m) m

-- | the generalized image of a signature morphism

imageOfMorphismAux :: (Morphism f e m -> e) -> Morphism f e m -> Sign f e

imageOfMorphismAux fE m =

inducedSignAux (\ _ _ _ _ _ -> fE m)

(sort_map m) (op_map m) (pred_map m) (extended_map m) (msource m)

type InducedSign f e m r =

Sort_map -> Op_map -> Pred_map -> m -> Sign f e -> r

-- | the induced signature image of a signature morphism

inducedSignAux :: InducedSign f e m e -> InducedSign f e m (Sign f e)

inducedSignAux f sm om pm em src =

let ms = mapSort sm

msorts = Set.map ms

in (emptySign $ f sm om pm em src)

{ sortSet = msorts $ sortSet src

, sortRel = Rel.map ms $ sortRel src

, emptySortSet = msorts $ emptySortSet src

, opMap = inducedOpMap sm om $ opMap src

, assocOps = inducedOpMap sm om $ assocOps src

, predMap = inducedPredMap sm pm $ predMap src }

inducedOpMap :: Sort_map -> Op_map -> OpMap -> OpMap

inducedOpMap sm fm = Map.foldWithKey

( \ i -> flip $ Set.fold ( \ ot ->

let (j, nt) = mapOpSym sm fm (i, ot)

in Rel.setInsert j nt)) Map.empty

inducedPredMap :: Sort_map -> Pred_map -> Map.Map Id (Set.Set PredType)

-> Map.Map Id (Set.Set PredType)

inducedPredMap sm pm = Map.foldWithKey

( \ i -> flip $ Set.fold ( \ ot ->

let (j, nt) = mapPredSym sm pm (i, ot)

in Rel.setInsert j nt)) Map.empty

legalMor :: Morphism f e m -> Bool

legalMor mor =

let s1 = msource mor

s2 = mtarget mor

sm = sort_map mor

msorts = Set.map $ mapSort sm

in legalSign s1

&& Set.isSubsetOf (msorts $ sortSet s1) (sortSet s2)

&& Set.isSubsetOf (msorts $ emptySortSet s1) (emptySortSet s2)

&& isSubOpMap (inducedOpMap sm (op_map mor) $ opMap s1) (opMap s2)

&& isSubMapSet (inducedPredMap sm (pred_map mor) $ predMap s1) (predMap s2)

&& legalSign s2

isInclOpMap :: Op_map -> Bool

isInclOpMap = all (\ ((i, _), (j, k)) -> i == j && k == Total) . Map.toList

idOrInclMorphism :: (e -> e -> Bool) -> Morphism f e m -> Morphism f e m

idOrInclMorphism isSubExt m =

let src = msource m

tar = mtarget m

in if isSubSig isSubExt tar src then m

else let diffOpMap = diffMapSet (opMap src) $ opMap tar in

m { op_map = Map.fromList $ concatMap (\ (i, s) ->

map (\ t -> ((i, t), (i, Total)))

$ Set.toList s) $ Map.toList diffOpMap }

sigInclusion :: (Pretty f, Pretty e)

=> m -- ^ computed extended morphism

-> (e -> e -> Bool) -- ^ subsignature test of extensions

-> (e -> e -> e) -- ^ difference of signature extensions

-> Sign f e -> Sign f e -> Result (Morphism f e m)

sigInclusion extEm isSubExt diffExt sigma1 sigma2 =

if isSubSig isSubExt sigma1 sigma2 then

return $ idOrInclMorphism isSubExt $ embedMorphism extEm sigma1 sigma2

else Result [Diag Error

("Attempt to construct inclusion between non-subsignatures:\n"

++ showDoc (diffSig diffExt sigma1 sigma2) "") nullRange] Nothing

addSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)

addSigM f a b = do

e <- f (extendedInfo a) $ extendedInfo b

return $ addSig (const $ const e) a b

morphismUnion :: (m -> m -> m) -- ^ join morphism extensions

-> (e -> e -> e) -- ^ join signature extensions

-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)

morphismUnion uniteM addSigExt =

morphismUnionM uniteM (\ e -> return . addSigExt e)

morphismUnionM :: (m -> m -> m) -- ^ join morphism extensions

-> (e -> e -> Result e) -- ^ join signature extensions

-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)

-- consider identity mappings but filter them eventually

morphismUnionM uniteM addSigExt mor1 mor2 =

let smap1 = sort_map mor1

smap2 = sort_map mor2

s1 = msource mor1

s2 = msource mor2

us1 = Set.difference (sortSet s1) $ Map.keysSet smap1

us2 = Set.difference (sortSet s2) $ Map.keysSet smap2

omap1 = op_map mor1

omap2 = op_map mor2

uo1 = foldr delOp (opMap s1) $ Map.keys omap1

uo2 = foldr delOp (opMap s2) $ Map.keys omap2

delOp (n, ot) m = diffMapSet m $ Map.singleton n $

Set.fromList [mkPartial ot, mkTotal ot]

uo = addOpMapSet uo1 uo2

pmap1 = pred_map mor1

pmap2 = pred_map mor2

up1 = foldr delPred (predMap s1) $ Map.keys pmap1

up2 = foldr delPred (predMap s2) $ Map.keys pmap2

up = addMapSet up1 up2

delPred (n, pt) m = diffMapSet m $ Map.singleton n $ Set.singleton pt

(sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of

Nothing -> (ds, Map.insert i j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of sort " ++ showId i " to "

++ showId j " and " ++ showId k "")

nullRange : ds, m)) ([], smap1)

(Map.toList smap2 ++ map (\ a -> (a, a))

(Set.toList $ Set.union us1 us2))

(ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc jsc m)

Just (k, p) -> if j == k then if p == t then (ds, m)

else (ds, Map.insert isc (j, Total) m) else

(Diag Error

("incompatible mapping of op " ++ showId i ":"

++ showDoc ot { opKind = t } " to "

++ showId j " and " ++ showId k "") nullRange : ds, m))

(sds, omap1) (Map.toList omap2 ++ concatMap

( \ (a, s) -> map ( \ ot -> ((a, mkPartial ot),

(a, opKind ot)))

$ Set.toList s) (Map.toList uo))

(pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of pred " ++ showId i ":"

++ showDoc pt " to " ++ showId j " and "

++ showId k "") nullRange : ds, m)) (ods, pmap1)

(Map.toList pmap2 ++ concatMap ( \ (a, s) -> map

( \ pt -> ((a, pt), a)) $ Set.toList s) (Map.toList up))

in if null pds then do

s3 <- addSigM addSigExt s1 s2

s4 <- addSigM addSigExt (mtarget mor1) $ mtarget mor2

let o3 = opMap s3

return

(embedMorphism (uniteM (extended_map mor1) $ extended_map mor2) s3 s4)

{ sort_map = Map.filterWithKey (/=) smap

, op_map = Map.filterWithKey

(\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot

(Map.findWithDefault Set.empty i o3)) omap

, pred_map = Map.filterWithKey (\ (i, _) j -> i /= j) pmap }

else Result pds Nothing

isSortInjective :: Morphism f e m -> Bool

isSortInjective m =

let ss = sortSet $ msource m

in Set.size ss == Set.size (Set.map (mapSort $ sort_map m) ss)

sumSize :: Map.Map a (Set.Set b) -> Int

sumSize = sum . map Set.size . Map.elems

-- morphism extension m is not considered here

isInjective :: Morphism f e m -> Bool

isInjective m = isSortInjective m && let

src = msource m

sm = sort_map m

os = opMap src

ps = predMap src

in sumSize os == sumSize (inducedOpMap sm (op_map m) os)

&& sumSize ps == sumSize (inducedPredMap sm (pred_map m) ps)

instance Pretty RawSymbol where

pretty rsym = case rsym of

ASymbol sy -> pretty sy

AKindedSymb k i -> pretty k <+> pretty i

printMorphism :: (e -> Doc) -> (m -> Doc) -> Morphism f e m

-> Doc

printMorphism fE fM mor =

let src = msource mor

tar = mtarget mor

ops = op_map mor

prSig s = specBraces (space <> printSign fE s)

srcD = prSig src

in if isInclusionMorphism (const True) mor then

if isSubSig (\ _ _ -> True) tar src then

fsep [text "identity morphism over", srcD]

else fsep

[ text "inclusion morphism of", srcD

, fsep $ if Map.null ops then

[ text "extended with"

, pretty $ Set.difference (symOf tar) $ symOf src ]

else

[ text "by totalizing"

, pretty $ Set.map (uncurry idToOpSymbol) $ Map.keysSet ops ]]

else fsep

[ pretty (morphismToSymbMapAux True mor)

$+$ fM (extended_map mor)

, colon <+> srcD, mapsto <+> prSig tar ]

instance (Pretty e, Show f, Pretty m) =>

Pretty (Morphism f e m) where

pretty = printMorphism pretty pretty