{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, DeriveDataTypeable #-}
{- |
Module      :  ./Maude/Sign.hs
Description :  Maude Signatures
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 signatures for Maude.
-}

module Maude.Sign (
    -- * Types

    -- ** The Signature type
    Sign (..),
    -- ** Auxiliary types
    SortSet,
    KindRel,
    SubsortRel,
    OpDecl,
    OpDeclSet,
    OpMap,
    Sentences,
    -- * Construction
    fromSpec,
    empty,
    -- * Combination
    union,
    intersection,
    -- * Conversion
    symbols,
    -- * Testing
    isLegal,
    isSubsign,
    -- * Modification
    simplifySentence,
    renameSort,
    renameLabel,
    renameOp,
    -- * Inline printing
    inlineSign
) where

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

import Maude.Sentence (Sentence)
import qualified Maude.Sentence as Sen

import Data.Data
import Data.Set (Set)
import Data.Map (Map)
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.Foldable as Fold
import qualified Common.Lib.Rel as Rel
import qualified Data.List as List

import Common.Doc hiding (empty)
import qualified Common.Doc as Doc
import Common.DocUtils (Pretty (..))
import Common.Utils (nubOrd)

-- * Types

-- ** Auxiliary types

type SortSet = SymbolSet
type KindSet = SymbolSet
type SubsortRel = SymbolRel
type OpDecl = (Set Symbol, [Attr])
type OpDeclSet = Set OpDecl
type OpMap = Map Qid OpDeclSet
type Sentences = Set Sentence
type KindRel = Map Symbol Symbol

-- ** The Signature type

-- | The Signature of a Maude 'Module'.
data Sign = Sign {
        Sign -> SortSet
sorts :: SortSet,               -- ^ The 'Set' of 'Sort's
        Sign -> SortSet
kinds :: KindSet,               -- ^ The 'Set' of 'Kind's
        Sign -> SubsortRel
subsorts :: SubsortRel,         -- ^ The 'Rel'ation of 'Sort's
        Sign -> OpMap
ops :: OpMap,                   -- ^ The 'Map' of 'Operator's
        Sign -> Sentences
sentences :: Sentences,         -- ^ The 'Set' of 'Sentence's
        Sign -> KindRel
kindRel :: KindRel
        -- ^ The 'Set' of 'Sentence's for the kind function
    } deriving (Int -> Sign -> ShowS
[Sign] -> ShowS
Sign -> String
(Int -> Sign -> ShowS)
-> (Sign -> String) -> ([Sign] -> ShowS) -> Show Sign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Sign] -> ShowS
$cshowList :: [Sign] -> ShowS
show :: Sign -> String
$cshow :: Sign -> String
showsPrec :: Int -> Sign -> ShowS
$cshowsPrec :: Int -> Sign -> ShowS
Show, Eq Sign
Eq Sign =>
(Sign -> Sign -> Ordering)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Bool)
-> (Sign -> Sign -> Sign)
-> (Sign -> Sign -> Sign)
-> Ord Sign
Sign -> Sign -> Bool
Sign -> Sign -> Ordering
Sign -> Sign -> Sign
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 :: Sign -> Sign -> Sign
$cmin :: Sign -> Sign -> Sign
max :: Sign -> Sign -> Sign
$cmax :: Sign -> Sign -> Sign
>= :: Sign -> Sign -> Bool
$c>= :: Sign -> Sign -> Bool
> :: Sign -> Sign -> Bool
$c> :: Sign -> Sign -> Bool
<= :: Sign -> Sign -> Bool
$c<= :: Sign -> Sign -> Bool
< :: Sign -> Sign -> Bool
$c< :: Sign -> Sign -> Bool
compare :: Sign -> Sign -> Ordering
$ccompare :: Sign -> Sign -> Ordering
$cp1Ord :: Eq Sign
Ord, Sign -> Sign -> Bool
(Sign -> Sign -> Bool) -> (Sign -> Sign -> Bool) -> Eq Sign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Sign -> Sign -> Bool
$c/= :: Sign -> Sign -> Bool
== :: Sign -> Sign -> Bool
$c== :: Sign -> Sign -> Bool
Eq, Typeable)

-- ** 'Sign' instances

instance Pretty Sign where
    pretty :: Sign -> Doc
pretty sign :: Sign
sign = let
        descend :: (a -> c -> c) -> Set a -> c -> c
descend = (c -> Set a -> c) -> Set a -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((c -> Set a -> c) -> Set a -> c -> c)
-> ((a -> c -> c) -> c -> Set a -> c)
-> (a -> c -> c)
-> Set a
-> c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c -> c) -> c -> Set a -> c
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
        -- print sort declarations
        pr'sorts :: [a] -> Doc
pr'sorts ss :: [a]
ss = if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ss then Doc
Doc.empty else
            [Doc] -> Doc
hsep [String -> Doc
keyword "sorts", [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
ss, Doc
dot]
        -- print kind declarations
        pr'kinds :: [a] -> Doc
pr'kinds ks :: [a]
ks = if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ks then Doc
Doc.empty else
            [Doc] -> Doc
hsep [String -> Doc
keyword "kinds", [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
ks, Doc
dot]
        -- print subsort declarations
        pr'sups :: SortSet -> Doc
pr'sups = [Doc] -> Doc
hsep ([Doc] -> Doc) -> (SortSet -> [Doc]) -> SortSet -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Doc) -> [Symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty ([Symbol] -> [Doc]) -> (SortSet -> [Symbol]) -> SortSet -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortSet -> [Symbol]
forall a. Set a -> [a]
Set.elems
        pr'pair :: a -> SortSet -> [Doc] -> [Doc]
pr'pair sub :: a
sub sups :: SortSet
sups = (:) (Doc -> [Doc] -> [Doc])
-> ([Doc] -> Doc) -> [Doc] -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> [Doc] -> [Doc]) -> [Doc] -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
            [String -> Doc
keyword "subsort", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
sub, Doc
less, SortSet -> Doc
pr'sups SortSet
sups, Doc
dot]
        pr'subs :: Map Symbol SortSet -> Doc
pr'subs = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Map Symbol SortSet -> [Doc]) -> Map Symbol SortSet -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> SortSet -> [Doc] -> [Doc])
-> [Doc] -> Map Symbol SortSet -> [Doc]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Symbol -> SortSet -> [Doc] -> [Doc]
forall a. Pretty a => a -> SortSet -> [Doc] -> [Doc]
pr'pair []
        -- print operator declarations
        pr'decl :: a -> a -> Doc
pr'decl attrs :: a
attrs symb :: a
symb = [Doc] -> Doc
hsep
            [String -> Doc
keyword "op", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
symb, a -> Doc
forall a. Pretty a => a -> Doc
pretty a
attrs, Doc
dot]
        pr'ods :: (Set a, a) -> [Doc] -> [Doc]
pr'ods (decls :: Set a
decls, attrs :: a
attrs) = (a -> [Doc] -> [Doc]) -> Set a -> [Doc] -> [Doc]
forall a c. (a -> c -> c) -> Set a -> c -> c
descend ((:) (Doc -> [Doc] -> [Doc]) -> (a -> Doc) -> a -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Doc
forall a a. (Pretty a, Pretty a) => a -> a -> Doc
pr'decl a
attrs) Set a
decls
        pr'ocs :: Set (SortSet, [Attr]) -> [Doc] -> [Doc]
