{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Maude/Morphism.hs
Description :  Maude Morphisms
Copyright   :  (c) Martin Kuehl, Uni Bremen 2008-2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  mkhl@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Definition of morphisms for Maude.
-}

module Maude.Morphism (
    -- * Types

    -- ** The Morphism type
    Morphism (..),
    -- ** Auxiliary type
    SortMap,
    KindMap,
    OpMap,
    -- * Construction
    fromSignRenamings,
    fromSignsRenamings,
    empty,
    identity,
    inclusion,
    -- * Combination
    inverse,
    union,
    compose,
    -- * Testing
    isInclusion,
    isLegal,
    -- * Conversion
    symbolMap,
    -- * Modification
    setTarget,
    qualifySorts,
    applyRenamings,
    extendWithSortRenaming,
    -- * Application
    translateSentence,
    translateSorts,
) where

import Maude.AS_Maude
import Maude.Symbol
import Maude.Meta
import Maude.Util
import Maude.Printing ()

import Maude.Sign (Sign, kindRel, KindRel)
import Maude.Sentence (Sentence)
import qualified Maude.Sign as Sign

import Data.Data
import Data.List (partition)
import Data.Maybe (fromJust)
import qualified Data.Set as Set
import qualified Data.Map as Map

import Common.Result (Result)

import Common.Doc hiding (empty)
import Common.DocUtils (Pretty (..))

import Control.Monad (unless)
import qualified Control.Monad.Fail as Fail

-- * Types

-- ** Auxiliary types

type SortMap = SymbolMap
type KindMap = SymbolMap
type OpMap = SymbolMap
type LabelMap = SymbolMap

-- ** The Morphism type

data Morphism = Morphism {
        Morphism -> Sign
source :: Sign,
        Morphism -> Sign
target :: Sign,
        Morphism -> SortMap
sortMap :: SortMap,
        Morphism -> SortMap
kindMap :: KindMap,
        Morphism -> SortMap
opMap :: OpMap,
        Morphism -> SortMap
labelMap :: LabelMap
    } deriving (Int -> Morphism -> ShowS
[Morphism] -> ShowS
Morphism -> String
(Int -> Morphism -> ShowS)
-> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Morphism] -> ShowS
$cshowList :: [Morphism] -> ShowS
show :: Morphism -> String
$cshow :: Morphism -> String
showsPrec :: Int -> Morphism -> ShowS
$cshowsPrec :: Int -> Morphism -> ShowS
Show, Eq Morphism
Eq Morphism =>
(Morphism -> Morphism -> Ordering)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Morphism)
-> (Morphism -> Morphism -> Morphism)
-> Ord Morphism
Morphism -> Morphism -> Bool
Morphism -> Morphism -> Ordering
Morphism -> Morphism -> Morphism
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 :: Morphism -> Morphism -> Morphism
$cmin :: Morphism -> Morphism -> Morphism
max :: Morphism -> Morphism -> Morphism
$cmax :: Morphism -> Morphism -> Morphism
>= :: Morphism -> Morphism -> Bool
$c>= :: Morphism -> Morphism -> Bool
> :: Morphism -> Morphism -> Bool
$c> :: Morphism -> Morphism -> Bool
<= :: Morphism -> Morphism -> Bool
$c<= :: Morphism -> Morphism -> Bool
< :: Morphism -> Morphism -> Bool
$c< :: Morphism -> Morphism -> Bool
compare :: Morphism -> Morphism -> Ordering
$ccompare :: Morphism -> Morphism -> Ordering
$cp1Ord :: Eq Morphism
Ord, Morphism -> Morphism -> Bool
(Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool) -> Eq Morphism
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Morphism -> Morphism -> Bool
$c/= :: Morphism -> Morphism -> Bool
== :: Morphism -> Morphism -> Bool
$c== :: Morphism -> Morphism -> Bool
Eq, Typeable)

-- ** 'Morphism' instances

instance Pretty Morphism where
    pretty :: Morphism -> Doc
pretty mor :: Morphism
mor = let
        pr'pair :: Doc -> a -> a -> Doc
pr'pair txt :: Doc
txt left :: a
left right :: a
right = [Doc] -> Doc
hsep
            [Doc
txt, a -> Doc
forall a. Pretty a => a -> Doc
pretty a
left, String -> Doc
text "to", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
right]
        pr'ops :: a -> a -> Doc
pr'ops src :: a
src tgt :: a
tgt = Doc -> a -> Qid -> Doc
forall a a. (Pretty a, Pretty a) => Doc -> a -> a -> Doc
pr'pair (String -> Doc
text "op") a
src (a -> Qid
forall a. HasName a => a -> Qid
getName a
tgt)
        pr'map :: (a -> b -> Doc) -> Map a b -> Doc
