{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Hybrid/HybridSign.hs
License     :  GPLv2 or higher, see LICENSE.txt

Stability   :  provisional
Portability :  portable

Signatures for hybrid logic, as extension of CASL signatures.
-}

module Hybrid.HybridSign where

import Hybrid.AS_Hybrid

import CASL.Sign

import qualified Common.Lib.MapSet as MapSet
import Common.Id

import Data.Data
import qualified Data.List as List
import qualified Data.Map as Map

data HybridSign = HybridSign
  { HybridSign -> OpMap
rigidOps :: OpMap
  , HybridSign -> PredMap
rigidPreds :: PredMap
  , HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies :: Map.Map SIMPLE_ID [AnHybFORM]
  , HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies :: Map.Map SIMPLE_ID [AnHybFORM]
  , HybridSign -> Map Id [AnHybFORM]
termModies :: Map.Map Id [AnHybFORM] -- SORT
  } deriving (Int -> HybridSign -> ShowS
[HybridSign] -> ShowS
HybridSign -> String
(Int -> HybridSign -> ShowS)
-> (HybridSign -> String)
-> ([HybridSign] -> ShowS)
-> Show HybridSign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HybridSign] -> ShowS
$cshowList :: [HybridSign] -> ShowS
show :: HybridSign -> String
$cshow :: HybridSign -> String
showsPrec :: Int -> HybridSign -> ShowS
$cshowsPrec :: Int -> HybridSign -> ShowS
Show, HybridSign -> HybridSign -> Bool
(HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> Bool) -> Eq HybridSign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: HybridSign -> HybridSign -> Bool
$c/= :: HybridSign -> HybridSign -> Bool
== :: HybridSign -> HybridSign -> Bool
$c== :: HybridSign -> HybridSign -> Bool
Eq, Eq HybridSign
Eq HybridSign =>
(HybridSign -> HybridSign -> Ordering)
-> (HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> Bool)
-> (HybridSign -> HybridSign -> HybridSign)
-> (HybridSign -> HybridSign -> HybridSign)
-> Ord HybridSign
HybridSign -> HybridSign -> Bool
HybridSign -> HybridSign -> Ordering
HybridSign -> HybridSign -> HybridSign
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 :: HybridSign -> HybridSign -> HybridSign
$cmin :: HybridSign -> HybridSign -> HybridSign
max :: HybridSign -> HybridSign -> HybridSign
$cmax :: HybridSign -> HybridSign -> HybridSign
>= :: HybridSign -> HybridSign -> Bool
$c>= :: HybridSign -> HybridSign -> Bool
> :: HybridSign -> HybridSign -> Bool
$c> :: HybridSign -> HybridSign -> Bool
<= :: HybridSign -> HybridSign -> Bool
$c<= :: HybridSign -> HybridSign -> Bool
< :: HybridSign -> HybridSign -> Bool
$c< :: HybridSign -> HybridSign -> Bool
compare :: HybridSign -> HybridSign -> Ordering
$ccompare :: HybridSign -> HybridSign -> Ordering
$cp1Ord :: Eq HybridSign
Ord, Typeable, Typeable HybridSign
Constr
DataType
Typeable HybridSign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> HybridSign -> c HybridSign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c HybridSign)
-> (HybridSign -> Constr)
-> (HybridSign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c HybridSign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c HybridSign))
-> ((forall b. Data b => b -> b) -> HybridSign -> HybridSign)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> HybridSign -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> HybridSign -> r)
-> (forall u. (forall d. Data d => d -> u) -> HybridSign -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> HybridSign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign)
-> Data HybridSign
HybridSign -> Constr
HybridSign -> DataType
(forall b. Data b => b -> b) -> HybridSign -> HybridSign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HybridSign -> c HybridSign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HybridSign
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> HybridSign -> u
forall u. (forall d. Data d => d -> u) -> HybridSign -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HybridSign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HybridSign -> c HybridSign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HybridSign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HybridSign)
$cHybridSign :: Constr
$tHybridSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
gmapMp :: (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
gmapM :: (forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> HybridSign -> m HybridSign
gmapQi :: Int -> (forall d. Data d => d -> u) -> HybridSign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> HybridSign -> u
gmapQ :: (forall d. Data d => d -> u) -> HybridSign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> HybridSign -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> HybridSign -> r
gmapT :: (forall b. Data b => b -> b) -> HybridSign -> HybridSign
$cgmapT :: (forall b. Data b => b -> b) -> HybridSign -> HybridSign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HybridSign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HybridSign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c HybridSign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c HybridSign)
dataTypeOf :: HybridSign -> DataType
$cdataTypeOf :: HybridSign -> DataType
toConstr :: HybridSign -> Constr
$ctoConstr :: HybridSign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HybridSign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c HybridSign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HybridSign -> c HybridSign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> HybridSign -> c HybridSign
$cp1Data :: Typeable HybridSign
Data)