pr'ocs = ((SortSet, [Attr]) -> [Doc] -> [Doc])
-> Set (SortSet, [Attr]) -> [Doc] -> [Doc]
forall a c. (a -> c -> c) -> Set a -> c -> c
descend (SortSet, [Attr]) -> [Doc] -> [Doc]
forall a a. (Pretty a, Pretty a) => (Set a, a) -> [Doc] -> [Doc]
pr'ods
        pr'ops :: Map k (Set (SortSet, [Attr])) -> Doc
pr'ops = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Map k (Set (SortSet, [Attr])) -> [Doc])
-> Map k (Set (SortSet, [Attr]))
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (SortSet, [Attr]) -> [Doc] -> [Doc])
-> [Doc] -> Map k (Set (SortSet, [Attr])) -> [Doc]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr Set (SortSet, [Attr]) -> [Doc] -> [Doc]
pr'ocs []
        in [Doc] -> Doc
vcat [ [Symbol] -> Doc
forall a. Pretty a => [a] -> Doc
pr'sorts ([Symbol] -> Doc) -> [Symbol] -> Doc
forall a b. (a -> b) -> a -> b
$ SortSet -> [Symbol]
forall a. Set a -> [a]
Set.elems (SortSet -> [Symbol]) -> SortSet -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign -> SortSet
sorts Sign
sign
                , [Symbol] -> Doc
forall a. Pretty a => [a] -> Doc
pr'kinds ([Symbol] -> Doc) -> [Symbol] -> Doc
forall a b. (a -> b) -> a -> b
$ SortSet -> [Symbol]
forall a. Set a -> [a]
Set.elems (SortSet -> [Symbol]) -> SortSet -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign -> SortSet
kinds Sign
sign
                , Map Symbol SortSet -> Doc
pr'subs (Map Symbol SortSet -> Doc) -> Map Symbol SortSet -> Doc
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Map Symbol SortSet
forall a. Rel a -> Map a (Set a)
Rel.toMap (SubsortRel -> Map Symbol SortSet)
-> SubsortRel -> Map Symbol SortSet
forall a b. (a -> b) -> a -> b
$ SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (SubsortRel -> SubsortRel) -> SubsortRel -> SubsortRel
forall a b. (a -> b) -> a -> b
$ Sign -> SubsortRel
subsorts Sign
sign
                , OpMap -> Doc
forall k. Map k (Set (SortSet, [Attr])) -> Doc
pr'ops (OpMap -> Doc) -> OpMap -> Doc
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign]
                {- , pretty "op kind : Sort -> Kind ."
                , prettyPrint $ kindRel sign
                NOTE: Leaving out Sentences for now.
                , pretty $ Set.toList $ sentences sign ] -}

instance HasSorts Sign where
    getSorts :: Sign -> SortSet
getSorts = Sign -> SortSet
sorts
    mapSorts :: KindRel -> Sign -> Sign
mapSorts mp :: KindRel
mp sign :: Sign
sign = Sign
sign {
        sorts :: SortSet
sorts = KindRel -> SortSet -> SortSet
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mp (SortSet -> SortSet) -> SortSet -> SortSet
forall a b. (a -> b) -> a -> b
$ Sign -> SortSet
sorts Sign
sign,
        kinds :: SortSet
kinds = KindRel -> SortSet -> SortSet
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mp (SortSet -> SortSet) -> SortSet -> SortSet
forall a b. (a -> b) -> a -> b
$ Sign -> SortSet
kinds Sign
sign,
        subsorts :: SubsortRel
subsorts = KindRel -> SubsortRel -> SubsortRel
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mp (SubsortRel -> SubsortRel) -> SubsortRel -> SubsortRel
forall a b. (a -> b) -> a -> b
$ Sign -> SubsortRel
subsorts Sign
sign,
        ops :: OpMap
ops = KindRel -> OpMap -> OpMap
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mp (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign,
        kindRel :: KindRel
kindRel = KindRel -> KindRel -> KindRel
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mp (KindRel -> KindRel) -> KindRel -> KindRel
forall a b. (a -> b) -> a -> b
$ Sign -> KindRel
kindRel Sign
sign
        {- NOTE: Leaving out Sentences for now.
        sentences = mapSorts mp $ sentences sign -}
    }

instance {-# OVERLAPS #-} HasSorts KindRel where
    getSorts :: KindRel -> SortSet
getSorts = KindRel -> SortSet
getSortsKindRel
    mapSorts :: KindRel -> KindRel -> KindRel
mapSorts = KindRel -> KindRel -> KindRel
renameSortKindRel

instance HasOps Sign where
    getOps :: Sign -> SortSet
getOps = let
        descend :: (a -> c -> c) -> Set a -> c -> c
descend = (c -> Set a -> c) -> Set a -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((c -> Set a -> c) -> Set a -> c -> c)
-> ((a -> c -> c) -> c -> Set a -> c)
-> (a -> c -> c)
-> Set a
-> c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c -> c) -> c -> Set a -> c
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
        insert :: Set (SortSet, b) -> SortSet -> SortSet
insert = ((SortSet, b) -> SortSet -> SortSet)
-> Set (SortSet, b) -> SortSet -> SortSet
forall a c. (a -> c -> c) -> Set a -> c -> c
descend (((SortSet, b) -> SortSet -> SortSet)
 -> Set (SortSet, b) -> SortSet -> SortSet)
-> ((SortSet, b) -> SortSet -> SortSet)
-> Set (SortSet, b)
-> SortSet
-> SortSet
forall a b. (a -> b) -> a -> b
$ (Symbol -> SortSet -> SortSet) -> SortSet -> SortSet -> SortSet
forall a c. (a -> c -> c) -> Set a -> c -> c
descend Symbol -> SortSet -> SortSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (SortSet -> SortSet -> SortSet)
-> ((SortSet, b) -> SortSet) -> (SortSet, b) -> SortSet -> SortSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SortSet, b) -> SortSet
forall a b. (a, b) -> a
fst
        in (Set (SortSet, [Attr]) -> SortSet -> SortSet)
-> SortSet -> OpMap -> SortSet
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr Set (SortSet, [Attr]) -> SortSet -> SortSet
forall b. Set (SortSet, b) -> SortSet -> SortSet
insert SortSet
forall a. Set a
Set.empty (OpMap -> SortSet) -> (Sign -> OpMap) -> Sign -> SortSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> OpMap
ops
    mapOps :: KindRel -> Sign -> Sign
mapOps mp :: KindRel
mp sign :: Sign
sign = let
        subrel :: SubsortRel
subrel = Sign -> SubsortRel
subsorts Sign
sign
        opmap :: OpMap
opmap = Sign -> OpMap
ops Sign
sign
        update :: Symbol -> Symbol -> OpMap -> OpMap
update src :: Symbol
src tgt :: Symbol
tgt = SubsortRel -> Symbol -> Symbol -> [Attr] -> OpMap -> OpMap
mapOpDecl SubsortRel
subrel Symbol
src Symbol
tgt []
        in Sign
sign {
            ops :: OpMap
ops = (Symbol -> Symbol -> OpMap -> OpMap) -> OpMap -> KindRel -> OpMap
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Symbol -> Symbol -> OpMap -> OpMap
update OpMap
opmap KindRel
mp
            -- NOTE: Leaving out Sentences for now.
        }

instance HasLabels Sign where
    getLabels :: Sign -> SortSet
getLabels = Sentences -> SortSet
forall a. HasLabels a => a -> SortSet
getLabels (Sentences -> SortSet) -> (Sign -> Sentences) -> Sign -> SortSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sentences
sentences
    mapLabels :: KindRel -> Sign -> Sign
