{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Common/ExtSign.hs
Description :  signatures with symbol sets
Copyright   :  (c) DFKI GmbH, Uni Bremen 2002-2007
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Some functions that operate over signatures need to be extended to work over
signatures with symbol sets for every logic
-}

module Common.ExtSign where

import Data.Data
import qualified Data.Set as Set

import Common.Doc
import Common.DocUtils

{- | signatures with symbol sets.
(The Ord instance is needed for the ATC generation) -}
data ExtSign sign symbol = ExtSign
  { ExtSign sign symbol -> sign
plainSign :: sign
  , ExtSign sign symbol -> Set symbol
nonImportedSymbols :: Set.Set symbol
  } deriving (Int -> ExtSign sign symbol -> ShowS
[ExtSign sign symbol] -> ShowS
ExtSign sign symbol -> String
(Int -> ExtSign sign symbol -> ShowS)
-> (ExtSign sign symbol -> String)
-> ([ExtSign sign symbol] -> ShowS)
-> Show (ExtSign sign symbol)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall sign symbol.
(Show sign, Show symbol) =>
Int -> ExtSign sign symbol -> ShowS
forall sign symbol.
(Show sign, Show symbol) =>
[ExtSign sign symbol] -> ShowS
forall sign symbol.
(Show sign, Show symbol) =>
ExtSign sign symbol -> String
showList :: [ExtSign sign symbol] -> ShowS
$cshowList :: forall sign symbol.
(Show sign, Show symbol) =>
[ExtSign sign symbol] -> ShowS
show :: ExtSign sign symbol -> String
$cshow :: forall sign symbol.
(Show sign, Show symbol) =>
ExtSign sign symbol -> String
showsPrec :: Int -> ExtSign sign symbol -> ShowS
$cshowsPrec :: forall sign symbol.
(Show sign, Show symbol) =>
Int -> ExtSign sign symbol -> ShowS
Show, ReadPrec [ExtSign sign symbol]
ReadPrec (ExtSign sign symbol)
Int -> ReadS (ExtSign sign symbol)
ReadS [ExtSign sign symbol]
(Int -> ReadS (ExtSign sign symbol))
-> ReadS [ExtSign sign symbol]
-> ReadPrec (ExtSign sign symbol)
-> ReadPrec [ExtSign sign symbol]
-> Read (ExtSign sign symbol)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadPrec [ExtSign sign symbol]
forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadPrec (ExtSign sign symbol)
forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
Int -> ReadS (ExtSign sign symbol)
forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadS [ExtSign sign symbol]
readListPrec :: ReadPrec [ExtSign sign symbol]
$creadListPrec :: forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadPrec [ExtSign sign symbol]
readPrec :: ReadPrec (ExtSign sign symbol)
$creadPrec :: forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadPrec (ExtSign sign symbol)
readList :: ReadS [ExtSign sign symbol]
$creadList :: forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
ReadS [ExtSign sign symbol]
readsPrec :: Int -> ReadS (ExtSign sign symbol)
$creadsPrec :: forall sign symbol.
(Read sign, Read symbol, Ord symbol) =>
Int -> ReadS (ExtSign sign symbol)
Read, Typeable, Typeable (ExtSign sign symbol)
Constr
DataType
Typeable (ExtSign sign symbol) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> ExtSign sign symbol
 -> c (ExtSign sign symbol))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol))
-> (ExtSign sign symbol -> Constr)
-> (ExtSign sign symbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ExtSign sign symbol)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (ExtSign sign symbol)))
-> ((forall b. Data b => b -> b)
    -> ExtSign sign symbol -> ExtSign sign symbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ExtSign sign symbol -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ExtSign sign symbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ExtSign sign symbol -> m (ExtSign sign symbol))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExtSign sign symbol -> m (ExtSign sign symbol))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ExtSign sign symbol -> m (ExtSign sign symbol))
