c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuDescription : Symbols and signature morphisms for the CASL logic

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

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuMaintainer : Christian.Maeder@dfki.de

402ffc909b645ddb2d5c76343bf74a6cb33c6205Christian MaederStability : provisional

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuPortability : portable

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai CodescuSymbols and signature morphisms for the CASL logic

90d7cac36f60438bd35124e3389b5bce6d114b46Christian Maeder-}

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu{-

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutodo:

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuthe qualification only applies to __+__ !

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederpossibly reuse SYMB_KIND for Kind

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu-}

392634badbe11a21c7825ee0e1ee132220a2539eMihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermodule CASL.Morphism where

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport CASL.Sign

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport CASL.AS_Basic_CASL

5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maeder

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowskiimport qualified Data.Map as Map

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport qualified Data.Set as Set

5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maederimport qualified Common.Lib.Rel as Rel

5418aa59492005c2ca40436ab84c4029cd2922a5Christian Maederimport Common.Doc

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Common.DocUtils

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Common.Id

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescuimport Common.Keywords

3bc502518f75cd5a21aa2f608a31f50c19134db0Christian Maederimport Common.Result

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescuimport Control.Exception (assert)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype SymbolSet = Set.Set Symbol

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescutype SymbolMap = Map.Map Symbol Symbol

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescudata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu deriving (Show, Eq, Ord)

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescu

7b5ba6a2f3990cf508f90e55e1d59068e6aaa6a3Mihai Codescuinstance PosItem RawSymbol where

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu getRange rs =

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu case rs of

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu ASymbol s -> getRange s

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu AnID i -> getRange i

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder AKindedId _ i -> getRange i

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype RawSymbolSet = Set.Set RawSymbol

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype RawSymbolMap = Map.Map RawSymbol RawSymbol

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescudata Kind = SortKind | FunKind | PredKind

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu deriving (Show, Eq, Ord)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype Sort_map = Map.Map SORT SORT

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu-- always use the partial profile as key!

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype Fun_map = Map.Map (Id,OpType) (Id, FunKind)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescutype Pred_map = Map.Map (Id,PredType) Id

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescudata Morphism f e m = Morphism

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu { msource :: Sign f e

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , mtarget :: Sign f e

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , sort_map :: Sort_map

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , fun_map :: Fun_map

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , pred_map :: Pred_map

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , extended_map :: m

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu } deriving (Eq, Show)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapSort :: Sort_map -> SORT -> SORT

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapSort sorts s = Map.findWithDefault s s sorts

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpType :: Sort_map -> OpType -> OpType

272a5a82588ab4115dac5eb81d43d74929e99ad7Till MossakowskimapOpType sorts t = if Map.null sorts then t else

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu t { opArgs = map (mapSort sorts) $ opArgs t

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , opRes = mapSort sorts $ opRes t }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumakeTotal :: FunKind -> OpType -> OpType

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumakeTotal Total t = t { opKind = Total }

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumakeTotal _ t = t

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapOpSym sMap fMap (i, ot) =

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu let mot = mapOpType sMap ot in

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu case Map.lookup (i, ot {opKind = Partial} ) fMap of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> (i, mot)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu Just (j, k) -> (j, makeTotal k mot)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- | Check if two OpTypes are equal modulo totality or partiality

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescucompatibleOpTypes :: OpType -> OpType -> Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedercompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapPredType :: Sort_map -> PredType -> PredType

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapPredType sorts t = if Map.null sorts then t else

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu t { predArgs = map (mapSort sorts) $ predArgs t }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescumapPredSym sMap fMap (i, pt) =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype Ext f e m = Sign f e -> Sign f e -> m

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu

142cf75c6377873ccc72450202fe7f0df94a6dffMihai CodescuembedMorphism :: Ext f e m -> Sign f e -> Sign f e -> Morphism f e m

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuembedMorphism extEm a b = Morphism

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu { msource = a

142cf75c6377873ccc72450202fe7f0df94a6dffMihai Codescu , mtarget = b

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu , sort_map = Map.empty

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescu , fun_map = Map.empty

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu , pred_map = Map.empty

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski , extended_map = extEm a b

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski }

80875f917d741946a39d0ec0b5721e46ba609823Till Mossakowski

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToSortSymbol :: Id -> Symbol

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToSortSymbol idt = Symbol idt SortAsItemType

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToOpSymbol :: Id -> OpType -> Symbol

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToPredSymbol :: Id -> PredType -> Symbol

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

