55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder{- |

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuModule : $Header$

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

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

1e09f2a31712311820bd128b55ab4792603959bbJonathan von Schroeder

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuMaintainer : maeder@tzi.de

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescuStability : provisional

1e09f2a31712311820bd128b55ab4792603959bbJonathan von SchroederPortability : portable

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

1e09f2a31712311820bd128b55ab4792603959bbJonathan von SchroederSymbols and signature morphisms for the CASL logic

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-}

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu{-

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescutodo:

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuissue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuthe qualification only applies to __+__ !

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescupossibly reuse SYMB_KIND for Kind

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-}

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroedermodule CASL.Morphism where

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport CASL.Sign

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport CASL.AS_Basic_CASL

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.Id

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.Result

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.Keywords

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von Schroederimport qualified Common.Lib.Map as Map

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport qualified Common.Lib.Set as Set

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport qualified Common.Lib.Rel as Rel

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Control.Monad

31d6d9286988dc31639d105841296759aeb743e0Jonathan von Schroederimport Common.PrettyPrint

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Control.Exception (assert)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuimport Common.Doc

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroederimport Common.DocUtils

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroederimport Common.Print_AS_Annotation

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescudata SymbType = OpAsItemType OpType

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu -- since symbols do not speak about totality, the totality

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu -- information in OpType has to be ignored

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu | PredAsItemType PredType

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu | SortAsItemType

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu deriving (Show)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu-- Ordering and equality of symbol types has to ingore totality information

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuinstance Ord SymbType where

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (OpAsItemType ot1) (OpAsItemType ot2) =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (opArgs ot1,opRes ot1) (opArgs ot2,opRes ot2)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (OpAsItemType _) _ = LT

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (PredAsItemType pt1) (PredAsItemType pt2) =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare pt1 pt2

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (PredAsItemType _) (OpAsItemType _) = GT

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare (PredAsItemType _) SortAsItemType = LT

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare SortAsItemType SortAsItemType = EQ

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu compare SortAsItemType _ = GT

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuinstance Eq SymbType where

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu t1 == t2 = compare t1 t2 == EQ

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescudata Symbol = Symbol {symName :: Id, symbType :: SymbType}

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu deriving (Show, Eq, Ord)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescuinstance PosItem Symbol where

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu getRange = getRange . symName

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescutype SymbolSet = Set.Set Symbol

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescutype SymbolMap = Map.Map Symbol Symbol

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescudata RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder deriving (Show, Eq, Ord)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maederinstance PosItem RawSymbol where

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder getRange rs =

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder case rs of

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu ASymbol s -> getRange s

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu AnID i -> getRange i

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu AKindedId _ i -> getRange i

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maedertype RawSymbolSet = Set.Set RawSymbol

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescutype RawSymbolMap = Map.Map RawSymbol RawSymbol

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescudata Kind = SortKind | FunKind | PredKind

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu deriving (Show, Eq, Ord)

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroedertype Sort_map = Map.Map SORT SORT

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder-- allways use the partial profile as key!

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maedertype Fun_map = Map.Map (Id,OpType) (Id, FunKind)

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maedertype Pred_map = Map.Map (Id,PredType) Id

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroederdata Morphism f e m = Morphism {msource :: Sign f e,

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder mtarget :: Sign f e,

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder sort_map :: Sort_map,

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder fun_map :: Fun_map,

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder pred_map :: Pred_map,

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder extended_map :: m}

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder deriving (Eq, Show)

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermapSort :: Sort_map -> SORT -> SORT

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermapSort sorts s = Map.findWithDefault s s sorts

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder

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

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von SchroedermapOpType sorts t = if Map.null sorts then t else

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder t { opArgs = map (mapSort sorts) $ opArgs t

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von Schroeder , opRes = mapSort sorts $ opRes t }

69fd87e4b078ee518487bbfa5f4589392a132993Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType

69fd87e4b078ee518487bbfa5f4589392a132993Jonathan von SchroedermapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder

