{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Propositional/Sign.hs
Description :  Signature for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

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

  Definition of signatures for propositional logic

  Ref.

    Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
    What is a Logic?.
    In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
    2005.
-}

module Propositional.Sign
    (Sign (..)                     -- Propositional Signatures
    , id2SimpleId
    , pretty                        -- pretty printing
    , isLegalSignature              -- is a signature ok?
    , addToSig                      -- adds an id to the given Signature
    , unite                         -- union of signatures
    , emptySig                      -- empty signature
    , isSubSigOf                    -- is subsiganture?
    , sigDiff                       -- Difference of Signatures
    , sigUnion                      -- Union for Logic.Logic
    ) where

import Data.Data
import qualified Data.Set as Set

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

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

instance Pretty Sign where
    pretty :: Sign -> Doc
pretty = Sign -> Doc
printSign

id2SimpleId :: Id -> Token
id2SimpleId :: Id -> Token
id2SimpleId i :: Id
i = case (Token -> Bool) -> [Token] -> [Token]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Token -> Bool) -> Token -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Token -> Bool
isPlace) ([Token] -> [Token]) -> [Token] -> [Token]
forall a b. (a -> b) -> a -> b
$ Id -> [Token]
getTokens Id
i of
  [] -> String -> Token
forall a. HasCallStack => String -> a
error "id2SimpleId"
  c :: Token
c : _ -> Token
c

{- | determines whether a signature is vaild
all sets are ok, so glued to true -}
isLegalSignature :: Sign -> Bool
isLegalSignature :: Sign -> Bool
isLegalSignature _ = Bool
True

-- | pretty printing for Signatures
printSign :: Sign -> Doc
printSign :: Sign -> Doc
printSign s :: Sign
s =
    [Doc] -> Doc
hsep [String -> Doc
text "prop", [Doc] -> Doc
sepByCommas ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ (Id -> Doc) -> [Id] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Id -> Doc
forall a. Pretty a => a -> Doc
pretty ([Id] -> [Doc]) -> [Id] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
s]

-- | Adds an Id to the signature
addToSig :: Sign -> Id -> Sign
addToSig :: Sign -> Id -> Sign
addToSig sig :: Sign
sig tok :: Id
tok = Sign :: Set Id -> Sign
Sign {items :: Set Id
items = Id -> Set Id -> Set Id
forall a. Ord a => a -> Set a -> Set a
Set.insert Id
tok (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
sig}

-- | Union of signatures
unite :: Sign -> Sign -> Sign
unite :: Sign -> Sign -> Sign
unite sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set Id -> Sign
Sign {items :: Set Id
items = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Sign -> Set Id
items Sign
sig1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
sig2}

-- | The empty signature
emptySig :: Sign
emptySig :: Sign
emptySig = Sign :: Set Id -> Sign
Sign {items :: Set Id
items = Set Id
forall a. Set a
Set.empty}

-- | Determines if sig1 is subsignature of sig2
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf :: Sign -> Sign -> Bool
isSubSigOf sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Set Id -> Set Id -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Sign -> Set Id
items Sign
sig1) (Set Id -> Bool) -> Set Id -> Bool
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
sig2

-- | difference of Signatures
sigDiff :: Sign -> Sign -> Sign
sigDiff :: Sign -> Sign -> Sign
sigDiff sig1 :: Sign
sig1 sig2 :: Sign
sig2 = Sign :: Set Id -> Sign
Sign {items :: Set Id
items = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set Id
items Sign
sig1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign -> Set Id
items Sign
sig2}

{- | union of Signatures
or do I have to care about more things here? -}
sigUnion :: Sign -> Sign -> Result Sign
sigUnion :: Sign -> Sign -> Result Sign
sigUnion s1 :: Sign
s1 = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Debug "All fine sigUnion" Range
nullRange]
    (Maybe Sign -> Result Sign)
-> (Sign -> Maybe Sign) -> Sign -> Result Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Maybe Sign
forall a. a -> Maybe a
Just (Sign -> Maybe Sign) -> (Sign -> Sign) -> Sign -> Maybe Sign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Sign -> Sign
unite Sign
s1