mapLabels mp :: KindRel
mp sign :: Sign
sign = Sign
sign {
        sentences :: Sentences
sentences = KindRel -> Sentences -> Sentences
forall a. HasLabels a => KindRel -> a -> a
mapLabels KindRel
mp (Sentences -> Sentences) -> Sentences -> Sentences
forall a b. (a -> b) -> a -> b
$ Sign -> Sentences
sentences Sign
sign
    }

-- * Construction

-- | Separate Sort, Subsort and Operator declaration 'Statement's.
partitionStmts :: [Statement] -> ([Sort], [SubsortDecl], [Operator])
partitionStmts :: [Statement] -> ([Sort], [SubsortDecl], [Operator])
partitionStmts = let
    switch :: ([Sort], [SubsortDecl], [Operator])
-> Statement -> ([Sort], [SubsortDecl], [Operator])
switch (sorts' :: [Sort]
sorts', subs' :: [SubsortDecl]
subs', ops' :: [Operator]
ops') stmt :: Statement
stmt = case Statement
stmt of
        SortStmnt sort :: Sort
sort -> (Sort
sort Sort -> [Sort] -> [Sort]
forall a. a -> [a] -> [a]
: [Sort]
sorts', [SubsortDecl]
subs', [Operator]
ops')
        SubsortStmnt sub :: SubsortDecl
sub -> ([Sort]
sorts', SubsortDecl
sub SubsortDecl -> [SubsortDecl] -> [SubsortDecl]
forall a. a -> [a] -> [a]
: [SubsortDecl]
subs', [Operator]
ops')
        OpStmnt op :: Operator
op -> ([Sort]
sorts', [SubsortDecl]
subs', Operator
op Operator -> [Operator] -> [Operator]
forall a. a -> [a] -> [a]
: [Operator]
ops')
        _ -> ([Sort]
sorts', [SubsortDecl]
subs', [Operator]
ops')
    in (([Sort], [SubsortDecl], [Operator])
 -> Statement -> ([Sort], [SubsortDecl], [Operator]))
-> ([Sort], [SubsortDecl], [Operator])
-> [Statement]
-> ([Sort], [SubsortDecl], [Operator])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([Sort], [SubsortDecl], [Operator])
-> Statement -> ([Sort], [SubsortDecl], [Operator])
switch ([], [], [])

-- | Extract the 'Sign'ature from the given 'Module'.
fromSpec :: Module -> Sign
fromSpec :: Module -> Sign
fromSpec (Module _ _ stmts :: [Statement]
stmts) = let
    sents :: [Sentence]
sents = (Sentence -> Bool) -> [Sentence] -> [Sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Sentence -> Bool) -> Sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Bool
Sen.isRule) ([Sentence] -> [Sentence])
-> ([Statement] -> [Sentence]) -> [Statement] -> [Sentence]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Statement] -> [Sentence]
Sen.fromStatements ([Statement] -> [Sentence]) -> [Statement] -> [Sentence]
forall a b. (a -> b) -> a -> b
$ [Statement]
stmts
    (sort'list :: [Sort]
sort'list, sub'list :: [SubsortDecl]
sub'list, op'list :: [Operator]
op'list) = [Statement] -> ([Sort], [SubsortDecl], [Operator])
partitionStmts [Statement]
stmts
    ins'sorts :: Sign -> Sign
ins'sorts = (Sign -> [Sort] -> Sign) -> [Sort] -> Sign -> Sign
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Sort -> Sign -> Sign) -> Sign -> [Sort] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Sort -> Sign -> Sign
insertSort) [Sort]
sort'list
    ins'subs :: Sign -> Sign
ins'subs = (Sign -> [SubsortDecl] -> Sign) -> [SubsortDecl] -> Sign -> Sign
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((SubsortDecl -> Sign -> Sign) -> Sign -> [SubsortDecl] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SubsortDecl -> Sign -> Sign
insertSubsort) [SubsortDecl]
sub'list
    ins'ops :: Sign -> Sign
ins'ops = (Sign -> [Operator] -> Sign) -> [Operator] -> Sign -> Sign
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Operator -> Sign -> Sign) -> Sign -> [Operator] -> Sign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Operator -> Sign -> Sign
insertOp) [Operator]
op'list
    sign :: Sign
sign = Sign -> Sign
ins'ops (Sign -> Sign) -> (Sign -> Sign) -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign
ins'subs (Sign -> Sign) -> (Sign -> Sign) -> Sign -> Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign
ins'sorts (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Sign
empty
    sbs :: SubsortRel
sbs = SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (SubsortRel -> SubsortRel) -> SubsortRel -> SubsortRel
forall a b. (a -> b) -> a -> b
$ Sign -> SubsortRel
subsorts Sign
sign
    kr :: KindRel
kr = SortSet -> SubsortRel -> KindRel
getkindRel (Sign -> SortSet
sorts Sign
sign) SubsortRel
sbs
    in Sign
sign {
        kinds :: SortSet
kinds = KindRel -> SortSet
kindsFromMap KindRel
kr,
        subsorts :: SubsortRel
subsorts = SubsortRel
sbs,
        ops :: OpMap
ops = OpMap -> OpMap
addPartial (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign,
        sentences :: Sentences
sentences = [Sentence] -> Sentences
forall a. Ord a => [a] -> Set a
Set.fromList [Sentence]
sents,
        kindRel :: KindRel
kindRel = KindRel
kr
    }

addPartial :: OpMap -> OpMap
addPartial :: OpMap -> OpMap
addPartial = (Set (SortSet, [Attr]) -> Set (SortSet, [Attr])) -> OpMap -> OpMap
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
partialODS

partialODS :: OpDeclSet -> OpDeclSet
partialODS :: Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
partialODS = ((SortSet, [Attr]) -> (SortSet, [Attr]))
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (SortSet, [Attr]) -> (SortSet, [Attr])
partialSet

partialSet :: (Set Symbol, [Attr]) -> (Set Symbol, [Attr])
partialSet :: (SortSet, [Attr]) -> (SortSet, [Attr])
partialSet (ss :: SortSet
ss, ats :: [Attr]
ats) = (SortSet -> SortSet -> SortSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union SortSet
ss SortSet
ss', [Attr]
ats)
      where ss' :: SortSet
ss' = (Symbol -> Symbol) -> SortSet -> SortSet
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> Symbol
partialOp SortSet
ss

partialOp :: Symbol -> Symbol
partialOp :: Symbol -> Symbol
partialOp (Operator q :: Qid
q ss :: [Symbol]
ss s :: Symbol
s) =
  Qid -> [Symbol] -> Symbol -> Symbol
Operator Qid
q ((Symbol -> Symbol) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Symbol
sortSym2kindSym [Symbol]
ss) (Symbol -> Symbol) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol
sortSym2kindSym Symbol
s
partialOp s :: Symbol
s = Symbol
s

sortSym2kindSym :: Symbol -> Symbol
sortSym2kindSym :: Symbol -> Symbol
sortSym2kindSym (Sort q :: Qid
q) = Qid -> Symbol
Kind Qid
q
sortSym2kindSym s :: Symbol
s = Symbol
s

-- | The empty 'Sign'ature.
empty :: Sign
empty :: Sign
empty = Sign :: SortSet
-> SortSet -> SubsortRel -> OpMap -> Sentences -> KindRel -> Sign
Sign {
    sorts :: SortSet
sorts = SortSet
forall a. Set a
Set.empty,
    kinds :: SortSet
kinds = SortSet
forall a. Set a
Set.empty,
    subsorts :: SubsortRel
subsorts = SubsortRel
forall a. Rel a
Rel.empty,
    ops :: OpMap
ops = OpMap
forall k a. Map k a
Map.empty,
    sentences :: Sentences
sentences = Sentences
forall a. Set a
Set.empty,
    kindRel :: KindRel
kindRel = KindRel
forall k a. Map k a
Map.empty
}

inlineSign :: Sign -> Doc
inlineSign :: Sign -> Doc
inlineSign sign :: Sign
sign = let
        descend :: (a -> c -> c) -> Set a -> c -> c
descend = (c -> Set a -> c) -> Set a -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((c -> Set a -> c) -> Set a -> c -> c)
-> ((a -> c -> c) -> c -> Set a -> c)
-> (a -> c -> c)
-> Set a
-> c
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c -> c) -> c -> Set a -> c
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold
        -- print sort declarations
        pr'sorts :: [a] -> Doc
