{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./ExtModal/ExtModalSign.hs
Copyright   :  DFKI GmbH 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  codruta.liliana@gmail.com
Stability   :  experimental
Portability :  portable

Signatures for extended modal logic as extension of CASL signatures.
In contrast to theoretical descriptions we keep separate sets of the flexible
operations to ensure that operations i.e. from CASL free types are rigid
by default.
-}

module ExtModal.ExtModalSign where

import CASL.Sign

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

import Data.Data
import qualified Data.Set as Set

data EModalSign = EModalSign
        { EModalSign -> OpMap
flexOps :: OpMap
        , EModalSign -> PredMap
flexPreds :: PredMap
        , EModalSign -> Set Id
modalities :: Set.Set Id -- do not store sentences in signature
        , EModalSign -> Set Id
timeMods :: Set.Set Id
        , EModalSign -> Set Id
termMods :: Set.Set Id -- sorts that need to be mapped
        , EModalSign -> Set Id
nominals :: Set.Set Id
        } deriving (Int -> EModalSign -> ShowS
[EModalSign] -> ShowS
EModalSign -> String
(Int -> EModalSign -> ShowS)
-> (EModalSign -> String)
-> ([EModalSign] -> ShowS)
-> Show EModalSign
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EModalSign] -> ShowS
$cshowList :: [EModalSign] -> ShowS
show :: EModalSign -> String
$cshow :: EModalSign -> String
showsPrec :: Int -> EModalSign -> ShowS
$cshowsPrec :: Int -> EModalSign -> ShowS
Show, EModalSign -> EModalSign -> Bool
(EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> Bool) -> Eq EModalSign
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EModalSign -> EModalSign -> Bool
$c/= :: EModalSign -> EModalSign -> Bool
== :: EModalSign -> EModalSign -> Bool
$c== :: EModalSign -> EModalSign -> Bool
Eq, Eq EModalSign
Eq EModalSign =>
(EModalSign -> EModalSign -> Ordering)
-> (EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> Bool)
-> (EModalSign -> EModalSign -> EModalSign)
-> (EModalSign -> EModalSign -> EModalSign)
-> Ord EModalSign
EModalSign -> EModalSign -> Bool
EModalSign -> EModalSign -> Ordering
EModalSign -> EModalSign -> EModalSign
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 :: EModalSign -> EModalSign -> EModalSign
$cmin :: EModalSign -> EModalSign -> EModalSign
max :: EModalSign -> EModalSign -> EModalSign
$cmax :: EModalSign -> EModalSign -> EModalSign
>= :: EModalSign -> EModalSign -> Bool
$c>= :: EModalSign -> EModalSign -> Bool
> :: EModalSign -> EModalSign -> Bool
$c> :: EModalSign -> EModalSign -> Bool
<= :: EModalSign -> EModalSign -> Bool
$c<= :: EModalSign -> EModalSign -> Bool
< :: EModalSign -> EModalSign -> Bool
$c< :: EModalSign -> EModalSign -> Bool
compare :: EModalSign -> EModalSign -> Ordering
$ccompare :: EModalSign -> EModalSign -> Ordering
$cp1Ord :: Eq EModalSign
Ord, Typeable, Typeable EModalSign
Constr
DataType
Typeable EModalSign =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> EModalSign -> c EModalSign)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c EModalSign)
-> (EModalSign -> Constr)
-> (EModalSign -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c EModalSign))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c EModalSign))
-> ((forall b. Data b => b -> b) -> EModalSign -> EModalSign)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> EModalSign -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> EModalSign -> r)
-> (forall u. (forall d. Data d => d -> u) -> EModalSign -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> EModalSign -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign)
-> Data EModalSign
EModalSign -> Constr
EModalSign -> DataType
(forall b. Data b => b -> b) -> EModalSign -> EModalSign
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EModalSign -> c EModalSign
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EModalSign
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) -> EModalSign -> u
forall u. (forall d. Data d => d -> u) -> EModalSign -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EModalSign
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EModalSign -> c EModalSign
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EModalSign)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EModalSign)
$cEModalSign :: Constr
$tEModalSign :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
gmapMp :: (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
gmapM :: (forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> EModalSign -> m EModalSign
gmapQi :: Int -> (forall d. Data d => d -> u) -> EModalSign -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> EModalSign -> u
gmapQ :: (forall d. Data d => d -> u) -> EModalSign -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> EModalSign -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> EModalSign -> r
gmapT :: (forall b. Data b => b -> b) -> EModalSign -> EModalSign
$cgmapT :: (forall b. Data b => b -> b) -> EModalSign -> EModalSign
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EModalSign)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c EModalSign)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c EModalSign)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c EModalSign)
dataTypeOf :: EModalSign -> DataType
$cdataTypeOf :: EModalSign -> DataType
toConstr :: EModalSign -> Constr
$ctoConstr :: EModalSign -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EModalSign
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c EModalSign
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EModalSign -> c EModalSign
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> EModalSign -> c EModalSign
$cp1Data :: Typeable EModalSign
Data)

