{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CASL_DL/Sign.hs
Description :  Signatures for DL logics, as extension of CASL signatures
Copyright   :  (c) Klaus Luettich, Uni Bremen 2004
License     :  GPLv2 or higher, see LICENSE.txt

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

Signatures for DL logics, as extension of CASL signatures.
-}

module CASL_DL.Sign where

import Data.Data
import qualified Data.Map as Map

import Common.Id
import Common.Doc
import Common.DocUtils

import CASL.AS_Basic_CASL
import CASL_DL.AS_CASL_DL
import CASL_DL.Print_AS ()

import Data.List (union, (\\), isPrefixOf)
import Control.Exception

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

data PropertyType = AnnoProperty
                  | OntoProperty deriving (Int -> PropertyType -> ShowS
[PropertyType] -> ShowS
PropertyType -> String
(Int -> PropertyType -> ShowS)
-> (PropertyType -> String)
-> ([PropertyType] -> ShowS)
-> Show PropertyType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PropertyType] -> ShowS
$cshowList :: [PropertyType] -> ShowS
show :: PropertyType -> String
$cshow :: PropertyType -> String
showsPrec :: Int -> PropertyType -> ShowS
$cshowsPrec :: Int -> PropertyType -> ShowS
Show, PropertyType -> PropertyType -> Bool
(PropertyType -> PropertyType -> Bool)
-> (PropertyType -> PropertyType -> Bool) -> Eq PropertyType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PropertyType -> PropertyType -> Bool
$c/= :: PropertyType -> PropertyType -> Bool
== :: PropertyType -> PropertyType -> Bool
$c== :: PropertyType -> PropertyType -> Bool
Eq, Eq PropertyType
Eq PropertyType =>
(PropertyType -> PropertyType -> Ordering)
-> (PropertyType -> PropertyType -> Bool)
-> (PropertyType -> PropertyType -> Bool)
-> (PropertyType -> PropertyType -> Bool)
-> (PropertyType -> PropertyType -> Bool)
-> (PropertyType -> PropertyType -> PropertyType)
-> (PropertyType -> PropertyType -> PropertyType)
-> Ord PropertyType
PropertyType -> PropertyType -> Bool
PropertyType -> PropertyType -> Ordering
PropertyType -> PropertyType -> PropertyType
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 :: PropertyType -> PropertyType -> PropertyType
$cmin :: PropertyType -> PropertyType -> PropertyType
max :: PropertyType -> PropertyType -> PropertyType
$cmax :: PropertyType -> PropertyType -> PropertyType
>= :: PropertyType -> PropertyType -> Bool
$c>= :: PropertyType -> PropertyType -> Bool
> :: PropertyType -> PropertyType -> Bool
$c> :: PropertyType -> PropertyType -> Bool
<= :: PropertyType -> PropertyType -> Bool
$c<= :: PropertyType -> PropertyType -> Bool
< :: PropertyType -> PropertyType -> Bool
$c< :: PropertyType -> PropertyType -> Bool
compare :: PropertyType -> PropertyType -> Ordering
$ccompare :: PropertyType -> PropertyType -> Ordering
$cp1Ord :: Eq PropertyType
Ord, Typeable, Typeable PropertyType
Constr
DataType
Typeable PropertyType =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> PropertyType -> c PropertyType)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c PropertyType)
-> (PropertyType -> Constr)
-> (PropertyType -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c PropertyType))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c PropertyType))
-> ((forall b. Data b => b -> b) -> PropertyType -> PropertyType)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> PropertyType -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> PropertyType -> r)
-> (forall u. (forall d. Data d => d -> u) -> PropertyType -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> PropertyType -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType)
-> Data PropertyType
PropertyType -> Constr
PropertyType -> DataType
(forall b. Data b => b -> b) -> PropertyType -> PropertyType
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropertyType -> c PropertyType
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropertyType
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) -> PropertyType -> u
forall u. (forall d. Data d => d -> u) -> PropertyType -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropertyType
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropertyType -> c PropertyType
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropertyType)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropertyType)
$cOntoProperty :: Constr
$cAnnoProperty :: Constr
$tPropertyType :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
gmapMp :: (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
gmapM :: (forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> PropertyType -> m PropertyType
gmapQi :: Int -> (forall d. Data d => d -> u) -> PropertyType -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> PropertyType -> u
gmapQ :: (forall d. Data d => d -> u) -> PropertyType -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> PropertyType -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> PropertyType -> r
gmapT :: (forall b. Data b => b -> b) -> PropertyType -> PropertyType
$cgmapT :: (forall b. Data b => b -> b) -> PropertyType -> PropertyType
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropertyType)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c PropertyType)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c PropertyType)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c PropertyType)
dataTypeOf :: PropertyType -> DataType
$cdataTypeOf :: PropertyType -> DataType
toConstr :: PropertyType -> Constr
$ctoConstr :: PropertyType -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropertyType
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c PropertyType
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropertyType -> c PropertyType
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> PropertyType -> c PropertyType
$cp1Data :: Typeable PropertyType
Data)

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