pr'map fun :: a -> b -> Doc
fun = [Doc] -> Doc
vcat ([Doc] -> Doc) -> (Map a b -> [Doc]) -> Map a b -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> Doc) -> [(a, b)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> b -> Doc) -> (a, b) -> Doc
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> Doc
fun) ([(a, b)] -> [Doc]) -> (Map a b -> [(a, b)]) -> Map a b -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList
        smap :: Doc
smap = (Symbol -> Symbol -> Doc) -> SortMap -> Doc
forall a b. (a -> b -> Doc) -> Map a b -> Doc
pr'map (Doc -> Symbol -> Symbol -> Doc
forall a a. (Pretty a, Pretty a) => Doc -> a -> a -> Doc
pr'pair (Doc -> Symbol -> Symbol -> Doc) -> Doc -> Symbol -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "sort") (SortMap -> Doc) -> SortMap -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
sortMap Morphism
mor
        kmap :: Doc
kmap = (Symbol -> Symbol -> Doc) -> SortMap -> Doc
forall a b. (a -> b -> Doc) -> Map a b -> Doc
pr'map (Doc -> Symbol -> Symbol -> Doc
forall a a. (Pretty a, Pretty a) => Doc -> a -> a -> Doc
pr'pair (Doc -> Symbol -> Symbol -> Doc) -> Doc -> Symbol -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "kind") (SortMap -> Doc) -> SortMap -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
kindMap Morphism
mor
        omap :: Doc
omap = (Symbol -> Symbol -> Doc) -> SortMap -> Doc
forall a b. (a -> b -> Doc) -> Map a b -> Doc
pr'map Symbol -> Symbol -> Doc
forall a a. (Pretty a, HasName a) => a -> a -> Doc
pr'ops (SortMap -> Doc) -> SortMap -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
opMap Morphism
mor
        lmap :: Doc
lmap = (Symbol -> Symbol -> Doc) -> SortMap -> Doc
forall a b. (a -> b -> Doc) -> Map a b -> Doc
pr'map (Doc -> Symbol -> Symbol -> Doc
forall a a. (Pretty a, Pretty a) => Doc -> a -> a -> Doc
pr'pair (Doc -> Symbol -> Symbol -> Doc) -> Doc -> Symbol -> Symbol -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text "label") (SortMap -> Doc) -> SortMap -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
labelMap Morphism
mor
        s :: Doc
s = Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
mor
        t :: Doc
t = Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
mor
        in [Doc] -> Doc
vcat [ Doc
smap, Doc
kmap, Doc
omap, Doc
lmap, String -> Doc
forall a. Pretty a => a -> Doc
pretty "\nSource:\n", Doc
s
                , String -> Doc
forall a. Pretty a => a -> Doc
pretty "\nTarget\n", Doc
t ]

-- * Helper functions

-- ** to modify Morphisms

