ExtModalSign.hs revision 1a38107941725211e7c3f051f7a8f5e12199f03a
{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module : $Header$
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
{ flexOps :: OpMap
, flexPreds :: PredMap
, modalities :: Set.Set Id -- do not store sentences in signature
, timeMods :: Set.Set Id
, termMods :: Set.Set Id -- sorts that need to be mapped
, nominals :: Set.Set Id
} deriving (Show, Eq, Ord, Typeable, Data)
nomPType :: PredType
nomPType = PredType []
nomPId :: Token -> Id
nomPId t = mkId [t]
correctSign :: Sign f EModalSign -> Sign f EModalSign
correctSign s = let e = extendedInfo s in
s { extendedInfo = e
{ flexOps = interOpMapSet (flexOps e) $ opMap s
, flexPreds = interMapSet (flexPreds e) $ predMap s }}
emptyEModalSign :: EModalSign
emptyEModalSign =
addEModalSign :: EModalSign -> EModalSign -> EModalSign
addEModalSign ms1 ms2 = ms1
{ flexOps = addOpMapSet (flexOps ms1) (flexOps ms2)
, flexPreds = MapSet.union (flexPreds ms1) (flexPreds ms2)
, modalities = Set.union (modalities ms1) $ modalities ms2
, timeMods = Set.union (timeMods ms1)
(timeMods ms2)
, termMods = Set.union (termMods ms1) $ termMods ms2
, nominals = Set.union (nominals ms1) (nominals ms2)
}
interEModalSign :: EModalSign -> EModalSign -> EModalSign
interEModalSign ms1 ms2 = ms1
{ flexOps = interOpMapSet (flexOps ms1) (flexOps ms2)
, flexPreds = MapSet.intersection (flexPreds ms1) (flexPreds ms2)
, modalities = Set.intersection (modalities ms1) $ modalities ms2
, timeMods = Set.intersection (timeMods ms1)
(timeMods ms2)
, termMods = Set.intersection (termMods ms1) $ termMods ms2
, nominals = Set.intersection (nominals ms1) (nominals ms2)
}
diffEModalSign :: EModalSign -> EModalSign -> EModalSign
diffEModalSign ms1 ms2 = ms1
{ flexOps = diffOpMapSet (flexOps ms1) (flexOps ms2)
, flexPreds = MapSet.difference (flexPreds ms1) (flexPreds ms2)
, modalities = Set.difference (modalities ms1) $ modalities ms2
, timeMods = Set.difference (timeMods ms1)
(timeMods ms2)
, termMods = Set.difference (termMods ms1) $ termMods ms2
, nominals = Set.difference (nominals ms1) (nominals ms2)
} where
isSubEModalSign :: EModalSign -> EModalSign -> Bool
isSubEModalSign ms1 ms2 =
isSubOpMap (flexOps ms1) (flexOps ms2)
&& MapSet.isSubmapOf (flexPreds ms1) (flexPreds ms2)
&& Set.isSubsetOf (modalities ms1) (modalities ms2)
&& Set.isSubsetOf (timeMods ms1) (timeMods ms2)
&& Set.isSubsetOf (termMods ms1) (termMods ms2)
&& Set.isSubsetOf (nominals ms1) (nominals ms2)