073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu{- |

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : $Header$

e5636f167d8113960d320407cbbd7cd3580241d4Christian MaederDescription : Symbols and signature morphisms for the CASL logic

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

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan PascanuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan PascanuMaintainer : Christian.Maeder@dfki.de

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan PascanuStability : provisional

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan PascanuPortability : portable

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu

56c56b2181e76c239929ddade2925ba5c3f3fffdChristian MaederSymbols and signature morphisms for the CASL logic

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu-}

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu{-

dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian Maedertodo:

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanuissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederthe qualification only applies to __+__ !

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Grosspossibly reuse SYMB_KIND for Kind

334cfff54edf14ec98e2bcda86ff6aa197b56931Christian Maeder-}

334cfff54edf14ec98e2bcda86ff6aa197b56931Christian Maeder

334cfff54edf14ec98e2bcda86ff6aa197b56931Christian Maedermodule CASL.Morphism where

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport CASL.Sign

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport CASL.AS_Basic_CASL

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport qualified Data.Map as Map

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Data.Set as Set

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Common.Lib.Rel as Rel

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Common.Doc

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Common.DocUtils

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Common.Id

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Common.Keywords

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Common.Result

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederimport Control.Exception (assert)

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype SymbolSet = Set.Set Symbol

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype SymbolMap = Map.Map Symbol Symbol

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Grossdata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder deriving (Show, Eq, Ord)

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederinstance PosItem RawSymbol where

318943f341be7d545e618821114c1736cf7ef887Markus Gross getRange rs = case rs of

318943f341be7d545e618821114c1736cf7ef887Markus Gross ASymbol s -> getRange s

318943f341be7d545e618821114c1736cf7ef887Markus Gross AnID i -> getRange i

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder AKindedId _ i -> getRange i

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype RawSymbolSet = Set.Set RawSymbol

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype RawSymbolMap = Map.Map RawSymbol RawSymbol

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maederdata Kind = SortKind | FunKind | PredKind deriving (Show, Eq, Ord)

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype Sort_map = Map.Map SORT SORT

21ceb77765fba1a10a105dd623754e08f7424889Razvan Pascanu-- always use the partial profile as key!

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype Fun_map = Map.Map (Id, OpType) (Id, FunKind)

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maedertype Pred_map = Map.Map (Id, PredType) Id

a5e7871c93e65ddab6a704080001f0ac8f3acec8Razvan Pascanutype CASLMor = Morphism () () ()

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata MorKind = IdMor | InclMor | OtherMor deriving (Show, Eq, Ord)

d3e316bd19c271eacba5756671939050b26d3669Christian Maeder

d3e316bd19c271eacba5756671939050b26d3669Christian Maederdata Morphism f e m = Morphism

d3e316bd19c271eacba5756671939050b26d3669Christian Maeder { msource :: Sign f e

d3e316bd19c271eacba5756671939050b26d3669Christian Maeder , mtarget :: Sign f e

a5e7871c93e65ddab6a704080001f0ac8f3acec8Razvan Pascanu , morKind :: MorKind

21ceb77765fba1a10a105dd623754e08f7424889Razvan Pascanu , sort_map :: Sort_map

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder , fun_map :: Fun_map

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder , pred_map :: Pred_map

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder , extended_map :: m

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder } deriving Show

82b2fa76ca0a5b9cb7d6d058016649f00d356704Christian Maeder

a5e7871c93e65ddab6a704080001f0ac8f3acec8Razvan PascanuisInclusionMorphism :: Morphism f e m -> Bool

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederisInclusionMorphism m = morKind m <= InclMor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Grossinstance (Eq f, Eq e, Eq m) => Eq (Morphism f e m) where

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross m1 == m2 = msource m1 == msource m2 &&

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross (morKind m1 == IdMor && morKind m2 == IdMor

871a13a2ea9edd5c02390e3a734e5c238d23147aChristian Maeder || mtarget m1 == mtarget m2) &&

871a13a2ea9edd5c02390e3a734e5c238d23147aChristian Maeder sort_map m1 == sort_map m2 &&

