{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Maude/Symbol.hs
Description :  Maude Symbols
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 symbols for Maude.
-}

module Maude.Symbol (
    {- * Types
    The Symbol type -}
    Symbol (..),
    -- ** Auxiliary types
    Symbols,
    SymbolSet,
    SymbolMap,
    SymbolRel,
    SymbolKind (..),
    sym_kind,
    kindSym2sortSym,
    -- * Conversion
    toId,
    qualify,
    asSort,
    asKind,
    toType,
    toOperator,
    -- * Construction
    mkOpTotal,
    mkOpPartial,
    -- * Testing
    sameKind,
) where

import Maude.AS_Maude
import Maude.Meta.HasName

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

import Common.Id (Id, mkId, mkSimpleId, GetRange, getRange, nullRange)
import Common.Doc
import Common.DocUtils (Pretty (..))

import Data.Maybe (fromJust)

-- * Types

{- ** The Symbol type
A 'Sort', 'Kind', 'Label', or 'Operator'. -}
data Symbol = Sort Qid                      -- ^ A 'Sort' Symbol
            | Kind Qid                      -- ^ A 'Kind' Symbol
            | Labl Qid                      -- ^ A 'Label' Symbol
            | Operator Qid Symbols Symbol   -- ^ A qualified 'Operator' Symbol
            | OpWildcard Qid                -- ^ A wildcard 'Operator' Symbol
            deriving (Int -> Symbol -> ShowS
[Symbol] -> ShowS
Symbol -> String
(Int -> Symbol -> ShowS)
-> (Symbol -> String) -> ([Symbol] -> ShowS) -> Show Symbol
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symbol] -> ShowS
$cshowList :: [Symbol] -> ShowS
show :: Symbol -> String
$cshow :: Symbol -> String
showsPrec :: Int -> Symbol -> ShowS
$cshowsPrec :: Int -> Symbol -> ShowS
Show, ReadPrec [Symbol]
ReadPrec Symbol
Int -> ReadS Symbol
ReadS [Symbol]
(Int -> ReadS Symbol)
-> ReadS [Symbol]
-> ReadPrec Symbol
-> ReadPrec [Symbol]
-> Read Symbol
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Symbol]
$creadListPrec :: ReadPrec [Symbol]
readPrec :: ReadPrec Symbol
$creadPrec :: ReadPrec Symbol
readList :: ReadS [Symbol]
$creadList :: ReadS [Symbol]
readsPrec :: Int -> ReadS Symbol
$creadsPrec :: Int -> ReadS Symbol
Read, Eq Symbol
Eq Symbol =>
(Symbol -> Symbol -> Ordering)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Symbol)
-> (Symbol -> Symbol -> Symbol)
-> Ord Symbol
Symbol -> Symbol -> Bool
Symbol -> Symbol -> Ordering
Symbol -> Symbol -> Symbol
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 :: Symbol -> Symbol -> Symbol
$cmin :: Symbol -> Symbol -> Symbol
max :: Symbol -> Symbol -> Symbol
$cmax :: Symbol -> Symbol -> Symbol
>= :: Symbol -> Symbol -> Bool
$c>= :: Symbol -> Symbol -> Bool
> :: Symbol -> Symbol -> Bool
$c> :: Symbol -> Symbol -> Bool
<= :: Symbol -> Symbol -> Bool
$c<= :: Symbol -> Symbol -> Bool
< :: Symbol -> Symbol -> Bool
$c< :: Symbol -> Symbol -> Bool
compare :: Symbol -> Symbol -> Ordering
$ccompare :: Symbol -> Symbol -> Ordering
$cp1Ord :: Eq Symbol
Ord, Symbol -> Symbol -> Bool
(Symbol -> Symbol -> Bool)
-> (Symbol -> Symbol -> Bool) -> Eq Symbol
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol -> Symbol -> Bool
$c/= :: Symbol -> Symbol -> Bool
== :: Symbol -> Symbol -> Bool
$c== :: Symbol -> Symbol -> Bool
Eq, Typeable)
-- ** Auxiliary types
type Symbols = [Symbol]
type SymbolSet = Set Symbol
type SymbolMap = Map Symbol Symbol
type SymbolRel = Rel Symbol