nomPType :: PredType
nomPType :: PredType
nomPType = [Id] -> PredType
PredType []

nomPId :: Token -> Id
nomPId :: Token -> Id
nomPId t :: Token
t = [Token] -> Id
mkId [Token
t]

correctSign :: Sign f EModalSign -> Sign f EModalSign
correctSign :: Sign f EModalSign -> Sign f EModalSign
correctSign s :: Sign f EModalSign
s = let e :: EModalSign
e = Sign f EModalSign -> EModalSign
forall f e. Sign f e -> e
extendedInfo Sign f EModalSign
s in
  Sign f EModalSign
s { extendedInfo :: EModalSign
extendedInfo = EModalSign
e
      { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
interOpMapSet (EModalSign -> OpMap
flexOps EModalSign
e) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f EModalSign -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f EModalSign
s
      , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
interMapSet (EModalSign -> PredMap
flexPreds EModalSign
e) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f EModalSign -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f EModalSign
s }}

emptyEModalSign :: EModalSign
emptyEModalSign :: EModalSign
emptyEModalSign =
  OpMap
-> PredMap -> Set Id -> Set Id -> Set Id -> Set Id -> EModalSign
EModalSign OpMap
forall a b. MapSet a b
MapSet.empty PredMap
forall a b. MapSet a b
MapSet.empty Set Id
forall a. Set a
Set.empty Set Id
forall a. Set a
Set.empty Set Id
forall a. Set a
Set.empty Set Id
forall a. Set a
Set.empty

addEModalSign :: EModalSign -> EModalSign -> EModalSign
addEModalSign :: EModalSign -> EModalSign -> EModalSign
addEModalSign ms1 :: EModalSign
ms1 ms2 :: EModalSign
ms2 = EModalSign
ms1
        { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
addOpMapSet (EModalSign -> OpMap
flexOps EModalSign
ms1) (EModalSign -> OpMap
flexOps EModalSign
ms2)
        , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union (EModalSign -> PredMap
flexPreds EModalSign
ms1) (EModalSign -> PredMap
flexPreds EModalSign
ms2)
        , modalities :: Set Id
modalities = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EModalSign -> Set Id
modalities EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
ms2
        , timeMods :: Set Id
timeMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EModalSign -> Set Id
timeMods EModalSign
ms1)
                            (EModalSign -> Set Id
timeMods EModalSign
ms2)
        , termMods :: Set Id
termMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EModalSign -> Set Id
termMods EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
termMods EModalSign
ms2
        , nominals :: Set Id
nominals = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (EModalSign -> Set Id
nominals EModalSign
ms1) (EModalSign -> Set Id
nominals EModalSign
ms2)
        }