pr'sorts ss :: [a]
ss = if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ss then Doc
Doc.empty else
            [Doc] -> Doc
hsep [String -> Doc
keyword "sorts", [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
ss, Doc
dot]
        -- print subsort declarations
        pr'sups :: SortSet -> Doc
pr'sups = [Doc] -> Doc
hsep ([Doc] -> Doc) -> (SortSet -> [Doc]) -> SortSet -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> Doc) -> [Symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty ([Symbol] -> [Doc]) -> (SortSet -> [Symbol]) -> SortSet -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SortSet -> [Symbol]
forall a. Set a -> [a]
Set.elems
        pr'pair :: a -> SortSet -> [Doc] -> [Doc]
pr'pair sub :: a
sub sups :: SortSet
sups = (:) (Doc -> [Doc] -> [Doc])
-> ([Doc] -> Doc) -> [Doc] -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc] -> Doc
hsep ([Doc] -> [Doc] -> [Doc]) -> [Doc] -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
            [String -> Doc
keyword "subsort", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
sub, Doc
less, SortSet -> Doc
pr'sups SortSet
sups, Doc
dot]
        pr'subs :: Map Symbol SortSet -> Doc
pr'subs = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Map Symbol SortSet -> [Doc]) -> Map Symbol SortSet -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Symbol -> SortSet -> [Doc] -> [Doc])
-> [Doc] -> Map Symbol SortSet -> [Doc]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Symbol -> SortSet -> [Doc] -> [Doc]
forall a. Pretty a => a -> SortSet -> [Doc] -> [Doc]
pr'pair []
        -- print operator decparations
        pr'decl :: a -> a -> Doc
pr'decl attrs :: a
attrs symb :: a
symb = [Doc] -> Doc
hsep
            [String -> Doc
keyword "op", a -> Doc
forall a. Pretty a => a -> Doc
pretty a
symb, a -> Doc
forall a. Pretty a => a -> Doc
pretty a
attrs, Doc
dot]
        pr'ods :: (Set a, a) -> [Doc] -> [Doc]
pr'ods (decls :: Set a
decls, attrs :: a
attrs) = (a -> [Doc] -> [Doc]) -> Set a -> [Doc] -> [Doc]
forall a c. (a -> c -> c) -> Set a -> c -> c
descend ((:) (Doc -> [Doc] -> [Doc]) -> (a -> Doc) -> a -> [Doc] -> [Doc]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> a -> Doc
forall a a. (Pretty a, Pretty a) => a -> a -> Doc
pr'decl a
attrs) Set a
decls
        pr'ocs :: Set (SortSet, [Attr]) -> [Doc] -> [Doc]
pr'ocs = ((SortSet, [Attr]) -> [Doc] -> [Doc])
-> Set (SortSet, [Attr]) -> [Doc] -> [Doc]
forall a c. (a -> c -> c) -> Set a -> c -> c
descend (SortSet, [Attr]) -> [Doc] -> [Doc]
forall a a. (Pretty a, Pretty a) => (Set a, a) -> [Doc] -> [Doc]
pr'ods
        pr'ops :: Map k (Set (SortSet, [Attr])) -> Doc
pr'ops = [Doc] -> Doc
vcat ([Doc] -> Doc)
-> (Map k (Set (SortSet, [Attr])) -> [Doc])
-> Map k (Set (SortSet, [Attr]))
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set (SortSet, [Attr]) -> [Doc] -> [Doc])
-> [Doc] -> Map k (Set (SortSet, [Attr])) -> [Doc]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr Set (SortSet, [Attr]) -> [Doc] -> [Doc]
pr'ocs []
        in [Doc] -> Doc
vcat [ [Symbol] -> Doc
forall a. Pretty a => [a] -> Doc
pr'sorts ([Symbol] -> Doc) -> [Symbol] -> Doc
forall a b. (a -> b) -> a -> b
$ SortSet -> [Symbol]
forall a. Set a -> [a]
Set.elems (SortSet -> [Symbol]) -> SortSet -> [Symbol]
forall a b. (a -> b) -> a -> b
$ Sign -> SortSet
sorts Sign
sign
                , Map Symbol SortSet -> Doc
pr'subs (Map Symbol SortSet -> Doc) -> Map Symbol SortSet -> Doc
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Map Symbol SortSet
forall a. Rel a -> Map a (Set a)
Rel.toMap (SubsortRel -> Map Symbol SortSet)
-> SubsortRel -> Map Symbol SortSet
forall a b. (a -> b) -> a -> b
$ SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a
Rel.transReduce (SubsortRel -> SubsortRel) -> SubsortRel -> SubsortRel
forall a b. (a -> b) -> a -> b
$ Sign -> SubsortRel
subsorts Sign
sign
                , OpMap -> Doc
forall k. Map k (Set (SortSet, [Attr])) -> Doc
pr'ops (OpMap -> Doc) -> OpMap -> Doc
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign ]

-- ** Auxiliary construction

-- | Insert a 'Sort' into a 'Sign'ature.
insertSort :: Sort -> Sign -> Sign
insertSort :: Sort -> Sign -> Sign
insertSort sort :: Sort
sort sign :: Sign
sign = let
    insert :: Sort -> SortSet -> SortSet
insert = Symbol -> SortSet -> SortSet
forall a. Ord a => a -> Set a -> Set a
Set.insert (Symbol -> SortSet -> SortSet)
-> (Sort -> Symbol) -> Sort -> SortSet -> SortSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol
    in Sign
sign {sorts :: SortSet
sorts = Sort -> SortSet -> SortSet
insert Sort
sort (Sign -> SortSet
sorts Sign
sign)}

-- | Insert a 'SubsortDecl' into a 'Sign'ature.
insertSubsort :: SubsortDecl -> Sign -> Sign
insertSubsort :: SubsortDecl -> Sign -> Sign
insertSubsort decl :: SubsortDecl
decl sign :: Sign
sign = let
    insert :: SubsortDecl -> SubsortRel -> SubsortRel
insert (Subsort sub :: Sort
sub super :: Sort
super) = Symbol -> Symbol -> SubsortRel -> SubsortRel
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (Sort -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Sort
sub) (Sort -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Sort
super)
    in Sign
sign {subsorts :: SubsortRel
subsorts = SubsortDecl -> SubsortRel -> SubsortRel
insert SubsortDecl
decl (Sign -> SubsortRel
subsorts Sign
sign)}

