4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$

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

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian MaederMaintainer : maeder@tzi.de

3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : provisional

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederPortability : portable

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederSymbols and signature morphisms for the CASL logic

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder-}

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maeder{-

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maedertodo:

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maederthe qualification only applies to __+__ !

ac142c1b088711f911018d8108a64be80b2f2a58Christian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maederpossibly reuse SYMB_KIND for Kind

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder-}

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maedermodule CASL.Morphism where

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maeder

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport CASL.Sign

23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport CASL.AS_Basic_CASL

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder

4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport qualified Common.Lib.Map as Map

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport qualified Common.Lib.Set as Set

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport qualified Common.Lib.Rel as Rel

975642b989852fc24119c59cf40bc1af653608ffChristian Maederimport Common.Doc

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Common.DocUtils

1c67beb3720d0b84d8d71ee2012166a09be81fbdChristian Maederimport Common.Id

62925f4a144f45b5ed1e7c841f891d13f51e553dChristian Maederimport Common.Keywords

715ffaf874309df081d1e1cd8e05073fc1227729Christian Maederimport Common.Result

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder

53301de22afd7190981b363b57c48df86fcb50f7Christian Maederimport Control.Exception (assert)

cdaff0507c1b7240e2660dbb311f9c4646a6d14aChristian Maeder

f3cd81f98592d1dbf301f48af31677a6a0cc666aChristian Maedertype SymbolSet = Set.Set Symbol

ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maedertype SymbolMap = Map.Map Symbol Symbol

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maederdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder deriving (Show, Eq, Ord)

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

e47d29b522739fbf08aac80c6faa447dde113fbcChristian Maederinstance PosItem RawSymbol where

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder getRange rs =

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian Maeder case rs of

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder ASymbol s -> getRange s

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder AnID i -> getRange i

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder AKindedId _ i -> getRange i

975642b989852fc24119c59cf40bc1af653608ffChristian Maeder

836e72a3c413366ba9801726f3b249c7791cb9caChristian Maedertype RawSymbolSet = Set.Set RawSymbol

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maederdata Kind = SortKind | FunKind | PredKind

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder deriving (Show, Eq, Ord)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedertype Sort_map = Map.Map SORT SORT

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder-- allways use the partial profile as key!

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maedertype Fun_map = Map.Map (Id,OpType) (Id, FunKind)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maedertype Pred_map = Map.Map (Id,PredType) Id

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederdata Morphism f e m = Morphism

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder { msource :: Sign f e

53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder , mtarget :: Sign f e

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , sort_map :: Sort_map

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , fun_map :: Fun_map

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder , pred_map :: Pred_map

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , extended_map :: m

fa45d098e1c9d468f128be9505eb7e5b2705b304Christian Maeder } deriving (Eq, Show)

25612a7b3ce708909298d5426406592473880a20Christian Maeder

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermapSort :: Sort_map -> SORT -> SORT

35cd0c10843c2cdbbe29f00a2a5d7e5e4f2d0064Christian MaedermapSort sorts s = Map.findWithDefault s s sorts

c1db3d36c29a6324745a86dbcba18b8e4cd9f338Christian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedermapOpType :: Sort_map -> OpType -> OpType

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapOpType sorts t = if Map.null sorts then t else

7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder t { opArgs = map (mapSort sorts) $ opArgs t

1eb10c0c30323eed3cc21082fd242cd09a612dc5Christian Maeder , opRes = mapSort sorts $ opRes t }

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedermapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaedermakeTotal :: FunKind -> OpType -> OpType

18b709ce961d68328da768318dcc70067f066d86Christian MaedermakeTotal Total t = t { opKind = Total }

ac142c1b088711f911018d8108a64be80b2f2a58Christian MaedermakeTotal _ t = t

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian MaedermapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)

0216a1580abf46ed8981f25e89d6fd99b2944ac2Christian MaedermapOpSym sMap fMap (i, ot) =

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder let mot = mapOpType sMap ot in

36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder case Map.lookup (i, ot {opKind = Partial} ) fMap of

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder Nothing -> (i, mot)

