{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CASL/Morphism.hs
Description :  Symbols and signature morphisms for the CASL logic
Copyright   :  (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (MPTC+FD)

Symbols and signature morphisms for the CASL logic
-}

module CASL.Morphism
  ( SymbolSet
  , SymbolMap
  , RawSymbol (..)
  , Morphism (..)
  , idMor
  , legalMor
  , DefMorExt (..)
  , emptyMorExt
  , MorphismExtension (..)
  , retExtMap
  , CASLMor
  , isInclusionMorphism
  , isSortInjective
  , isInjective
  , Sort_map
  , Pred_map
  , Op_map
  , embedMorphism
  , mapCASLMor
  , sigInclusion
  , composeM
  , plainMorphismUnion
  , morphismUnion
  , morphismUnionM
  , idOrInclMorphism
  , morphismToSymbMap
  , symsetOf
  , symOf
  , sigSymsOf
  , addSigM
  , idToRaw
  , typedSymbKindToRaw
  , symbolToRaw
  , insertRsys
  , mapSort
  , mapOpSym
  , mapPredSym
  , mapOpType
  , mapPredType
  , matches
  , compatibleOpTypes
  , imageOfMorphism
  , RawSymbolMap
  , InducedSign
  , inducedSignAux
  , rawSymName
  , inducedOpMap
  , inducedPredMap
  , statSymbMapItems
  , statSymbItems
  ) where

import CASL.Sign
import CASL.AS_Basic_CASL

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.Result
import Common.Utils (composeMap)

import Control.Monad
import qualified Control.Monad.Fail as Fail

type SymbolSet = Set.Set Symbol
type SymbolMap = Map.Map Symbol Symbol

data RawSymbol = ASymbol Symbol | AKindedSymb SYMB_KIND Id
                 deriving (Int -> RawSymbol -> ShowS
[RawSymbol] -> ShowS
RawSymbol -> String
(Int -> RawSymbol -> ShowS)
-> (RawSymbol -> String)
-> ([RawSymbol] -> ShowS)
-> Show RawSymbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RawSymbol] -> ShowS
$cshowList :: [RawSymbol] -> ShowS
show :: RawSymbol -> String
$cshow :: RawSymbol -> String
showsPrec :: Int -> RawSymbol -> ShowS
$cshowsPrec :: Int -> RawSymbol -> ShowS
Show, RawSymbol -> RawSymbol -> Bool
(RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool) -> Eq RawSymbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RawSymbol -> RawSymbol -> Bool
$c/= :: RawSymbol -> RawSymbol -> Bool
== :: RawSymbol -> RawSymbol -> Bool
$c== :: RawSymbol -> RawSymbol -> Bool
Eq, Eq RawSymbol
Eq RawSymbol =>
(RawSymbol -> RawSymbol -> Ordering)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> Bool)
-> (RawSymbol -> RawSymbol -> RawSymbol)
-> (RawSymbol -> RawSymbol -> RawSymbol)
-> Ord RawSymbol
RawSymbol -> RawSymbol -> Bool
RawSymbol -> RawSymbol -> Ordering
RawSymbol -> RawSymbol -> RawSymbol
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: RawSymbol -> RawSymbol -> RawSymbol
$cmin :: RawSymbol -> RawSymbol -> RawSymbol
max :: RawSymbol -> RawSymbol -> RawSymbol
$cmax :: RawSymbol -> RawSymbol -> RawSymbol
>= :: RawSymbol -> RawSymbol -> Bool
$c>= :: RawSymbol -> RawSymbol -> Bool
> :: RawSymbol -> RawSymbol -> Bool
$c> :: RawSymbol -> RawSymbol -> Bool
<= :: RawSymbol -> RawSymbol -> Bool
$c<= :: RawSymbol -> RawSymbol -> Bool
< :: RawSymbol -> RawSymbol -> Bool
$c< :: RawSymbol -> RawSymbol -> Bool
compare :: RawSymbol -> RawSymbol -> Ordering
$ccompare :: RawSymbol -> RawSymbol -> Ordering
$cp1Ord :: Eq RawSymbol
Ord, Typeable, Typeable RawSymbol
Constr
DataType
Typeable RawSymbol =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> RawSymbol -> c RawSymbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c RawSymbol)
-> (RawSymbol -> Constr)
-> (RawSymbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c RawSymbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol))
-> ((forall b. Data b => b -> b) -> RawSymbol -> RawSymbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> RawSymbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> RawSymbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol)
-> Data RawSymbol
RawSymbol -> Constr
RawSymbol -> DataType
(forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> RawSymbol -> u
forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
$cAKindedSymb :: Constr
$cASymbol :: Constr
$tRawSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapMp :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapM :: (forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> RawSymbol -> m RawSymbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> RawSymbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> RawSymbol -> u
gmapQ :: (forall d. Data d => d -> u) -> RawSymbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> RawSymbol -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> RawSymbol -> r
gmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
$cgmapT :: (forall b. Data b => b -> b) -> RawSymbol -> RawSymbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c RawSymbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c RawSymbol)
dataTypeOf :: RawSymbol -> DataType
$cdataTypeOf :: RawSymbol -> DataType
toConstr :: RawSymbol -> Constr
$ctoConstr :: RawSymbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c RawSymbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> RawSymbol -> c RawSymbol
$cp1Data :: Typeable RawSymbol
Data)

instance GetRange RawSymbol where
    getRange :: RawSymbol -> Range
getRange rs :: RawSymbol
rs = case RawSymbol
rs of
        ASymbol s :: Symbol
s -> Symbol -> Range
forall a. GetRange a => a -> Range
getRange Symbol
s
        AKindedSymb _ i :: Id
i -> Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i

type RawSymbolMap = Map.Map RawSymbol RawSymbol

type Sort_map = Map.Map SORT SORT
-- always use the partial profile as key!
type Op_map = Map.Map (Id, OpType) (Id, OpKind)
type Pred_map = Map.Map (Id, PredType) Id

data Morphism f e m = Morphism
  { Morphism f e m -> Sign f e
msource :: Sign f e
  , Morphism f e m -> Sign f e
mtarget :: Sign f e
  , Morphism f e m -> Sort_map
sort_map :: Sort_map
  , Morphism f e m -> Op_map
op_map :: Op_map
  , Morphism f e m -> Pred_map
pred_map :: Pred_map
  , Morphism f e m -> m
extended_map :: m
  } deriving (Int -> Morphism f e m -> ShowS
[Morphism f e m] -> ShowS
Morphism f e m -> String
(Int -> Morphism f e m -> ShowS)
-> (Morphism f e m -> String)
-> ([Morphism f e m] -> ShowS)
-> Show (Morphism f e m)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall f e m.
(Show f, Show e, Show m) =>
Int -> Morphism f e m -> ShowS
forall f e m. (Show f, Show e, Show m) => [Morphism f e m] -> ShowS
forall f e m. (Show f, Show e, Show m) => Morphism f e m -> String
showList :: [Morphism f e m] -> ShowS
$cshowList :: forall f e m. (Show f, Show e, Show m) => [Morphism f e m] -> ShowS
show :: Morphism f e m -> String
$cshow :: forall f e m. (Show f, Show e, Show m) => Morphism f e m -> String
showsPrec :: Int -> Morphism f e m -> ShowS
$cshowsPrec :: forall f e m.
(Show f, Show e, Show m) =>
Int -> Morphism f e m -> ShowS
Show, Morphism f e m -> Morphism f e m -> Bool
(Morphism f e m -> Morphism f e m -> Bool)
-> (Morphism f e m -> Morphism f e m -> Bool)
-> Eq (Morphism f e m)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall f e m.
(Eq e, Eq m) =>
Morphism f e m -> Morphism f e m -> Bool
/= :: Morphism f e m -> Morphism f e m -> Bool
$c/= :: forall f e m.
(Eq e, Eq m) =>
Morphism f e m -> Morphism f e m -> Bool
== :: Morphism f e m -> Morphism f e m -> Bool
$c== :: forall f e m.
(Eq e, Eq m) =>
Morphism f e m -> Morphism f e m -> Bool
Eq, Eq (Morphism f e m)
Eq (Morphism f e m) =>
(Morphism f e m -> Morphism f e m -> Ordering)
-> (Morphism f e m -> Morphism f e m -> Bool)
-> (Morphism f e m -> Morphism f e m -> Bool)
-> (Morphism f e m -> Morphism f e m -> Bool)
-> (Morphism f e m -> Morphism f e m -> Bool)
-> (Morphism f e m -> Morphism f e m -> Morphism f e m)
-> (Morphism f e m -> Morphism f e m -> Morphism f e m)
-> Ord (Morphism f e m)
Morphism f e m -> Morphism f e m -> Bool
Morphism f e m -> Morphism f e m -> Ordering
Morphism f e m -> Morphism f e m -> Morphism f e m
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall f e m. (Ord e, Ord m) => Eq (Morphism f e m)
forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Bool
forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Ordering
forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Morphism f e m
min :: Morphism f e m -> Morphism f e m -> Morphism f e m
$cmin :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Morphism f e m
max :: Morphism f e m -> Morphism f e m -> Morphism f e m
$cmax :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Morphism f e m
>= :: Morphism f e m -> Morphism f e m -> Bool
$c>= :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Bool
> :: Morphism f e m -> Morphism f e m -> Bool
$c> :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Bool
<= :: Morphism f e m -> Morphism f e m -> Bool
$c<= :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Bool
< :: Morphism f e m -> Morphism f e m -> Bool
$c< :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Bool
compare :: Morphism f e m -> Morphism f e m -> Ordering
$ccompare :: forall f e m.
(Ord e, Ord m) =>
Morphism f e m -> Morphism f e m -> Ordering
$cp1Ord :: forall f e m. (Ord e, Ord m) => Eq (Morphism f e m)
Ord, Typeable, Typeable (Morphism f e m)
Constr
DataType
Typeable (Morphism f e m) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Morphism f e m))
-> (Morphism f e m -> Constr)
-> (Morphism f e m -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Morphism f e m)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (Morphism f e m)))
-> ((forall b. Data b => b -> b)
    -> Morphism f e m -> Morphism f e m)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> Morphism f e m -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> Morphism f e m -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> Morphism f e m -> m (Morphism f e m))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Morphism f e m -> m (Morphism f e m))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> Morphism f e m -> m (Morphism f e m))
-> Data (Morphism f e m)
Morphism f e m -> Constr
Morphism f e m -> DataType
(forall b. Data b => b -> b) -> Morphism f e m -> Morphism f e m
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Morphism f e m)
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> Morphism f e m -> u
forall u. (forall d. Data d => d -> u) -> Morphism f e m -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
forall f e m. (Data f, Data e, Data m) => Typeable (Morphism f e m)
forall f e m. (Data f, Data e, Data m) => Morphism f e m -> Constr
forall f e m.
(Data f, Data e, Data m) =>
Morphism f e m -> DataType
forall f e m.
(Data f, Data e, Data m) =>
(forall b. Data b => b -> b) -> Morphism f e m -> Morphism f e m
forall f e m u.
(Data f, Data e, Data m) =>
Int -> (forall d. Data d => d -> u) -> Morphism f e m -> u
forall f e m u.
(Data f, Data e, Data m) =>
(forall d. Data d => d -> u) -> Morphism f e m -> [u]
forall f e m r r'.
(Data f, Data e, Data m) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
forall f e m r r'.
(Data f, Data e, Data m) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
forall f e m (m :: * -> *).
(Data f, Data e, Data m, Monad m) =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
forall f e m (m :: * -> *).
(Data f, Data e, Data m, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
forall f e m (c :: * -> *).
(Data f, Data e, Data m) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Morphism f e m)
forall f e m (c :: * -> *).
(Data f, Data e, Data m) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m)
forall f e m (t :: * -> *) (c :: * -> *).
(Data f, Data e, Data m, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Morphism f e m))
forall f e m (t :: * -> * -> *) (c :: * -> *).
(Data f, Data e, Data m, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Morphism f e m))
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Morphism f e m)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Morphism f e m))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Morphism f e m))
$cMorphism :: Constr
$tMorphism :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
$cgmapMo :: forall f e m (m :: * -> *).
(Data f, Data e, Data m, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
gmapMp :: (forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
$cgmapMp :: forall f e m (m :: * -> *).
(Data f, Data e, Data m, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
gmapM :: (forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
$cgmapM :: forall f e m (m :: * -> *).
(Data f, Data e, Data m, Monad m) =>
(forall d. Data d => d -> m d)
-> Morphism f e m -> m (Morphism f e m)
gmapQi :: Int -> (forall d. Data d => d -> u) -> Morphism f e m -> u
$cgmapQi :: forall f e m u.
(Data f, Data e, Data m) =>
Int -> (forall d. Data d => d -> u) -> Morphism f e m -> u
gmapQ :: (forall d. Data d => d -> u) -> Morphism f e m -> [u]
$cgmapQ :: forall f e m u.
(Data f, Data e, Data m) =>
(forall d. Data d => d -> u) -> Morphism f e m -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
$cgmapQr :: forall f e m r r'.
(Data f, Data e, Data m) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
$cgmapQl :: forall f e m r r'.
(Data f, Data e, Data m) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Morphism f e m -> r
gmapT :: (forall b. Data b => b -> b) -> Morphism f e m -> Morphism f e m
$cgmapT :: forall f e m.
(Data f, Data e, Data m) =>
(forall b. Data b => b -> b) -> Morphism f e m -> Morphism f e m
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Morphism f e m))
$cdataCast2 :: forall f e m (t :: * -> * -> *) (c :: * -> *).
(Data f, Data e, Data m, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (Morphism f e m))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (Morphism f e m))
$cdataCast1 :: forall f e m (t :: * -> *) (c :: * -> *).
(Data f, Data e, Data m, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Morphism f e m))
dataTypeOf :: Morphism f e m -> DataType
$cdataTypeOf :: forall f e m.
(Data f, Data e, Data m) =>
Morphism f e m -> DataType
toConstr :: Morphism f e m -> Constr
$ctoConstr :: forall f e m. (Data f, Data e, Data m) => Morphism f e m -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Morphism f e m)
$cgunfold :: forall f e m (c :: * -> *).
(Data f, Data e, Data m) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Morphism f e m)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m)
$cgfoldl :: forall f e m (c :: * -> *).
(Data f, Data e, Data m) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Morphism f e m -> c (Morphism f e m)
$cp1Data :: forall f e m. (Data f, Data e, Data m) => Typeable (Morphism f e m)
Data)