d3e316bd19c271eacba5756671939050b26d3669Christian Maeder fun_map m1 == fun_map m2 &&

d3e316bd19c271eacba5756671939050b26d3669Christian Maeder pred_map m1 == pred_map m2 &&

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross extended_map m1 == extended_map m2

c5ccc4a821d73f9c36f61ac1f8a7a7732d67e407Markus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapSort :: Sort_map -> SORT -> SORT

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapSort sorts s = Map.findWithDefault s s sorts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpType :: Sort_map -> OpType -> OpType

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpType sorts t = if Map.null sorts then t else

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross t { opArgs = map (mapSort sorts) $ opArgs t

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross , opRes = mapSort sorts $ opRes t }

c5ccc4a821d73f9c36f61ac1f8a7a7732d67e407Markus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmakeTotal :: FunKind -> OpType -> OpType

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmakeTotal fk t = case fk of

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Total -> t { opKind = Total }

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross _ -> t

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapOpSym sMap fMap (i, ot) = let mot = mapOpType sMap ot in

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross case Map.lookup (i, ot {opKind = Partial} ) fMap of

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Nothing -> (i, mot)

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Just (j, k) -> (j, makeTotal k mot)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

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

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrosscompatibleOpTypes :: OpType -> OpType -> Bool

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrosscompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapPredType :: Sort_map -> PredType -> PredType

a5e7871c93e65ddab6a704080001f0ac8f3acec8Razvan PascanumapPredType sorts t = if Map.null sorts then t else

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder t { predArgs = map (mapSort sorts) $ predArgs t }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossmapPredSym sMap fMap (i, pt) =

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu (Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu

aaced058178957397182dca9cbe127fa210b3034Christian MaederembedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m

aaced058178957397182dca9cbe127fa210b3034Christian MaederembedMorphism extEm a b = Morphism

aaced058178957397182dca9cbe127fa210b3034Christian Maeder { msource = a

aaced058178957397182dca9cbe127fa210b3034Christian Maeder , mtarget = b

aaced058178957397182dca9cbe127fa210b3034Christian Maeder , morKind = OtherMor -- unknown for most uses

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross , sort_map = Map.empty

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross , fun_map = Map.empty

aaced058178957397182dca9cbe127fa210b3034Christian Maeder , pred_map = Map.empty

aaced058178957397182dca9cbe127fa210b3034Christian Maeder , extended_map = extEm }

aaced058178957397182dca9cbe127fa210b3034Christian Maeder

aaced058178957397182dca9cbe127fa210b3034Christian MaedersymbTypeToKind :: SymbType -> Kind

aaced058178957397182dca9cbe127fa210b3034Christian MaedersymbTypeToKind st = case st of

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross OpAsItemType _ -> FunKind

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu PredAsItemType _ -> PredKind

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder SortAsItemType -> SortKind

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder

aaced058178957397182dca9cbe127fa210b3034Christian MaedersymbolToRaw :: Symbol -> RawSymbol

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan PascanusymbolToRaw sym = ASymbol sym

aaced058178957397182dca9cbe127fa210b3034Christian Maeder

aaced058178957397182dca9cbe127fa210b3034Christian MaederidToRaw :: Id -> RawSymbol

aaced058178957397182dca9cbe127fa210b3034Christian MaederidToRaw x = AnID x

aaced058178957397182dca9cbe127fa210b3034Christian Maeder

aaced058178957397182dca9cbe127fa210b3034Christian MaederrawSymName :: RawSymbol -> Id

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossrawSymName rs = case rs of

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross ASymbol sym -> symName sym

aaced058178957397182dca9cbe127fa210b3034Christian Maeder AnID i -> i

aaced058178957397182dca9cbe127fa210b3034Christian Maeder AKindedId _ i -> i

aaced058178957397182dca9cbe127fa210b3034Christian Maeder

aaced058178957397182dca9cbe127fa210b3034Christian MaedersymOf :: Sign f e -> SymbolSet

aaced058178957397182dca9cbe127fa210b3034Christian MaedersymOf sigma = let

aaced058178957397182dca9cbe127fa210b3034Christian Maeder sorts = Set.map idToSortSymbol $ sortSet sigma

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu ops = Set.fromList $

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

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu $ Map.toList $ opMap sigma

876bd2c70a93981cc80f8376284616bce4a0fefcChristian Maeder preds = Set.fromList $

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

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

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

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu

dbc98cd8a9a829e020cfa0a9f3aff89de75caaa9Christian MaederstatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan PascanustatSymbMapItems sl = do

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu ls <- sequence $ map s1 sl

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

c5ccc4a821d73f9c36f61ac1f8a7a7732d67e407Markus Gross where

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

fefee7e1dee1ee5f0768a03a4abae88d1ca2c3fdRazvan Pascanu insertRsys m (rsy1,rsy2) = do

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross m1 <- m

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross case Map.lookup rsy1 m1 of

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Nothing -> return $ Map.insert rsy1 rsy2 m1

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Just rsy3 ->

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrosssymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol, RawSymbol)

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrosssymbOrMapToRaw k sm = do

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross let (u, v) = case sm of