-- | Insert an 'Operator' declaration into an 'Operator' 'Map'.
insertOpDecl :: SymbolRel -> Symbol -> [Attr] -> OpMap -> OpMap
insertOpDecl :: SubsortRel -> Symbol -> [Attr] -> OpMap -> OpMap
insertOpDecl rel :: SubsortRel
rel symb :: Symbol
symb attrs :: [Attr]
attrs opmap :: OpMap
opmap = let
    merge :: Set (SortSet, [Attr])
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
merge decls :: Set (SortSet, [Attr])
decls = let
        decl :: (SortSet, [Attr])
decl : _ = Set (SortSet, [Attr]) -> [(SortSet, [Attr])]
forall a. Set a -> [a]
Set.toList Set (SortSet, [Attr])
decls
        syms :: SortSet
syms = Symbol -> SortSet -> SortSet
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
symb (SortSet -> SortSet) -> SortSet -> SortSet
forall a b. (a -> b) -> a -> b
$ (SortSet, [Attr]) -> SortSet
forall a b. (a, b) -> a
fst (SortSet, [Attr])
decl
        attr :: [Attr]
attr = [Attr] -> [Attr]
forall a. Ord a => [a] -> [a]
nubOrd ([Attr] -> [Attr]) -> [Attr] -> [Attr]
forall a b. (a -> b) -> a -> b
$ [Attr] -> [Attr] -> [Attr]
mergeAttrs [Attr]
attrs ([Attr] -> [Attr]) -> [Attr] -> [Attr]
forall a b. (a -> b) -> a -> b
$ (SortSet, [Attr]) -> [Attr]
forall a b. (a, b) -> b
snd (SortSet, [Attr])
decl
        in (SortSet, [Attr]) -> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
forall a. Ord a => a -> Set a -> Set a
Set.insert ((SortSet, [Attr])
 -> Set (SortSet, [Attr]) -> Set (SortSet, [Attr]))
-> (SortSet, [Attr])
-> Set (SortSet, [Attr])
-> Set (SortSet, [Attr])
forall a b. (a -> b) -> a -> b
$ if Set (SortSet, [Attr]) -> Bool
forall a. Set a -> Bool
Set.null Set (SortSet, [Attr])
decls
           then (Symbol -> SortSet
forall a. AsSymbol a => a -> SortSet
asSymbolSet Symbol
symb, [Attr]
attrs)
           else (SortSet
syms, [Attr]
attr)
    name :: Qid
name = Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
symb
    same'kind :: (SortSet, b) -> Bool
same'kind = (Symbol -> Bool) -> SortSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.any (SubsortRel -> Symbol -> Symbol -> Bool
sameKind SubsortRel
rel Symbol
symb) (SortSet -> Bool)
-> ((SortSet, b) -> SortSet) -> (SortSet, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SortSet, b) -> SortSet
forall a b. (a, b) -> a
fst
    old'ops :: Set (SortSet, [Attr])
old'ops = Set (SortSet, [Attr]) -> Qid -> OpMap -> Set (SortSet, [Attr])
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (SortSet, [Attr])
forall a. Set a
Set.empty Qid
name OpMap
opmap
    (same :: Set (SortSet, [Attr])
same, rest :: Set (SortSet, [Attr])
rest) = ((SortSet, [Attr]) -> Bool)
-> Set (SortSet, [Attr])
-> (Set (SortSet, [Attr]), Set (SortSet, [Attr]))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (SortSet, [Attr]) -> Bool
forall b. (SortSet, b) -> Bool
same'kind Set (SortSet, [Attr])
old'ops
    new'ops :: Set (SortSet, [Attr])
new'ops = Set (SortSet, [Attr])
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
merge Set (SortSet, [Attr])
same Set (SortSet, [Attr])
rest
    in Qid -> Set (SortSet, [Attr]) -> OpMap -> OpMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Qid
name Set (SortSet, [Attr])
new'ops OpMap
opmap

-- | Map 'Operator' declarations of the given 'Kind' in an 'Operator' 'Map'.
mapOpDecl :: SymbolRel -> Symbol -> Symbol -> [Attr] -> OpMap -> OpMap
mapOpDecl :: SubsortRel -> Symbol -> Symbol -> [Attr] -> OpMap -> OpMap
mapOpDecl rel :: SubsortRel
rel src :: Symbol
src tgt :: Symbol
tgt attrs :: [Attr]
attrs opmap :: OpMap
opmap = let
    merge :: Set (a, [Attr]) -> Set (a, [Attr]) -> Set (a, [Attr])
merge decls :: Set (a, [Attr])
decls = case Set (a, [Attr]) -> [(a, [Attr])]
forall a. Set a -> [a]
Set.toList Set (a, [Attr])
decls of
        [] -> Set (a, [Attr]) -> Set (a, [Attr])
forall a. a -> a
id
        (ft :: a
ft, sd :: [Attr]
sd) : _ -> let
          syms :: a
syms = KindRel -> a -> a
forall a. HasOps a => KindRel -> a -> a
mapOps (Symbol -> Symbol -> KindRel
forall k a. k -> a -> Map k a
Map.singleton Symbol
src Symbol
tgt) a
ft
          attr :: [Attr]
attr = [Attr] -> [Attr]
forall a. Ord a => [a] -> [a]
nubOrd ([Attr] -> [Attr]) -> [Attr] -> [Attr]
forall a b. (a -> b) -> a -> b
$ [Attr] -> [Attr] -> [Attr]
mergeAttrs [Attr]
attrs [Attr]
sd
          in (a, [Attr]) -> Set (a, [Attr]) -> Set (a, [Attr])
forall a. Ord a => a -> Set a -> Set a
Set.insert (a
syms, [Attr]
attr)
    src'name :: Qid
src'name = Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
src
    tgt'name :: Qid
tgt'name = Symbol -> Qid
forall a. HasName a => a -> Qid
getName Symbol
tgt
    same'kind :: (SortSet, b) -> Bool
same'kind = (Symbol -> Bool) -> SortSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.any (SubsortRel -> Symbol -> Symbol -> Bool
sameKind SubsortRel
rel Symbol
src) (SortSet -> Bool)
-> ((SortSet, b) -> SortSet) -> (SortSet, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SortSet, b) -> SortSet
forall a b. (a, b) -> a
fst
    src'ops :: Set (SortSet, [Attr])
src'ops = Set (SortSet, [Attr]) -> Qid -> OpMap -> Set (SortSet, [Attr])
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (SortSet, [Attr])
forall a. Set a
Set.empty Qid
src'name OpMap
opmap
    tgt'ops :: Set (SortSet, [Attr])
tgt'ops = Set (SortSet, [Attr]) -> Qid -> OpMap -> Set (SortSet, [Attr])
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Set (SortSet, [Attr])
forall a. Set a
Set.empty Qid
tgt'name OpMap
opmap
    (same :: Set (SortSet, [Attr])
same, rest :: Set (SortSet, [Attr])
rest) = ((SortSet, [Attr]) -> Bool)
-> Set (SortSet, [Attr])
-> (Set (SortSet, [Attr]), Set (SortSet, [Attr]))
forall a. (a -> Bool) -> Set a -> (Set a, Set a)
Set.partition (SortSet, [Attr]) -> Bool
forall b. (SortSet, b) -> Bool
same'kind Set (SortSet, [Attr])
src'ops
    has'rest :: Maybe (Set (SortSet, [Attr]))
has'rest = if Set (SortSet, [Attr]) -> Bool
forall a. Set a -> Bool
Set.null Set (SortSet, [Attr])
rest then Maybe (Set (SortSet, [Attr]))
forall a. Maybe a
Nothing else Set (SortSet, [Attr]) -> Maybe (Set (SortSet, [Attr]))
forall a. a -> Maybe a
Just Set (SortSet, [Attr])
rest
    set'decl :: OpMap -> OpMap