data SymbolKind = SortK | KindK | LablK | OpK 
        deriving (Int -> SymbolKind -> ShowS
[SymbolKind] -> ShowS
SymbolKind -> String
(Int -> SymbolKind -> ShowS)
-> (SymbolKind -> String)
-> ([SymbolKind] -> ShowS)
-> Show SymbolKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymbolKind] -> ShowS
$cshowList :: [SymbolKind] -> ShowS
show :: SymbolKind -> String
$cshow :: SymbolKind -> String
showsPrec :: Int -> SymbolKind -> ShowS
$cshowsPrec :: Int -> SymbolKind -> ShowS
Show, ReadPrec [SymbolKind]
ReadPrec SymbolKind
Int -> ReadS SymbolKind
ReadS [SymbolKind]
(Int -> ReadS SymbolKind)
-> ReadS [SymbolKind]
-> ReadPrec SymbolKind
-> ReadPrec [SymbolKind]
-> Read SymbolKind
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [SymbolKind]
$creadListPrec :: ReadPrec [SymbolKind]
readPrec :: ReadPrec SymbolKind
$creadPrec :: ReadPrec SymbolKind
readList :: ReadS [SymbolKind]
$creadList :: ReadS [SymbolKind]
readsPrec :: Int -> ReadS SymbolKind
$creadsPrec :: Int -> ReadS SymbolKind
Read, Eq SymbolKind
Eq SymbolKind =>
(SymbolKind -> SymbolKind -> Ordering)
-> (SymbolKind -> SymbolKind -> Bool)
-> (SymbolKind -> SymbolKind -> Bool)
-> (SymbolKind -> SymbolKind -> Bool)
-> (SymbolKind -> SymbolKind -> Bool)
-> (SymbolKind -> SymbolKind -> SymbolKind)
-> (SymbolKind -> SymbolKind -> SymbolKind)
-> Ord SymbolKind
SymbolKind -> SymbolKind -> Bool
SymbolKind -> SymbolKind -> Ordering
SymbolKind -> SymbolKind -> SymbolKind
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 :: SymbolKind -> SymbolKind -> SymbolKind
$cmin :: SymbolKind -> SymbolKind -> SymbolKind
max :: SymbolKind -> SymbolKind -> SymbolKind
$cmax :: SymbolKind -> SymbolKind -> SymbolKind
>= :: SymbolKind -> SymbolKind -> Bool
$c>= :: SymbolKind -> SymbolKind -> Bool
> :: SymbolKind -> SymbolKind -> Bool
$c> :: SymbolKind -> SymbolKind -> Bool
<= :: SymbolKind -> SymbolKind -> Bool
$c<= :: SymbolKind -> SymbolKind -> Bool
< :: SymbolKind -> SymbolKind -> Bool
$c< :: SymbolKind -> SymbolKind -> Bool
compare :: SymbolKind -> SymbolKind -> Ordering
$ccompare :: SymbolKind -> SymbolKind -> Ordering
$cp1Ord :: Eq SymbolKind
Ord, SymbolKind -> SymbolKind -> Bool
(SymbolKind -> SymbolKind -> Bool)
-> (SymbolKind -> SymbolKind -> Bool) -> Eq SymbolKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymbolKind -> SymbolKind -> Bool
$c/= :: SymbolKind -> SymbolKind -> Bool
== :: SymbolKind -> SymbolKind -> Bool
$c== :: SymbolKind -> SymbolKind -> Bool
Eq, Typeable)

-- | the kind of a symbol

sym_kind :: Symbol -> SymbolKind
sym_kind :: Symbol -> SymbolKind
sym_kind (Sort _) = SymbolKind
SortK
sym_kind (Kind _) = SymbolKind
KindK
sym_kind (Labl _) = SymbolKind
LablK
sym_kind _ = SymbolKind
OpK

instance Pretty SymbolKind where 
 pretty :: SymbolKind -> Doc
pretty k :: SymbolKind
k = case SymbolKind
k of
   SortK -> String -> Doc
text "sort"
   KindK -> String -> Doc
text "kind"
   LablK -> String -> Doc
text "label"
   OpK   -> String -> Doc
text "op"


 


-- ** Symbol instances

instance HasName Symbol where
    getName :: Symbol -> Qid
getName symb :: Symbol
symb = case Symbol
symb of
        Sort qid :: Qid
qid -> Qid
qid
        Kind qid :: Qid
qid -> Qid
qid
        Labl qid :: Qid
qid -> Qid
qid
        OpWildcard qid :: Qid
qid -> Qid
qid
        Operator qid :: Qid
qid _ _ -> Qid
qid
    mapName :: (Qid -> Qid) -> Symbol -> Symbol
mapName mp :: Qid -> Qid
mp symb :: Symbol
symb = case Symbol
symb of
        Sort qid :: Qid