5ee62f0dddc5aaecd714c9db705ecc9ce3cb4c48Ewaryst Schulz Symb s -> (s, s)

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross Symb_map s t _ -> (s, t)

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross w <- symbToRaw k u

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross x <- symbToRaw k v

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross return (w, x)

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossstatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrossstatSymbItems sl =

c5ccc4a821d73f9c36f61ac1f8a7a7732d67e407Markus Gross fmap concat (sequence (map s1 sl))

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

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus GrosssymbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus GrosssymbToRaw k si = case si of

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross Symb_id idt -> return $ symbKindToRaw k idt

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross Qual_id idt t _ -> typedSymbKindToRaw k idt t

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus Gross

834c2e71b8e390e5b05c8d02bb6eb22621125133Markus GrosssymbKindToRaw :: SYMB_KIND -> Id -> RawSymbol

62701196316f14649127d84501c0cd6bc2dfa14aMarkus GrosssymbKindToRaw sk idt = case sk of

62701196316f14649127d84501c0cd6bc2dfa14aMarkus Gross Implicit -> AnID idt

b324cda6178c49ddeead3ce62b832ccf644cbcabRazvan Pascanu _ -> AKindedId (case sk of

37b6827bfa49c2fe7e2c74ee7f29fec7be4c5a19Markus Gross Sorts_kind -> SortKind

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder Preds_kind -> PredKind

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder _ -> FunKind) idt

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder

3664a630439d8d4841d17febbd74bd1dedd909d4Christian MaedertypedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol

3664a630439d8d4841d17febbd74bd1dedd909d4Christian MaedertypedSymbKindToRaw k idt t = let

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder err = plain_error (AnID idt)

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder (showDoc idt ":" ++ showDoc t

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder "does not have kind" ++ showDoc k "") nullRange

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder aSymb = ASymbol $ case t of

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder O_type ot -> idToOpSymbol idt $ toOpType ot

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder P_type pt -> idToPredSymbol idt $ toPredType pt

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder -- in case of ambiguity, return a constant function type

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder -- this deviates from the CASL summary !!!

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder A_type s ->

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

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder in idToOpSymbol idt ot

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder in case k of

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder Implicit -> return aSymb

007b23e277c9479bdd14275e21d5e5434e6fe413Christian Maeder Sorts_kind -> err

073c366331dc2d49c8fa86bdfedec3327dabf05bRazvan Pascanu Ops_kind -> case t of

6dd950bc2cd04caadeaf12ec11cbcad8befd8e2cChristian Maeder P_type _ -> err

334cfff54edf14ec98e2bcda86ff6aa197b56931Christian Maeder _ -> return aSymb

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross Preds_kind -> case t of

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross O_type _ -> err

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross A_type s -> return $ ASymbol $

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross let pt = PredType {predArgs = [s]}

007b23e277c9479bdd14275e21d5e5434e6fe413Christian Maeder in idToPredSymbol idt pt