emptyHybridSign :: HybridSign
emptyHybridSign :: HybridSign
emptyHybridSign = OpMap
-> PredMap
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map Id [AnHybFORM]
-> HybridSign
HybridSign OpMap
forall a b. MapSet a b
MapSet.empty PredMap
forall a b. MapSet a b
MapSet.empty
                             Map SIMPLE_ID [AnHybFORM]
forall k a. Map k a
Map.empty Map SIMPLE_ID [AnHybFORM]
forall k a. Map k a
Map.empty Map Id [AnHybFORM]
forall k a. Map k a
Map.empty

addHybridSign :: HybridSign -> HybridSign -> HybridSign
addHybridSign :: HybridSign -> HybridSign -> HybridSign
addHybridSign a :: HybridSign
a b :: HybridSign
b = HybridSign
a
  { rigidOps :: OpMap
rigidOps = OpMap -> OpMap -> OpMap
addOpMapSet (HybridSign -> OpMap
rigidOps HybridSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> OpMap
rigidOps HybridSign
b
  , rigidPreds :: PredMap
rigidPreds = PredMap -> PredMap -> PredMap
addMapSet (HybridSign -> PredMap
rigidPreds HybridSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> PredMap
rigidPreds HybridSign
b
  , modies :: Map SIMPLE_ID [AnHybFORM]
modies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
a) (Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
b
  , nomies :: Map SIMPLE_ID [AnHybFORM]
nomies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
a) (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
b)
  , termModies :: Map Id [AnHybFORM]
termModies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union (HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
a) (Map Id [AnHybFORM] -> Map Id [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
b }

interMap :: Ord a => ([b] -> [b] -> [b]) -> Map.Map a [b] -> Map.Map a [b]
         -> Map.Map a [b]
interMap :: ([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap f :: [b] -> [b] -> [b]
f m :: Map a [b]
m = ([b] -> Bool) -> Map a [b] -> Map a [b]
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool) -> ([b] -> Bool) -> [b] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [b] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (Map a [b] -> Map a [b])
-> (Map a [b] -> Map a [b]) -> Map a [b] -> Map a [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
forall k a b c.
Ord k =>
(a -> b -> c) -> Map k a -> Map k b -> Map k c
Map.intersectionWith [b] -> [b] -> [b]
f Map a [b]
m

interHybridSign :: HybridSign -> HybridSign -> HybridSign
interHybridSign :: HybridSign -> HybridSign -> HybridSign
interHybridSign a :: HybridSign
a b :: HybridSign
b = HybridSign
a
  { rigidOps :: OpMap
rigidOps = OpMap -> OpMap -> OpMap
interOpMapSet (HybridSign -> OpMap
rigidOps HybridSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> OpMap
rigidOps HybridSign
b
  , rigidPreds :: PredMap
rigidPreds = PredMap -> PredMap -> PredMap
interMapSet (HybridSign -> PredMap
rigidPreds HybridSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> PredMap
rigidPreds HybridSign
b
  , modies :: Map SIMPLE_ID [AnHybFORM]
modies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall a b.
Ord a =>
([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
a) (Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
b
  , nomies :: Map SIMPLE_ID [AnHybFORM]
nomies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall a b.
Ord a =>
([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
a) (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
b)
  , termModies :: Map Id [AnHybFORM]
termModies = ([AnHybFORM] -> [AnHybFORM] -> [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall a b.
Ord a =>
([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap [AnHybFORM] -> [AnHybFORM] -> [AnHybFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect (HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
a) (Map Id [AnHybFORM] -> Map Id [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
b }

diffHybridSign :: HybridSign -> HybridSign -> HybridSign
diffHybridSign :: HybridSign -> HybridSign -> HybridSign
diffHybridSign a :: HybridSign
a b :: HybridSign
b = HybridSign
a
  { rigidOps :: OpMap
rigidOps = OpMap -> OpMap -> OpMap
diffOpMapSet (HybridSign -> OpMap
rigidOps HybridSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> OpMap
rigidOps HybridSign
b
  , rigidPreds :: PredMap
rigidPreds = PredMap -> PredMap -> PredMap
diffMapSet (HybridSign -> PredMap
rigidPreds HybridSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ HybridSign -> PredMap
rigidPreds HybridSign
b
  , modies :: Map SIMPLE_ID [AnHybFORM]
modies = ([AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith [AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM]
forall a. Eq a => [a] -> [a] -> Maybe [a]
diffList (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
a) (Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
b
  , nomies :: Map SIMPLE_ID [AnHybFORM]
nomies = ([AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM])
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
-> Map SIMPLE_ID [AnHybFORM]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith [AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM]
forall a. Eq a => [a] -> [a] -> Maybe [a]
diffList (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
a) (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
b)
  , termModies :: Map Id [AnHybFORM]
termModies = ([AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith [AnHybFORM] -> [AnHybFORM] -> Maybe [AnHybFORM]
forall a. Eq a => [a] -> [a] -> Maybe [a]
diffList (HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
a) (Map Id [AnHybFORM] -> Map Id [AnHybFORM])
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM]
forall a b. (a -> b) -> a -> b
$ HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
b
  } where
     diffList :: [a] -> [a] -> Maybe [a]
diffList c :: [a]
c d :: [a]
d = let e :: [a]
e = [a]
c [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [a]
d in
                    if [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
e then Maybe [a]
forall a. Maybe a
Nothing else [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a]
e

isSubHybridSign :: HybridSign -> HybridSign -> Bool
isSubHybridSign :: HybridSign -> HybridSign -> Bool
isSubHybridSign a :: HybridSign
a b :: HybridSign
b =
    OpMap -> OpMap -> Bool
isSubOpMap (HybridSign -> OpMap
rigidOps HybridSign
a) (HybridSign -> OpMap
rigidOps HybridSign
b)
    Bool -> Bool -> Bool
&& PredMap -> PredMap -> Bool
isSubMap (HybridSign -> PredMap
rigidPreds HybridSign
a) (HybridSign -> PredMap
rigidPreds HybridSign
b)
    Bool -> Bool -> Bool
&& ([AnHybFORM] -> [AnHybFORM] -> Bool)
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy [AnHybFORM] -> [AnHybFORM] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
sublist (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
a) (HybridSign -> Map SIMPLE_ID [AnHybFORM]
modies HybridSign
b)
    Bool -> Bool -> Bool
&& ([AnHybFORM] -> [AnHybFORM] -> Bool)
-> Map SIMPLE_ID [AnHybFORM] -> Map SIMPLE_ID [AnHybFORM] -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy [AnHybFORM] -> [AnHybFORM] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
sublist (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
a) (HybridSign -> Map SIMPLE_ID [AnHybFORM]
nomies HybridSign
b)
    Bool -> Bool -> Bool
&& ([AnHybFORM] -> [AnHybFORM] -> Bool)
-> Map Id [AnHybFORM] -> Map Id [AnHybFORM] -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy [AnHybFORM] -> [AnHybFORM] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
sublist (HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
a) (HybridSign -> Map Id [AnHybFORM]
termModies HybridSign
b)
    where sublist :: [a] -> [a] -> Bool
sublist l1 :: [a]
l1 l2 :: [a]
l2 = [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
List.union [a]
l2 [a]
l1 [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
l2