Sign.hs revision a14767aeac3e78ed100f5b75e210ba563ee10dba
c63ebf815c8a874525cf18670ad74847f7fc7b26Christian MaederModule : $Header$
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederDescription : Signature for propositional logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007
456238178f89e5a3de2988ee6c8af924297d52d9Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : luecke@informatik.uni-bremen.de
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : experimental
43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : portable
f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian MaederDefinition of signatures for propositional logic
e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maeder Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder What is a Logic?.
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhaeuser.
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder (Sign (..) -- Propositional Signatures
404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich ,pretty -- pretty printing
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder ,isLegalSignature -- is a signature ok?
d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder ,addToSig -- adds an id to the given Signature
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder ,unite -- union of sigantures
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder ,emptySig -- empty signature
bab2d88d650448628730ed3b65c9f99c52500e8cChristian Maeder ,isSubSigOf -- is subsiganture?
3e8b136f23ed57d40ee617f49bcac37830b58cabChristian Maeder ,sigDiff -- Difference of Signatures
ef9e8535c168d3f774d9e74368a2317a9eda5826Christian Maeder ,sigUnion -- Union for Logic.Logic
5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maederimport qualified Data.Set as Set
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- | Datatype for propositional Signatures
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- Signatures are just sets
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroedernewtype Sign = Sign {items :: Set.Set Id} deriving (Eq, Show)
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroederinstance Pretty Sign where
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder pretty = printSign
3dde4051c307b609159a097f08a05108fdd036efJonathan von Schroeder-- | determines whether a signature is vaild
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder-- all sets are ok, so glued to true
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederisLegalSignature :: Sign -> Bool
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederisLegalSignature _ = True
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian Maeder-- | pretty printing for Signatures
8b767d09a78927b111f5596fdff9ca7d2c1a439fChristian MaederprintSign :: Sign -> Doc
4b4a0b61b72cf8478a5d4d5002bca9f699401363Christian Maeder hsep [text "prop", sepByCommas $ map pretty $ Set.toList $ items s]
308834907a120fd8771e18292ed2ca9cd767c12dChristian Maeder-- | Adds an Id to the signature
bab2d88d650448628730ed3b65c9f99c52500e8cChristian MaederaddToSig :: Sign -> Id -> Sign
9f226cec9f978edaba67aee4c4e04e3d3b994b87Daniel CalegariaddToSig sig tok = Sign {items = Set.insert tok $ items sig}
6a2dad705deefd1b7a7e09b84fd2d75f2213be47Christian Maeder-- | Union of signatures
a7c27282e71cf4505026645f96d4f5cb8a284e32Christian Maederunite :: Sign -> Sign -> Sign
363939beade943a02b31004cea09dec34fa8a6d9Christian Maederunite sig1 sig2 = Sign {items = Set.union (items sig1) $ items sig2}
f04e8f3ff56405901be968fd4c6e9769239f1a9bKlaus Luettich-- | The empty signature
6aea82c63ba1d2efc0329bc784a14e521469ec20Christian MaederemptySig :: Sign
4ba08bfca0cc8d9da65397b8dfd2654fdb4c0e62Christian MaederemptySig = Sign {items = Set.empty}
431d34c7007a787331c4e5ec997badb0f8190fc7Christian Maeder-- | Determines if sig1 is subsignature of sig2
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian MaederisSubSigOf :: Sign -> Sign -> Bool
f5c0884429b01e74c6e658ded921fb2e16dfb478Christian MaederisSubSigOf sig1 sig2 = Set.isSubsetOf (items sig1) $ items sig2
f1541d4a151dbd08002dbd14e7eb1d5dde253689Christian Maeder-- | difference of Signatures
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedersigDiff :: Sign -> Sign -> Sign
6dc9bc98d0854fe2e3dd3bfc4275096a0c28ee1cChristian MaedersigDiff sig1 sig2 = Sign{items = Set.difference (items sig1) $ items sig2}
23ffcc44ca8612feccbd8fda63fa5be7ab5f9dc3Christian Maeder-- | union of Signatures
61fa0ac06ede811c7aad54ec4c4202346727368eChristian Maeder-- or do I have to care about more things here?
c0c2380bced8159ff0297ece14eba948bd236471Christian MaedersigUnion :: Sign -> Sign -> Result Sign
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaedersigUnion s1 s2 = Result [Diag Debug "All fine sigUnion" nullRange]
63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder $ Just $ unite s1 s2