803425dfe6a5da41b9cea480788980fa104545adMihai CodescusymbTypeToKind :: SymbType -> Kind

803425dfe6a5da41b9cea480788980fa104545adMihai CodescusymbTypeToKind (OpAsItemType _) = FunKind

803425dfe6a5da41b9cea480788980fa104545adMihai CodescusymbTypeToKind (PredAsItemType _) = PredKind

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbTypeToKind SortAsItemType = SortKind

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian MaedersymbolToRaw :: Symbol -> RawSymbol

803425dfe6a5da41b9cea480788980fa104545adMihai CodescusymbolToRaw sym = ASymbol sym

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToRaw :: Id -> RawSymbol

803425dfe6a5da41b9cea480788980fa104545adMihai CodescuidToRaw x = AnID x

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

803425dfe6a5da41b9cea480788980fa104545adMihai CodescurawSymName :: RawSymbol -> Id

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrawSymName (ASymbol sym) = symName sym

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescurawSymName (AnID i) = i

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescurawSymName (AKindedId _ i) = i

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu

803425dfe6a5da41b9cea480788980fa104545adMihai CodescusymOf :: Sign f e -> SymbolSet

96d8cf9817eeb0d26cba09ca192fc5a33e27bc09mcodescusymOf sigma =

b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder let sorts = Set.map idToSortSymbol $ sortSet sigma

b7f625188b6bf3d708b2a1b64a6cea7880708adbChristian Maeder ops = Set.fromList $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ Set.toList ts) $

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu Map.toList $ opMap sigma

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu preds = Set.fromList $

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

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu $ Set.toList ts) $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.toList $ predMap sigma

803425dfe6a5da41b9cea480788980fa104545adMihai Codescu in Set.unions [sorts, ops, preds]

statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

statSymbMapItems sl = do

ls <- sequence $ map s1 sl

foldl insertRsys (return Map.empty) (concat ls)

where

s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)

insertRsys m (rsy1,rsy2) = do

m1 <- m

case Map.lookup rsy1 m1 of

Nothing -> return $ Map.insert rsy1 rsy2 m1

Just rsy3 ->

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

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

pairM :: Monad m => (m a,m b) -> m (a,b)

pairM (x, y) = do

a <- x

b <- y

return (a,b)

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

symbOrMapToRaw k (Symb s) = pairM (symbToRaw k s,symbToRaw k s)

symbOrMapToRaw k (Symb_map s t _) = pairM (symbToRaw k s,symbToRaw k t)

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

statSymbItems sl =

fmap concat (sequence (map s1 sl))

where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)

symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol

symbToRaw k (Symb_id idt) = return $ symbKindToRaw k idt

symbToRaw k (Qual_id idt t _) = typedSymbKindToRaw k idt t

symbKindToRaw :: SYMB_KIND -> Id -> RawSymbol

symbKindToRaw sk idt = case sk of

Implicit -> AnID idt

_ -> AKindedId (case sk of

Sorts_kind -> SortKind

Preds_kind -> PredKind

_ -> FunKind) idt

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

typedSymbKindToRaw k idt t =

let err = plain_error (AnID 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 -> return aSymb

Sorts_kind -> err

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

symbMapToMorphism :: Ext f e 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

fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)

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

mapFun i ots m = Set.fold (insFun i) m ots

insFun 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, ot {opKind = Partial}) (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 (Morphism { msource = sigma1,

mtarget = sigma2,

sort_map = sort_map1,

fun_map = fun_map1,

pred_map = pred_map1,

extended_map = extEm sigma1 sigma2})

morphismToSymbMap :: Morphism f e m -> SymbolMap

morphismToSymbMap mor =

let

src = msource mor

sorts = sort_map mor

ops = fun_map mor

preds = pred_map mor

sortSymMap = Set.fold ( \ s -> Map.insert (idToSortSymbol s) $

idToSortSymbol $ mapSort sorts s)

Map.empty $ sortSet src

opSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> Map.insert (idToOpSymbol i t)

$ uncurry idToOpSymbol $ mapOpSym sorts ops (i, t)) m s)

Map.empty $ opMap src

predSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> Map.insert (idToPredSymbol i t)

$ uncurry idToPredSymbol $ mapPredSym sorts preds (i, t)) m s)

Map.empty $ predMap src

in

foldr Map.union sortSymMap [opSymMap,predSymMap]

matches :: Symbol -> RawSymbol -> Bool