data AnnoLiteral = AL_Term (TERM DL_FORMULA)
                 | AL_Id Id
                   deriving (Int -> AnnoLiteral -> ShowS
[AnnoLiteral] -> ShowS
AnnoLiteral -> String
(Int -> AnnoLiteral -> ShowS)
-> (AnnoLiteral -> String)
-> ([AnnoLiteral] -> ShowS)
-> Show AnnoLiteral
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AnnoLiteral] -> ShowS
$cshowList :: [AnnoLiteral] -> ShowS
show :: AnnoLiteral -> String
$cshow :: AnnoLiteral -> String
showsPrec :: Int -> AnnoLiteral -> ShowS
$cshowsPrec :: Int -> AnnoLiteral -> ShowS
Show, AnnoLiteral -> AnnoLiteral -> Bool
(AnnoLiteral -> AnnoLiteral -> Bool)
-> (AnnoLiteral -> AnnoLiteral -> Bool) -> Eq AnnoLiteral
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AnnoLiteral -> AnnoLiteral -> Bool
$c/= :: AnnoLiteral -> AnnoLiteral -> Bool
== :: AnnoLiteral -> AnnoLiteral -> Bool
$c== :: AnnoLiteral -> AnnoLiteral -> Bool
Eq, Eq AnnoLiteral
Eq AnnoLiteral =>
(AnnoLiteral -> AnnoLiteral -> Ordering)
-> (AnnoLiteral -> AnnoLiteral -> Bool)
-> (AnnoLiteral -> AnnoLiteral -> Bool)
-> (AnnoLiteral -> AnnoLiteral -> Bool)
-> (AnnoLiteral -> AnnoLiteral -> Bool)
-> (AnnoLiteral -> AnnoLiteral -> AnnoLiteral)
-> (AnnoLiteral -> AnnoLiteral -> AnnoLiteral)
-> Ord AnnoLiteral
AnnoLiteral -> AnnoLiteral -> Bool
AnnoLiteral -> AnnoLiteral -> Ordering
AnnoLiteral -> AnnoLiteral -> AnnoLiteral
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 :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral
$cmin :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral
max :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral
$cmax :: AnnoLiteral -> AnnoLiteral -> AnnoLiteral
>= :: AnnoLiteral -> AnnoLiteral -> Bool
$c>= :: AnnoLiteral -> AnnoLiteral -> Bool
> :: AnnoLiteral -> AnnoLiteral -> Bool
$c> :: AnnoLiteral -> AnnoLiteral -> Bool
<= :: AnnoLiteral -> AnnoLiteral -> Bool
$c<= :: AnnoLiteral -> AnnoLiteral -> Bool
< :: AnnoLiteral -> AnnoLiteral -> Bool
$c< :: AnnoLiteral -> AnnoLiteral -> Bool
compare :: AnnoLiteral -> AnnoLiteral -> Ordering
$ccompare :: AnnoLiteral -> AnnoLiteral -> Ordering
$cp1Ord :: Eq AnnoLiteral
Ord, Typeable, Typeable AnnoLiteral
Constr
DataType
Typeable AnnoLiteral =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c AnnoLiteral)
-> (AnnoLiteral -> Constr)
-> (AnnoLiteral -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c AnnoLiteral))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c AnnoLiteral))
-> ((forall b. Data b => b -> b) -> AnnoLiteral -> AnnoLiteral)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r)
-> (forall u. (forall d. Data d => d -> u) -> AnnoLiteral -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> AnnoLiteral -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral)
-> Data AnnoLiteral
AnnoLiteral -> Constr
AnnoLiteral -> DataType
(forall b. Data b => b -> b) -> AnnoLiteral -> AnnoLiteral
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AnnoLiteral
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) -> AnnoLiteral -> u
forall u. (forall d. Data d => d -> u) -> AnnoLiteral -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AnnoLiteral
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AnnoLiteral)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AnnoLiteral)
$cAL_Id :: Constr
$cAL_Term :: Constr
$tAnnoLiteral :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
gmapMp :: (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
gmapM :: (forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> AnnoLiteral -> m AnnoLiteral
gmapQi :: Int -> (forall d. Data d => d -> u) -> AnnoLiteral -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> AnnoLiteral -> u
gmapQ :: (forall d. Data d => d -> u) -> AnnoLiteral -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> AnnoLiteral -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> AnnoLiteral -> r
gmapT :: (forall b. Data b => b -> b) -> AnnoLiteral -> AnnoLiteral
$cgmapT :: (forall b. Data b => b -> b) -> AnnoLiteral -> AnnoLiteral
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AnnoLiteral)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c AnnoLiteral)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c AnnoLiteral)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c AnnoLiteral)
dataTypeOf :: AnnoLiteral -> DataType
$cdataTypeOf :: AnnoLiteral -> DataType
toConstr :: AnnoLiteral -> Constr
$ctoConstr :: AnnoLiteral -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AnnoLiteral
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c AnnoLiteral
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> AnnoLiteral -> c AnnoLiteral
$cp1Data :: Typeable AnnoLiteral
Data)

