content: {-# 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 {items :: Set.Set Id}
    deriving (Show, Eq, Ord, Typeable, Data)
  
  instance Pretty Sign where
      pretty = printSign
  
  id2SimpleId :: Id -> Token
  id2SimpleId i = case filter (not . isPlace) $ getTokens i of
    [] -> error "id2SimpleId"
    c : _ -> c
  
  {- | determines whether a signature is vaild
  all sets are ok, so glued to true -}
  isLegalSignature :: Sign -> Bool
  isLegalSignature _ = True
  
  -- | pretty printing for Signatures
  printSign :: Sign -> Doc
  printSign s =
      hsep [text "prop", sepByCommas $ map pretty $ Set.toList $ items s]
  
  -- | Adds an Id to the signature
  addToSig :: Sign -> Id -> Sign
  addToSig sig tok = Sign {items = Set.insert tok $ items sig}
  
  -- | Union of signatures
  unite :: Sign -> Sign -> Sign
  unite sig1 sig2 = Sign {items = Set.union (items sig1) $ items sig2}
  
  -- | The empty signature
  emptySig :: Sign
  emptySig = Sign {items = Set.empty}
  
  -- | Determines if sig1 is subsignature of sig2
  isSubSigOf :: Sign -> Sign -> Bool
  isSubSigOf sig1 sig2 = Set.isSubsetOf (items sig1) $ items sig2
  
  -- | difference of Signatures
  sigDiff :: Sign -> Sign -> Sign
  sigDiff sig1 sig2 = Sign {items = Set.difference (items sig1) $ items sig2}
  
  {- | union of Signatures
  or do I have to care about more things here? -}
  sigUnion :: Sign -> Sign -> Result Sign
  sigUnion s1 = Result [Diag Debug "All fine sigUnion" nullRange]
      . Just . unite s1
  