{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Modal/ModalSign.hs
Copyright   :  (c) Till Mossakowski, C. Maeder, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

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

module Modal.ModalSign where

import Modal.AS_Modal

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

emptyModalSign :: ModalSign
emptyModalSign :: ModalSign
emptyModalSign = OpMap
-> PredMap
-> Map SIMPLE_ID [AnModFORM]
-> Map Id [AnModFORM]
-> ModalSign
ModalSign OpMap
forall a b. MapSet a b
MapSet.empty PredMap
forall a b. MapSet a b
MapSet.empty Map SIMPLE_ID [AnModFORM]
forall k a. Map k a
Map.empty Map Id [AnModFORM]
forall k a. Map k a
Map.empty

addModalSign :: ModalSign -> ModalSign -> ModalSign
addModalSign :: ModalSign -> ModalSign -> ModalSign
addModalSign a :: ModalSign
a b :: ModalSign
b = ModalSign
a
  { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
addOpMapSet (ModalSign -> OpMap
flexOps ModalSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> OpMap
flexOps ModalSign
b
  , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
addMapSet (ModalSign -> PredMap
flexPreds ModalSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> PredMap
flexPreds ModalSign
b
  , modies :: Map SIMPLE_ID [AnModFORM]
modies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
a) (Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM])
-> Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
b
  , termModies :: Map Id [AnModFORM]
termModies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.union (ModalSign -> Map Id [AnModFORM]
termModies ModalSign
a) (Map Id [AnModFORM] -> Map Id [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map Id [AnModFORM]
termModies ModalSign
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

interModalSign :: ModalSign -> ModalSign -> ModalSign
interModalSign :: ModalSign -> ModalSign -> ModalSign
interModalSign a :: ModalSign
a b :: ModalSign
b = ModalSign
a
  { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
interOpMapSet (ModalSign -> OpMap
flexOps ModalSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> OpMap
flexOps ModalSign
b
  , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
interMapSet (ModalSign -> PredMap
flexPreds ModalSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> PredMap
flexPreds ModalSign
b
  , modies :: Map SIMPLE_ID [AnModFORM]
modies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
forall a b.
Ord a =>
([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
a) (Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM])
-> Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
b
  , termModies :: Map Id [AnModFORM]
termModies = ([AnModFORM] -> [AnModFORM] -> [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall a b.
Ord a =>
([b] -> [b] -> [b]) -> Map a [b] -> Map a [b] -> Map a [b]
interMap [AnModFORM] -> [AnModFORM] -> [AnModFORM]
forall a. Eq a => [a] -> [a] -> [a]
List.intersect (ModalSign -> Map Id [AnModFORM]
termModies ModalSign
a) (Map Id [AnModFORM] -> Map Id [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map Id [AnModFORM]
termModies ModalSign
b }

diffModalSign :: ModalSign -> ModalSign -> ModalSign
diffModalSign :: ModalSign -> ModalSign -> ModalSign
diffModalSign a :: ModalSign
a b :: ModalSign
b = ModalSign
a
  { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
diffOpMapSet (ModalSign -> OpMap
flexOps ModalSign
a) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> OpMap
flexOps ModalSign
b
  , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
diffMapSet (ModalSign -> PredMap
flexPreds ModalSign
a) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ ModalSign -> PredMap
flexPreds ModalSign
b
  , modies :: Map SIMPLE_ID [AnModFORM]
modies = ([AnModFORM] -> [AnModFORM] -> Maybe [AnModFORM])
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
-> Map SIMPLE_ID [AnModFORM]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith [AnModFORM] -> [AnModFORM] -> Maybe [AnModFORM]
forall a. Eq a => [a] -> [a] -> Maybe [a]
diffList (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
a) (Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM])
-> Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
b
  , termModies :: Map Id [AnModFORM]
termModies = ([AnModFORM] -> [AnModFORM] -> Maybe [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith [AnModFORM] -> [AnModFORM] -> Maybe [AnModFORM]
forall a. Eq a => [a] -> [a] -> Maybe [a]
diffList (ModalSign -> Map Id [AnModFORM]
termModies ModalSign
a) (Map Id [AnModFORM] -> Map Id [AnModFORM])
-> Map Id [AnModFORM] -> Map Id [AnModFORM]
forall a b. (a -> b) -> a -> b
$ ModalSign -> Map Id [AnModFORM]
termModies ModalSign
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

isSubModalSign :: ModalSign -> ModalSign -> Bool
isSubModalSign :: ModalSign -> ModalSign -> Bool
isSubModalSign a :: ModalSign
a b :: ModalSign
b =
    OpMap -> OpMap -> Bool
isSubOpMap (ModalSign -> OpMap
flexOps ModalSign
a) (ModalSign -> OpMap
flexOps ModalSign
b)
    Bool -> Bool -> Bool
&& PredMap -> PredMap -> Bool
isSubMap (ModalSign -> PredMap
flexPreds ModalSign
a) (ModalSign -> PredMap
flexPreds ModalSign
b)
    Bool -> Bool -> Bool
&& ([AnModFORM] -> [AnModFORM] -> Bool)
-> Map SIMPLE_ID [AnModFORM] -> Map SIMPLE_ID [AnModFORM] -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy [AnModFORM] -> [AnModFORM] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
sublist (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
a) (ModalSign -> Map SIMPLE_ID [AnModFORM]
modies ModalSign
b)
    Bool -> Bool -> Bool
&& ([AnModFORM] -> [AnModFORM] -> Bool)
-> Map Id [AnModFORM] -> Map Id [AnModFORM] -> Bool
forall k a b.
Ord k =>
(a -> b -> Bool) -> Map k a -> Map k b -> Bool
Map.isSubmapOfBy [AnModFORM] -> [AnModFORM] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
sublist (ModalSign -> Map Id [AnModFORM]
termModies ModalSign
a) (ModalSign -> Map Id [AnModFORM]
termModies ModalSign
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