mapTarget :: (Sign -> Sign) -> Morphism -> Morphism
mapTarget :: (Sign -> Sign) -> Morphism -> Morphism
mapTarget func :: Sign -> Sign
func mor :: Morphism
mor = Morphism
mor { target :: Sign
target = Sign -> Sign
func (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
mor }

mapSortMap :: (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap :: (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap func :: SortMap -> SortMap
func mor :: Morphism
mor = Morphism
mor { sortMap :: SortMap
sortMap = SortMap -> SortMap
func (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
sortMap Morphism
mor }
mapOpMap :: (OpMap -> OpMap) -> Morphism -> Morphism
mapOpMap :: (SortMap -> SortMap) -> Morphism -> Morphism
mapOpMap func :: SortMap -> SortMap
func mor :: Morphism
mor = Morphism
mor { opMap :: SortMap
opMap = SortMap -> SortMap
func (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
opMap Morphism
mor }
mapLabelMap :: (LabelMap -> LabelMap) -> Morphism -> Morphism
mapLabelMap :: (SortMap -> SortMap) -> Morphism -> Morphism
mapLabelMap func :: SortMap -> SortMap
func mor :: Morphism
mor = Morphism
mor { labelMap :: SortMap
labelMap = SortMap -> SortMap
func (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
labelMap Morphism
mor }

-- ** to handle Renamings

-- TODO: Handle Attrs in Op Renamings.
renamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
renamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
renamingSymbolsMaybe rename :: Renaming
rename = case Renaming
rename of
    SortRenaming src :: Sort
src tgt :: Sort
tgt -> (Symbol, Symbol) -> Maybe (Symbol, Symbol)
forall a. a -> Maybe a
Just (Sort -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Sort
src, Sort -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Sort
tgt)
    LabelRenaming src :: LabelId
src tgt :: LabelId
tgt -> (Symbol, Symbol) -> Maybe (Symbol, Symbol)
forall a. a -> Maybe a
Just (LabelId -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol LabelId
src, LabelId -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol LabelId
tgt)
    OpRenaming1 src :: OpId
src (To tgt :: OpId
tgt _) -> (Symbol, Symbol) -> Maybe (Symbol, Symbol)
forall a. a -> Maybe a
Just (OpId -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol OpId
src, OpId -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol OpId
tgt)
    OpRenaming2 src :: OpId
src dom :: [Type]
dom cod :: Type
cod (To tgt :: OpId
tgt _) -> let
        src' :: Operator
src' = OpId -> [Type] -> Type -> [Attr] -> Operator
Op OpId
src [Type]
dom Type
cod []
        tgt' :: Operator
tgt' = OpId -> [Type] -> Type -> [Attr] -> Operator
Op OpId
tgt [Type]
dom Type
cod []
        in (Symbol, Symbol) -> Maybe (Symbol, Symbol)
forall a. a -> Maybe a
Just (Operator -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Operator
src', Operator -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Operator
tgt')
    TermMap _ _ -> Maybe (Symbol, Symbol)
forall a. Maybe a
Nothing

-- | Extract the 'Symbol's from a 'Renaming', if possible.
renamingSymbols :: Renaming -> (Symbol, Symbol)
renamingSymbols :: Renaming -> (Symbol, Symbol)
renamingSymbols = Maybe (Symbol, Symbol) -> (Symbol, Symbol)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Symbol, Symbol) -> (Symbol, Symbol))
-> (Renaming -> Maybe (Symbol, Symbol))
-> Renaming
-> (Symbol, Symbol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Renaming -> Maybe (Symbol, Symbol)
renamingSymbolsMaybe

-- | Separate Operator and other Renamings.
partitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
partitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
partitionRenamings = let
    is'op :: Renaming -> Bool
is'op renaming :: Renaming
renaming = case Renaming
renaming of
        OpRenaming1 _ _ -> Bool
True
        OpRenaming2 {} -> Bool
True
        _ -> Bool
False
    in (Renaming -> Bool) -> [Renaming] -> ([Renaming], [Renaming])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Renaming -> Bool
is'op

-- ** to apply Renamings to Morphisms

{- | Insert an 'Operator' 'Renaming' into a 'Morphism'.
Iff apply is True, apply the Renaming to the Morphism's target Signature. -}
insertOpRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertOpRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertOpRenaming apply :: Bool
apply rename :: Renaming
rename = let
    syms :: (Symbol, Symbol)
syms = Renaming -> (Symbol, Symbol)
renamingSymbols Renaming
rename
    add'op :: Morphism -> Morphism
add'op = (SortMap -> SortMap) -> Morphism -> Morphism
mapOpMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> SortMap -> SortMap)
-> (Symbol, Symbol) -> SortMap -> SortMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Symbol, Symbol)
syms
    use'op :: [Attr] -> Morphism -> Morphism
use'op attrs :: [Attr]
attrs = if Bool
apply
        then (Sign -> Sign) -> Morphism -> Morphism
mapTarget ((Sign -> Sign) -> Morphism -> Morphism)
-> (Sign -> Sign) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> [Attr] -> Sign -> Sign)
-> (Symbol, Symbol) -> [Attr] -> Sign -> Sign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> [Attr] -> Sign -> Sign
Sign.renameOp (Symbol, Symbol)
syms [Attr]
attrs
        else Morphism -> Morphism
forall a. a -> a
id
    in case Renaming
rename of
        OpRenaming1 _ (To _ attrs :: [Attr]
attrs) -> [Attr] -> Morphism -> Morphism
use'op [Attr]
attrs (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
add'op
        OpRenaming2 _ _ _ (To _ attrs :: [Attr]
attrs) -> [Attr] -> Morphism -> Morphism
use'op [Attr]
attrs (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
add'op
        _ -> Morphism -> Morphism
forall a. a -> a
id

{- | Insert a non-Operator 'Renaming' into a 'Morphism'.
iff True, apply the Renaming to the target Sign -}
insertRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertRenaming :: Bool -> Renaming -> Morphism -> Morphism
insertRenaming apply :: Bool
apply rename :: Renaming
rename = let
    syms :: (Symbol, Symbol)
syms = Renaming -> (Symbol, Symbol)
renamingSymbols Renaming
rename
    add'sort :: Morphism -> Morphism
add'sort = (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> SortMap -> SortMap)
-> (Symbol, Symbol) -> SortMap -> SortMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Symbol, Symbol)
syms
    use'sort :: Morphism -> Morphism
use'sort = if Bool
apply
        then (Sign -> Sign) -> Morphism -> Morphism
mapTarget ((Sign -> Sign) -> Morphism -> Morphism)
-> (Sign -> Sign) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> Sign -> Sign)
-> (Symbol, Symbol) -> Sign -> Sign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> Sign -> Sign
Sign.renameSort (Symbol, Symbol)
syms
        else Morphism -> Morphism
forall a. a -> a
id
    ren'sort :: Morphism -> Morphism
ren'sort = (SortMap -> SortMap) -> Morphism -> Morphism
mapOpMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> SortMap -> SortMap)
-> (Symbol, Symbol) -> SortMap -> SortMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> SortMap -> SortMap
renameSortOpMap (Symbol, Symbol)
syms
    add'labl :: Morphism -> Morphism
add'labl = (SortMap -> SortMap) -> Morphism -> Morphism
mapLabelMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> SortMap -> SortMap)
-> (Symbol, Symbol) -> SortMap -> SortMap
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Symbol, Symbol)
syms
    use'labl :: Morphism -> Morphism
use'labl = if Bool
apply
        then (Sign -> Sign) -> Morphism -> Morphism
mapTarget ((Sign -> Sign) -> Morphism -> Morphism)
-> (Sign -> Sign) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> Sign -> Sign)
-> (Symbol, Symbol) -> Sign -> Sign
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Symbol -> Symbol -> Sign -> Sign
Sign.renameLabel (Symbol, Symbol)
syms
        else Morphism -> Morphism