set'decl = Qid -> Set (SortSet, [Attr]) -> OpMap -> OpMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Qid
tgt'name (Set (SortSet, [Attr]) -> OpMap -> OpMap)
-> Set (SortSet, [Attr]) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Set (SortSet, [Attr])
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
forall a.
(Ord a, HasOps a) =>
Set (a, [Attr]) -> Set (a, [Attr]) -> Set (a, [Attr])
merge Set (SortSet, [Attr])
same Set (SortSet, [Attr])
tgt'ops
    set'rest :: OpMap -> OpMap
set'rest = (Set (SortSet, [Attr]) -> Maybe (Set (SortSet, [Attr])))
-> Qid -> OpMap -> OpMap
forall k a. Ord k => (a -> Maybe a) -> k -> Map k a -> Map k a
Map.update (Maybe (Set (SortSet, [Attr]))
-> Set (SortSet, [Attr]) -> Maybe (Set (SortSet, [Attr]))
forall a b. a -> b -> a
const Maybe (Set (SortSet, [Attr]))
has'rest) Qid
src'name
    in OpMap -> OpMap
set'rest (OpMap -> OpMap) -> (OpMap -> OpMap) -> OpMap -> OpMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> OpMap
set'decl (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ OpMap
opmap

-- | Insert an 'Operator' declaration into a 'Sign'ature.
insertOp :: Operator -> Sign -> Sign
insertOp :: Operator -> Sign -> Sign
insertOp op :: Operator
op sign :: Sign
sign = let
    subrel :: SubsortRel
subrel = Sign -> SubsortRel
subsorts Sign
sign
    insert :: Operator -> OpMap -> OpMap
insert (Op _ _ _ as :: [Attr]
as) = SubsortRel -> Symbol -> [Attr] -> OpMap -> OpMap
insertOpDecl SubsortRel
subrel (Operator -> Symbol
forall a. AsSymbol a => a -> Symbol
asSymbol Operator
op) [Attr]
as
    in Sign
sign {ops :: OpMap
ops = Operator -> OpMap -> OpMap
insert Operator
op (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign}

-- | Merge new 'Attr'ibutes with the old ones.
mergeAttrs :: [Attr] -> [Attr] -> [Attr]
mergeAttrs :: [Attr] -> [Attr] -> [Attr]
mergeAttrs = let
    similar :: Attr -> Attr -> Bool
similar (Prec _) (Prec _) = Bool
True
    similar (Gather _) (Gather _) = Bool
True
    similar (Format _) (Format _) = Bool
True
    -- Other Attributes don't change in Renamings.
    similar _ _ = Bool
False
    update :: Attr -> [Attr] -> [Attr]
update new :: Attr
new = (:) Attr
new ([Attr] -> [Attr]) -> ([Attr] -> [Attr]) -> [Attr] -> [Attr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Attr -> Bool) -> [Attr] -> [Attr]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Attr -> Bool) -> Attr -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Attr -> Attr -> Bool
similar Attr
new)
    in ([Attr] -> [Attr] -> [Attr]) -> [Attr] -> [Attr] -> [Attr]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (([Attr] -> [Attr] -> [Attr]) -> [Attr] -> [Attr] -> [Attr])
-> ([Attr] -> [Attr] -> [Attr]) -> [Attr] -> [Attr] -> [Attr]
forall a b. (a -> b) -> a -> b
$ ([Attr] -> Attr -> [Attr]) -> [Attr] -> [Attr] -> [Attr]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (([Attr] -> Attr -> [Attr]) -> [Attr] -> [Attr] -> [Attr])
-> ([Attr] -> Attr -> [Attr]) -> [Attr] -> [Attr] -> [Attr]
forall a b. (a -> b) -> a -> b
$ (Attr -> [Attr] -> [Attr]) -> [Attr] -> Attr -> [Attr]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Attr -> [Attr] -> [Attr]
update

-- * Combination

-- | The union of two 'Sign'atures.
union :: Sign -> Sign -> Sign
union :: Sign -> Sign -> Sign
union sig1 :: Sign
sig1 sig2 :: Sign
sig2 = let
    apply :: (t -> t -> t) -> (Sign -> t) -> t
apply func :: t -> t -> t
func items :: Sign -> t
items = t -> t -> t
func (Sign -> t
items Sign
sig1) (Sign -> t
items Sign
sig2)
    kr :: KindRel
kr = SortSet -> SubsortRel -> KindRel
getkindRel ((SortSet -> SortSet -> SortSet) -> (Sign -> SortSet) -> SortSet
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SortSet -> SortSet -> SortSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union Sign -> SortSet
sorts) ((SubsortRel -> SubsortRel -> SubsortRel)
-> (Sign -> SubsortRel) -> SubsortRel
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SubsortRel -> SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Sign -> SubsortRel
subsorts)
    in Sign :: SortSet
-> SortSet -> SubsortRel -> OpMap -> Sentences -> KindRel -> Sign
Sign {
        sorts :: SortSet
sorts = (SortSet -> SortSet -> SortSet) -> (Sign -> SortSet) -> SortSet
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SortSet -> SortSet -> SortSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union Sign -> SortSet
sorts,
        kinds :: SortSet
kinds = KindRel -> SortSet
kindsFromMap KindRel
kr,
        subsorts :: SubsortRel
subsorts = (SubsortRel -> SubsortRel -> SubsortRel)
-> (Sign -> SubsortRel) -> SubsortRel
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SubsortRel -> SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Sign -> SubsortRel
subsorts,
        ops :: OpMap
ops = (OpMap -> OpMap -> OpMap) -> (Sign -> OpMap) -> OpMap
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply ((Set (SortSet, [Attr])
 -> Set (SortSet, [Attr]) -> Set (SortSet, [Attr]))
-> OpMap -> OpMap -> OpMap
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Set (SortSet, [Attr])
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
forall a. Ord a => Set a -> Set a -> Set a
Set.union) Sign -> OpMap
ops,
        sentences :: Sentences
sentences = (Sentences -> Sentences -> Sentences)
-> (Sign -> Sentences) -> Sentences
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply Sentences -> Sentences -> Sentences
forall a. Ord a => Set a -> Set a -> Set a
Set.union Sign -> Sentences
sentences,
        kindRel :: KindRel
kindRel = KindRel
kr
    }

-- | The intersection of two 'Sign'atures.
intersection :: Sign -> Sign -> Sign
intersection :: Sign -> Sign -> Sign
intersection sig1 :: Sign
sig1 sig2 :: Sign
sig2 = let
    apply :: (t -> t -> t) -> (Sign -> t) -> t
apply func :: t -> t -> t
func items :: Sign -> t
items = t -> t -> t
func (Sign -> t
items Sign
sig1) (Sign -> t
items Sign
sig2)
    kr :: KindRel
kr = SortSet -> SubsortRel -> KindRel
getkindRel ((SortSet -> SortSet -> SortSet) -> (Sign -> SortSet) -> SortSet
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SortSet -> SortSet -> SortSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union Sign -> SortSet
sorts) ((SubsortRel -> SubsortRel -> SubsortRel)
-> (Sign -> SubsortRel) -> SubsortRel
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SubsortRel -> SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union Sign -> SubsortRel
subsorts)
    in Sign :: SortSet
