module HyLo.Signature( Signature, emptySignature, buildSignature,
addNomToSig, delNomFromSig,
addPropToSig, delPropFromSig,
addRelToSig, delRelFromSig,
isNomInSig, isPropInSig, isRelInSig,
merge, commonSig,
relSymbols, propSymbols, nomSymbols,
isSubsignatureOf,
HasSignature(..),
IsRelSym(..), hasInv,
unit_tests )
where
import Data.Maybe ( isJust )
import Data.Monoid ( Monoid(..) )
import Data.Set ( Set )
import qualified Data.Set as Set
import Test.QuickCheck ( Arbitrary(..), Property, (==>) )
import HyLo.Test ( UnitTest, runTest )
import Control.Monad ( liftM3 )
import Data.Set.Arbitrary()
data Signature n p r = Sig{nomSymbols :: Set n,
propSymbols :: Set p,
relSymbols :: Set r}
deriving (Eq, Read, Show)
emptySignature :: Signature n p r
emptySignature = Sig Set.empty Set.empty Set.empty
buildSignature :: Set n -> Set p -> Set r -> Signature n p r
buildSignature = Sig
addNomToSig :: Ord n => n -> Signature n p r -> Signature n p r
addNomToSig n (Sig ns ps rs) = Sig (Set.insert n ns) ps rs
delNomFromSig :: Ord n => n -> Signature n p r -> Signature n p r
delNomFromSig n (Sig ns ps rs) = Sig (Set.delete n ns) ps rs
addPropToSig :: Ord p => p -> Signature n p r -> Signature n p r
addPropToSig p (Sig ns ps rs) = Sig ns (Set.insert p ps) rs
delPropFromSig :: Ord p => p -> Signature n p r -> Signature n p r
delPropFromSig p (Sig ns ps rs) = Sig ns (Set.delete p ps) rs
addRelToSig :: Ord r => r -> Signature n p r -> Signature n p r
addRelToSig r (Sig ns ps rs) = Sig ns ps (Set.insert r rs)
delRelFromSig :: Ord r => r -> Signature n p r -> Signature n p r
delRelFromSig r (Sig ns ps rs) = Sig ns ps (Set.delete r rs)
isNomInSig :: Ord n => n -> Signature n p r -> Bool
isNomInSig n (Sig ns _ _) = Set.member n ns
isPropInSig :: Ord p => p -> Signature n p r -> Bool
isPropInSig p (Sig _ ps _) = Set.member p ps
isRelInSig :: Ord r => r -> Signature n p r -> Bool
isRelInSig r (Sig _ _ rs) = Set.member r rs
merge :: (Ord n, Ord p, Ord r)
=> Signature n p r
-> Signature n p r
-> Signature n p r
merge (Sig nl pl rl) (Sig nr pr rr) = Sig (nl `Set.union` nr)
(pl `Set.union` pr)
(rl `Set.union` rr)
commonSig :: (Ord n, Ord p, Ord r)
=> Signature n p r
-> Signature n p r
-> Signature n p r
commonSig (Sig nl pl rl) (Sig nr pr rr) = Sig (nl `Set.intersection` nr)
(pl `Set.intersection` pr)
(rl `Set.intersection` rr)
isSubsignatureOf :: (Ord n, Ord p, Ord r)
=> Signature n p r
-> Signature n p r
-> Bool
(Sig nl pl rl) `isSubsignatureOf` (Sig nr pr rr) = and [nl `Set.isSubsetOf` nr,
pl `Set.isSubsetOf` pr,
rl `Set.isSubsetOf` rr]
class HasSignature a where
type NomsOf a :: *
type PropsOf a :: *
type RelsOf a :: *
getSignature :: a -> Signature (NomsOf a) (PropsOf a) (RelsOf a)
instance HasSignature (Signature n p r) where
type NomsOf (Signature n p r) = n
type PropsOf (Signature n p r) = p
type RelsOf (Signature n p r) = r
getSignature = id
instance (Ord n, Ord p, Ord r) => Monoid (Signature n p r) where
mempty = emptySignature
mappend = merge
class Ord r => IsRelSym r where
invRel :: r -> Maybe r
hasInv :: IsRelSym r => r -> Bool
hasInv = isJust . invRel
instance (Arbitrary n, Ord n, Arbitrary p, Ord p, Arbitrary r, Ord r)
=> Arbitrary (Signature n p r) where
arbitrary = liftM3 buildSignature arbitrary arbitrary arbitrary
coarbitrary (Sig n p r) = coarbitrary n . coarbitrary p . coarbitrary r
type TestNom = Int
type TestProp = [Int]
type TestRel = [[Int]]
type TestSig = Signature TestNom TestProp TestRel
prop_add_del_nom :: TestNom -> TestSig -> Property
prop_add_del_nom n s = not (n `Set.member` nomSymbols s) ==> s == add_del s
where add_del = delNomFromSig n . addNomToSig n
prop_add_del_prop :: TestProp -> TestSig -> Property
prop_add_del_prop p s = not (p `Set.member` propSymbols s) ==> s == add_del s
where add_del = delPropFromSig p . addPropToSig p
prop_add_del_rel :: TestRel -> TestSig -> Property
prop_add_del_rel r s = not (r `Set.member` relSymbols s) ==> s == add_del s
where add_del = delRelFromSig r . addRelToSig r
prop_commonSig_id :: TestSig -> Bool
prop_commonSig_id s = commonSig s s == s
prop_commonSig_incl :: TestSig -> TestSig -> Bool
prop_commonSig_incl s1 s2 = ss `isSubsignatureOf` s1 && ss `isSubsignatureOf` s2
where ss = commonSig s1 s2
unit_tests :: UnitTest
unit_tests = [
("add/del nom", runTest prop_add_del_nom),
("add/del prop", runTest prop_add_del_prop),
("add/del rel", runTest prop_add_del_rel),
("commonSig id", runTest prop_commonSig_id),
("commonSig inclusion", runTest prop_commonSig_incl)]