9c5b1136299d9052e4e995614a3a36a051a2682fChristian Maeder Just (j, k) -> (j, makeTotal k mot)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

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

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedercompatibleOpTypes :: OpType -> OpType -> Bool

797f811e57952d59e73b8cd03b667eef276db972Christian MaedercompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian Maeder

fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian MaedermapPredType :: Sort_map -> PredType -> PredType

797f811e57952d59e73b8cd03b667eef276db972Christian MaedermapPredType sorts t = if Map.null sorts then t else

797f811e57952d59e73b8cd03b667eef276db972Christian Maeder t { predArgs = map (mapSort sorts) $ predArgs t }

18b709ce961d68328da768318dcc70067f066d86Christian Maeder

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill MossakowskimapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian MaedermapPredSym sMap fMap (i, pt) =

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

18b709ce961d68328da768318dcc70067f066d86Christian Maedertype Ext f e m = Sign f e -> Sign f e -> m

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaederembedMorphism :: Ext f e m -> Sign f e -> Sign f e -> Morphism f e m

3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaederembedMorphism extEm a b = Morphism

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder { msource = a

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder , mtarget = b

3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder , sort_map = Map.empty

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder , fun_map = Map.empty

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder , pred_map = Map.empty

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder , extended_map = extEm a b

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder }

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian Maeder

22fc8a1bd14dc53c5c7f482d2e0c04eb5ee4beb4Christian MaederidToSortSymbol :: Id -> Symbol

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederidToSortSymbol idt = Symbol idt SortAsItemType

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederidToOpSymbol :: Id -> OpType -> Symbol

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaederidToPredSymbol :: Id -> PredType -> Symbol

adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian MaederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaedersymbTypeToKind :: SymbType -> Kind

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersymbTypeToKind (OpAsItemType _) = FunKind

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersymbTypeToKind (PredAsItemType _) = PredKind

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersymbTypeToKind SortAsItemType = SortKind

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersymbolToRaw :: Symbol -> RawSymbol

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian MaedersymbolToRaw sym = ASymbol sym

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaederidToRaw :: Id -> RawSymbol

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian MaederidToRaw x = AnID x

9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian MaederrawSymName :: RawSymbol -> Id

369454f9b2dbea113cbb40544a9b0f31425b2c69Christian MaederrawSymName (ASymbol sym) = symName sym

11d6ec73ee5550e00cb56b221bdbeb709142e779Christian MaederrawSymName (AnID i) = i

9c5b1136299d9052e4e995614a3a36a051a2682fChristian MaederrawSymName (AKindedId _ i) = i

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder

ac142c1b088711f911018d8108a64be80b2f2a58Christian MaedersymOf :: Sign f e -> SymbolSet

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian MaedersymOf sigma =

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

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder ops = Set.fromList $

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t)

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder $ Set.toList ts) $

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder Map.toList $ opMap sigma

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder preds = Set.fromList $

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

fcec1ffa4a95dbc47cf23f75e6843ceff93a925eChristian Maeder $ Set.toList ts) $

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder Map.toList $ predMap sigma

f454c20b6c126bea7d31d400cc8824b9ee8cc6eaChristian Maeder in Set.unions [sorts, ops, preds]

b52ad1aed6b1eb8b8416aaf100695f54ea59aea0Christian Maeder

65835942d66905c377fa503e0d577df5aade58feChristian MaederstatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

65835942d66905c377fa503e0d577df5aade58feChristian MaederstatSymbMapItems sl = do

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ls <- sequence $ map s1 sl

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

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder where

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

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder insertRsys m (rsy1,rsy2) = do

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder m1 <- m

b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder case Map.lookup rsy1 m1 of

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Nothing -> return $ Map.insert rsy1 rsy2 m1

aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Just rsy3 ->

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

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder ++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange

5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder

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 -> return $ AKindedId SortKind idt

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) $ Rel.keysSet smap1

us2 = Set.difference (sortSet s2) $ Rel.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