forall a. a -> a
id
    in case Renaming
rename of
        SortRenaming _ _ -> Morphism -> Morphism
ren'sort (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
use'sort (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
add'sort
        LabelRenaming _ _ -> Morphism -> Morphism
use'labl (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
add'labl
        _ -> Morphism -> Morphism
forall a. a -> a
id

-- | Rename sorts in the profiles of an operator map.
renameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
renameSortOpMap :: Symbol -> Symbol -> SortMap -> SortMap
renameSortOpMap from :: Symbol
from to :: Symbol
to = (Symbol -> Symbol) -> SortMap -> SortMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((Symbol -> Symbol) -> SortMap -> SortMap)
-> (Symbol -> Symbol) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ SortMap -> Symbol -> Symbol
forall a. HasSorts a => SortMap -> a -> a
mapSorts (SortMap -> Symbol -> Symbol) -> SortMap -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> SortMap
forall k a. k -> a -> Map k a
Map.singleton Symbol
from Symbol
to

-- | Insert 'Renaming's into a 'Morphism'.
insertRenamings :: Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings :: Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings apply :: Bool
apply mor :: Morphism
mor rens :: [Renaming]
rens = let
    (ops :: [Renaming]
ops, rest :: [Renaming]
rest) = [Renaming] -> ([Renaming], [Renaming])
partitionRenamings [Renaming]
rens
    add'ops :: Morphism -> Morphism
add'ops = (Morphism -> [Renaming] -> Morphism)
-> [Renaming] -> Morphism -> Morphism
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Renaming -> Morphism -> Morphism)
-> Morphism -> [Renaming] -> Morphism
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Renaming -> Morphism -> Morphism)
 -> Morphism -> [Renaming] -> Morphism)
-> (Renaming -> Morphism -> Morphism)
-> Morphism
-> [Renaming]
-> Morphism
forall a b. (a -> b) -> a -> b
$ Bool -> Renaming -> Morphism -> Morphism
insertOpRenaming Bool
apply) [Renaming]
ops
    add'rest :: Morphism -> Morphism
add'rest = (Morphism -> [Renaming] -> Morphism)
-> [Renaming] -> Morphism -> Morphism
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Renaming -> Morphism -> Morphism)
-> Morphism -> [Renaming] -> Morphism
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Renaming -> Morphism -> Morphism)
 -> Morphism -> [Renaming] -> Morphism)
-> (Renaming -> Morphism -> Morphism)
-> Morphism
-> [Renaming]
-> Morphism
forall a b. (a -> b) -> a -> b
$ Bool -> Renaming -> Morphism -> Morphism
insertRenaming Bool
apply) [Renaming]
rest
    in Morphism -> Morphism
add'rest (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
add'ops (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Morphism
mor

-- * Construction

-- | Create a 'Morphism' from an initial 'Sign'ature and a list of 'Renaming's.
fromSignRenamings :: Sign -> [Renaming] -> Morphism
fromSignRenamings :: Sign -> [Renaming] -> Morphism
fromSignRenamings s :: Sign
s rs :: [Renaming]
rs = Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings Bool
True (Sign -> Morphism
identity Sign
s) [Renaming]
rs

-- | Create a 'Morphism' from a pair of 'Sign'atures and a list of 'Renaming's.
fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
fromSignsRenamings sign1 :: Sign
sign1 sign2 :: Sign
sign2 rs :: [Renaming]
rs =
  Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings Bool
False (Sign -> Sign -> Morphism
inclusion Sign
sign1 Sign
sign2) [Renaming]
rs

-- | the empty 'Morphism'
empty :: Morphism
empty :: Morphism
empty = Sign -> Morphism
identity Sign
Sign.empty

-- | the identity 'Morphism'
identity :: Sign -> Morphism
identity :: Sign -> Morphism
identity sign :: Sign
sign = Sign -> Sign -> Morphism
inclusion Sign
sign Sign
sign

