{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./Temporal/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 Temporal.Sign
    (Sign (..)                     -- Propositional Signatures
    , pretty                        -- pretty printing
    , isLegalSignature              -- is a signature ok?
    , addToSig                      -- adds an id to the given Signature
    , unite                         -- union of sigantures
    , 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 (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, 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, Typeable)

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

{- | 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 s2 :: Sign
s2 = [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) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just (Sign -> Maybe Sign) -> Sign -> Maybe Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Sign
unite Sign
s1 Sign
s2