-> SortSet -> SubsortRel -> OpMap -> Sentences -> KindRel -> Sign
Sign {
        sorts :: SortSet
sorts = (SortSet -> SortSet -> SortSet) -> (Sign -> SortSet) -> SortSet
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SortSet -> SortSet -> SortSet
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Sign -> SortSet
sorts,
        kinds :: SortSet
kinds = KindRel -> SortSet
kindsFromMap KindRel
kr,
        subsorts :: SubsortRel
subsorts = (SubsortRel -> SubsortRel -> SubsortRel)
-> (Sign -> SubsortRel) -> SubsortRel
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SubsortRel -> SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.intersection Sign -> SubsortRel
subsorts,
        ops :: OpMap
ops = (OpMap -> OpMap -> OpMap) -> (Sign -> OpMap) -> OpMap
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply OpMap -> OpMap -> OpMap
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection Sign -> OpMap
ops,
        sentences :: Sentences
sentences = (Sentences -> Sentences -> Sentences)
-> (Sign -> Sentences) -> Sentences
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply Sentences -> Sentences -> Sentences
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Sign -> Sentences
sentences,
        kindRel :: KindRel
kindRel = KindRel
kr
    }

-- * Conversion

-- | Extract the 'Set' of all 'Symbol's from a 'Sign'ature.
symbols :: Sign -> SymbolSet
symbols :: Sign -> SortSet
symbols sign :: Sign
sign = [SortSet] -> SortSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [ Sign -> SortSet
forall a. HasSorts a => a -> SortSet
getSorts Sign
sign, Sign -> SortSet
forall a. HasOps a => a -> SortSet
getOps Sign
sign, Sign -> SortSet
forall a. HasLabels a => a -> SortSet
getLabels Sign
sign ]

-- * Testing

-- | True iff the argument is a legal 'Sign'ature.
isLegal :: Sign -> Bool
isLegal :: Sign -> Bool
isLegal sign :: Sign
sign = let
    has'sort :: Symbol -> Bool
has'sort sort :: Symbol
sort = Symbol -> SortSet -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Symbol -> Symbol
asSort Symbol
sort) (Sign -> SortSet
sorts Sign
sign)
    has'subsorts :: Bool
has'subsorts = (Symbol -> Bool) -> SortSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.all Symbol -> Bool
has'sort (SortSet -> Bool) -> (SubsortRel -> SortSet) -> SubsortRel -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SubsortRel -> SortSet
forall a. HasSorts a => a -> SortSet
getSorts (SubsortRel -> Bool) -> SubsortRel -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> SubsortRel
subsorts Sign
sign
    has'ops :: Bool
has'ops = (Symbol -> Bool) -> SortSet -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
Fold.all Symbol -> Bool
has'sort (SortSet -> Bool) -> (OpMap -> SortSet) -> OpMap -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. OpMap -> SortSet
forall a. HasSorts a => a -> SortSet
getSorts (OpMap -> Bool) -> OpMap -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> OpMap
ops Sign
sign
    in Bool
has'subsorts Bool -> Bool -> Bool
&& Bool
has'ops

-- | True iff the first argument is a subsignature of the second.
isSubsign :: Sign -> Sign -> Bool
isSubsign :: Sign -> Sign -> Bool
isSubsign sig1 :: Sign
sig1 sig2 :: Sign
sig2 = let
    apply :: (t -> t -> t) -> (Sign -> t) -> t
apply func :: t -> t -> t
func items :: Sign -> t
items = t -> t -> t
func (Sign -> t
items Sign
sig1) (Sign -> t
items Sign
sig2)
    has'sorts :: Bool
has'sorts = (SortSet -> SortSet -> Bool) -> (Sign -> SortSet) -> Bool
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SortSet -> SortSet -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Sign -> SortSet
sorts
    has'subsorts :: Bool
has'subsorts = (SubsortRel -> SubsortRel -> Bool) -> (Sign -> SubsortRel) -> Bool
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply SubsortRel -> SubsortRel -> Bool
forall a. Ord a => Rel a -> Rel a -> Bool
Rel.isSubrelOf Sign -> SubsortRel
subsorts
    has'ops :: Bool
has'ops = (OpMap -> OpMap -> Bool) -> (Sign -> OpMap) -> Bool
forall t t. (t -> t -> t) -> (Sign -> t) -> t
apply ((Set (SortSet, [Attr]) -> Set (SortSet, [Attr]) -> Bool)
-> OpMap -> OpMap -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy Set (SortSet, [Attr]) -> Set (SortSet, [Attr]) -> Bool
subODS) Sign -> OpMap
ops
    in Bool
has'sorts Bool -> Bool -> Bool
&& Bool
has'subsorts Bool -> Bool -> Bool
&& Bool
has'ops

subODS :: OpDeclSet -> OpDeclSet -> Bool
subODS :: Set (SortSet, [Attr]) -> Set (SortSet, [Attr]) -> Bool
subODS ods1 :: Set (SortSet, [Attr])
ods1 ods2 :: Set (SortSet, [Attr])
ods2 = Set (SortSet, [Attr]) -> Set (SortSet, [Attr]) -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set (SortSet, [Attr])
ods1' Set (SortSet, [Attr])
ods2'
    where ods1' :: Set (SortSet, [Attr])
ods1' = Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
removeAttsODS Set (SortSet, [Attr])
ods1
          ods2' :: Set (SortSet, [Attr])
ods2' = Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
removeAttsODS Set (SortSet, [Attr])
ods2

removeAttsODS :: OpDeclSet -> OpDeclSet
removeAttsODS :: Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
removeAttsODS = ((SortSet, [Attr]) -> (SortSet, [Attr]))
-> Set (SortSet, [Attr]) -> Set (SortSet, [Attr])
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (SortSet, [Attr]) -> (SortSet, [Attr])
removeAtts

removeAtts :: (Set Symbol, [Attr]) -> (Set Symbol, [Attr])
removeAtts :: (SortSet, [Attr]) -> (SortSet, [Attr])
removeAtts (ss :: SortSet
ss, _) = (SortSet
ss, [])

-- * Modification

-- TODO: Add real implementation of simplification. Maybe.

-- | Simplification of sentences (leave out qualifications)
simplifySentence :: Sign -> Sentence -> Sentence
simplifySentence :: Sign -> Sentence -> Sentence
simplifySentence _ = Sentence -> Sentence
forall a. a -> a
id

-- | Rename the given 'Sort' in the given 'Sign'ature.
renameSort :: Symbol -> Symbol -> Sign -> Sign
renameSort :: Symbol -> Symbol -> Sign -> Sign
renameSort from :: Symbol
from to :: Symbol
to = KindRel -> Sign -> Sign
forall a. HasSorts a => KindRel -> a -> a
mapSorts (KindRel -> Sign -> Sign) -> KindRel -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> KindRel
forall k a. k -> a -> Map k a
Map.singleton Symbol
from Symbol
to

-- | Rename the given 'Label' in the given 'Sign'ature.
renameLabel :: Symbol -> Symbol -> Sign -> Sign
renameLabel :: Symbol -> Symbol -> Sign -> Sign
renameLabel from :: Symbol
from to :: Symbol
to = KindRel -> Sign -> Sign
forall a. HasLabels a => KindRel -> a -> a
mapLabels (KindRel -> Sign -> Sign) -> KindRel -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Symbol -> Symbol -> KindRel
forall k a. k -> a -> Map k a
Map.singleton Symbol
from Symbol
to

-- | Rename the given 'Operator' in the given 'Sign'ature.
renameOp :: Symbol -> Symbol -> [Attr] -> Sign -> Sign
renameOp :: Symbol -> Symbol -> [Attr] -> Sign -> Sign
renameOp from :: Symbol
from to :: Symbol
to attrs :: [Attr]
attrs sign :: Sign
sign = let
    subrel :: SubsortRel