a6c883b6eaec47ce57e62656b09577cab13e1be7Jonathan von SchroedermakeTotal :: FunKind -> OpType -> OpType

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaedermakeTotal Total t = t { opKind = Total }

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedermakeTotal _ t = t

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von SchroedermapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermapOpSym sMap fMap (i, ot) =

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder let mot = mapOpType sMap ot in

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder case Map.lookup (i, ot {opKind = Partial} ) fMap of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Nothing -> (i, mot)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Just (j, k) -> (j, makeTotal k mot)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder-- | Check if two OpTypes are equal modulo totality or partiality

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedercompatibleOpTypes :: OpType -> OpType -> Bool

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedercompatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedermapPredType :: Sort_map -> PredType -> PredType

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedermapPredType sorts t = if Map.null sorts then t else

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder t { predArgs = map (mapSort sorts) $ predArgs t }

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

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

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von SchroedermapPredSym sMap fMap (i, pt) =

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

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

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

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von SchroederembedMorphism :: Ext f e m -> Sign f e -> Sign f e -> Morphism f e m

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian MaederembedMorphism extEm a b =

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder Morphism

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder { msource = a

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder , mtarget = b

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder , sort_map = Map.empty

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder , fun_map = Map.empty

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder , pred_map = Map.empty

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder , extended_map = extEm a b

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder }

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederidToSortSymbol :: Id -> Symbol

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von SchroederidToSortSymbol idt = Symbol idt SortAsItemType

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von SchroederidToOpSymbol :: Id -> OpType -> Symbol

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von SchroederidToOpSymbol idt typ = Symbol idt (OpAsItemType typ)

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von SchroederidToPredSymbol :: Id -> PredType -> Symbol

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von SchroederidToPredSymbol idt typ = Symbol idt (PredAsItemType typ)

3f232df590a3fafc60a218589c3a3f0a3c359b44Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbTypeToKind :: SymbType -> Kind

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbTypeToKind (OpAsItemType _) = FunKind

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbTypeToKind (PredAsItemType _) = PredKind

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedersymbTypeToKind SortAsItemType = SortKind

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedersymbolToRaw :: Symbol -> RawSymbol

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbolToRaw sym = ASymbol sym

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederidToRaw :: Id -> RawSymbol

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederidToRaw x = AnID x

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederrawSymName :: RawSymbol -> Id

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroederrawSymName (ASymbol sym) = symName sym

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrawSymName (AnID i) = i

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederrawSymName (AKindedId _ i) = i

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von Schroeder

1dfa74e3151ce63c12483d7268fe096d82e82076Jonathan von SchroedersymOf :: Sign f e -> SymbolSet

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymOf sigma =

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder let sorts = Set.map idToSortSymbol $ sortSet sigma

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder ops = Set.fromList $

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

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder $ Set.toList ts) $

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder Map.toList $ opMap sigma

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder preds = Set.fromList $

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

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder $ Set.toList ts) $

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder Map.toList $ predMap sigma

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder in Set.unions [sorts, ops, preds]

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederstatSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederstatSymbMapItems sl = do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ls <- sequence $ map s1 sl

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder foldl insertRsys (return Map.empty) (concat ls)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder where

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder insertRsys m (rsy1,rsy2) = do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m1 <- m

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder case Map.lookup rsy1 m1 of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Nothing -> return $ Map.insert rsy1 rsy2 m1

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Just rsy3 ->

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder plain_error m1 ("Symbol " ++ showPretty rsy1 " mapped twice to "

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

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederpairM :: Monad m => (m a,m b) -> m (a,b)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroederpairM (x,y) = do

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a <- x

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder b <- y

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (a,b)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol,RawSymbol)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbOrMapToRaw k (Symb s) = pairM (symbToRaw k s,symbToRaw k s)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbOrMapToRaw k (Symb_map s t _) = pairM (symbToRaw k s,symbToRaw k t)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederstatSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von SchroederstatSymbItems sl =

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder fmap concat (sequence (map s1 sl))

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von Schroeder

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von SchroedersymbToRaw k (Symb_id idt) = return $ symbKindToRaw k idt

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedersymbToRaw k (Qual_id idt t _) = typedSymbKindToRaw k idt t

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

87836973cf6a4ed22295454c58242fc926a83f42Jonathan von SchroedersymbKindToRaw :: SYMB_KIND -> Id -> RawSymbol

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von SchroedersymbKindToRaw sk idt = case sk of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Implicit -> AnID idt