qid -> Qid -> Symbol
Sort (Qid -> Symbol) -> Qid -> Symbol
forall a b. (a -> b) -> a -> b
$ (Qid -> Qid) -> Qid -> Qid
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName Qid -> Qid
mp Qid
qid
        Kind qid :: Qid
qid -> Qid -> Symbol
Kind (Qid -> Symbol) -> Qid -> Symbol
forall a b. (a -> b) -> a -> b
$ (Qid -> Qid) -> Qid -> Qid
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName Qid -> Qid
mp Qid
qid
        Labl qid :: Qid
qid -> Qid -> Symbol
Labl (Qid -> Symbol) -> Qid -> Symbol
forall a b. (a -> b) -> a -> b
$ (Qid -> Qid) -> Qid -> Qid
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName Qid -> Qid
mp Qid
qid
        OpWildcard qid :: Qid
qid -> Qid -> Symbol
OpWildcard (Qid -> Symbol) -> Qid -> Symbol
forall a b. (a -> b) -> a -> b
$ (Qid -> Qid) -> Qid -> Qid
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName Qid -> Qid
mp Qid
qid
        Operator qid :: Qid
qid dom :: [Symbol]
dom cod :: Symbol
cod -> Qid -> [Symbol] -> Symbol -> Symbol
Operator ((Qid -> Qid) -> Qid -> Qid
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName Qid -> Qid
mp Qid
qid) [Symbol]
dom Symbol
cod

instance Pretty Symbol where
    pretty :: Symbol -> Doc
pretty symb :: Symbol
symb = case Symbol
symb of
        Sort qid :: Qid
qid -> Qid -> Doc
forall a. Pretty a => a -> Doc
pretty Qid
qid
        Kind qid :: Qid
qid -> Doc -> Doc
brackets (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Qid -> Doc
forall a. Pretty a => a -> Doc
pretty Qid
qid
        Labl qid :: Qid
qid -> Qid -> Doc
forall a. Pretty a => a -> Doc
pretty Qid
qid
        OpWildcard qid :: Qid
qid -> Qid -> Doc
forall a. Pretty a => a -> Doc
pretty Qid
qid
        Operator qid :: Qid
qid dom :: [Symbol]
dom cod :: Symbol
cod -> [Doc] -> Doc
hsep
            [Qid -> Doc
forall a. Pretty a => a -> Doc
pretty Qid
qid, Doc
colon, [Doc] -> Doc
hsep ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Symbol -> Doc) -> [Symbol] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty [Symbol]
dom, Doc
funArrow, Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
cod]

instance GetRange Symbol where
    getRange :: Symbol -> Range
getRange _ = Range
nullRange

-- * Conversion

-- | Convert 'Symbol' to 'Id'.
toId :: Symbol -> Id
toId :: Symbol -> Id
toId = [Qid] -> Id
mkId ([Qid] -> Id) -> (Symbol -> [Qid]) -> Symbol -> Id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qid -> [Qid]
forall (m :: * -> *) a. Monad m => a -> m a
return (Qid -> [Qid]) -> (Symbol -> Qid) -> Symbol -> [Qid]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Qid
forall a. HasName a => a -> Qid
getName

-- | Qualify the 'Symbol' name with a 'Qid'.
qualify :: Qid -> Symbol -> Symbol
qualify :: Qid -> Symbol -> Symbol
qualify qid :: Qid
qid = let prepend :: a -> Qid
prepend sym :: a
sym = String -> Qid
mkSimpleId (String -> Qid) -> String -> Qid
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [Qid -> String
forall a. Show a => a -> String
show Qid
qid, "$", a -> String
forall a. Show a => a -> String
show a
sym]
              in (Qid -> Qid) -> Symbol -> Symbol
forall a. HasName a => (Qid -> Qid) -> a -> a
mapName ((Qid -> Qid) -> Symbol -> Symbol)
-> (Qid -> Qid) -> Symbol -> Symbol
forall a b. (a -> b) -> a -> b
$ Qid -> Qid
forall a. Show a => a -> Qid
prepend (Qid -> Qid) -> (Qid -> Qid) -> Qid -> Qid
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qid -> Qid
forall a. HasName a => a -> Qid
getName

-- | Convert 'Symbol' to 'Symbol', changing 'Kind's to 'Sort's.
asSort :: Symbol -> Symbol
asSort :: Symbol -> Symbol
asSort symb :: Symbol
symb = case Symbol
symb of
    Kind qid :: Qid
qid -> Qid -> Symbol
Sort Qid
qid
    _ -> Symbol
