module Term.Term.FunctionSymbols (
FunSym(..)
, ACSym(..)
, CSym(..)
, Privacy(..)
, NoEqSym
, FunSig
, NoEqFunSig
, expSymString
, invSymString
, pmultSymString
, emapSymString
, unionSymString
, expSym
, pmultSym
, oneSym
, invSym
, pairSym
, fstSym
, sndSym
, dhFunSig
, bpFunSig
, msetFunSig
, pairFunSig
, dhReducibleFunSig
, bpReducibleFunSig
, implicitFunSig
) where
import Data.Typeable
import Data.Generics
import Data.DeriveTH
import Data.Binary
import Control.DeepSeq
import Data.ByteString (ByteString)
import Extension.Data.ByteString ()
import Data.ByteString.Char8 ()
import Data.Set (Set)
import qualified Data.Set as S
data ACSym = Union | Mult
deriving (Eq, Ord, Typeable, Data, Show)
data Privacy = Private | Public
deriving (Eq, Ord, Typeable, Data, Show)
type NoEqSym = (ByteString, (Int, Privacy))
data CSym = EMap
deriving (Eq, Ord, Typeable, Data, Show)
data FunSym = NoEq NoEqSym
| AC ACSym
| C CSym
| List
deriving (Eq, Ord, Typeable, Data, Show)
type FunSig = Set FunSym
type NoEqFunSig = Set NoEqSym
expSymString, invSymString :: ByteString
expSymString = "exp"
invSymString = "inv"
unionSymString :: ByteString
unionSymString = "union"
emapSymString, pmultSymString :: ByteString
emapSymString = "em"
pmultSymString = "pmult"
pairSym, expSym, invSym, oneSym, fstSym, sndSym, pmultSym :: NoEqSym
pairSym = ("pair",(2,Public))
expSym = (expSymString,(2,Public))
invSym = (invSymString,(1,Public))
oneSym = ("one",(0,Public))
fstSym = ("fst",(1,Public))
sndSym = ("snd",(1,Public))
pmultSym = (pmultSymString,(2,Public))
dhFunSig :: FunSig
dhFunSig = S.fromList [ AC Mult, NoEq expSym, NoEq oneSym, NoEq invSym ]
bpFunSig :: FunSig
bpFunSig = S.fromList [ NoEq pmultSym, C EMap ]
msetFunSig :: FunSig
msetFunSig = S.fromList [AC Union]
pairFunSig :: NoEqFunSig
pairFunSig = S.fromList [ pairSym, fstSym, sndSym ]
dhReducibleFunSig :: FunSig
dhReducibleFunSig = S.fromList [ NoEq expSym, NoEq invSym ]
bpReducibleFunSig :: FunSig
bpReducibleFunSig = S.fromList [ NoEq pmultSym, C EMap ]
implicitFunSig :: FunSig
implicitFunSig = S.fromList [ NoEq invSym, NoEq pairSym
, AC Mult, AC Union ]
$( derive makeNFData ''Privacy)
$( derive makeNFData ''CSym)
$( derive makeNFData ''FunSym)
$( derive makeNFData ''ACSym)
$( derive makeBinary ''Privacy)
$( derive makeBinary ''CSym)
$( derive makeBinary ''FunSym)
$( derive makeBinary ''ACSym)