data DefMorExt e = DefMorExt e deriving (Typeable, Typeable (DefMorExt e)
Constr
DataType
Typeable (DefMorExt e) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (DefMorExt e))
-> (DefMorExt e -> Constr)
-> (DefMorExt e -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (DefMorExt e)))
-> ((forall b. Data b => b -> b) -> DefMorExt e -> DefMorExt e)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r)
-> (forall u. (forall d. Data d => d -> u) -> DefMorExt e -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> DefMorExt e -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e))
-> Data (DefMorExt e)
DefMorExt e -> Constr
DefMorExt e -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e))
(forall b. Data b => b -> b) -> DefMorExt e -> DefMorExt e
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DefMorExt e)
forall e. Data e => Typeable (DefMorExt e)
forall e. Data e => DefMorExt e -> Constr
forall e. Data e => DefMorExt e -> DataType
forall e.
Data e =>
(forall b. Data b => b -> b) -> DefMorExt e -> DefMorExt e
forall e u.
Data e =>
Int -> (forall d. Data d => d -> u) -> DefMorExt e -> u
forall e u.
Data e =>
(forall d. Data d => d -> u) -> DefMorExt e -> [u]
forall e r r'.
Data e =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
forall e r r'.
Data e =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
forall e (m :: * -> *).
(Data e, Monad m) =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
forall e (m :: * -> *).
(Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
forall e (c :: * -> *).
Data e =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DefMorExt e)
forall e (c :: * -> *).
Data e =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e)
forall e (t :: * -> *) (c :: * -> *).
(Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e))
forall e (t :: * -> * -> *) (c :: * -> *).
(Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DefMorExt e))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> DefMorExt e -> u
forall u. (forall d. Data d => d -> u) -> DefMorExt e -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DefMorExt e)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DefMorExt e))
$cDefMorExt :: Constr
$tDefMorExt :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
$cgmapMo :: forall e (m :: * -> *).
(Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
gmapMp :: (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
$cgmapMp :: forall e (m :: * -> *).
(Data e, MonadPlus m) =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
gmapM :: (forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
$cgmapM :: forall e (m :: * -> *).
(Data e, Monad m) =>
(forall d. Data d => d -> m d) -> DefMorExt e -> m (DefMorExt e)
gmapQi :: Int -> (forall d. Data d => d -> u) -> DefMorExt e -> u
$cgmapQi :: forall e u.
Data e =>
Int -> (forall d. Data d => d -> u) -> DefMorExt e -> u
gmapQ :: (forall d. Data d => d -> u) -> DefMorExt e -> [u]
$cgmapQ :: forall e u.
Data e =>
(forall d. Data d => d -> u) -> DefMorExt e -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
$cgmapQr :: forall e r r'.
Data e =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
$cgmapQl :: forall e r r'.
Data e =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> DefMorExt e -> r
gmapT :: (forall b. Data b => b -> b) -> DefMorExt e -> DefMorExt e
$cgmapT :: forall e.
Data e =>
(forall b. Data b => b -> b) -> DefMorExt e -> DefMorExt e
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DefMorExt e))
$cdataCast2 :: forall e (t :: * -> * -> *) (c :: * -> *).
(Data e, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (DefMorExt e))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e))
$cdataCast1 :: forall e (t :: * -> *) (c :: * -> *).
(Data e, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (DefMorExt e))
dataTypeOf :: DefMorExt e -> DataType
$cdataTypeOf :: forall e. Data e => DefMorExt e -> DataType
toConstr :: DefMorExt e -> Constr
$ctoConstr :: forall e. Data e => DefMorExt e -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DefMorExt e)
$cgunfold :: forall e (c :: * -> *).
Data e =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (DefMorExt e)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e)
$cgfoldl :: forall e (c :: * -> *).
Data e =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> DefMorExt e -> c (DefMorExt e)
$cp1Data :: forall e. Data e => Typeable (DefMorExt e)
Data)

instance Show (DefMorExt e) where
  show :: DefMorExt e -> String
show = String -> DefMorExt e -> String
forall a b. a -> b -> a
const ""

instance Ord (DefMorExt e) where
  compare :: DefMorExt e -> DefMorExt e -> Ordering
compare _ = Ordering -> DefMorExt e -> Ordering
forall a b. a -> b -> a
const Ordering
EQ

instance Eq (DefMorExt e) where
  == :: DefMorExt e -> DefMorExt e -> Bool
(==) e :: DefMorExt e
e = (Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ) (Ordering -> Bool)
-> (DefMorExt e -> Ordering) -> DefMorExt e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DefMorExt e -> DefMorExt e -> Ordering
forall a. Ord a => a -> a -> Ordering
compare DefMorExt e
e

emptyMorExt :: DefMorExt e
emptyMorExt :: DefMorExt e
emptyMorExt = e -> DefMorExt e
forall e. e -> DefMorExt e
DefMorExt (e -> DefMorExt e) -> e -> DefMorExt e
forall a b. (a -> b) -> a -> b
$ String -> e
forall a. HasCallStack => String -> a
error "emptyMorExt"

instance Pretty (DefMorExt e) where
  pretty :: DefMorExt e -> Doc
pretty _ = Doc
empty

class (Pretty e, Pretty m) => MorphismExtension e m | m -> e where
   ideMorphismExtension :: e -> m
   composeMorphismExtension :: Morphism f e m -> Morphism f e m -> Result m
   inverseMorphismExtension :: Morphism f e m -> Result m
   inverseMorphismExtension = m -> Result m
forall (m :: * -> *) a. Monad m => a -> m a
return (m -> Result m)
-> (Morphism f e m -> m) -> Morphism f e m -> Result m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map
   isInclusionMorphismExtension :: m -> Bool
   prettyMorphismExtension :: Morphism f e m -> Doc
   prettyMorphismExtension = m -> Doc
forall a. Pretty a => a -> Doc
pretty (m -> Doc) -> (Morphism f e m -> m) -> Morphism f e m -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map
   legalMorphismExtension :: Morphism f e m -> Result ()
   legalMorphismExtension _ = () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance MorphismExtension () () where
   ideMorphismExtension :: () -> ()
ideMorphismExtension _ = ()
   composeMorphismExtension :: Morphism f () () -> Morphism f () () -> Result ()
composeMorphismExtension _ = () -> Result ()
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Result ())
-> (Morphism f () () -> ()) -> Morphism f () () -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f () () -> ()
forall f e m. Morphism f e m -> m
extended_map
   isInclusionMorphismExtension :: () -> Bool
isInclusionMorphismExtension _ = Bool
True

instance Pretty e => MorphismExtension e (DefMorExt e) where
   ideMorphismExtension :: e -> DefMorExt e
ideMorphismExtension _ = DefMorExt e
forall e. DefMorExt e
emptyMorExt
   composeMorphismExtension :: Morphism f e (DefMorExt e)
-> Morphism f e (DefMorExt e) -> Result (DefMorExt e)
composeMorphismExtension _ = DefMorExt e -> Result (DefMorExt e)
forall (m :: * -> *) a. Monad m => a -> m a
return (DefMorExt e -> Result (DefMorExt e))
-> (Morphism f e (DefMorExt e) -> DefMorExt e)
-> Morphism f e (DefMorExt e)
-> Result (DefMorExt e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e (DefMorExt e) -> DefMorExt e
forall f e m. Morphism f e m -> m
extended_map
   isInclusionMorphismExtension :: DefMorExt e -> Bool
isInclusionMorphismExtension _ = Bool
True

type CASLMor = Morphism () () ()

isInclusionMorphism :: (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism :: (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism f :: m -> Bool
f m :: Morphism f e m
m = m -> Bool
f (Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map Morphism f e m
m) Bool -> Bool -> Bool
&& Sort_map -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m)
  Bool -> Bool -> Bool
&& Pred_map -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m) Bool -> Bool -> Bool
&& Op_map -> Bool
isInclOpMap (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m)

mapSort :: Sort_map -> SORT -> SORT
mapSort :: Sort_map -> Id -> Id
mapSort sorts :: Sort_map
sorts s :: Id
s = Id -> Id -> Sort_map -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
s Id
s Sort_map
sorts

mapOpType :: Sort_map -> OpType -> OpType
mapOpType :: Sort_map -> OpType -> OpType
mapOpType sorts :: Sort_map
sorts t :: OpType
t = if Sort_map -> Bool
forall k a. Map k a -> Bool
Map.null Sort_map
sorts then OpType
t else
  OpType
t { opArgs :: [Id]
opArgs = (Id -> Id) -> [Id] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Sort_map -> Id -> Id
mapSort Sort_map
sorts) ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
t
    , opRes :: Id
opRes = Sort_map -> Id -> Id
mapSort Sort_map
sorts (Id -> Id) -> Id -> Id
forall a b. (a -> b) -> a -> b
$ OpType -> Id
opRes OpType
t }

makeTotal :: OpKind -> OpType -> OpType
makeTotal :: OpKind -> OpType -> OpType
makeTotal fk :: OpKind
fk t :: OpType
t = case OpKind
fk of
  Total -> OpType -> OpType
mkTotal OpType
t
  _ -> OpType
t

mapOpSym :: Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym :: Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym sMap :: Sort_map
sMap oMap :: Op_map
oMap (i :: Id
i, ot :: OpType
ot) = let mot :: OpType
mot = Sort_map -> OpType -> OpType
mapOpType Sort_map
sMap OpType
ot in
  case (Id, OpType) -> Op_map -> Maybe (Id, OpKind)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id
i, OpType -> OpType
mkPartial OpType
ot) Op_map
oMap of
    Nothing -> (Id
i, OpType
mot)
    Just (j :: Id
j, k :: OpKind
k) -> (Id
j, OpKind -> OpType -> OpType
makeTotal OpKind
k OpType
mot)

-- | Check if two OpTypes are equal modulo totality or partiality
compatibleOpTypes :: OpType -> OpType -> Bool
compatibleOpTypes :: OpType -> OpType -> Bool
compatibleOpTypes ot1 :: OpType
ot1 ot2 :: OpType
ot2 = OpType -> [Id]
opSorts OpType
ot1 [Id] -> [Id] -> Bool
forall a. Eq a => a -> a -> Bool
== OpType -> [Id]
opSorts OpType
ot2

mapPredType :: Sort_map -> PredType -> PredType
mapPredType :: Sort_map -> PredType -> PredType
mapPredType sorts :: Sort_map
sorts t :: PredType
t = if Sort_map -> Bool
forall k a. Map k a -> Bool
Map.null Sort_map
sorts then PredType
t else
  PredType
t { predArgs :: [Id]
predArgs = (Id -> Id) -> [Id] -> [Id]
forall a b. (a -> b) -> [a] -> [b]
map (Sort_map -> Id -> Id
mapSort Sort_map
sorts) ([Id] -> [Id]) -> [Id] -> [Id]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
t }

mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym sMap :: Sort_map
sMap oMap :: Pred_map
oMap (i :: Id
i, pt :: PredType
pt) =
    (Id -> (Id, PredType) -> Pred_map -> Id
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Id
i (Id
i, PredType
pt) Pred_map
oMap, Sort_map -> PredType -> PredType
mapPredType Sort_map
sMap PredType
pt)

embedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism extEm :: m
extEm a :: Sign f e
a b :: Sign f e
b = Morphism :: forall f e m.
Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
Morphism
  { msource :: Sign f e
msource = Sign f e
a
  , mtarget :: Sign f e
mtarget = Sign f e
b
  , sort_map :: Sort_map
sort_map = Sort_map
forall k a. Map k a
Map.empty
  , op_map :: Op_map
op_map = Op_map
forall k a. Map k a
Map.empty
  , pred_map :: Pred_map
pred_map = Pred_map
forall k a. Map k a
Map.empty
  , extended_map :: m
extended_map = m
extEm }

-- | given empty extensions convert a morphism
mapCASLMor :: e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor :: e -> m -> Morphism f1 e1 m1 -> Morphism f e m
mapCASLMor e :: e
e me :: m
me m :: Morphism f1 e1 m1
m =
  (m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
me (e -> Sign f1 e1 -> Sign f e
forall e f1 e1 f. e -> Sign f1 e1 -> Sign f e
embedSign e
e (Sign f1 e1 -> Sign f e) -> Sign f1 e1 -> Sign f e
forall a b. (a -> b) -> a -> b
$ Morphism f1 e1 m1 -> Sign f1 e1
forall f e m. Morphism f e m -> Sign f e
msource Morphism f1 e1 m1
m) (Sign f e -> Morphism f e m) -> Sign f e -> Morphism f e m
forall a b. (a -> b) -> a -> b
$ e -> Sign f1 e1 -> Sign f e
forall e f1 e1 f. e -> Sign f1 e1 -> Sign f e
embedSign e
e (Sign f1 e1 -> Sign f e) -> Sign f1 e1 -> Sign f e
forall a b. (a -> b) -> a -> b
$ Morphism f1 e1 m1 -> Sign f1 e1
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f1 e1 m1
m)
  { sort_map :: Sort_map
sort_map = Morphism f1 e1 m1 -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f1 e1 m1
m
  , op_map :: Op_map
op_map = Morphism f1 e1 m1 -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f1 e1 m1
m
  , pred_map :: Pred_map
pred_map = Morphism f1 e1 m1 -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f1 e1 m1
m }

symbolToRaw :: Symbol -> RawSymbol
symbolToRaw :: Symbol -> RawSymbol
symbolToRaw = Symbol -> RawSymbol
ASymbol

idToRaw :: Id -> RawSymbol
idToRaw :: Id -> RawSymbol
idToRaw = SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit

rawSymName :: RawSymbol -> Id
rawSymName :: RawSymbol -> Id
rawSymName rs :: RawSymbol
rs = case RawSymbol
rs of
  ASymbol sym :: Symbol
sym -> Symbol -> Id
symName Symbol
sym
  AKindedSymb _ i :: Id
i -> Id
i

sortSyms :: Sign f e -> SymbolSet
sortSyms :: Sign f e -> SymbolSet
sortSyms = (Id -> Symbol) -> Set Id -> SymbolSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Symbol
idToSortSymbol (Set Id -> SymbolSet)
-> (Sign f e -> Set Id) -> Sign f e -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet

opSyms :: Sign f e -> [Symbol]
opSyms :: Sign f e -> [Symbol]
opSyms = ((Id, OpType) -> Symbol) -> [(Id, OpType)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ((Id -> OpType -> Symbol) -> (Id, OpType) -> Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> OpType -> Symbol
idToOpSymbol) ([(Id, OpType)] -> [Symbol])
-> (Sign f e -> [(Id, OpType)]) -> Sign f e -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id OpType -> [(Id, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (MapSet Id OpType -> [(Id, OpType)])
-> (Sign f e -> MapSet Id OpType) -> Sign f e -> [(Id, OpType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap

predSyms :: Sign f e -> [Symbol]
predSyms :: Sign f e -> [Symbol]
predSyms = ((Id, PredType) -> Symbol) -> [(Id, PredType)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map ((Id -> PredType -> Symbol) -> (Id, PredType) -> Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> PredType -> Symbol
idToPredSymbol) ([(Id, PredType)] -> [Symbol])
-> (Sign f e -> [(Id, PredType)]) -> Sign f e -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id PredType -> [(Id, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (MapSet Id PredType -> [(Id, PredType)])
-> (Sign f e -> MapSet Id PredType) -> Sign f e -> [(Id, PredType)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap

{- | returns the symbol sets of the signature in the correct dependency order
, i.e., sorts first, then ops and predicates. Result list is of length two. -}
symOf :: Sign f e -> [SymbolSet]
symOf :: Sign f e -> [SymbolSet]
symOf s :: Sign f e
s = [ Sign f e -> SymbolSet
forall f e. Sign f e -> SymbolSet
sortSyms Sign f e
s, [Symbol] -> SymbolSet
forall a. Ord a => [a] -> Set a
Set.fromList ([Symbol] -> SymbolSet) -> [Symbol] -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Sign f e -> [Symbol]
forall f e. Sign f e -> [Symbol]
predSyms Sign f e
s [Symbol] -> [Symbol] -> [Symbol]
forall a. [a] -> [a] -> [a]
++ Sign f e -> [Symbol]
forall f e. Sign f e -> [Symbol]
opSyms Sign f e
s ]

sigSymsOf :: Sign f e -> [Symbol]
sigSymsOf :: Sign f e -> [Symbol]
sigSymsOf s :: Sign f e
s = [[Symbol]] -> [Symbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  [ SymbolSet -> [Symbol]
forall a. Set a -> [a]
Set.toList (SymbolSet -> [Symbol]) -> SymbolSet -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign f e -> SymbolSet
forall f e. Sign f e -> SymbolSet
sortSyms Sign f e
s
  , ((Id, Id) -> Symbol) -> [(Id, Id)] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ (a :: Id
a, b :: Id
b) -> Id -> SymbType -> Symbol
Symbol Id
a (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbType
SubsortAsItemType Id
b)
    ([(Id, Id)] -> [Symbol])
-> (Rel Id -> [(Id, Id)]) -> Rel Id -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> [(Id, Id)]
forall a. Rel a -> [(a, a)]
Rel.toList (Rel Id -> [(Id, Id)])
-> (Rel Id -> Rel Id) -> Rel Id -> [(Id, Id)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (Rel Id -> Rel Id) -> (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel Id -> [Symbol]) -> Rel Id -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
s
    -- assume sort relation to be the transitive closure
  , Sign f e -> [Symbol]
forall f e. Sign f e -> [Symbol]
opSyms Sign f e
s
  , Sign f e -> [Symbol]
forall f e. Sign f e -> [Symbol]
predSyms Sign f e
s ]

-- | set of symbols for a signature
symsetOf :: Sign f e -> SymbolSet
symsetOf :: Sign f e -> SymbolSet
symsetOf = [SymbolSet] -> SymbolSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([SymbolSet] -> SymbolSet)
-> (Sign f e -> [SymbolSet]) -> Sign f e -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> [SymbolSet]
forall f e. Sign f e -> [SymbolSet]
symOf

checkSymbList :: [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList :: [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList l :: [SYMB_OR_MAP]
l = case [SYMB_OR_MAP]
l of
         Symb (Symb_id a :: Id
a) : Symb (Qual_id b :: Id
b t :: TYPE
t _) : r :: [SYMB_OR_MAP]
r -> DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning
           ("profile '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TYPE -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TYPE
t "' does not apply to '"
            String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
a "' but only to") Id
b Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList [SYMB_OR_MAP]
r
         _ : r :: [SYMB_OR_MAP]
r -> [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList [SYMB_OR_MAP]
r
         [] -> []

insertRsys :: (Pretty r, GetRange r, Ord r)
  => (r -> Id) -> (r -> Maybe Id) -> (Id -> r)
    -> (r -> Maybe Id) -> (Id -> r) -> Map.Map r r -> (r, r)
      -> Result (Map.Map r r)
insertRsys :: (r -> Id)
-> (r -> Maybe Id)
-> (Id -> r)
-> (r -> Maybe Id)
-> (Id -> r)
-> Map r r
-> (r, r)
-> Result (Map r r)
insertRsys rawId :: r -> Id
rawId getSort :: r -> Maybe Id
getSort mkSort :: Id -> r
mkSort getImplicit :: r -> Maybe Id
getImplicit mkImplicit :: Id -> r
mkImplicit m1 :: Map r r
m1 (rsy1 :: r
rsy1, rsy2 :: r
rsy2) =
  let m3 :: Map r r
m3 = r -> r -> Map r r -> Map r r
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert r
rsy1 r
rsy2 Map r r
m1 in
        case r -> Map r r -> Maybe r
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup r
rsy1 Map r r
m1 of
          Nothing -> case r -> Maybe Id
getSort r
rsy1 of
            Just i :: Id
i ->
              case r -> Map r r -> Maybe r
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id -> r
mkImplicit Id
i) Map r r
m1 of
                Just r2 :: r
r2 | Id -> Maybe Id
forall a. a -> Maybe a
Just (r -> Id
rawId r
rsy2) Maybe Id -> Maybe Id -> Bool
forall a. Eq a => a -> a -> Bool
== r -> Maybe Id
getImplicit r
r2 ->
                  Map r r -> String -> Range -> Result (Map r r)
forall a. a -> String -> Range -> Result a
warning Map r r
m1 ("ignoring separate mapping for sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                    Id -> String
forall a. Show a => a -> String
show Id
i) (Range -> Result (Map r r)) -> Range -> Result (Map r r)
forall a b. (a -> b) -> a -> b
$ Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i
                _ -> Map r r -> Result (Map r r)
forall (m :: * -> *) a. Monad m => a -> m a
return Map r r
m3
            Nothing -> case r -> Maybe Id
getImplicit r
rsy1 of
              Just i :: Id
i -> let rsy3 :: r
rsy3 = Id -> r
mkSort Id
i in case r -> Map r r -> Maybe r
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup r
rsy3 Map r r
m1 of
                Just r2 :: r
r2 | Id -> Maybe Id
forall a. a -> Maybe a
Just (r -> Id
rawId r
rsy2) Maybe Id -> Maybe Id -> Bool
forall a. Eq a => a -> a -> Bool
== r -> Maybe Id
getSort r
r2 ->
                  Map r r -> String -> Range -> Result (Map r r)
forall a. a -> String -> Range -> Result a
warning (r -> Map r r -> Map r r
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete r
rsy3 Map r r
m3)
                      ("ignoring extra mapping of sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++
                       Id -> String
forall a. Show a => a -> String
show Id
i) (Range -> Result (Map r r)) -> Range -> Result (Map r r)
forall a b. (a -> b) -> a -> b
$ Id -> Range
forall a. GetRange a => a -> Range
getRange Id
i
                   {- this case cannot occur, because unkinded names cannot
                      follow kinded ones:
                      in "sort s |-> t, o |-> q" "o" will be a sort, too. -}
                _ -> Map r r -> Result (Map r r)
forall (m :: * -> *) a. Monad m => a -> m a
return Map r r
m3
              _ -> Map r r -> Result (Map r r)
forall (m :: * -> *) a. Monad m => a -> m a
return Map r r
m3
          Just rsy3 :: r
rsy3 -> if r
rsy2 r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
rsy3 then
            Map r r -> String -> Range -> Result (Map r r)
forall a. a -> String -> Range -> Result a
hint Map r r
m1 ("ignoring duplicate mapping of "
                       String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> ShowS
forall a. Pretty a => a -> ShowS
showDoc r
rsy1 "") (Range -> Result (Map r r)) -> Range -> Result (Map r r)
forall a b. (a -> b) -> a -> b
$ r -> Range
forall a. GetRange a => a -> Range
getRange r
rsy1 else
              Map r r -> String -> Range -> Result (Map r r)
forall a. a -> String -> Range -> Result a
plain_error Map r r
m1 ("Symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> ShowS
forall a. Pretty a => a -> ShowS
showDoc r
rsy1 " mapped twice to "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> ShowS
forall a. Pretty a => a -> ShowS
showDoc r
rsy2 " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ r -> ShowS
forall a. Pretty a => a -> ShowS
showDoc r
rsy3 "") Range
nullRange

statSymbMapItems :: Sign f e -> Maybe (Sign f e) -> [SYMB_MAP_ITEMS]
  -> Result RawSymbolMap
statSymbMapItems :: Sign f e
-> Maybe (Sign f e) -> [SYMB_MAP_ITEMS] -> Result RawSymbolMap
statSymbMapItems sig :: Sign f e
sig msig :: Maybe (Sign f e)
msig sl :: [SYMB_MAP_ITEMS]
sl = do
  let st :: SYMB_MAP_ITEMS -> Result [(RawSymbol, RawSymbol)]
st (Symb_map_items kind :: SYMB_KIND
kind l :: [SYMB_OR_MAP]
l _) = do
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList [SYMB_OR_MAP]
l
        ([[(RawSymbol, RawSymbol)]] -> [(RawSymbol, RawSymbol)])
-> Result [[(RawSymbol, RawSymbol)]]
-> Result [(RawSymbol, RawSymbol)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[(RawSymbol, RawSymbol)]] -> [(RawSymbol, RawSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (Result [[(RawSymbol, RawSymbol)]]
 -> Result [(RawSymbol, RawSymbol)])
-> Result [[(RawSymbol, RawSymbol)]]
-> Result [(RawSymbol, RawSymbol)]
forall a b. (a -> b) -> a -> b
$ (SYMB_OR_MAP -> Result [(RawSymbol, RawSymbol)])
-> [SYMB_OR_MAP] -> Result [[(RawSymbol, RawSymbol)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign f e
-> Maybe (Sign f e)
-> SYMB_KIND
-> SYMB_OR_MAP
-> Result [(RawSymbol, RawSymbol)]
forall f e.
Sign f e
-> Maybe (Sign f e)
-> SYMB_KIND
-> SYMB_OR_MAP
-> Result [(RawSymbol, RawSymbol)]
symbOrMapToRaw Sign f e
sig Maybe (Sign f e)
msig SYMB_KIND
kind) [SYMB_OR_MAP]
l
      getSort :: RawSymbol -> Maybe Id
getSort rsy :: RawSymbol
rsy = case RawSymbol
rsy of
        ASymbol (Symbol i :: Id
i SortAsItemType) -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i
        _ -> Maybe Id
forall a. Maybe a
Nothing
      getImplicit :: RawSymbol -> Maybe Id
getImplicit rsy :: RawSymbol
rsy = case RawSymbol
rsy of
        AKindedSymb Implicit i :: Id
i -> Id -> Maybe Id
forall a. a -> Maybe a
Just Id
i
        _ -> Maybe Id
forall a. Maybe a
Nothing
      mkSort :: Id -> RawSymbol
mkSort i :: Id
i = Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbType -> Symbol
Symbol Id
i SymbType
SortAsItemType
      mkImplicit :: Id -> RawSymbol
mkImplicit = SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit
  [[(RawSymbol, RawSymbol)]]
ls <- (SYMB_MAP_ITEMS -> Result [(RawSymbol, RawSymbol)])
-> [SYMB_MAP_ITEMS] -> Result [[(RawSymbol, RawSymbol)]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SYMB_MAP_ITEMS -> Result [(RawSymbol, RawSymbol)]
st [SYMB_MAP_ITEMS]
sl
  (RawSymbolMap -> (RawSymbol, RawSymbol) -> Result RawSymbolMap)
-> RawSymbolMap -> [(RawSymbol, RawSymbol)] -> Result RawSymbolMap
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM ((RawSymbol -> Id)
-> (RawSymbol -> Maybe Id)
-> (Id -> RawSymbol)
-> (RawSymbol -> Maybe Id)
-> (Id -> RawSymbol)
-> RawSymbolMap
-> (RawSymbol, RawSymbol)
-> Result RawSymbolMap
forall r.
(Pretty r, GetRange r, Ord r) =>
(r -> Id)
-> (r -> Maybe Id)
-> (Id -> r)
-> (r -> Maybe Id)
-> (Id -> r)
-> Map r r
-> (r, r)
-> Result (Map r r)
insertRsys RawSymbol -> Id
rawSymName RawSymbol -> Maybe Id
getSort Id -> RawSymbol
mkSort RawSymbol -> Maybe Id
getImplicit Id -> RawSymbol
mkImplicit)
                    RawSymbolMap
forall k a. Map k a
Map.empty ([[(RawSymbol, RawSymbol)]] -> [(RawSymbol, RawSymbol)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(RawSymbol, RawSymbol)]]
ls)

symbOrMapToRaw :: Sign f e -> Maybe (Sign f e) -> SYMB_KIND -> SYMB_OR_MAP
   -> Result [(RawSymbol, RawSymbol)]
symbOrMapToRaw :: Sign f e
-> Maybe (Sign f e)
-> SYMB_KIND
-> SYMB_OR_MAP
-> Result [(RawSymbol, RawSymbol)]
symbOrMapToRaw sig :: Sign f e
sig msig :: Maybe (Sign f e)
msig k :: SYMB_KIND
k sm :: SYMB_OR_MAP
sm = case SYMB_OR_MAP
sm of
    Symb s :: SYMB
s -> do
      RawSymbol
v <- Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw Bool
True Sign f e
sig SYMB_KIND
k SYMB
s
      [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawSymbol
v, RawSymbol
v)]
    Symb_map s :: SYMB
s t :: SYMB
t _ -> do
      [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ case (SYMB
s, SYMB
t) of
        (Symb_id a :: Id
a, Symb_id b :: Id
b) | Id
a Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
b ->
          [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "unneeded identical mapping of" Id
a]
        _ -> []
      RawSymbol
w <- Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw Bool
True Sign f e
sig SYMB_KIND
k SYMB
s
      RawSymbol
x <- case Maybe (Sign f e)
msig of
             Nothing -> Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw Bool
False Sign f e
sig SYMB_KIND
k SYMB
t
             Just tsig :: Sign f e
tsig -> Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw Bool
True Sign f e
tsig SYMB_KIND
k SYMB
t
      let mkS :: Id -> RawSymbol
mkS = Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> (Id -> Symbol) -> Id -> RawSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> Symbol
idToSortSymbol
      case (SYMB
s, SYMB
t) of
        (Qual_id _ t1 :: TYPE
t1 _, Qual_id _ t2 :: TYPE
t2 _) -> case (TYPE
t1, TYPE
t2) of
          (O_type (Op_type _ args1 :: [Id]
args1 res1 :: Id
res1 _), O_type (Op_type _ args2 :: [Id]
args2 res2 :: Id
res2 _))
            | [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args2 -> -- ignore partiality
            [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)])
-> [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall a b. (a -> b) -> a -> b
$ (RawSymbol
w, RawSymbol
x) (RawSymbol, RawSymbol)
-> [(RawSymbol, RawSymbol)] -> [(RawSymbol, RawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> RawSymbol
mkS Id
res1, Id -> RawSymbol
mkS Id
res2)
              (RawSymbol, RawSymbol)
-> [(RawSymbol, RawSymbol)] -> [(RawSymbol, RawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> Id -> (RawSymbol, RawSymbol))
-> [Id] -> [Id] -> [(RawSymbol, RawSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ s1 :: Id
s1 s2 :: Id
s2 -> (Id -> RawSymbol
mkS Id
s1, Id -> RawSymbol
mkS Id
s2)) [Id]
args1 [Id]
args2
          (P_type (Pred_type args1 :: [Id]
args1 _), P_type (Pred_type args2 :: [Id]
args2 _))
            | [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
args2 ->
            [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)])
-> [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall a b. (a -> b) -> a -> b
$ (RawSymbol
w, RawSymbol
x)
              (RawSymbol, RawSymbol)
-> [(RawSymbol, RawSymbol)] -> [(RawSymbol, RawSymbol)]
forall a. a -> [a] -> [a]
: (Id -> Id -> (RawSymbol, RawSymbol))
-> [Id] -> [Id] -> [(RawSymbol, RawSymbol)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\ s1 :: Id
s1 s2 :: Id
s2 -> (Id -> RawSymbol
mkS Id
s1, Id -> RawSymbol
mkS Id
s2)) [Id]
args1 [Id]
args2
          (O_type (Op_type _ [] res1 :: Id
res1 _), A_type s2 :: Id
s2) ->
            [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawSymbol
w, RawSymbol
x), (Id -> RawSymbol
mkS Id
res1, Id -> RawSymbol
mkS Id
s2)]
          (A_type s1 :: Id
s1, O_type (Op_type _ [] res2 :: Id
res2 _)) ->
            [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawSymbol
w, RawSymbol
x), (Id -> RawSymbol
mkS Id
s1, Id -> RawSymbol
mkS Id
res2)]
          (A_type s1 :: Id
s1, A_type s2 :: Id
s2) ->
            [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawSymbol
w, RawSymbol
x), (Id -> RawSymbol
mkS Id
s1, Id -> RawSymbol
mkS Id
s2)]
          _ -> String -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result [(RawSymbol, RawSymbol)])
-> String -> Result [(RawSymbol, RawSymbol)]
forall a b. (a -> b) -> a -> b
$ "profiles '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TYPE -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TYPE
t1 "' and '"
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ TYPE -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TYPE
t2 "' do not match"
        _ -> [(RawSymbol, RawSymbol)] -> Result [(RawSymbol, RawSymbol)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(RawSymbol
w, RawSymbol
x)]

statSymbItems :: Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems :: Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems sig :: Sign f e
sig sl :: [SYMB_ITEMS]
sl =
  let st :: SYMB_ITEMS -> Result [RawSymbol]
st (Symb_items kind :: SYMB_KIND
kind l :: [SYMB]
l _) = do
        [Diagnosis] -> Result ()
appendDiags ([Diagnosis] -> Result ()) -> [Diagnosis] -> Result ()
forall a b. (a -> b) -> a -> b
$ [SYMB_OR_MAP] -> [Diagnosis]
checkSymbList ([SYMB_OR_MAP] -> [Diagnosis]) -> [SYMB_OR_MAP] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ (SYMB -> SYMB_OR_MAP) -> [SYMB] -> [SYMB_OR_MAP]
forall a b. (a -> b) -> [a] -> [b]
map SYMB -> SYMB_OR_MAP
Symb [SYMB]
l
        (SYMB -> Result RawSymbol) -> [SYMB] -> Result [RawSymbol]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw Bool
True Sign f e
sig SYMB_KIND
kind) [SYMB]
l
  in ([[RawSymbol]] -> [RawSymbol])
-> Result [[RawSymbol]] -> Result [RawSymbol]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[RawSymbol]] -> [RawSymbol]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((SYMB_ITEMS -> Result [RawSymbol])
-> [SYMB_ITEMS] -> Result [[RawSymbol]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SYMB_ITEMS -> Result [RawSymbol]
st [SYMB_ITEMS]
sl)

-- | bool indicates if a deeper symbol check is possible for target symbols
symbToRaw :: Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw :: Bool -> Sign f e -> SYMB_KIND -> SYMB -> Result RawSymbol
symbToRaw b :: Bool
b sig :: Sign f e
sig k :: SYMB_KIND
k si :: SYMB
si = case SYMB
si of
  Symb_id idt :: Id
idt -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ case SYMB_KIND
k of
    Sorts_kind -> Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
idToSortSymbol Id
idt
    _ -> SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
k Id
idt
  Qual_id idt :: Id
idt t :: TYPE
t _ -> Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE -> Result RawSymbol
forall f e.
Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE -> Result RawSymbol
typedSymbKindToRaw Bool
b Sign f e
sig SYMB_KIND
k Id
idt TYPE
t

typedSymbKindToRaw :: Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE
  -> Result RawSymbol
typedSymbKindToRaw :: Bool -> Sign f e -> SYMB_KIND -> Id -> TYPE -> Result RawSymbol
typedSymbKindToRaw b :: Bool
b sig :: Sign f e
sig k :: SYMB_KIND
k idt :: Id
idt t :: TYPE
t = let
     pm :: MapSet Id PredType
pm = Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sig
     om :: MapSet Id OpType
om = Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sig
     getSet :: MapSet Id b -> Set b
getSet = Id -> MapSet Id b -> Set b
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
idt
     err :: Result RawSymbol
err = RawSymbol -> String -> Range -> Result RawSymbol
forall a. a -> String -> Range -> Result a
plain_error (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit Id
idt)
              (Id -> ShowS
forall a. Pretty a => a -> ShowS
showDoc Id
idt ":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ TYPE -> ShowS
forall a. Pretty a => a -> ShowS
showDoc TYPE
t
               "does not have kind" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SYMB_KIND -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SYMB_KIND
k "") (Id -> Range
forall a. GetRange a => a -> Range
getRange Id
idt)
     aSymb :: RawSymbol
aSymb = Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ case TYPE
t of
       O_type ot :: OP_TYPE
ot -> Id -> OpType -> Symbol
idToOpSymbol Id
idt (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
ot
       P_type pt :: PRED_TYPE
pt -> Id -> PredType -> Symbol
idToPredSymbol Id
idt (PredType -> Symbol) -> PredType -> Symbol
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
toPredType PRED_TYPE
pt
       A_type s :: Id
s -> Id -> OpType -> Symbol
idToOpSymbol Id
idt (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ Id -> OpType
sortToOpType Id
s
     unKnown :: Result RawSymbol
unKnown = do
       [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> RawSymbol -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown symbol" RawSymbol
aSymb]
       RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
    in case SYMB_KIND
k of
    Implicit -> case TYPE
t of
      A_type s :: Id
s -> if Bool
b then do
          let pt :: PredType
pt = Id -> PredType
sortToPredType Id
s
              ot :: OpType
ot = Id -> OpType
sortToOpType Id
s
              pot :: OpType
pot = OpType -> OpType
mkPartial OpType
ot
              hasPred :: Bool
hasPred = PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PredType
pt (Set PredType -> Bool) -> Set PredType -> Bool
forall a b. (a -> b) -> a -> b
$ MapSet Id PredType -> Set PredType
forall b. MapSet Id b -> Set b
getSet MapSet Id PredType
pm
              hasOp :: Bool
hasOp = OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
ot (Set OpType -> Bool) -> Set OpType -> Bool
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> Set OpType
forall b. MapSet Id b -> Set b
getSet MapSet Id OpType
om
              hasPOp :: Bool
hasPOp = OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
pot (Set OpType -> Bool) -> Set OpType -> Bool
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> Set OpType
forall b. MapSet Id b -> Set b
getSet MapSet Id OpType
om
              bothWarn :: Result ()
bothWarn = Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
hasPred (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
                [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "considering operation only" Id
idt]
          if Bool
hasOp then do
              [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "matched constant" Id
idt]
              Result ()
bothWarn
              RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
            else if Bool
hasPOp then do
              Result ()
bothWarn
              [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "constant is partial" Id
idt]
              RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> OpType -> Symbol
idToOpSymbol Id
idt OpType
pot
            else if Bool
hasPred then do
              [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "matched unary predicate" Id
idt]
              RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> PredType -> Symbol
idToPredSymbol Id
idt PredType
pt
            else Result RawSymbol
unKnown
        else do
          [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "qualify name as pred or op" Id
idt]
          RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
      _ -> RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
    Ops_kind -> case TYPE
t of
        P_type _ -> Result RawSymbol
err
        _ ->
          let ot :: OpType
ot = case TYPE
t of
                     O_type aot :: OP_TYPE
aot -> OP_TYPE -> OpType
toOpType OP_TYPE
aot
                     A_type s :: Id
s -> Id -> OpType
sortToOpType Id
s
                     P_type _ -> String -> OpType
forall a. HasCallStack => String -> a
error "CASL.typedSymbKindToRaw.Ops_kind"
              pot :: OpType
pot = OpType -> OpType
mkPartial OpType
ot
              isMem :: OpType -> Bool
isMem aot :: OpType
aot = OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
aot (Set OpType -> Bool) -> Set OpType -> Bool
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> Set OpType
forall b. MapSet Id b -> Set b
getSet MapSet Id OpType
om
          in if Bool
b then
            if OpType -> Bool
isMem OpType
ot then RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
            else if OpType -> Bool
isMem OpType
pot then do
             [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning "operation is partial" Id
idt]
             RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return (RawSymbol -> Result RawSymbol) -> RawSymbol -> Result RawSymbol
forall a b. (a -> b) -> a -> b
$ Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> OpType -> Symbol
idToOpSymbol Id
idt OpType
pot
            else Result RawSymbol
unKnown
          else RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
aSymb
    Preds_kind -> case TYPE
t of
        O_type _ -> Result RawSymbol
err
        _ ->
          let pt :: PredType
pt = case TYPE
t of
                     A_type s :: Id
s -> Id -> PredType
sortToPredType Id
s
                     P_type qt :: PRED_TYPE
qt -> PRED_TYPE -> PredType
toPredType PRED_TYPE
qt
                     O_type _ -> String -> PredType
forall a. HasCallStack => String -> a
error "CASL.typedSymbKindToRaw.Preds_kind"
              pSymb :: RawSymbol
pSymb = Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> PredType -> Symbol
idToPredSymbol Id
idt PredType
pt
          in if Bool
b then
              if PredType -> Set PredType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PredType
pt (Set PredType -> Bool) -> Set PredType -> Bool
forall a b. (a -> b) -> a -> b
$ MapSet Id PredType -> Set PredType
forall b. MapSet Id b -> Set b
getSet MapSet Id PredType
pm then do
                 [Diagnosis] -> Result ()
appendDiags [DiagKind -> String -> Id -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Hint "matched predicate" Id
idt]
                 RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
pSymb
              else Result RawSymbol
unKnown
             else RawSymbol -> Result RawSymbol
forall (m :: * -> *) a. Monad m => a -> m a
return RawSymbol
pSymb
    Sorts_kind -> Result RawSymbol
err

morphismToSymbMap :: Morphism f e m -> SymbolMap
morphismToSymbMap :: Morphism f e m -> SymbolMap
morphismToSymbMap = Bool -> Morphism f e m -> SymbolMap
forall f e m. Bool -> Morphism f e m -> SymbolMap
morphismToSymbMapAux Bool
False

morphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap
morphismToSymbMapAux :: Bool -> Morphism f e m -> SymbolMap
morphismToSymbMapAux b :: Bool
b mor :: Morphism f e m
mor = let
    src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor
    sorts :: Sort_map
sorts = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor
    ops :: Op_map
ops = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor
    preds :: Pred_map
preds = Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor
    sortSymMap :: SymbolMap
sortSymMap = (Id -> SymbolMap -> SymbolMap) -> SymbolMap -> Set Id -> SymbolMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
      (\ s :: Id
s -> let t :: Id
t = Sort_map -> Id -> Id
mapSort Sort_map
sorts Id
s in
         if Bool
b Bool -> Bool -> Bool
&& Id
s Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
t then SymbolMap -> SymbolMap
forall a. a -> a
id else
             Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> Symbol
idToSortSymbol Id
s) (Symbol -> SymbolMap -> SymbolMap)
-> Symbol -> SymbolMap -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
idToSortSymbol Id
t)
      SymbolMap
forall k a. Map k a
Map.empty (Set Id -> SymbolMap) -> Set Id -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
src
    opSymMap :: SymbolMap
opSymMap = (Id -> OpType -> SymbolMap -> SymbolMap)
-> SymbolMap -> MapSet Id OpType -> SymbolMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
      ( \ i :: Id
i t :: OpType
t -> let (j :: Id
j, k :: OpType
k) = Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym Sort_map
sorts Op_map
ops (Id
i, OpType
t) in
                 if Bool
b Bool -> Bool -> Bool
&& Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j Bool -> Bool -> Bool
&& OpType -> OpKind
opKind OpType
k OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpType -> OpKind
opKind OpType
t then SymbolMap -> SymbolMap
forall a. a -> a
id else
                     Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> OpType -> Symbol
idToOpSymbol Id
i OpType
t) (Symbol -> SymbolMap -> SymbolMap)
-> Symbol -> SymbolMap -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Id -> OpType -> Symbol
idToOpSymbol Id
j OpType
k)
      SymbolMap
forall k a. Map k a
Map.empty (MapSet Id OpType -> SymbolMap) -> MapSet Id OpType -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
src
    predSymMap :: SymbolMap
predSymMap = (Id -> PredType -> SymbolMap -> SymbolMap)
-> SymbolMap -> MapSet Id PredType -> SymbolMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
      ( \ i :: Id
i t :: PredType
t -> let (j :: Id
j, k :: PredType
k) = Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym Sort_map
sorts Pred_map
preds (Id
i, PredType
t) in
                 if Bool
b Bool -> Bool -> Bool
&& Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j then SymbolMap -> SymbolMap
forall a. a -> a
id else
                     Symbol -> Symbol -> SymbolMap -> SymbolMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id -> PredType -> Symbol
idToPredSymbol Id
i PredType
t) (Symbol -> SymbolMap -> SymbolMap)
-> Symbol -> SymbolMap -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Id -> PredType -> Symbol
idToPredSymbol Id
j PredType
k)
      SymbolMap
forall k a. Map k a
Map.empty (MapSet Id PredType -> SymbolMap)
-> MapSet Id PredType -> SymbolMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
src
  in (SymbolMap -> SymbolMap -> SymbolMap)
-> SymbolMap -> [SymbolMap] -> SymbolMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SymbolMap -> SymbolMap -> SymbolMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SymbolMap
sortSymMap [SymbolMap
opSymMap, SymbolMap
predSymMap]

matches :: Symbol -> RawSymbol -> Bool
matches :: Symbol -> RawSymbol -> Bool
matches (Symbol idt :: Id
idt k :: SymbType
k) rs :: RawSymbol
rs = case RawSymbol
rs of
    ASymbol (Symbol id2 :: Id
id2 k2 :: SymbType
k2) -> Id
idt Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
id2 Bool -> Bool -> Bool
&& case (SymbType
k, SymbType
k2) of
     (OpAsItemType ot :: OpType
ot, OpAsItemType ot2 :: OpType
ot2) -> OpType -> OpType -> Bool
compatibleOpTypes OpType
ot OpType
ot2
     _ -> SymbType
k SymbType -> SymbType -> Bool
forall a. Eq a => a -> a -> Bool
== SymbType
k2
    AKindedSymb rk :: SYMB_KIND
rk di :: Id
di -> let res :: Bool
res = Id
idt Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
di in case (SymbType
k, SYMB_KIND
rk) of
        (_, Implicit) -> Bool
res
        (SortAsItemType, Sorts_kind) -> Bool
res
        (OpAsItemType _, Ops_kind) -> Bool
res
        (PredAsItemType _, Preds_kind) -> Bool
res
        _ -> Bool
False

idMor :: m -> Sign f e -> Morphism f e m
idMor :: m -> Sign f e -> Morphism f e m
idMor extEm :: m
extEm sigma :: Sign f e
sigma = m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extEm Sign f e
sigma Sign f e
sigma

composeM :: Eq e => (Morphism f e m -> Morphism f e m -> Result m)
         -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM :: (Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM comp :: Morphism f e m -> Morphism f e m -> Result m
comp mor1 :: Morphism f e m
mor1 mor2 :: Morphism f e m
mor2 = do
  let sMap1 :: Sort_map
sMap1 = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor1
      src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor1
      tar :: Sign f e
tar = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor2
      oMap1 :: Op_map
oMap1 = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor1
      pMap1 :: Pred_map
pMap1 = Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor1
      sMap2 :: Sort_map
sMap2 = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor2
      oMap2 :: Op_map
oMap2 = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor2
      pMap2 :: Pred_map
pMap2 = Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor2
      sMap :: Sort_map
sMap = Sort_map -> Sort_map -> Sort_map -> Sort_map
forall a b. Ord a => Map a b -> Map a a -> Map a a -> Map a a
composeMap (Set Id -> Sort_map
forall a. Ord a => Set a -> Map a a
MapSet.setToMap (Set Id -> Sort_map) -> Set Id -> Sort_map
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
src) Sort_map
sMap1 Sort_map
sMap2
      oMap :: Op_map
oMap = if Op_map -> Bool
forall k a. Map k a -> Bool
Map.null Op_map
oMap2 then Op_map
oMap1 else
                 (Id -> OpType -> Op_map -> Op_map)
-> Op_map -> MapSet Id OpType -> Op_map
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey ( \ i :: Id
i ot :: OpType
ot ->
                       let (ni :: Id
ni, nt :: OpType
nt) = Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym Sort_map
sMap2 Op_map
oMap2
                             ((Id, OpType) -> (Id, OpType)) -> (Id, OpType) -> (Id, OpType)
forall a b. (a -> b) -> a -> b
$ Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym Sort_map
sMap1 Op_map
oMap1 (Id
i, OpType
ot)
                           k :: OpKind
k = OpType -> OpKind
opKind OpType
nt
                       in if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ni Bool -> Bool -> Bool
&& OpType -> OpKind
opKind OpType
ot OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
k then Op_map -> Op_map
forall a. a -> a
id else
                          (Id, OpType) -> (Id, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
i, OpType -> OpType
mkPartial OpType
ot) (Id
ni, OpKind
k))
                     Op_map
forall k a. Map k a
Map.empty (MapSet Id OpType -> Op_map) -> MapSet Id OpType -> Op_map
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
src
      pMap :: Pred_map
pMap = if Pred_map -> Bool
forall k a. Map k a -> Bool
Map.null Pred_map
pMap2 then Pred_map
pMap1 else
                 (Id -> PredType -> Pred_map -> Pred_map)
-> Pred_map -> MapSet Id PredType -> Pred_map
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey ( \ i :: Id
i pt :: PredType
pt ->
                       let ni :: Id
ni = (Id, PredType) -> Id
forall a b. (a, b) -> a
fst ((Id, PredType) -> Id) -> (Id, PredType) -> Id
forall a b. (a -> b) -> a -> b
$ Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym Sort_map
sMap2 Pred_map
pMap2
                             ((Id, PredType) -> (Id, PredType))
-> (Id, PredType) -> (Id, PredType)
forall a b. (a -> b) -> a -> b
$ Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym Sort_map
sMap1 Pred_map
pMap1 (Id
i, PredType
pt)
                       in if Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ni then Pred_map -> Pred_map
forall a. a -> a
id else (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
i, PredType
pt) Id
ni)
                      Pred_map
forall k a. Map k a
Map.empty (MapSet Id PredType -> Pred_map) -> MapSet Id PredType -> Pred_map
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
src
  m
extComp <- Morphism f e m -> Morphism f e m -> Result m
comp Morphism f e m
mor1 Morphism f e m
mor2
  let emb :: Morphism f e m
emb = m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extComp Sign f e
src Sign f e
tar
  Morphism f e m -> Result (Morphism f e m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism f e m -> Result (Morphism f e m))
-> Morphism f e m -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Morphism f e m
forall f e m. Morphism f e m -> Morphism f e m
cleanMorMaps Morphism f e m
emb
     { sort_map :: Sort_map
sort_map = Sort_map
sMap
     , op_map :: Op_map
op_map = Op_map
oMap
     , pred_map :: Pred_map
pred_map = Pred_map
pMap }

legalSign :: Sign f e -> Bool
legalSign :: Sign f e -> Bool
legalSign sigma :: Sign f e
sigma =
  (Id -> Bool) -> Set Id -> Bool
forall a. (a -> Bool) -> Set a -> Bool
MapSet.setAll Id -> Bool
legalSort (Map Id (Set Id) -> Set Id
forall b a. Ord b => Map a (Set b) -> Set b
MapSet.setElems (Map Id (Set Id) -> Set Id)
-> (Rel Id -> Map Id (Set Id)) -> Rel Id -> Set Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Map Id (Set Id)
forall a. Rel a -> Map a (Set a)
Rel.toMap (Rel Id -> Set Id) -> Rel Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sigma)
  Bool -> Bool -> Bool
&& (OpType -> Bool) -> MapSet Id OpType -> Bool
forall b a. Ord b => (b -> Bool) -> MapSet a b -> Bool
MapSet.all OpType -> Bool
legalOpType (Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sigma)
  Bool -> Bool -> Bool
&& (PredType -> Bool) -> MapSet Id PredType -> Bool
forall b a. Ord b => (b -> Bool) -> MapSet a b -> Bool
MapSet.all PredType -> Bool
legalPredType (Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sigma)
  where sorts :: Set Id
sorts = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sigma
        legalSort :: Id -> Bool
legalSort s :: Id
s = Id -> Set Id -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Id
s Set Id
sorts
        legalOpType :: OpType -> Bool
legalOpType t :: OpType
t = -- omitted for VSE Boolean: legalSort (opRes t)
                        (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
legalSort (OpType -> [Id]
opArgs OpType
t)
        legalPredType :: PredType -> Bool
legalPredType = (Id -> Bool) -> [Id] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Id -> Bool
legalSort ([Id] -> Bool) -> (PredType -> [Id]) -> PredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PredType -> [Id]
predArgs

-- | the image of a signature morphism
imageOfMorphism :: Morphism f e m -> Sign f e
imageOfMorphism :: Morphism f e m -> Sign f e
imageOfMorphism m :: Morphism f e m
m = (Morphism f e m -> e) -> Morphism f e m -> Sign f e
forall f e m. (Morphism f e m -> e) -> Morphism f e m -> Sign f e
imageOfMorphismAux (e -> Morphism f e m -> e
forall a b. a -> b -> a
const (e -> Morphism f e m -> e) -> e -> Morphism f e m -> e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo (Sign f e -> e) -> Sign f e -> e
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m) Morphism f e m
m

-- | the generalized image of a signature morphism
imageOfMorphismAux :: (Morphism f e m -> e) -> Morphism f e m -> Sign f e
imageOfMorphismAux :: (Morphism f e m -> e) -> Morphism f e m -> Sign f e
imageOfMorphismAux fE :: Morphism f e m -> e
fE m :: Morphism f e m
m =
  InducedSign f e m e -> InducedSign f e m (Sign f e)
forall f e m. InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux (\ _ _ _ _ _ -> Morphism f e m -> e
fE Morphism f e m
m)
         (Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m) (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m) (Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map Morphism f e m
m) (Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m)

type InducedSign f e m r =
  Sort_map -> Op_map -> Pred_map -> m -> Sign f e -> r

-- | the induced signature image of a signature morphism
inducedSignAux :: InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux :: InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux f :: InducedSign f e m e
f sm :: Sort_map
sm om :: Op_map
om pm :: Pred_map
pm em :: m
em src :: Sign f e
src =
  let ms :: Id -> Id
ms = Sort_map -> Id -> Id
mapSort Sort_map
sm
      msorts :: Set Id -> Set Id
msorts = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Id -> Id
ms
  in (e -> Sign f e
forall e f. e -> Sign f e
emptySign (e -> Sign f e) -> e -> Sign f e
forall a b. (a -> b) -> a -> b
$ InducedSign f e m e
f Sort_map
sm Op_map
om Pred_map
pm m
em Sign f e
src)
  { sortRel :: Rel Id
sortRel = Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel Id -> Rel Id) -> (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rel Id -> Rel Id
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel Id -> Rel Id) -> (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id -> Id) -> Rel Id -> Rel Id
forall a b. (Ord a, Ord b) => (a -> b) -> Rel a -> Rel b
Rel.map Id -> Id
ms (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
src
    -- sorts may fall together and need to be removed as trivial relation
  , emptySortSet :: Set Id
emptySortSet = Set Id -> Set Id
msorts (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
src
  , opMap :: MapSet Id OpType
opMap = Sort_map -> Op_map -> MapSet Id OpType -> MapSet Id OpType
inducedOpMap Sort_map
sm Op_map
om (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
src
  , assocOps :: MapSet Id OpType
assocOps = Sort_map -> Op_map -> MapSet Id OpType -> MapSet Id OpType
inducedOpMap Sort_map
sm Op_map
om (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
assocOps Sign f e
src
  , predMap :: MapSet Id PredType
predMap = Sort_map -> Pred_map -> MapSet Id PredType -> MapSet Id PredType
inducedPredMap Sort_map
sm Pred_map
pm (MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
src
  , annoMap :: AnnoMap
annoMap = Sort_map -> Op_map -> Pred_map -> AnnoMap -> AnnoMap
inducedAnnoMap Sort_map
sm Op_map
om Pred_map
pm (AnnoMap -> AnnoMap) -> AnnoMap -> AnnoMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> AnnoMap
forall f e. Sign f e -> AnnoMap
annoMap Sign f e
src
  }

inducedOpMap :: Sort_map -> Op_map -> OpMap -> OpMap
inducedOpMap :: Sort_map -> Op_map -> MapSet Id OpType -> MapSet Id OpType
inducedOpMap sm :: Sort_map
sm fm :: Op_map
fm = (Id -> OpType -> MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType -> MapSet Id OpType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  (\ i :: Id
i ot :: OpType
ot -> let (j :: Id
j, nt :: OpType
nt) = Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym Sort_map
sm Op_map
fm (Id
i, OpType
ot)
     in Id -> OpType -> MapSet Id OpType -> MapSet Id OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
j OpType
nt) MapSet Id OpType
forall a b. MapSet a b
MapSet.empty

inducedPredMap :: Sort_map -> Pred_map -> PredMap -> PredMap
inducedPredMap :: Sort_map -> Pred_map -> MapSet Id PredType -> MapSet Id PredType
inducedPredMap sm :: Sort_map
sm pm :: Pred_map
pm = (Id -> PredType -> MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  ( \ i :: Id
i pt :: PredType
pt -> let (j :: Id
j, nt :: PredType
nt) = Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym Sort_map
sm Pred_map
pm (Id
i, PredType
pt)
      in Id -> PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
j PredType
nt) MapSet Id PredType
forall a b. MapSet a b
MapSet.empty

inducedAnnoMap :: Sort_map -> Op_map -> Pred_map -> AnnoMap -> AnnoMap
inducedAnnoMap :: Sort_map -> Op_map -> Pred_map -> AnnoMap -> AnnoMap
inducedAnnoMap sm :: Sort_map
sm om :: Op_map
om pm :: Pred_map
pm = (Symbol -> Annotation -> AnnoMap -> AnnoMap)
-> AnnoMap -> AnnoMap -> AnnoMap
forall a b c. (a -> b -> c -> c) -> c -> MapSet a b -> c
MapSet.foldWithKey
  ( \ sy :: Symbol
sy s :: Annotation
s -> Symbol -> Annotation -> AnnoMap -> AnnoMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (Sort_map -> Op_map -> Pred_map -> Symbol -> Symbol
mapSymbol Sort_map
sm Op_map
om Pred_map
pm Symbol
sy) Annotation
s) AnnoMap
forall a b. MapSet a b
MapSet.empty

mapSymbol :: Sort_map -> Op_map -> Pred_map -> Symbol -> Symbol
mapSymbol :: Sort_map -> Op_map -> Pred_map -> Symbol -> Symbol
mapSymbol sm :: Sort_map
sm om :: Op_map
om pm :: Pred_map
pm (Symbol i :: Id
i ty :: SymbType
ty) = case SymbType
ty of
  SortAsItemType -> Id -> SymbType -> Symbol
Symbol (Sort_map -> Id -> Id
mapSort Sort_map
sm Id
i) SymbType
SortAsItemType
  SubsortAsItemType j :: Id
j ->
    Id -> SymbType -> Symbol
Symbol (Sort_map -> Id -> Id
mapSort Sort_map
sm Id
i) (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ Id -> SymbType
SubsortAsItemType (Id -> SymbType) -> Id -> SymbType
forall a b. (a -> b) -> a -> b
$ Sort_map -> Id -> Id
mapSort Sort_map
sm Id
j
  OpAsItemType ot :: OpType
ot -> let (j :: Id
j, nt :: OpType
nt) = Sort_map -> Op_map -> (Id, OpType) -> (Id, OpType)
mapOpSym Sort_map
sm Op_map
om (Id
i, OpType
ot) in
    Id -> SymbType -> Symbol
Symbol Id
j (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> SymbType
OpAsItemType OpType
nt
  PredAsItemType pt :: PredType
pt -> let (j :: Id
j, nt :: PredType
nt) = Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)
mapPredSym Sort_map
sm Pred_map
pm (Id
i, PredType
pt) in
    Id -> SymbType -> Symbol
Symbol Id
j (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType PredType
nt

legalMor :: MorphismExtension e m => Morphism f e m -> Result ()
legalMor :: Morphism f e m -> Result ()
legalMor mor :: Morphism f e m
mor =
  let s1 :: Sign f e
s1 = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor
      s2 :: Sign f e
s2 = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor
      sm :: Sort_map
sm = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor
      msorts :: Set Id -> Set Id
msorts = (Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Id -> Id) -> Set Id -> Set Id) -> (Id -> Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sort_map -> Id -> Id
mapSort Sort_map
sm
  in if Sign f e -> Bool
forall f e. Sign f e -> Bool
legalSign Sign f e
s1
  Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Set Id -> Set Id
msorts (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
s1) (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
s2)
  Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Set Id -> Set Id
msorts (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
s1) (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
s2)
  Bool -> Bool -> Bool
&& MapSet Id OpType -> MapSet Id OpType -> Bool
isSubOpMap (Sort_map -> Op_map -> MapSet Id OpType -> MapSet Id OpType
inducedOpMap Sort_map
sm (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor) (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s1) (Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s2)
  Bool -> Bool -> Bool
&& MapSet Id PredType -> MapSet Id PredType -> Bool
isSubMap (Sort_map -> Pred_map -> MapSet Id PredType -> MapSet Id PredType
inducedPredMap Sort_map
sm (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor) (MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s1) (Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s2)
  Bool -> Bool -> Bool
&& Sign f e -> Bool
forall f e. Sign f e -> Bool
legalSign Sign f e
s2
  then Morphism f e m -> Result ()
forall e m f. MorphismExtension e m => Morphism f e m -> Result ()
legalMorphismExtension Morphism f e m
mor else String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal CASL morphism"

isInclOpMap :: Op_map -> Bool
isInclOpMap :: Op_map -> Bool
isInclOpMap = (((Id, OpType), (Id, OpKind)) -> Bool)
-> [((Id, OpType), (Id, OpKind))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ ((i :: Id
i, _), (j :: Id
j, _)) -> Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
j) ([((Id, OpType), (Id, OpKind))] -> Bool)
-> (Op_map -> [((Id, OpType), (Id, OpKind))]) -> Op_map -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Op_map -> [((Id, OpType), (Id, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList

idOrInclMorphism :: Morphism f e m -> Morphism f e m
idOrInclMorphism :: Morphism f e m -> Morphism f e m
idOrInclMorphism m :: Morphism f e m
m =
  let src :: MapSet Id OpType
src = Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap (Sign f e -> MapSet Id OpType) -> Sign f e -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
      tar :: MapSet Id OpType
tar = Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap (Sign f e -> MapSet Id OpType) -> Sign f e -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
m
  in if MapSet Id OpType -> MapSet Id OpType -> Bool
isSubOpMap MapSet Id OpType
tar MapSet Id OpType
src then Morphism f e m
m
     else let diffOpMap :: Map Id (Set OpType)
diffOpMap = MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType -> Map Id (Set OpType)
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> MapSet Id OpType -> MapSet Id OpType
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference MapSet Id OpType
src MapSet Id OpType
tar in
          Morphism f e m
m { op_map :: Op_map
op_map = [((Id, OpType), (Id, OpKind))] -> Op_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((Id, OpType), (Id, OpKind))] -> Op_map)
-> [((Id, OpType), (Id, OpKind))] -> Op_map
forall a b. (a -> b) -> a -> b
$ ((Id, Set OpType) -> [((Id, OpType), (Id, OpKind))])
-> [(Id, Set OpType)] -> [((Id, OpType), (Id, OpKind))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (i :: Id
i, s :: Set OpType
s) ->
              (OpType -> ((Id, OpType), (Id, OpKind)))
-> [OpType] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: OpType
t -> ((Id
i, OpType
t), (Id
i, OpKind
Total)))
                 ([OpType] -> [((Id, OpType), (Id, OpKind))])
-> [OpType] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> a -> b
$ Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
s) ([(Id, Set OpType)] -> [((Id, OpType), (Id, OpKind))])
-> [(Id, Set OpType)] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> a -> b
$ Map Id (Set OpType) -> [(Id, Set OpType)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Id (Set OpType)
diffOpMap }

sigInclusion :: m -- ^ computed extended morphism
             -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion :: m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion extEm :: m
extEm sigma1 :: Sign f e
sigma1 =
     Morphism f e m -> Result (Morphism f e m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism f e m -> Result (Morphism f e m))
-> (Sign f e -> Morphism f e m)
-> Sign f e
-> Result (Morphism f e m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> Morphism f e m
forall f e m. Morphism f e m -> Morphism f e m
idOrInclMorphism (Morphism f e m -> Morphism f e m)
-> (Sign f e -> Morphism f e m) -> Sign f e -> Morphism f e m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extEm Sign f e
sigma1

addSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM :: (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM f :: e -> e -> m e
f a :: Sign f e
a b :: Sign f e
b = do
  e
e <- e -> e -> m e
f (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (e -> m e) -> e -> m e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b
  Sign f e -> m (Sign f e)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign f e -> m (Sign f e)) -> Sign f e -> m (Sign f e)
forall a b. (a -> b) -> a -> b
$ (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig ((e -> e) -> e -> e -> e
forall a b. a -> b -> a
const ((e -> e) -> e -> e -> e) -> (e -> e) -> e -> e -> e
forall a b. (a -> b) -> a -> b
$ e -> e -> e
forall a b. a -> b -> a
const e
e) Sign f e
a Sign f e
b

plainMorphismUnion :: (e -> e -> e) -- ^ join signature extensions
  -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion :: (e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion = (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
forall f e m.
(Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnion Morphism f e m -> Morphism f e m -> Result m
forall b f e m. b -> Morphism f e m -> Result m
retExtMap

retExtMap :: b -> Morphism f e m -> Result m
retExtMap :: b -> Morphism f e m -> Result m
retExtMap = (Morphism f e m -> Result m) -> b -> Morphism f e m -> Result m
forall a b. a -> b -> a
const ((Morphism f e m -> Result m) -> b -> Morphism f e m -> Result m)
-> (Morphism f e m -> Result m) -> b -> Morphism f e m -> Result m
forall a b. (a -> b) -> a -> b
$ m -> Result m
forall (m :: * -> *) a. Monad m => a -> m a
return (m -> Result m)
-> (Morphism f e m -> m) -> Morphism f e m -> Result m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map

morphismUnion :: (Morphism f e m -> Morphism f e m -> Result m)
  -- ^ join morphism extensions
  -> (e -> e -> e) -- ^ join signature extensions
  -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
morphismUnion :: (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnion uniteM :: Morphism f e m -> Morphism f e m -> Result m
uniteM addSigExt :: e -> e -> e
addSigExt =
    (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Result e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
forall f e m.
(Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Result e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnionM Morphism f e m -> Morphism f e m -> Result m
uniteM (\ e :: e
e -> e -> Result e
forall (m :: * -> *) a. Monad m => a -> m a
return (e -> Result e) -> (e -> e) -> e -> Result e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> e -> e
addSigExt e
e)

morphismUnionM :: (Morphism f e m -> Morphism f e m -> Result m)
 -- ^ join morphism extensions
 -> (e -> e -> Result e) -- ^ join signature extensions
 -> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
-- consider identity mappings but filter them eventually
morphismUnionM :: (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Result e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnionM uniteM :: Morphism f e m -> Morphism f e m -> Result m
uniteM addSigExt :: e -> e -> Result e
addSigExt mor1 :: Morphism f e m
mor1 mor2 :: Morphism f e m
mor2 =
  let smap1 :: Sort_map
smap1 = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor1
      smap2 :: Sort_map
smap2 = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
mor2
      s1 :: Sign f e
s1 = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor1
      s2 :: Sign f e
s2 = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor2
      us1 :: Set Id
us1 = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
s1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sort_map -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Sort_map
smap1
      us2 :: Set Id
us2 = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
s2) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sort_map -> Set Id
forall k a. Map k a -> Set k
Map.keysSet Sort_map
smap2
      omap1 :: Op_map
omap1 = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor1
      omap2 :: Op_map
omap2 = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor2
      uo1 :: MapSet Id OpType
uo1 = ((Id, OpType) -> MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> [(Id, OpType)] -> MapSet Id OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, OpType) -> MapSet Id OpType -> MapSet Id OpType
delOp (Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s1) ([(Id, OpType)] -> MapSet Id OpType)
-> [(Id, OpType)] -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Op_map -> [(Id, OpType)]
forall k a. Map k a -> [k]
Map.keys Op_map
omap1
      uo2 :: MapSet Id OpType
uo2 = ((Id, OpType) -> MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> [(Id, OpType)] -> MapSet Id OpType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, OpType) -> MapSet Id OpType -> MapSet Id OpType
delOp (Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s2) ([(Id, OpType)] -> MapSet Id OpType)
-> [(Id, OpType)] -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Op_map -> [(Id, OpType)]
forall k a. Map k a -> [k]
Map.keys Op_map
omap2
      delOp :: (Id, OpType) -> MapSet Id OpType -> MapSet Id OpType
delOp (n :: Id
n, ot :: OpType
ot) m :: MapSet Id OpType
m = MapSet Id OpType -> MapSet Id OpType -> MapSet Id OpType
diffOpMapSet MapSet Id OpType
m (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ [(Id, [OpType])] -> MapSet Id OpType
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList [(Id
n, [OpType -> OpType
mkTotal OpType
ot])]
      uo :: MapSet Id OpType
uo = MapSet Id OpType -> MapSet Id OpType -> MapSet Id OpType
addOpMapSet MapSet Id OpType
uo1 MapSet Id OpType
uo2
      pmap1 :: Pred_map
pmap1 = Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor1
      pmap2 :: Pred_map
pmap2 = Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
mor2
      up1 :: MapSet Id PredType
up1 = ((Id, PredType) -> MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> [(Id, PredType)] -> MapSet Id PredType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, PredType) -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delPred (Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s1) ([(Id, PredType)] -> MapSet Id PredType)
-> [(Id, PredType)] -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ Pred_map -> [(Id, PredType)]
forall k a. Map k a -> [k]
Map.keys Pred_map
pmap1
      up2 :: MapSet Id PredType
up2 = ((Id, PredType) -> MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> [(Id, PredType)] -> MapSet Id PredType
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Id, PredType) -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => (a, b) -> MapSet a b -> MapSet a b
delPred (Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s2) ([(Id, PredType)] -> MapSet Id PredType)
-> [(Id, PredType)] -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ Pred_map -> [(Id, PredType)]
forall k a. Map k a -> [k]
Map.keys Pred_map
pmap2
      up :: MapSet Id PredType
up = MapSet Id PredType -> MapSet Id PredType -> MapSet Id PredType
addMapSet MapSet Id PredType
up1 MapSet Id PredType
up2
      delPred :: (a, b) -> MapSet a b -> MapSet a b
delPred (n :: a
n, pt :: b
pt) = a -> b -> MapSet a b -> MapSet a b
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.delete a
n b
pt
      (sds :: [Diagnosis]
sds, smap :: Sort_map
smap) = ((Id, Id) -> ([Diagnosis], Sort_map) -> ([Diagnosis], Sort_map))
-> ([Diagnosis], Sort_map) -> [(Id, Id)] -> ([Diagnosis], Sort_map)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (i :: Id
i, j :: Id
j) (ds :: [Diagnosis]
ds, m :: Sort_map
m) -> case Id -> Sort_map -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Id
i Sort_map
m of
          Nothing -> ([Diagnosis]
ds, Id -> Id -> Sort_map -> Sort_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
i Id
j Sort_map
m)
          Just k :: Id
k -> if Id
j Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
k then ([Diagnosis]
ds, Sort_map
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of sort " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
i " to "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
j " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
k "")
               Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, Sort_map
m)) ([], Sort_map
smap1)
          (Sort_map -> [(Id, Id)]
forall k a. Map k a -> [(k, a)]
Map.toList Sort_map
smap2 [(Id, Id)] -> [(Id, Id)] -> [(Id, Id)]
forall a. [a] -> [a] -> [a]
++ (Id -> (Id, Id)) -> [Id] -> [(Id, Id)]
forall a b. (a -> b) -> [a] -> [b]
map (\ a :: Id
a -> (Id
a, Id
a))
                      (Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set Id
us1 Set Id
us2))
      (ods :: [Diagnosis]
ods, omap :: Op_map
omap) = (((Id, OpType), (Id, OpKind))
 -> ([Diagnosis], Op_map) -> ([Diagnosis], Op_map))
-> ([Diagnosis], Op_map)
-> [((Id, OpType), (Id, OpKind))]
-> ([Diagnosis], Op_map)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (isc :: (Id, OpType)
isc@(i :: Id
i, ot :: OpType
ot), jsc :: (Id, OpKind)
jsc@(j :: Id
j, t :: OpKind
t)) (ds :: [Diagnosis]
ds, m :: Op_map
m) ->
          case (Id, OpType) -> Op_map -> Maybe (Id, OpKind)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id, OpType)
isc Op_map
m of
          Nothing -> ([Diagnosis]
ds, (Id, OpType) -> (Id, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, OpType)
isc (Id, OpKind)
jsc Op_map
m)
          Just (k :: Id
k, p :: OpKind
p) -> if Id
j Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
k then if OpKind
p OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
t then ([Diagnosis]
ds, Op_map
m)
                            else ([Diagnosis]
ds, (Id, OpType) -> (Id, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, OpType)
isc (Id
j, OpKind
Total) Op_map
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of op " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
i ":"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ OpType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc (OpKind -> OpType -> OpType
setOpKind OpKind
t OpType
ot) " to "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
j " and " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
k "") Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, Op_map
m))
           ([Diagnosis]
sds, Op_map
omap1) (Op_map -> [((Id, OpType), (Id, OpKind))]
forall k a. Map k a -> [(k, a)]
Map.toList Op_map
omap2 [((Id, OpType), (Id, OpKind))]
-> [((Id, OpType), (Id, OpKind))] -> [((Id, OpType), (Id, OpKind))]
forall a. [a] -> [a] -> [a]
++ ((Id, OpType) -> ((Id, OpType), (Id, OpKind)))
-> [(Id, OpType)] -> [((Id, OpType), (Id, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map
              ( \ (a :: Id
a, ot :: OpType
ot) -> ((Id
a, OpType -> OpType
mkPartial OpType
ot), (Id
a, OpType -> OpKind
opKind OpType
ot)))
              (MapSet Id OpType -> [(Id, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList MapSet Id OpType
uo))
      (pds :: [Diagnosis]
pds, pmap :: Pred_map
pmap) = (((Id, PredType), Id)
 -> ([Diagnosis], Pred_map) -> ([Diagnosis], Pred_map))
-> ([Diagnosis], Pred_map)
-> [((Id, PredType), Id)]
-> ([Diagnosis], Pred_map)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ( \ (isc :: (Id, PredType)
isc@(i :: Id
i, pt :: PredType
pt), j :: Id
j) (ds :: [Diagnosis]
ds, m :: Pred_map
m) ->
          case (Id, PredType) -> Pred_map -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id, PredType)
isc Pred_map
m of
          Nothing -> ([Diagnosis]
ds, (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id, PredType)
isc Id
j Pred_map
m)
          Just k :: Id
k -> if Id
j Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
k then ([Diagnosis]
ds, Pred_map
m) else
              (DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Error
               ("incompatible mapping of pred " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
i ":"
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ PredType -> ShowS
forall a. Pretty a => a -> ShowS
showDoc PredType
pt " to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
j " and "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> ShowS
showId Id
k "") Range
nullRange Diagnosis -> [Diagnosis] -> [Diagnosis]
forall a. a -> [a] -> [a]
: [Diagnosis]
ds, Pred_map
m)) ([Diagnosis]
ods, Pred_map
pmap1)
          (Pred_map -> [((Id, PredType), Id)]
forall k a. Map k a -> [(k, a)]
Map.toList Pred_map
pmap2 [((Id, PredType), Id)]
-> [((Id, PredType), Id)] -> [((Id, PredType), Id)]
forall a. [a] -> [a] -> [a]
++ ((Id, PredType) -> ((Id, PredType), Id))
-> [(Id, PredType)] -> [((Id, PredType), Id)]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (a :: Id
a, pt :: PredType
pt) -> ((Id
a, PredType
pt), Id
a))
                  (MapSet Id PredType -> [(Id, PredType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList MapSet Id PredType
up))
  in if [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Diagnosis]
pds then do
    Sign f e
s3 <- (e -> e -> Result e) -> Sign f e -> Sign f e -> Result (Sign f e)
forall (m :: * -> *) e f.
Monad m =>
(e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM e -> e -> Result e
addSigExt Sign f e
s1 Sign f e
s2
    Sign f e
s4 <- (e -> e -> Result e) -> Sign f e -> Sign f e -> Result (Sign f e)
forall (m :: * -> *) e f.
Monad m =>
(e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM e -> e -> Result e
addSigExt (Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor1) (Sign f e -> Result (Sign f e)) -> Sign f e -> Result (Sign f e)
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor2
    m
extM <- Morphism f e m -> Morphism f e m -> Result m
uniteM Morphism f e m
mor1 Morphism f e m
mor2
    Morphism f e m -> Result (Morphism f e m)
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism f e m -> Result (Morphism f e m))
-> Morphism f e m -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Morphism f e m
forall f e m. Morphism f e m -> Morphism f e m
cleanMorMaps
      (m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
extM Sign f e
s3 Sign f e
s4)
      { sort_map :: Sort_map
sort_map = Sort_map
smap
      , op_map :: Op_map
op_map = Op_map
omap
      , pred_map :: Pred_map
pred_map = Pred_map
pmap }
    else [Diagnosis] -> Maybe (Morphism f e m) -> Result (Morphism f e m)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [Diagnosis]
pds Maybe (Morphism f e m)
forall a. Maybe a
Nothing

cleanMorMaps :: Morphism f e m -> Morphism f e m
cleanMorMaps :: Morphism f e m -> Morphism f e m
cleanMorMaps m :: Morphism f e m
m = Morphism f e m
m
  { sort_map :: Sort_map
sort_map = (Id -> Id -> Bool) -> Sort_map -> Sort_map
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Sort_map -> Sort_map) -> Sort_map -> Sort_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m
  , op_map :: Op_map
op_map = ((Id, OpType) -> (Id, OpKind) -> Bool) -> Op_map -> Op_map
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey
        (\ (i :: Id
i, ot :: OpType
ot) (j :: Id
j, k :: OpKind
k) -> Id
i Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
/= Id
j Bool -> Bool -> Bool
|| OpKind
k OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpKind
Total Bool -> Bool -> Bool
&& OpType -> Set OpType -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member OpType
ot
         (Id -> MapSet Id OpType -> Set OpType
forall a b. Ord a => a -> MapSet a b -> Set b
MapSet.lookup Id
i (MapSet Id OpType -> Set OpType) -> MapSet Id OpType -> Set OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap (Sign f e -> MapSet Id OpType) -> Sign f e -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m)) (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m
  , pred_map :: Pred_map
pred_map = ((Id, PredType) -> Id -> Bool) -> Pred_map -> Pred_map
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Id -> Id -> Bool)
-> ((Id, PredType) -> Id) -> (Id, PredType) -> Id -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Id, PredType) -> Id
forall a b. (a, b) -> a
fst) (Pred_map -> Pred_map) -> Pred_map -> Pred_map
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m }

isSortInjective :: Morphism f e m -> Bool
isSortInjective :: Morphism f e m -> Bool
isSortInjective m :: Morphism f e m
m =
    let ss :: Set Id
ss = Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet (Sign f e -> Set Id) -> Sign f e -> Set Id
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
    in Set Id -> Int
forall a. Set a -> Int
Set.size Set Id
ss Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Set Id -> Int
forall a. Set a -> Int
Set.size ((Id -> Id) -> Set Id -> Set Id
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Sort_map -> Id -> Id
mapSort (Sort_map -> Id -> Id) -> Sort_map -> Id -> Id
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m) Set Id
ss)

sumSize :: MapSet.MapSet a b -> Int
sumSize :: MapSet a b -> Int
sumSize = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> (MapSet a b -> [Int]) -> MapSet a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set b -> Int) -> [Set b] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Set b -> Int
forall a. Set a -> Int
Set.size ([Set b] -> [Int])
-> (MapSet a b -> [Set b]) -> MapSet a b -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a (Set b) -> [Set b]
forall k a. Map k a -> [a]
Map.elems (Map a (Set b) -> [Set b])
-> (MapSet a b -> Map a (Set b)) -> MapSet a b -> [Set b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet a b -> Map a (Set b)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

-- morphism extension m is not considered here
isInjective :: Morphism f e m -> Bool
isInjective :: Morphism f e m -> Bool
isInjective m :: Morphism f e m
m = Morphism f e m -> Bool
forall f e m. Morphism f e m -> Bool
isSortInjective Morphism f e m
m Bool -> Bool -> Bool
&& let
    src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
m
    sm :: Sort_map
sm = Morphism f e m -> Sort_map
forall f e m. Morphism f e m -> Sort_map
sort_map Morphism f e m
m
    os :: MapSet Id OpType
os = Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
src
    ps :: MapSet Id PredType
ps = Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
src
    in MapSet Id OpType -> Int
forall a b. MapSet a b -> Int
sumSize MapSet Id OpType
os Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== MapSet Id OpType -> Int
forall a b. MapSet a b -> Int
sumSize (Sort_map -> Op_map -> MapSet Id OpType -> MapSet Id OpType
inducedOpMap Sort_map
sm (Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
m) MapSet Id OpType
os)
       Bool -> Bool -> Bool
&& MapSet Id PredType -> Int
forall a b. MapSet a b -> Int
sumSize MapSet Id PredType
ps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== MapSet Id PredType -> Int
forall a b. MapSet a b -> Int
sumSize (Sort_map -> Pred_map -> MapSet Id PredType -> MapSet Id PredType
inducedPredMap Sort_map
sm (Morphism f e m -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map Morphism f e m
m) MapSet Id PredType
ps)

instance Pretty RawSymbol where
  pretty :: RawSymbol -> Doc
pretty rsym :: RawSymbol
rsym = case RawSymbol
rsym of
    ASymbol sy :: Symbol
sy -> Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
sy
    AKindedSymb k :: SYMB_KIND
k i :: Id
i -> SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty SYMB_KIND
k Doc -> Doc -> Doc
<+> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i

printMorphism :: (e -> e -> Bool) -> (m -> Bool) -> (e -> Doc)
  -> (Morphism f e m -> Doc) -> Morphism f e m -> Doc
printMorphism :: (e -> e -> Bool)
-> (m -> Bool)
-> (e -> Doc)
-> (Morphism f e m -> Doc)
-> Morphism f e m
-> Doc
printMorphism isSubSigExt :: e -> e -> Bool
isSubSigExt isInclMorExt :: m -> Bool
isInclMorExt fE :: e -> Doc
fE fM :: Morphism f e m -> Doc
fM mor :: Morphism f e m
mor =
    let src :: Sign f e
src = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
msource Morphism f e m
mor
        tar :: Sign f e
tar = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor
        ops :: Op_map
ops = Morphism f e m -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map Morphism f e m
mor
        prSig :: Sign f e -> Doc
prSig s :: Sign f e
s = Doc -> Doc
specBraces (Doc
space Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> (e -> Doc) -> Sign f e -> Doc
forall e f. (e -> Doc) -> Sign f e -> Doc
printSign e -> Doc
fE Sign f e
s)
        srcD :: Doc
srcD = Sign f e -> Doc
forall f. Sign f e -> Doc
prSig Sign f e
src
    in [Doc] -> Doc
fsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if (m -> Bool) -> Morphism f e m -> Bool
forall m f e. (m -> Bool) -> Morphism f e m -> Bool
isInclusionMorphism m -> Bool
isInclMorExt Morphism f e m
mor then
              if (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig e -> e -> Bool
isSubSigExt Sign f e
tar Sign f e
src then
                  [String -> Doc
text "identity morphism over", Doc
srcD]
              else
                  [String -> Doc
text "inclusion morphism of", Doc
srcD
                 , if Op_map -> Bool
forall k a. Map k a -> Bool
Map.null Op_map
ops then Doc
empty
                   else [Doc] -> Doc
fsep
                   [String -> Doc
text "by totalizing",
                    SymbolSet -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbolSet -> Doc) -> SymbolSet -> Doc
forall a b. (a -> b) -> a -> b
$ ((Id, OpType) -> Symbol) -> Set (Id, OpType) -> SymbolSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((Id -> OpType -> Symbol) -> (Id, OpType) -> Symbol
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Id -> OpType -> Symbol
idToOpSymbol) (Set (Id, OpType) -> SymbolSet) -> Set (Id, OpType) -> SymbolSet
forall a b. (a -> b) -> a -> b
$ Op_map -> Set (Id, OpType)
forall k a. Map k a -> Set k
Map.keysSet Op_map
ops]]
    else
      [ Doc -> Doc
braces (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ (Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> SymbolMap -> Doc
forall a b.
(Pretty a, Pretty b) =>
(Doc -> Doc)
-> ([Doc] -> Doc) -> (Doc -> Doc -> Doc) -> Map a b -> Doc
printMap Doc -> Doc
forall a. a -> a
id [Doc] -> Doc
sepByCommas Doc -> Doc -> Doc
pairElems
          (Bool -> Morphism f e m -> SymbolMap
forall f e m. Bool -> Morphism f e m -> SymbolMap
morphismToSymbMapAux Bool
True Morphism f e m
mor) Doc -> Doc -> Doc
$+$ Morphism f e m -> Doc
fM Morphism f e m
mor
      , Doc
colon Doc -> Doc -> Doc
<+> Doc
srcD, Doc
mapsto Doc -> Doc -> Doc
<+> Sign f e -> Doc
forall f. Sign f e -> Doc
prSig Sign f e
tar ]

instance (SignExtension e, Pretty e, Show f, MorphismExtension e m)
  => Pretty (Morphism f e m) where
       pretty :: Morphism f e m -> Doc
pretty = (e -> e -> Bool)
-> (m -> Bool)
-> (e -> Doc)
-> (Morphism f e m -> Doc)
-> Morphism f e m
-> Doc
forall e m f.
(e -> e -> Bool)
-> (m -> Bool)
-> (e -> Doc)
-> (Morphism f e m -> Doc)
-> Morphism f e m
-> Doc
printMorphism e -> e -> Bool
forall e. SignExtension e => e -> e -> Bool
isSubSignExtension m -> Bool
forall e m. MorphismExtension e m => m -> Bool
isInclusionMorphismExtension
         e -> Doc
forall a. Pretty a => a -> Doc
pretty Morphism f e m -> Doc
forall e m f. MorphismExtension e m => Morphism f e m -> Doc
prettyMorphismExtension