symb

-- | Convert 'Symbol' to 'Symbol', changing 'Sort's to 'Kind's.
asKind :: Symbol -> Symbol
asKind :: Symbol -> Symbol
asKind symb :: Symbol
symb = case Symbol
symb of
    Sort qid :: Qid
qid -> Qid -> Symbol
Kind Qid
qid
    _ -> Symbol
symb

-- | True iff the argument is a 'Sort' or 'Kind'.
isType :: Symbol -> Bool
isType :: Symbol -> Bool
isType symb :: Symbol
symb = case Symbol
symb of
    Sort _ -> Bool
True
    Kind _ -> Bool
True
    _ -> Bool
False

toTypeMaybe :: Symbol -> Maybe Type
toTypeMaybe :: Symbol -> Maybe Type
toTypeMaybe symb :: Symbol
symb = case Symbol
symb of
    Sort qid :: Qid
qid -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> (Qid -> Type) -> Qid -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sort -> Type
TypeSort (Sort -> Type) -> (Qid -> Sort) -> Qid -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qid -> Sort
SortId (Qid -> Maybe Type) -> Qid -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Qid
qid
    Kind qid :: Qid
qid -> Type -> Maybe Type
forall a. a -> Maybe a
Just (Type -> Maybe Type) -> (Qid -> Type) -> Qid -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Type
TypeKind (Kind -> Type) -> (Qid -> Kind) -> Qid -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Qid -> Kind
KindId (Qid -> Maybe Type) -> Qid -> Maybe Type
forall a b. (a -> b) -> a -> b
$ Qid
qid
    _ -> Maybe Type
forall a. Maybe a
Nothing

-- | Convert 'Symbol' to 'Type', if possible.
toType :: Symbol -> Type
toType :: Symbol -> Type
toType = Maybe Type -> Type
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Type -> Type) -> (Symbol -> Maybe Type) -> Symbol -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Maybe Type
toTypeMaybe

-- | True iff the argument is a wildcard 'Operator'.
isOpWildcard :: Symbol -> Bool
isOpWildcard :: Symbol -> Bool
isOpWildcard symb :: Symbol
symb = case Symbol
symb of
    OpWildcard _ -> Bool
True
    _ -> Bool
False

-- | True iff the argument is a qualified 'Operator'.
isOperator :: Symbol -> Bool
isOperator :: Symbol -> Bool
isOperator symb :: Symbol
symb = case Symbol
symb of
    Operator {} -> Bool
True
    _ -> Bool
False

toOperatorMaybe :: Symbol -> Maybe Operator
toOperatorMaybe :: Symbol -> Maybe Operator
toOperatorMaybe symb :: Symbol
symb = case Symbol
symb of
    Operator qid :: Qid
qid dom :: [Symbol]
dom cod :: Symbol
cod -> Operator -> Maybe Operator
forall a. a -> Maybe a
Just (Operator -> Maybe Operator) -> Operator -> Maybe Operator
forall a b. (a -> b) -> a -> b
$
        OpId -> [Type] -> Type -> [Attr] -> Operator
Op (Qid -> OpId
OpId Qid
qid) ((Symbol -> Type) -> [Symbol] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> Type
toType [Symbol]
dom) (Symbol -> Type
toType Symbol
cod) []
    _ -> Maybe Operator
forall a. Maybe a
Nothing

-- | Convert 'Symbol' to 'Operator', if possible.
toOperator :: Symbol -> Operator
toOperator :: Symbol -> Operator
toOperator = Maybe Operator -> Operator
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Operator -> Operator)
-> (Symbol -> Maybe Operator) -> Symbol -> Operator
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Maybe Operator
toOperatorMaybe

-- * Construction

-- | Create a total 'Operator' 'Symbol' with the given profile.
mkOpTotal :: Qid -> [Qid] -> Qid -> Symbol
mkOpTotal :: Qid -> [Qid] -> Qid -> Symbol
mkOpTotal qid :: Qid
qid dom :: [Qid]
dom cod :: Qid
cod = Qid -> [Symbol] -> Symbol -> Symbol
Operator Qid
qid ((Qid -> Symbol) -> [Qid] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Qid -> Symbol
Sort [Qid]
dom) (Qid -> Symbol
Sort Qid
cod)

