Signature.hs

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

where

import Data.Set ( Set )
import qualified Data.Set as Set
import Data.Kind

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
    type PropsOf a :: Type
    type RelsOf a  :: Type
    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) => Semigroup (Signature n p r) where
    (<>) = merge

instance (Ord n, Ord p, Ord r) => Monoid (Signature n p r) where
    mempty  = emptySignature