-> Data (ExtSign sign symbol)
ExtSign sign symbol -> Constr
ExtSign sign symbol -> DataType
(forall b. Data b => b -> b)
-> ExtSign sign symbol -> ExtSign sign symbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ExtSign sign symbol
-> c (ExtSign sign symbol)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol)
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ExtSign sign symbol))
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) -> ExtSign sign symbol -> u
forall u.
(forall d. Data d => d -> u) -> ExtSign sign symbol -> [u]
forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
Typeable (ExtSign sign symbol)
forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
ExtSign sign symbol -> Constr
forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
ExtSign sign symbol -> DataType
forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
(forall b. Data b => b -> b)
-> ExtSign sign symbol -> ExtSign sign symbol
forall sign symbol u.
(Data sign, Data symbol, Ord symbol) =>
Int -> (forall d. Data d => d -> u) -> ExtSign sign symbol -> u
forall sign symbol u.
(Data sign, Data symbol, Ord symbol) =>
(forall d. Data d => d -> u) -> ExtSign sign symbol -> [u]
forall sign symbol r r'.
(Data sign, Data symbol, Ord symbol) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
forall sign symbol r r'.
(Data sign, Data symbol, Ord symbol) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
forall sign symbol (m :: * -> *).
(Data sign, Data symbol, Ord symbol, Monad m) =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
forall sign symbol (m :: * -> *).
(Data sign, Data symbol, Ord symbol, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
forall sign symbol (c :: * -> *).
(Data sign, Data symbol, Ord symbol) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol)
forall sign symbol (c :: * -> *).
(Data sign, Data symbol, Ord symbol) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ExtSign sign symbol
-> c (ExtSign sign symbol)
forall sign symbol (t :: * -> *) (c :: * -> *).
(Data sign, Data symbol, Ord symbol, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ExtSign sign symbol))
forall sign symbol (t :: * -> * -> *) (c :: * -> *).
(Data sign, Data symbol, Ord symbol, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ExtSign sign symbol))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ExtSign sign symbol
-> c (ExtSign sign symbol)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ExtSign sign symbol))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ExtSign sign symbol))
$cExtSign :: Constr
$tExtSign :: DataType
gmapMo :: (forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
$cgmapMo :: forall sign symbol (m :: * -> *).
(Data sign, Data symbol, Ord symbol, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
gmapMp :: (forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
$cgmapMp :: forall sign symbol (m :: * -> *).
(Data sign, Data symbol, Ord symbol, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
gmapM :: (forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
$cgmapM :: forall sign symbol (m :: * -> *).
(Data sign, Data symbol, Ord symbol, Monad m) =>
(forall d. Data d => d -> m d)
-> ExtSign sign symbol -> m (ExtSign sign symbol)
gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtSign sign symbol -> u
$cgmapQi :: forall sign symbol u.
(Data sign, Data symbol, Ord symbol) =>
Int -> (forall d. Data d => d -> u) -> ExtSign sign symbol -> u
gmapQ :: (forall d. Data d => d -> u) -> ExtSign sign symbol -> [u]
$cgmapQ :: forall sign symbol u.
(Data sign, Data symbol, Ord symbol) =>
(forall d. Data d => d -> u) -> ExtSign sign symbol -> [u]
gmapQr :: (r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
$cgmapQr :: forall sign symbol r r'.
(Data sign, Data symbol, Ord symbol) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
gmapQl :: (r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
$cgmapQl :: forall sign symbol r r'.
(Data sign, Data symbol, Ord symbol) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ExtSign sign symbol -> r
gmapT :: (forall b. Data b => b -> b)
-> ExtSign sign symbol -> ExtSign sign symbol
$cgmapT :: forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
(forall b. Data b => b -> b)
-> ExtSign sign symbol -> ExtSign sign symbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ExtSign sign symbol))
$cdataCast2 :: forall sign symbol (t :: * -> * -> *) (c :: * -> *).
(Data sign, Data symbol, Ord symbol, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ExtSign sign symbol))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (ExtSign sign symbol))
$cdataCast1 :: forall sign symbol (t :: * -> *) (c :: * -> *).
(Data sign, Data symbol, Ord symbol, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ExtSign sign symbol))
dataTypeOf :: ExtSign sign symbol -> DataType
$cdataTypeOf :: forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
ExtSign sign symbol -> DataType
toConstr :: ExtSign sign symbol -> Constr
$ctoConstr :: forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
ExtSign sign symbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol)
$cgunfold :: forall sign symbol (c :: * -> *).
(Data sign, Data symbol, Ord symbol) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ExtSign sign symbol)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ExtSign sign symbol
-> c (ExtSign sign symbol)
$cgfoldl :: forall sign symbol (c :: * -> *).
(Data sign, Data symbol, Ord symbol) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ExtSign sign symbol
-> c (ExtSign sign symbol)
$cp1Data :: forall sign symbol.
(Data sign, Data symbol, Ord symbol) =>
Typeable (ExtSign sign symbol)
Data)

instance (Ord sign) => Eq (ExtSign sign symbol) where
    a :: ExtSign sign symbol
a == :: ExtSign sign symbol -> ExtSign sign symbol -> Bool
== b :: ExtSign sign symbol
b = ExtSign sign symbol -> ExtSign sign symbol -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ExtSign sign symbol
a ExtSign sign symbol
b Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance (Ord sign) => Ord (ExtSign sign symbol) where
  compare :: ExtSign sign symbol -> ExtSign sign symbol -> Ordering
compare (ExtSign s1 :: sign
s1 _) (ExtSign s2 :: sign
s2 _) = sign -> sign -> Ordering
forall a. Ord a => a -> a -> Ordering
compare sign
s1 sign
s2

instance (Pretty sign, Pretty symbol)
    => Pretty (ExtSign sign symbol) where
  pretty :: ExtSign sign symbol -> Doc
pretty (ExtSign s :: sign
s sys :: Set symbol
sys) =
    [Doc] -> Doc
sep [sign -> Doc
forall a. Pretty a => a -> Doc
pretty sign
s, if Set symbol -> Bool
forall a. Set a -> Bool
Set.null Set symbol
sys then Doc
empty else Set symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Set symbol
sys]

mkExtSign :: sign -> ExtSign sign symbol
mkExtSign :: sign -> ExtSign sign symbol
mkExtSign s :: sign
s = sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
s Set symbol
forall a. Set a
Set.empty