module HyLo.Signature( Signature, emptySignature, buildSignature,
                       addNomToSig,  delNomFromSig,
                       addPropToSig, delPropFromSig,
                       addRelToSig,  delRelFromSig,
                       isNomInSig, isPropInSig, isRelInSig,
                       merge, commonSig,
                       relSymbols, propSymbols, nomSymbols,
                       isSubsignatureOf,
                       HasSignature(..),
                       --
                       unit_tests )

where

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

-- ----------------------
-- QuickCheck stuff
-- ----------------------

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)]