interEModalSign :: EModalSign -> EModalSign -> EModalSign
interEModalSign :: EModalSign -> EModalSign -> EModalSign
interEModalSign ms1 :: EModalSign
ms1 ms2 :: EModalSign
ms2 = EModalSign
ms1
        { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
interOpMapSet (EModalSign -> OpMap
flexOps EModalSign
ms1) (EModalSign -> OpMap
flexOps EModalSign
ms2)
        , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.intersection (EModalSign -> PredMap
flexPreds EModalSign
ms1) (EModalSign -> PredMap
flexPreds EModalSign
ms2)
        , modalities :: Set Id
modalities = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
modalities EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
ms2
        , timeMods :: Set Id
timeMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
timeMods EModalSign
ms1)
                            (EModalSign -> Set Id
timeMods EModalSign
ms2)
        , termMods :: Set Id
termMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
termMods EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
termMods EModalSign
ms2
        , nominals :: Set Id
nominals = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (EModalSign -> Set Id
nominals EModalSign
ms1) (EModalSign -> Set Id
nominals EModalSign
ms2)
        }

diffEModalSign :: EModalSign -> EModalSign -> EModalSign
diffEModalSign :: EModalSign -> EModalSign -> EModalSign
diffEModalSign ms1 :: EModalSign
ms1 ms2 :: EModalSign
ms2 = EModalSign
ms1
        { flexOps :: OpMap
flexOps = OpMap -> OpMap -> OpMap
diffOpMapSet (EModalSign -> OpMap
flexOps EModalSign
ms1) (EModalSign -> OpMap
flexOps EModalSign
ms2)
        , flexPreds :: PredMap
flexPreds = PredMap -> PredMap -> PredMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.difference (EModalSign -> PredMap
flexPreds EModalSign
ms1) (EModalSign -> PredMap
flexPreds EModalSign
ms2)
        , modalities :: Set Id
modalities = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (EModalSign -> Set Id
modalities EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
modalities EModalSign
ms2
        , timeMods :: Set Id
timeMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (EModalSign -> Set Id
timeMods EModalSign
ms1)
                            (EModalSign -> Set Id
timeMods EModalSign
ms2)
        , termMods :: Set Id
termMods = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (EModalSign -> Set Id
termMods EModalSign
ms1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ EModalSign -> Set Id
termMods EModalSign
ms2
        , nominals :: Set Id
nominals = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (EModalSign -> Set Id
nominals EModalSign
ms1) (EModalSign -> Set Id
nominals EModalSign
ms2)
        } where

isSubEModalSign :: EModalSign -> EModalSign -> Bool
isSubEModalSign :: EModalSign -> EModalSign -> Bool
isSubEModalSign ms1 :: EModalSign
ms1 ms2 :: EModalSign
ms2 =
        OpMap -> OpMap -> Bool
isSubOpMap (EModalSign -> OpMap
flexOps EModalSign
ms1) (EModalSign -> OpMap
flexOps EModalSign
ms2)
        Bool -> Bool -> Bool
&& PredMap -> PredMap -> Bool
forall a b. (Ord a, Ord b) => MapSet a b -> MapSet a b -> Bool
MapSet.isSubmapOf (EModalSign -> PredMap
flexPreds EModalSign
ms1) (EModalSign -> PredMap
flexPreds EModalSign
ms2)
        Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (EModalSign -> Set Id
modalities EModalSign
ms1) (EModalSign -> Set Id
modalities EModalSign
ms2)
        Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (EModalSign -> Set Id
timeMods EModalSign
ms1) (EModalSign -> Set Id
timeMods EModalSign
ms2)
        Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (EModalSign -> Set Id
termMods EModalSign
ms1) (EModalSign -> Set Id
termMods EModalSign
ms2)
        Bool -> Bool -> Bool
&& Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (EModalSign -> Set Id
nominals EModalSign
ms1) (EModalSign -> Set Id
nominals EModalSign
ms2)