-- | the inclusion 'Morphism'
inclusion :: Sign -> Sign -> Morphism
inclusion :: Sign -> Sign -> Morphism
inclusion src :: Sign
src tgt :: Sign
tgt = Morphism :: Sign
-> Sign -> SortMap -> SortMap -> SortMap -> SortMap -> Morphism
Morphism {
        source :: Sign
source = Sign
src,
        target :: Sign
target = Sign
tgt,
        sortMap :: SortMap
sortMap = SortMap
forall k a. Map k a
Map.empty,
        kindMap :: SortMap
kindMap = SortMap
forall k a. Map k a
Map.empty,
        opMap :: SortMap
opMap = SortMap
forall k a. Map k a
Map.empty,
        labelMap :: SortMap
labelMap = SortMap
forall k a. Map k a
Map.empty
    }

-- * Combination

-- | the inverse 'Morphism'
inverse :: Morphism -> Result Morphism
inverse :: Morphism -> Result Morphism
inverse mor :: Morphism
mor = let
    invertMap :: Map a Symbol -> Map Symbol a
invertMap = (a -> Symbol -> Map Symbol a -> Map Symbol a)
-> Map Symbol a -> Map a Symbol -> Map Symbol a
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey ((Symbol -> a -> Map Symbol a -> Map Symbol a)
-> a -> Symbol -> Map Symbol a -> Map Symbol a
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbol -> a -> Map Symbol a -> Map Symbol a
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert) Map Symbol a
forall k a. Map k a
Map.empty
    in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