334cfff54edf14ec98e2bcda86ff6aa197b56931Christian Maeder P_type _ -> return aSymb

731cd0f0482644003c87b697ede3a260c9ba3f8cRazvan Pascanu

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus GrosssymbMapToMorphism :: m -> Sign f e -> Sign f e

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

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus GrosssymbMapToMorphism extEm sigma1 sigma2 smap = let

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

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross mapMSort s m =

007b23e277c9479bdd14275e21d5e5434e6fe413Christian Maeder case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.insert s t m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> m

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)

1de2c2b676bc62accfeaa7d2dafd7c5fd26edb37Markus Gross pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)

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

d5b0c08cd74b1f34d7554a15db5afce75809e453Christian Maeder insFun i ot m =

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap

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

007b23e277c9479bdd14275e21d5e5434e6fe413Christian Maeder OpAsItemType oty -> let k = opKind oty in

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

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder else Map.insert (i, ot {opKind = Partial}) (j, k) m

d5b0c08cd74b1f34d7554a15db5afce75809e453Christian Maeder _ -> m

d5b0c08cd74b1f34d7554a15db5afce75809e453Christian Maeder _ -> m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapPred i pts m = Set.fold (insPred i) m pts

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insPred i pt m =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder of Just sym -> let j = symName sym in case symbType sym of

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in return (embedMorphism extEm sigma1 sigma2)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder { sort_map = sort_map1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , fun_map = fun_map1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , pred_map = pred_map1 }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermorphismToSymbMap :: Morphism f e m -> SymbolMap

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermorphismToSymbMap mor = let

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder src = msource mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sorts = sort_map mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ops = fun_map mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder preds = pred_map mor

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sortSymMap = Set.fold ( \ s -> Map.insert (idToSortSymbol s) $

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder idToSortSymbol $ mapSort sorts s)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.empty $ sortSet src

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder opSymMap = Map.foldWithKey

d5b0c08cd74b1f34d7554a15db5afce75809e453Christian Maeder ( \ i s m -> Set.fold

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder $ uncurry idToOpSymbol $ mapOpSym sorts ops (i, t)) m s)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.empty $ opMap src

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder predSymMap = Map.foldWithKey

007b23e277c9479bdd14275e21d5e5434e6fe413Christian Maeder ( \ i s m -> Set.fold

1b5da9e5e0f18cc30be775478569ee3a5fb23ddaMarkus Gross ( \ t -> Map.insert (idToPredSymbol i t)

3664a630439d8d4841d17febbd74bd1dedd909d4Christian Maeder $ 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 :: m -> Sign f e -> Morphism f e m

idMor extEm sigma = (embedMorphism extEm sigma sigma) { morKind = IdMor }

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

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

emb = (embedMorphism (comp (extended_map mor1) $ extended_map mor2)

src tar) { morKind = max (morKind mor1) $ morKind mor2 }

in return $

if Map.null sMap1 && Map.null sMap2 && Map.null fMap1 && Map.null fMap2

&& Map.null pMap1 && Map.null pMap2 then emb else emb

{ 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 }

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

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 s1) (sortSet s2)

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

&& isSubOpMap mops (opMap s2)

&& isSubMapSet mpreds (predMap s2)

&& legalSign s2

sigInclusion :: (Pretty f, Pretty e)

=> m -- ^ compute 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 (embedMorphism extEm sigma1 sigma2)

{ morKind = if isSubSig isSubExt sigma2 sigma1 then IdMor else InclMor }

else Result [Diag Error

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

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

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

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

s3 $ addSig addSigExt (mtarget mor1) $ mtarget mor2)

{ morKind = max (morKind mor1) $ morKind 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 }

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 =

let src = msource mor

tar = mtarget mor

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

srcD = prSig src

in case morKind mor of

IdMor -> fsep [text "identity morphism over", srcD]

InclMor -> fsep

[ text "inclusion morphism of", srcD

, text "extended with"

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

OtherMor -> fsep

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

$+$ fM (extended_map mor)

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

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

Pretty (Morphism f e m) where

pretty = printMorphism pretty pretty pretty