emptyCASL_DLSign :: CASL_DLSign
emptyCASL_DLSign :: CASL_DLSign
emptyCASL_DLSign = Map SIMPLE_ID PropertyType -> [AnnoAppl] -> CASL_DLSign
CASL_DLSign Map SIMPLE_ID PropertyType
forall k a. Map k a
Map.empty []

addCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
addCASL_DLSign a :: CASL_DLSign
a b :: CASL_DLSign
b = CASL_DLSign
a
     { annoProperties :: Map SIMPLE_ID PropertyType
annoProperties =
           (SIMPLE_ID -> PropertyType -> PropertyType -> PropertyType)
-> Map SIMPLE_ID PropertyType
-> Map SIMPLE_ID PropertyType
-> Map SIMPLE_ID PropertyType
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWithKey (String -> SIMPLE_ID -> PropertyType -> PropertyType -> PropertyType
throwAnnoError "CASL_DL.Sign.addCASL_DLSign:")
                  (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
a) (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
b)
     , annoPropertySens :: [AnnoAppl]
annoPropertySens = [AnnoAppl] -> [AnnoAppl] -> [AnnoAppl]
forall a. Eq a => [a] -> [a] -> [a]
union (CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
a) (CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
b)
     }

throwAnnoError :: String -> SIMPLE_ID
               -> PropertyType -> PropertyType -> PropertyType
throwAnnoError :: String -> SIMPLE_ID -> PropertyType -> PropertyType -> PropertyType
throwAnnoError s :: String
s k :: SIMPLE_ID
k e1 :: PropertyType
e1 e2 :: PropertyType
e2 =
    if PropertyType
e1 PropertyType -> PropertyType -> Bool
forall a. Eq a => a -> a -> Bool
== PropertyType
e2
       then PropertyType
e1
       else String -> PropertyType
forall a. HasCallStack => String -> a
error (String -> PropertyType) -> String -> PropertyType
forall a b. (a -> b) -> a -> b
$ String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ " Annotation Properties and Ontology Properties "
                String -> ShowS
forall a. [a] -> [a] -> [a]
++ "must have distinct names! (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SIMPLE_ID -> String
forall a. Show a => a -> String
show SIMPLE_ID
k String -> ShowS
forall a. [a] -> [a] -> [a]
++ ")"

diffCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
diffCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> CASL_DLSign
diffCASL_DLSign a :: CASL_DLSign
a b :: CASL_DLSign
b = CASL_DLSign
a
     { annoProperties :: Map SIMPLE_ID PropertyType
annoProperties = Map SIMPLE_ID PropertyType
-> Map SIMPLE_ID PropertyType -> Map SIMPLE_ID PropertyType
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.difference (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
a) (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
b)
     , annoPropertySens :: [AnnoAppl]
annoPropertySens = CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
a [AnnoAppl] -> [AnnoAppl] -> [AnnoAppl]
forall a. Eq a => [a] -> [a] -> [a]
\\ CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
b
     }

isSubCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> Bool
isSubCASL_DLSign :: CASL_DLSign -> CASL_DLSign -> Bool
isSubCASL_DLSign a :: CASL_DLSign
a b :: CASL_DLSign
b =
    Map SIMPLE_ID PropertyType -> Map SIMPLE_ID PropertyType -> Bool
forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
Map.isSubmapOf (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
a) (CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
b) Bool -> Bool -> Bool
&&
    (CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
a [AnnoAppl] -> [AnnoAppl] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isSublistOf` CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
b)

instance Pretty CASL_DLSign where
    pretty :: CASL_DLSign -> Doc
pretty dlSign :: CASL_DLSign
dlSign = if Map SIMPLE_ID PropertyType -> Bool
forall k a. Map k a -> Bool
Map.null (Map SIMPLE_ID PropertyType -> Bool)
-> Map SIMPLE_ID PropertyType -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
dlSign
                    then Bool -> Doc -> Doc
forall a. HasCallStack => Bool -> a -> a
assert ([AnnoAppl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([AnnoAppl] -> Bool) -> [AnnoAppl] -> Bool
forall a b. (a -> b) -> a -> b
$ CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
dlSign) Doc
empty
                    else PropertyType -> String -> Doc
printPropertyList PropertyType
AnnoProperty
                                           "%OWLAnnoProperties("
                         Doc -> Doc -> Doc
$+$
                         PropertyType -> String -> Doc
printPropertyList PropertyType
OntoProperty
                                           "%OWLOntologyProperties("
                         Doc -> Doc -> Doc
$+$
                         if [AnnoAppl] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
dlSign)
                         then Doc
empty
                         else String -> Doc
text "%OWLAnnotations(" Doc -> Doc -> Doc
<+>
                              [Doc] -> Doc
vcat (Doc -> [Doc] -> [Doc]
punctuate (String -> Doc
text "; ") ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                                    (AnnoAppl -> Doc) -> [AnnoAppl] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map AnnoAppl -> Doc
forall a. Pretty a => a -> Doc
pretty
                                     (CASL_DLSign -> [AnnoAppl]
annoPropertySens CASL_DLSign
dlSign)) Doc -> Doc -> Doc
<+>
                              String -> Doc
text ")%"
        where propertyList :: PropertyType -> [(SIMPLE_ID, PropertyType)]
propertyList ty :: PropertyType
ty = ((SIMPLE_ID, PropertyType) -> Bool)
-> [(SIMPLE_ID, PropertyType)] -> [(SIMPLE_ID, PropertyType)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, x :: PropertyType
x) -> PropertyType
x PropertyType -> PropertyType -> Bool
forall a. Eq a => a -> a -> Bool
== PropertyType
ty) ([(SIMPLE_ID, PropertyType)] -> [(SIMPLE_ID, PropertyType)])
-> [(SIMPLE_ID, PropertyType)] -> [(SIMPLE_ID, PropertyType)]
forall a b. (a -> b) -> a -> b
$
                                 Map SIMPLE_ID PropertyType -> [(SIMPLE_ID, PropertyType)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map SIMPLE_ID PropertyType -> [(SIMPLE_ID, PropertyType)])
-> Map SIMPLE_ID PropertyType -> [(SIMPLE_ID, PropertyType)]
forall a b. (a -> b) -> a -> b
$ CASL_DLSign -> Map SIMPLE_ID PropertyType
annoProperties CASL_DLSign
dlSign
              printPropertyList :: PropertyType -> String -> Doc
printPropertyList ty :: PropertyType
ty str :: String
str =
                  case PropertyType -> [(SIMPLE_ID, PropertyType)]
propertyList PropertyType
ty of
                    [] -> Doc
empty
                    l :: [(SIMPLE_ID, PropertyType)]
l -> String -> Doc
text String
str Doc -> Doc -> Doc
<+>
                          [Doc] -> Doc
fcat (Doc -> [Doc] -> [Doc]
punctuate Doc
comma ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$
                                ((SIMPLE_ID, PropertyType) -> Doc)
-> [(SIMPLE_ID, PropertyType)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (SIMPLE_ID -> Doc
forall a. Pretty a => a -> Doc
pretty (SIMPLE_ID -> Doc)
-> ((SIMPLE_ID, PropertyType) -> SIMPLE_ID)
-> (SIMPLE_ID, PropertyType)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SIMPLE_ID, PropertyType) -> SIMPLE_ID
forall a b. (a, b) -> a
fst) [(SIMPLE_ID, PropertyType)]
l) Doc -> Doc -> Doc
<+>
                          String -> Doc
text ")%"


instance Pretty AnnoAppl where
    pretty :: AnnoAppl -> Doc
pretty (AnnoAppl rel :: SIMPLE_ID
rel subj :: Id
subj obj :: AnnoLiteral
obj) = SIMPLE_ID -> Doc
forall a. Pretty a => a -> Doc
pretty SIMPLE_ID
rel Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>
                                     Doc -> Doc
parens (Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
subj Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
comma Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> AnnoLiteral -> Doc
forall a. Pretty a => a -> Doc
pretty AnnoLiteral
obj)

instance Pretty AnnoLiteral where
    pretty :: AnnoLiteral -> Doc
pretty annoLit :: AnnoLiteral
annoLit = case AnnoLiteral
annoLit of
                       AL_Term t :: TERM DL_FORMULA
t -> TERM DL_FORMULA -> Doc
forall a. Pretty a => a -> Doc
pretty TERM DL_FORMULA
t
                       AL_Id i :: Id
i -> Id -> Doc
forall a. Pretty a => a -> Doc
pretty Id
i

isSublistOf :: (Eq a) => [a] -> [a] -> Bool
isSublistOf :: [a] -> [a] -> Bool
isSublistOf ys :: [a]
ys l :: [a]
l = case [a]
l of
  [] -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
ys
  _ : l' :: [a]
l' -> [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isPrefixOf [a]
ys [a]
l Bool -> Bool -> Bool
|| [a] -> [a] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isSublistOf [a]
ys [a]
l'