-- | Create a partial 'Operator' 'Symbol' with the given profile.
mkOpPartial :: Qid -> [Qid] -> Qid -> Symbol
mkOpPartial :: Qid -> [Qid] -> Qid -> Symbol
mkOpPartial qid :: Qid
qid dom :: [Qid]
dom cod :: Qid
cod = Qid -> [Symbol] -> Symbol -> Symbol
Operator Qid
qid ((Qid -> Symbol) -> [Qid] -> [Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Qid -> Symbol
Sort [Qid]
dom) (Qid -> Symbol
Kind Qid
cod)

-- * Testing

{- | True iff both 'Symbol's are of the same 'Kind' in the given
'SymbolRel'. The 'isType' predicate is assumed to hold for both
'Symbol's; this precondition is /not/ checked. -}
typeSameKind :: SymbolRel -> Symbol -> Symbol -> Bool
typeSameKind :: SymbolRel -> Symbol -> Symbol -> Bool
typeSameKind rel :: SymbolRel
rel s1 :: Symbol
s1 s2 :: Symbol
s2 = let
    preds1 :: Set Symbol
preds1 = SymbolRel -> Symbol -> Set Symbol
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors SymbolRel
rel Symbol
s1
    preds2 :: Set Symbol
preds2 = SymbolRel -> Symbol -> Set Symbol
forall a. Ord a => Rel a -> a -> Set a
Rel.predecessors SymbolRel
rel Symbol
s2
    succs1 :: Set Symbol
succs1 = SymbolRel -> Symbol -> Set Symbol
forall a. Ord a => Rel a -> a -> Set a
Rel.succs SymbolRel
rel Symbol
s1
    succs2 :: Set Symbol
succs2 = SymbolRel -> Symbol -> Set Symbol
forall a. Ord a => Rel a -> a -> Set a
Rel.succs SymbolRel
rel Symbol
s2
    psect :: Set Symbol
psect = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Symbol
preds1 Set Symbol
preds2
    ssect :: Set Symbol
ssect = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Symbol
succs1 Set Symbol
succs2
    in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Symbol
s1 Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
s2
          , Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s2 Set Symbol
preds1
          , Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s1 Set Symbol
preds2
          , Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s2 Set Symbol
succs1
          , Symbol -> Set Symbol -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Symbol
s1 Set Symbol
succs2
          , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Bool
forall a. Set a -> Bool
Set.null Set Symbol
psect
          , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Bool
forall a. Set a -> Bool
Set.null Set Symbol
ssect ]

{- | True iff the 'Symbol's of both lists are pairwise of the same
'Kind' in the given 'SymbolRel'. -}
zipSameKind :: SymbolRel -> Symbols -> Symbols -> Bool
zipSameKind :: SymbolRel -> [Symbol] -> [Symbol] -> Bool
zipSameKind rel :: SymbolRel
rel s1 :: [Symbol]
s1 s2 :: [Symbol]
s2 = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ (Symbol -> Symbol -> Bool) -> [Symbol] -> [Symbol] -> [Bool]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (SymbolRel -> Symbol -> Symbol -> Bool
sameKind SymbolRel
rel) [Symbol]
s1 [Symbol]
s2

-- | True iff both 'Symbol's are of the same 'Kind' in the given 'SymbolRel'.
sameKind :: SymbolRel -> Symbol -> Symbol -> Bool
sameKind :: SymbolRel -> Symbol -> Symbol -> Bool
sameKind rel :: SymbolRel
rel s1 :: Symbol
s1 s2 :: Symbol
s2
    | Symbol -> Bool
isOpWildcard Symbol
s1 Bool -> Bool -> Bool
&& Symbol -> Bool
isOperator Symbol
s2 = Bool
True
    | Symbol -> Bool
isOperator Symbol
s1 Bool -> Bool -> Bool
&& Symbol -> Bool
isOpWildcard Symbol
s2 = Bool
True
    | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Symbol -> Bool
isType [Symbol
s1, Symbol
s2] = SymbolRel -> Symbol -> Symbol -> Bool
typeSameKind SymbolRel
rel (Symbol -> Symbol
kindSym2sortSym Symbol
s1) (Symbol -> Symbol
kindSym2sortSym Symbol
s2)
    | (Symbol -> Bool) -> [Symbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Symbol -> Bool
isOperator [Symbol
s1, Symbol
s2] = let
        Operator _ dom1 :: [Symbol]
dom1 _ = Symbol
s1
        Operator _ dom2 :: [Symbol]
dom2 _ = Symbol
s2
        in SymbolRel -> [Symbol] -> [Symbol] -> Bool
zipSameKind SymbolRel
rel [Symbol]
dom1 [Symbol]
dom2
    | Bool
otherwise = Bool
False

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