4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-# OPTIONS -fallow-undecidable-instances #-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{- |

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederModule : $Header$

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDescription : Instance of class Logic for propositional logic

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederMaintainer : luecke@tzi.de

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederStability : experimental

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederPortability : portable

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian MaederDefinition of signatures for propositional logic

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder{-

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Ref.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder What is a Logic?.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder 2005.

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder-}

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maedermodule Propositional.Sign where

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport qualified Data.Set as Set

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Id

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.Doc

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Common.DocUtils

4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maederimport Data.Typeable

import Common.ATerm.Conversion

-- Signatures are just sets

data Sign = Sign {items :: Set.Set Id}

deriving (Eq, Show)

instance Pretty Sign where

pretty = printSign

instance Typeable Sign

instance ShATermConvertible Sign

-- | determines whether a signature is vaild

-- all sets are ok, so glued to true

isLegalSignature :: Sign -> Bool

isLegalSignature _ = True

printSign :: Sign -> Doc

printSign s = text "{" <+> (sepByCommas $ map idDoc (Set.toList $ items s)) <+> text "}"