kindMorph Morphism :: Sign
-> Sign -> SortMap -> SortMap -> SortMap -> SortMap -> Morphism
Morphism {
        source :: Sign
source = Morphism -> Sign
target Morphism
mor,
        target :: Sign
target = Morphism -> Sign
source Morphism
mor,
        sortMap :: SortMap
sortMap = SortMap -> SortMap
forall a. Map a Symbol -> Map Symbol a
invertMap (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
sortMap Morphism
mor,
        kindMap :: SortMap
kindMap = SortMap -> SortMap
forall a. Map a Symbol -> Map Symbol a
invertMap (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
kindMap Morphism
mor,
        opMap :: SortMap
opMap = SortMap -> SortMap
forall a. Map a Symbol -> Map Symbol a
invertMap (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
opMap Morphism
mor,
        labelMap :: SortMap
labelMap = SortMap -> SortMap
forall a. Map a Symbol -> Map Symbol a
invertMap (SortMap -> SortMap) -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
labelMap Morphism
mor
    }

-- | the union of two 'Morphism's
union :: Morphism -> Morphism -> Morphism
union :: Morphism -> Morphism -> Morphism
union mor1 :: Morphism
mor1 mor2 :: Morphism
mor2 = let
    apply :: (t -> t -> t) -> (Morphism -> t) -> t
apply func :: t -> t -> t
func items :: Morphism -> t
items = t -> t -> t
func (Morphism -> t
items Morphism
mor1) (Morphism -> t
items Morphism
mor2)
    in Morphism -> Morphism
kindMorph Morphism :: Sign
-> Sign -> SortMap -> SortMap -> SortMap -> SortMap -> Morphism
Morphism {
        source :: Sign
source = (Sign -> Sign -> Sign) -> (Morphism -> Sign) -> Sign
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply Sign -> Sign -> Sign
Sign.union Morphism -> Sign
source,
        target :: Sign
target = (Sign -> Sign -> Sign) -> (Morphism -> Sign) -> Sign
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply Sign -> Sign -> Sign
Sign.union Morphism -> Sign
target,
        sortMap :: SortMap
sortMap = (SortMap -> SortMap -> SortMap) -> (Morphism -> SortMap) -> SortMap
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Morphism -> SortMap
sortMap,
        kindMap :: SortMap
kindMap = (SortMap -> SortMap -> SortMap) -> (Morphism -> SortMap) -> SortMap
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Morphism -> SortMap
kindMap,
        opMap :: SortMap
opMap = (SortMap -> SortMap -> SortMap) -> (Morphism -> SortMap) -> SortMap
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Morphism -> SortMap
opMap,
        labelMap :: SortMap
labelMap = (SortMap -> SortMap -> SortMap) -> (Morphism -> SortMap) -> SortMap
forall t t. (t -> t -> t) -> (Morphism -> t) -> t
apply SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Morphism -> SortMap
labelMap
    }

-- Just a shorthand for types inside compose.
type Extraction = Morphism -> SymbolMap

-- | the composition of two 'Morphism's
compose :: Morphism -> Morphism -> Result Morphism
compose :: Morphism -> Morphism -> Result Morphism
compose f :: Morphism
f g :: Morphism
g
    | Morphism -> Sign
target Morphism
f Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
/= Morphism -> Sign
source Morphism
g = String -> Result Morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail
        "target of the first and source of the second morphism are different"
    | Bool
otherwise = let
        {- Take SymbolMap |mp| of each Morphism.
        Convert each SymbolMap to a function.
        Compose those functions. -}
        map'map :: Extraction -> Symbol -> Symbol
        map'map :: (Morphism -> SortMap) -> Symbol -> Symbol
map'map mp :: Morphism -> SortMap
mp = SortMap -> Symbol -> Symbol
forall a. Ord a => Map a a -> a -> a
mapAsFunction (Morphism -> SortMap
mp Morphism
g) (Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortMap -> Symbol -> Symbol
forall a. Ord a => Map a a -> a -> a
mapAsFunction (Morphism -> SortMap
mp Morphism
f)
        {- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
        Insert the renaming mapping into a SymbolMap. -}
        insert :: Extraction -> Symbol -> SymbolMap -> SymbolMap
        insert :: (Morphism -> SortMap) -> Symbol -> SortMap -> SortMap
insert mp :: Morphism -> SortMap
mp x :: Symbol
x = let y :: Symbol
y = (Morphism -> SortMap) -> Symbol -> Symbol
map'map Morphism -> SortMap
mp Symbol
x
            in if Symbol
x Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
y then SortMap -> SortMap
forall a. a -> a
id else Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
x Symbol
y
        -- Map each symbol in |items| via the combined SymbolMaps |mp|.
        compose'map :: Extraction -> (Sign -> SymbolSet) -> SymbolMap
        compose'map :: (Morphism -> SortMap) -> (Sign -> SymbolSet) -> SortMap
compose'map mp :: Morphism -> SortMap
mp items :: Sign -> SymbolSet
items = if SortMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> SortMap
mp Morphism
g)
            -- if the SymbolMap of |g| is empty, we use the one from |f|
            then Morphism -> SortMap
mp Morphism
f
            {- otherwise we start with the SymbolSet from |source f|
            and construct a combined SymbolMap by applying both
            SymbolMaps (from |f| and |g|) to each item in |insert| -}
            else (Symbol -> SortMap -> SortMap) -> SortMap -> SymbolSet -> SortMap
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold ((Morphism -> SortMap) -> Symbol -> SortMap -> SortMap
insert Morphism -> SortMap
mp) SortMap
forall k a. Map k a
Map.empty (SymbolSet -> SortMap) -> SymbolSet -> SortMap
forall a b. (a -> b) -> a -> b
$ Sign -> SymbolSet
items (Morphism -> Sign
source Morphism
f)
        -- We want a morphism from |source f| to |target g|.
        mor :: Morphism
mor = Sign -> Sign -> Morphism
inclusion (Morphism -> Sign
source Morphism
f) (Morphism -> Sign
target Morphism
g)
        in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
kindMorph Morphism
mor {
            sortMap :: SortMap
sortMap = (Morphism -> SortMap) -> (Sign -> SymbolSet) -> SortMap
compose'map Morphism -> SortMap
sortMap Sign -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts,
            opMap :: SortMap
opMap = (Morphism -> SortMap) -> (Sign -> SymbolSet) -> SortMap
compose'map Morphism -> SortMap
opMap Sign -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps,
            labelMap :: SortMap
labelMap = (Morphism -> SortMap) -> (Sign -> SymbolSet) -> SortMap
compose'map Morphism -> SortMap
labelMap Sign -> SymbolSet
forall a. HasLabels a => a -> SymbolSet
getLabels
        }

-- * Testing

-- | True iff the 'Morphism' is an inclusion
isInclusion :: Morphism -> Bool
isInclusion :: Morphism -> Bool
isInclusion mor :: Morphism
mor = let
    null'sortMap :: Bool
null'sortMap = SortMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> SortMap
sortMap Morphism
mor)
    null'opMap :: Bool
null'opMap = SortMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> SortMap
opMap Morphism
mor)
    null'labelMap :: Bool
null'labelMap = SortMap -> Bool
forall k a. Map k a -> Bool
Map.null (Morphism -> SortMap
labelMap Morphism
mor)
    in Bool
null'sortMap Bool -> Bool -> Bool
&& Bool
null'opMap Bool -> Bool -> Bool
&& Bool
null'labelMap

-- | True iff the 'Morphism' is legal
isLegal :: Morphism -> Result ()
isLegal :: Morphism -> Result ()
isLegal mor :: Morphism
mor = let
    src :: Sign
src = Morphism -> Sign
source Morphism
mor
    tgt :: Sign
tgt = Morphism -> Sign
target Morphism
mor
    smap :: SortMap
smap = Morphism -> SortMap
sortMap Morphism
mor
    omap :: SortMap
omap = Morphism -> SortMap
opMap Morphism
mor
    lmap :: SortMap
lmap = Morphism -> SortMap
labelMap Morphism
mor
    subset :: Map a a -> (Sign -> Set a) -> Bool
subset mp :: Map a a
mp items :: Sign -> Set a
items = let mapped :: Set a -> Set a
mapped = (a -> a) -> Set a -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map ((a -> a) -> Set a -> Set a) -> (a -> a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Map a a -> a -> a
forall a. Ord a => Map a a -> a -> a
mapAsFunction Map a a
mp
        in Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Set a -> Set a
mapped (Set a -> Set a) -> Set a -> Set a
forall a b. (a -> b) -> a -> b
$ Sign -> Set a
items Sign
src) (Set a -> Bool) -> Set a -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set a
items Sign
tgt
    lg'source :: Bool
lg'source = Sign -> Bool
Sign.isLegal Sign
src
    lg'sortMap :: Bool
lg'sortMap = SortMap -> (Sign -> SymbolSet) -> Bool
forall a. Ord a => Map a a -> (Sign -> Set a) -> Bool
subset SortMap
smap Sign -> SymbolSet
forall a. HasSorts a => a -> SymbolSet
getSorts
    lg'opMap :: Bool
lg'opMap = SortMap -> (Sign -> SymbolSet) -> Bool
forall a. Ord a => Map a a -> (Sign -> Set a) -> Bool
subset SortMap
omap Sign -> SymbolSet
forall a. HasOps a => a -> SymbolSet
getOps
    lg'labelMap :: Bool
lg'labelMap = SortMap -> (Sign -> SymbolSet) -> Bool
forall a. Ord a => Map a a -> (Sign -> Set a) -> Bool
subset SortMap
lmap Sign -> SymbolSet
forall a. HasLabels a => a -> SymbolSet
getLabels
    lg'target :: Bool
lg'target = Sign -> Bool
Sign.isLegal Sign
tgt
    in Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and [Bool
lg'source, Bool
lg'sortMap, Bool
lg'opMap, Bool
lg'labelMap, Bool
lg'target]) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
       String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "illegal Maude morphism"

-- * Conversion

-- | extract the complete 'SymbolMap' of a 'Morphism'
symbolMap :: Morphism -> SymbolMap
symbolMap :: Morphism -> SortMap
symbolMap mor :: Morphism
mor = [SortMap] -> SortMap
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
Map.unions [Morphism -> SortMap
sortMap Morphism
mor, Morphism -> SortMap
opMap Morphism
mor, Morphism -> SortMap
labelMap Morphism
mor]

-- * Modification

-- | set a new target for a 'Morphism'
setTarget :: Sign -> Morphism -> Morphism
setTarget :: Sign -> Morphism -> Morphism
setTarget sg :: Sign
sg m :: Morphism
m = Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ (Sign -> Sign) -> Morphism -> Morphism
mapTarget (Sign -> Sign -> Sign
forall a b. a -> b -> a
const Sign
sg) Morphism
m

-- | qualify a list of 'Symbol's inside a 'Morphism'
qualifySorts :: Morphism -> Qid -> Symbols -> Morphism
qualifySorts :: Morphism -> Qid -> Symbols -> Morphism
qualifySorts mor :: Morphism
mor qid :: Qid
qid syms :: Symbols
syms = let
    insert :: Symbol -> SortMap -> SortMap
insert symb :: Symbol
symb = Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
symb (Symbol -> SortMap -> SortMap) -> Symbol -> SortMap -> SortMap
forall a b. (a -> b) -> a -> b
$ Qid -> Symbol -> Symbol
qualify Qid
qid Symbol
symb
    smap :: SortMap
smap = (Symbol -> SortMap -> SortMap) -> SortMap -> Symbols -> SortMap
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Symbol -> SortMap -> SortMap
insert SortMap
forall k a. Map k a
Map.empty Symbols
syms
    q'tgt :: Morphism -> Morphism
q'tgt = (Sign -> Sign) -> Morphism -> Morphism
mapTarget ((Sign -> Sign) -> Morphism -> Morphism)
-> (Sign -> Sign) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ SortMap -> Sign -> Sign
forall a. HasSorts a => SortMap -> a -> a
mapSorts SortMap
smap
    q'smap :: Morphism -> Morphism
q'smap = (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ SortMap -> SortMap -> SortMap
forall a. HasSorts a => SortMap -> a -> a
mapSorts SortMap
smap
    x'smap :: Morphism -> Morphism
x'smap = (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SortMap
smap
    in Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
q'tgt (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
x'smap (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
q'smap (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Morphism
mor

-- | apply a list of 'Renaming's to a 'Morphism'
applyRenamings :: Morphism -> [Renaming] -> Morphism
applyRenamings :: Morphism -> [Renaming] -> Morphism
applyRenamings m :: Morphism
m rs :: [Renaming]
rs = Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Bool -> Morphism -> [Renaming] -> Morphism
insertRenamings Bool
True Morphism
m [Renaming]
rs

-- | apply a 'Sort' 'Renaming' to a 'Morphism'
extendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
extendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
extendWithSortRenaming src :: Symbol
src tgt :: Symbol
tgt m :: Morphism
m = let
    add'sort :: Morphism -> Morphism
add'sort = (SortMap -> SortMap) -> Morphism -> Morphism
mapSortMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> SortMap -> SortMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Symbol
src Symbol
tgt
    use'sort :: Morphism -> Morphism
use'sort = (Sign -> Sign) -> Morphism -> Morphism
mapTarget ((Sign -> Sign) -> Morphism -> Morphism)
-> (Sign -> Sign) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> Sign -> Sign
Sign.renameSort Symbol
src Symbol
tgt
    ren'sort :: Morphism -> Morphism
ren'sort = (SortMap -> SortMap) -> Morphism -> Morphism
mapOpMap ((SortMap -> SortMap) -> Morphism -> Morphism)
-> (SortMap -> SortMap) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> SortMap -> SortMap
renameSortOpMap Symbol
src Symbol
tgt
    in Morphism -> Morphism
kindMorph (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
ren'sort (Morphism -> Morphism)
-> (Morphism -> Morphism) -> Morphism -> Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> Morphism
use'sort (Morphism -> Morphism) -> Morphism -> Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
add'sort Morphism
m

-- * Application

-- | translate a 'Sentence' along a 'Morphism'
translateSentence :: Morphism -> Sentence -> Result Sentence
translateSentence :: Morphism -> Sentence -> Result Sentence
translateSentence mor :: Morphism
mor = let
    smap :: Sentence -> Sentence
smap = SortMap -> Sentence -> Sentence
forall a. HasSorts a => SortMap -> a -> a
mapSorts (Morphism -> SortMap
sortMap Morphism
mor)
    omap :: Sentence -> Sentence
omap = SortMap -> Sentence -> Sentence
forall a. HasOps a => SortMap -> a -> a
mapOps (Morphism -> SortMap
opMap Morphism
mor)
    lmap :: Sentence -> Sentence
lmap = SortMap -> Sentence -> Sentence
forall a. HasLabels a => SortMap -> a -> a
mapLabels (Morphism -> SortMap
labelMap Morphism
mor)
    in Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (Sentence -> Sentence) -> Sentence -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Sentence
lmap (Sentence -> Sentence)
-> (Sentence -> Sentence) -> Sentence -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Sentence
smap (Sentence -> Sentence)
-> (Sentence -> Sentence) -> Sentence -> Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Sentence
omap

-- | translate 'Sort's along a 'Morphism'
translateSorts :: (HasSorts a) => Morphism -> a -> a
translateSorts :: Morphism -> a -> a
translateSorts = SortMap -> a -> a
forall a. HasSorts a => SortMap -> a -> a
mapSorts (SortMap -> a -> a) -> (Morphism -> SortMap) -> Morphism -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Morphism -> SortMap
sortMap

-- * Auxiliary functions
kindMorph :: Morphism -> Morphism
kindMorph :: Morphism -> Morphism
kindMorph morph :: Morphism
morph = Morphism
morph { kindMap :: SortMap
kindMap = SortMap -> [(Symbol, Symbol)] -> SortMap -> SortMap
kindMorphAux SortMap
kr1 [(Symbol, Symbol)]
sm SortMap
kr2}
     where kr1 :: SortMap
kr1 = Sign -> SortMap
kindRel (Sign -> SortMap) -> Sign -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
morph
           kr2 :: SortMap
kr2 = Sign -> SortMap
kindRel (Sign -> SortMap) -> Sign -> SortMap
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
morph
           sm :: [(Symbol, Symbol)]
sm = SortMap -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList (SortMap -> [(Symbol, Symbol)]) -> SortMap -> [(Symbol, Symbol)]
forall a b. (a -> b) -> a -> b
$ Morphism -> SortMap
sortMap Morphism
morph

kindMorphAux :: KindRel -> [(Symbol, Symbol)] -> KindRel -> KindMap
kindMorphAux :: SortMap -> [(Symbol, Symbol)] -> SortMap -> SortMap
kindMorphAux _ [] _ = SortMap
forall k a. Map k a
Map.empty
kindMorphAux kr1 :: SortMap
kr1 ((s1 :: Symbol
s1, s2 :: Symbol
s2) : ls :: [(Symbol, Symbol)]
ls) kr2 :: SortMap
kr2 = SortMap -> SortMap -> SortMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union SortMap
m SortMap
m'
     where m :: SortMap
m = SortMap -> [(Symbol, Symbol)] -> SortMap -> SortMap
kindMorphAux SortMap
kr1 [(Symbol, Symbol)]
ls SortMap
kr2
           (k1 :: Symbol
k1, k2 :: Symbol
k2) = case (Symbol -> SortMap -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s1 SortMap
kr1, Symbol -> SortMap -> Maybe Symbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s2 SortMap
kr2) of
              (Just r1 :: Symbol
r1, Just r2 :: Symbol
r2) -> (Symbol
r1, Symbol
r2)
              _ -> (Symbol
s1, Symbol
s1)
           m' :: SortMap
m' = if Symbol
k1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
k2
                then SortMap
forall k a. Map k a
Map.empty
                else Symbol -> Symbol -> SortMap
forall k a. k -> a -> Map k a
Map.singleton Symbol
k1 Symbol
k2