ab148c20add4ca4c956e36f56859dcc5c4dde187Jonathan von Schroeder _ -> AKindedId (case sk of

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Sorts_kind -> SortKind

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder Preds_kind -> PredKind

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu _ -> FunKind) idt

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescutypedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai CodescutypedSymbKindToRaw k idt t =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu let err = plain_error (AnID idt)

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder (showPretty idt ":" ++ showPretty t

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu "does not have kind" ++ showPretty k "") nullRange

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu aSymb = ASymbol $ case t of

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu O_type ot -> idToOpSymbol idt $ toOpType ot

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu P_type pt -> idToPredSymbol idt $ toPredType pt

ae20fe3ef7832827a9ee018899f30eeae98a706dJonathan von Schroeder -- in case of ambiguity, return a constant function type

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder -- this deviates from the CASL summary !!!

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder A_type s ->

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

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder in idToOpSymbol idt ot

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder in case k of

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder Implicit -> return aSymb

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder Sorts_kind -> return $ AKindedId SortKind idt

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder Ops_kind -> case t of

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder P_type _ -> err

6f3b0aa6cccf5105b22a1ae366ff59706538d937Jonathan von Schroeder _ -> return aSymb

6164cea1d448f9e9dccd9b4c79e57763b2758ddeJonathan von Schroeder Preds_kind -> case t of

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder O_type _ -> err

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder A_type s -> return $ ASymbol $

abbba0121ac69d254389160a7b92c52dc279b960Mihai Codescu let pt = PredType {predArgs = [s]}

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu in idToPredSymbol idt pt

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder P_type _ -> return aSymb

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian MaedersymbMapToMorphism :: Ext f e m -> Sign f e -> Sign f e

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder -> SymbolMap -> Result (Morphism f e m)

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian MaedersymbMapToMorphism extEm sigma1 sigma2 smap = let

3dfdf17a4bbad3dde93fab8ac588d5acda8a6f42Jonathan von Schroeder sort_map1 = Set.fold mapMSort Map.empty (sortSet sigma1)

9e30b0e74760a90c03c444cd290ba9af9d917f6eChristian Maeder mapMSort s m =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap

b93d7514eff107392e0ee8d7b659320fed06d64cJonathan von Schroeder 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

b93d7514eff107392e0ee8d7b659320fed06d64cJonathan von Schroeder fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder mapFun i ots m = Set.fold (insFun i) m ots

3596e64ec2f7c1d70dc4e975f7e3ec23a8e1eb67Jonathan von Schroeder insFun i ot m =

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap

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

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu OpAsItemType oty -> let k = opKind oty in

0fa7a99c279b7b59df56d86c3ada137b191fe8ebJonathan von Schroeder if j == i && opKind ot == k then m

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu else Map.insert (i, ot {opKind = Partial}) (j, k) m

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu _ -> m

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu _ -> m

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu mapPred i pts m = Set.fold (insPred i) m pts

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu insPred i pt m =

6fc41a5f93c1859888c6e6d6eb0ddff86d48fb45Mihai Codescu case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap

34626ff7551c3ceead22d049427a0b0e0d33a2e6Christian Maeder 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 :: (PrettyPrint e, PrettyPrint f)

=> 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 ":"

++ showPretty 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 ":"

++ showPretty 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

instance PrettyPrint Symbol where

printText0 ga = toText ga . pretty

instance Pretty Symbol where

pretty sy = pretty (symName sy) <>

case symbType sy of

SortAsItemType -> empty

st -> space <> colon <> pretty st

instance PrettyPrint SymbType where

-- op types try to place a question mark immediately after a colon

printText0 ga = toText ga . pretty

instance Pretty SymbType where

pretty st = case st of

OpAsItemType ot -> pretty ot

PredAsItemType pt -> space <> pretty pt

SortAsItemType -> empty

instance PrettyPrint Kind where

printText0 ga = toText ga . pretty

instance Pretty Kind where

pretty k = keyword $ case k of

SortKind -> sortS

FunKind -> opS

PredKind -> predS

instance PrettyPrint RawSymbol where

printText0 ga = toText ga . pretty

instance Pretty RawSymbol where

pretty rsym = case rsym of

ASymbol sy -> pretty sy

AnID i -> pretty i

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

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

PrettyPrint (Morphism f e m) where

printText0 ga = toText ga .

printMorphism (fromText ga) (fromText ga) (fromText ga)

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

printMorphism fF fE fM mor =

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

printSymbolMap :: SymbolMap -> Doc

printSymbolMap = printMap specBraces (fsep . punctuate comma)

(\ a b -> a <+> mapsto <+> b)