subrel = Sign -> SubsortRel
subsorts Sign
sign
    opmap :: OpMap
opmap = Sign -> OpMap
ops Sign
sign
    mapped :: OpMap
mapped = SubsortRel -> Symbol -> Symbol -> [Attr] -> OpMap -> OpMap
mapOpDecl SubsortRel
subrel Symbol
from Symbol
to [Attr]
attrs OpMap
opmap
    in Sign
sign { ops :: OpMap
ops = OpMap
mapped }

getkindRel :: SortSet -> SubsortRel -> KindRel
getkindRel :: SortSet -> SubsortRel -> KindRel
getkindRel ss :: SortSet
ss r :: SubsortRel
r = [Symbol] -> SubsortRel -> KindRel -> KindRel
kindRelList (SortSet -> [Symbol]
forall a. Set a -> [a]
Set.toList SortSet
ss) SubsortRel
r KindRel
forall k a. Map k a
Map.empty

kindRelList :: [Symbol] -> SubsortRel -> KindRel -> KindRel
kindRelList :: [Symbol] -> SubsortRel -> KindRel -> KindRel
kindRelList [] _ m :: KindRel
m = KindRel
m
kindRelList l :: [Symbol]
l@(s :: Symbol
s : _) r :: SubsortRel
r m :: KindRel
m = [Symbol] -> SubsortRel -> KindRel -> KindRel
kindRelList [Symbol]
not_rel SubsortRel
r KindRel
m'
      where (top :: Symbol
top : _) = [Symbol] -> [Symbol]
forall a. Ord a => [a] -> [a]
List.sort ([Symbol] -> [Symbol]) -> [Symbol] -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Symbol -> [Symbol]
getTop SubsortRel
r Symbol
s
            tc :: SubsortRel
tc = SubsortRel -> SubsortRel
forall a. Ord a => Rel a -> Rel a
Rel.transClosure SubsortRel
r
            (rel :: [Symbol]
rel, not_rel :: [Symbol]
not_rel) = Symbol -> SubsortRel -> [Symbol] -> ([Symbol], [Symbol])
sameKindList Symbol
s SubsortRel
tc [Symbol]
l
            f :: Symbol -> k -> Map k Symbol -> Map k Symbol
f x :: Symbol
x y :: k
y = k -> Symbol -> Map k Symbol -> Map k Symbol
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert k
y (Symbol -> Symbol
sortSym2kindSym Symbol
x)
            m' :: KindRel
m' = (Symbol -> KindRel -> KindRel) -> KindRel -> [Symbol] -> KindRel
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Symbol -> Symbol -> KindRel -> KindRel
forall k. Ord k => Symbol -> k -> Map k Symbol -> Map k Symbol
f Symbol
top) KindRel
m [Symbol]
rel

sameKindList :: Symbol -> SubsortRel -> [Symbol] -> ([Symbol], [Symbol])
sameKindList :: Symbol -> SubsortRel -> [Symbol] -> ([Symbol], [Symbol])
sameKindList _ _ [] = ([], [])
sameKindList t :: Symbol
t r :: SubsortRel
r (t' :: Symbol
t' : ts :: [Symbol]
ts) = if SubsortRel -> Symbol -> Symbol -> Bool
sameKind SubsortRel
r Symbol
t Symbol
t'
                       then (Symbol
t' Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
hold, [Symbol]
not_hold)
                       else ([Symbol]
hold, Symbol
t' Symbol -> [Symbol] -> [Symbol]
forall a. a -> [a] -> [a]
: [Symbol]
not_hold)
      where (hold :: [Symbol]
hold, not_hold :: [Symbol]
not_hold) = Symbol -> SubsortRel -> [Symbol] -> ([Symbol], [Symbol])
sameKindList Symbol
t SubsortRel
r [Symbol]
ts

getTop :: SubsortRel -> Symbol -> [Symbol]
getTop :: SubsortRel -> Symbol -> [Symbol]
getTop r :: SubsortRel
r tok :: Symbol
tok = case [Symbol]
succs of
           [] -> [Symbol
tok]
           toks :: [Symbol]
toks@(_ : _) -> (Symbol -> [Symbol]) -> [Symbol] -> [Symbol]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SubsortRel -> Symbol -> [Symbol]
getTop SubsortRel
r) [Symbol]
toks
      where succs :: [Symbol]
succs = SortSet -> [Symbol]
forall a. Set a -> [a]
Set.toList (SortSet -> [Symbol]) -> SortSet -> [Symbol]
forall a b. (a -> b) -> a -> b
$ SubsortRel -> Symbol -> SortSet
forall a. Ord a => Rel a -> a -> Set a
Rel.succs SubsortRel
r Symbol
tok

kindsFromMap :: KindRel -> KindSet
kindsFromMap :: KindRel -> SortSet
kindsFromMap kr :: KindRel
kr = ((Symbol, Symbol) -> SortSet -> SortSet)
-> SortSet -> [(Symbol, Symbol)] -> SortSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, y :: Symbol
y) z :: SortSet
z -> Symbol -> SortSet -> SortSet
forall a. Ord a => a -> Set a -> Set a
Set.insert Symbol
y SortSet
z) SortSet
forall a. Set a
Set.empty [(Symbol, Symbol)]
krl
      where krl :: [(Symbol, Symbol)]
krl = KindRel -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList KindRel
kr

getSortsKindRel :: KindRel -> SymbolSet
getSortsKindRel :: KindRel -> SortSet
getSortsKindRel = (Symbol -> Symbol -> SortSet -> SortSet)
-> SortSet -> KindRel -> SortSet
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Symbol -> Symbol -> SortSet -> SortSet
forall a p. Ord a => a -> p -> Set a -> Set a
f SortSet
forall a. Set a
Set.empty
      where f :: a -> p -> Set a -> Set a
f k :: a
k _ = a -> Set a -> Set a
forall a. Ord a => a -> Set a -> Set a
Set.insert a
k

renameSortKindRel :: Map Symbol Symbol -> KindRel -> KindRel
renameSortKindRel :: KindRel -> KindRel -> KindRel
renameSortKindRel m :: KindRel
m kr :: KindRel
kr = KindRel
kr'
      where krl :: [(Symbol, Symbol)]
krl = KindRel -> [(Symbol, Symbol)]
forall k a. Map k a -> [(k, a)]
Map.toList KindRel
kr
            f :: KindRel -> (a, b) -> [(a, b)] -> [(a, b)]
f mss :: KindRel
mss (x :: a
x, y :: b
y) = ((KindRel -> a -> a
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mss a
x, KindRel -> b -> b
forall a. HasSorts a => KindRel -> a -> a
mapSorts KindRel
mss b
y) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
:)
            krl' :: [(Symbol, Symbol)]
krl' = ((Symbol, Symbol) -> [(Symbol, Symbol)] -> [(Symbol, Symbol)])
-> [(Symbol, Symbol)] -> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (KindRel
-> (Symbol, Symbol) -> [(Symbol, Symbol)] -> [(Symbol, Symbol)]
forall a b.
(HasSorts a, HasSorts b) =>
KindRel -> (a, b) -> [(a, b)] -> [(a, b)]
f KindRel
m) [] [(Symbol, Symbol)]
krl
            kr' :: KindRel
kr' = [(Symbol, Symbol)] -> KindRel
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [(Symbol, Symbol)]
krl'