matches x@(Symbol idt k) rs = case rs of

ASymbol y -> x == y

AnID di -> idt == di

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

(SortAsItemType, SortKind) -> res

(OpAsItemType _, FunKind) -> res

(PredAsItemType _, PredKind) -> res

_ -> False

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

idMor extEm sigma = embedMorphism extEm sigma sigma

compose :: (Eq e, Eq f) => (m -> m -> m)

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

compose comp mor1 mor2 = if mtarget mor1 == msource mor2 then return $

let sMap1 = sort_map mor1

src = msource mor1

tar = mtarget mor2

fMap1 = fun_map mor1

pMap1 = pred_map mor1

sMap2 = sort_map mor2

fMap2 = fun_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

in

Morphism {

msource = src,

mtarget = tar,

sort_map = sMap,

fun_map = if Map.null fMap2 then fMap1 else

Map.foldWithKey ( \ i t m ->

Set.fold ( \ ot ->

let (ni, nt) = mapOpSym sMap2 fMap2 $

mapOpSym sMap1 fMap1 (i, ot)

k = opKind nt

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

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

Map.insert (i, ot {opKind = Partial }) (ni, k)) m t)

Map.empty $ opMap src,

pred_map = 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,

extended_map = comp (extended_map mor1) (extended_map mor2)

}

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 t = all legalSort (predArgs t)

legalMor :: Morphism f e m -> Bool

legalMor mor =

let s1 = msource mor

s2 = mtarget mor

smap = sort_map mor

msorts = Set.map (mapSort smap) $ sortSet s1

mops = Map.foldWithKey ( \ i ->

flip $ Set.fold ( \ ot ->

let (j, nt) = mapOpSym smap (fun_map mor) (i, ot)

in Rel.setInsert j nt)) Map.empty $ opMap s1

mpreds = Map.foldWithKey ( \ i ->

flip $ Set.fold ( \ pt ->

let (j, nt) = mapPredSym smap (pred_map mor) (i, pt)

in Rel.setInsert j nt)) Map.empty $ predMap s1

in

legalSign s1

&& Set.isSubsetOf msorts (sortSet s2)

&& isSubOpMap mops (opMap s2)

&& isSubMapSet mpreds (predMap s2)

&& legalSign s2

sigInclusion :: Ext f e m -- ^ compute extended morphism

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

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

sigInclusion extEm isSubExt sigma1 sigma2 =

assert (isSubSig isSubExt sigma1 sigma2) $

return (embedMorphism extEm sigma1 sigma2)

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)

-- consider identity mappings but filter them eventually

morphismUnion 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 = fun_map mor1

omap2 = fun_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 [ot {opKind = Partial}, ot {opKind =Total}]

uo = addMapSet 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, ot {opKind = Partial}),

(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))

s3 = addSig addSigExt s1 s2

o3 = opMap s3 in

if null pds then Result [] $ Just Morphism

{ msource = s3,

mtarget = addSig addSigExt (mtarget mor1) $ mtarget mor2,

sort_map = Map.filterWithKey (/=) smap,

fun_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,

extended_map = uniteM (extended_map mor1) $ extended_map mor2 }

else Result pds Nothing

isSortInjective :: Morphism f e m -> Bool

isSortInjective m =

null [() | k1 <- src, k2 <-src, k1 /= k2,

(Map.lookup k1 sm::Maybe SORT)==Map.lookup k2 sm]

where sm = sort_map m

src = Map.keys sm

isInjective :: Morphism f e m -> Bool

isInjective m =

null [() | k1 <- src, k2 <-src, k1 /= k2,

(Map.lookup k1 symmap::Maybe Symbol)==Map.lookup k2 symmap]

where src = Map.keys symmap

symmap = morphismToSymbMap m

instance Pretty Kind where

pretty k = keyword $ case k of

SortKind -> sortS

FunKind -> opS

PredKind -> predS

instance Pretty RawSymbol where

pretty rsym = case rsym of

ASymbol sy -> pretty sy

AnID i -> pretty i

AKindedId k i -> pretty k <+> pretty i

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

printMorphism fF fE fM mor =

pretty (Map.filterWithKey (/=) $ morphismToSymbMap mor)

$+$ fM (extended_map mor) $+$ colon $+$

specBraces (space <> printSign fF fE (msource mor) <> space)

$+$ text funS $+$

specBraces (space <> printSign fF fE (mtarget mor) <> space)

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

Pretty (Morphism f e m) where

pretty = printMorphism pretty pretty pretty