Term.VTerm

Terms with variables and constants.

Terms with constants and variables

data Lit c v

A Lit is either a constant or a variable. (Const is taken by Control.Applicative)

Constructors

Con c

Var v

Instances

Typeable2 Lit

Apply BLTerm

Apply LNTerm

Monad (Lit c)

Monad instance in the variable

Functor (Lit c)

Functor instance in the variable.

Applicative (Lit c)

Applicative instance in the variable.

Foldable (Lit c)

Foldable instance in the variable.

Traversable (Lit c)

Traversable instance in the variable.

(Eq c, Eq v) => Eq (Lit c v)

(Data c, Data v) => Data (Lit c v)

(Ord c, Ord v) => Ord (Lit c v)

(Show v, Show c) => Show (Lit c v)

(Binary c_1627486233, Binary v_1627486234) => Binary (Lit c_1627486233 v_1627486234)

(NFData c_1627486233, NFData v_1627486234) => NFData (Lit c_1627486233 v_1627486234)

Sized (Lit c v)

HasFrees v => HasFrees (Lit c v)

type VTerm c v = Term (Lit c v)

A VTerm is a term with constants and variables

varTerm :: v -> VTerm c v

varTerm v is the VTerm with the variable v.

constTerm :: c -> VTerm c v

constTerm c is the VTerm with the const c.

varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]

vars t returns a duplicate-free list of variables that occur in t.

occursVTerm :: Eq v => v -> VTerm c v -> Bool

occurs v t returns True if v occurs in t

constsVTerm :: IsConst c => VTerm c v -> [c]

constsVTerm t returns a duplicate-free list of constants that occur in t.

isVar :: VTerm c v -> Bool

Destructors

termVar :: VTerm c v -> Maybe v

Extract just the variable from a term that may be variable.

termVar' :: (Show c, Show v) => VTerm c v -> v

Extract just the variable from a term that must be variable, throw an error if this fails.

class (Ord v, Eq v, Show v) => IsVar v

collect class constraints for variables

Instances

IsVar LVar

class (Ord c, Eq c, Show c, Data c) => IsConst c

collect class constraints for constants

Instances

IsConst Name

Pretty printing and query functions.

prettyTerm :: (Document d, Show l) => (l -> d) -> Term l -> d

Pretty print a term.

showFunSymName :: FunSym -> String

Convert a function symbol to its name.

lits :: Ord a => Term a -> [a]

lits t returns all literals that occur in term t. List can contain duplicates.

Smart constructors

fAppOne :: Term a

Smart constructors for one, zero.

fAppExp :: Ord a => (Term a, Term a) -> Term a

Smart constructors for pair, exp, pmult, and emap.

fAppInv :: Term a -> Term a

Smart constructors for inv, fst, and snd.

fAppPMult :: Ord a => (Term a, Term a) -> Term a

Smart constructors for pair, exp, pmult, and emap.

fAppEMap :: Ord a => (Term a, Term a) -> Term a

Smart constructors for pair, exp, pmult, and emap.

fAppPair :: Ord a => (Term a, Term a) -> Term a

Smart constructors for pair, exp, pmult, and emap.

fAppFst :: Term a -> Term a

Smart constructors for inv, fst, and snd.

fAppSnd :: Term a -> Term a

Smart constructors for inv, fst, and snd.

Destructors and classifiers

isPair :: Show a => Term a -> Bool

True iff the term is a well-formed pair.

isInverse :: Show a => Term a -> Bool

True iff the term is a well-formed inverse.

isProduct :: Show a => Term a -> Bool

True iff the term is a well-formed product.

isUnion :: Show a => Term a -> Bool

True iff the term is a well-formed union.

isEMap :: Show a => Term a -> Bool

True iff the term is a well-formed emap.

isNullaryPublicFunction :: Term a -> Bool

True iff the term is a nullary, public function.

isPrivateFunction :: Term a -> Bool

AC, C, and NonAC funcion symbols

data FunSym

Function symbols

Constructors

NoEq NoEqSym

a free function function symbol of a given arity

AC ACSym

an AC function symbol, can be used n-ary

C CSym

a C function symbol of a given arity

List

a free n-ary function symbol of TOP sort

Instances

Eq FunSym

Data FunSym

Ord FunSym

Show FunSym

Typeable FunSym

Binary FunSym

NFData FunSym

data ACSym

AC function symbols.

Constructors

Union

Mult

Instances

Eq ACSym

Data ACSym

Ord ACSym

Show ACSym

Typeable ACSym

Binary ACSym

NFData ACSym

data CSym

C(ommutative) function symbols

Constructors

EMap

Instances

Eq CSym

Data CSym

Ord CSym

Show CSym

Typeable CSym

Binary CSym

NFData CSym

data Privacy

A function symbol can be either Private (unknown to adversary) or Public.

Constructors

Private

Public

Instances

Eq Privacy

Data Privacy

Ord Privacy

Show Privacy

Typeable Privacy

Binary Privacy

NFData Privacy

type NoEqSym

Arguments

 = (ByteString, (Int, Privacy))

operator name, arity, private

NoEq function symbols (with respect to the background theory).

Signatures

type FunSig = Set FunSym

Function signatures.

type NoEqFunSig = Set NoEqSym

NoEq function signatures.

concrete symbols strings

expSymString :: ByteString

invSymString :: ByteString

pmultSymString :: ByteString

emapSymString :: ByteString

unionSymString :: ByteString

Function symbols

expSym :: NoEqSym

Exponentiation.

pmultSym :: NoEqSym

Multiplication of points (in G1) on elliptic curve by scalars.

concrete signatures

dhFunSig :: FunSig

The signature for Diffie-Hellman function symbols.

bpFunSig :: FunSig

The signature for the bilinear pairing function symbols.

msetFunSig :: FunSig

The signature for the multiset function symbols.

pairFunSig :: NoEqFunSig

The signature for pairing.

dhReducibleFunSig :: FunSig

Reducible function symbols for DH.

bpReducibleFunSig :: FunSig

Reducible function symbols for BP.

implicitFunSig :: FunSig

Implicit function symbols.

class Sized a where

Methods

size :: a -> Int

Instances

Sized a => Sized [a]

Sized a => Sized (Term a)

Sized (Lit c v)

Sized (SubstVFresh c v)

Sized (Subst c v)

Terms

data Term a

A term in T(Sigma,a). Its constructors are kept abstract. Use viewTerm or viewTerm2 to inspect it.

Instances

Typeable1 Term

Foldable Term

Apply BLTerm

Apply LNTerm

Eq a => Eq (Term a)

Data a => Data (Term a)

Ord a => Ord (Term a)

Show a => Show (Term a)

Binary a_1627448972 => Binary (Term a_1627448972)

NFData a_1627448972 => NFData (Term a_1627448972)

Sized a => Sized (Term a)

(HasFrees l, Ord l) => HasFrees (Term l)

data TermView a

View on terms that corresponds to representation.

Constructors

Lit a

FApp FunSym [Term a]

Instances

Eq a => Eq (TermView a)

Ord a => Ord (TermView a)

Show a => Show (TermView a)

viewTerm :: Term a -> TermView a

Return the TermView of the given term.

data TermView2 a

View on terms that distinguishes function application of builtin symbols like exp.

Constructors

FExp (Term a) (Term a)

FInv (Term a)

FMult [Term a]

One

FPMult (Term a) (Term a)

FEMap (Term a) (Term a)

FUnion [Term a]

FPair (Term a) (Term a)

FAppNoEq NoEqSym [Term a]

FAppC CSym [Term a]

FList [Term a]

Lit2 a

Instances

Eq a => Eq (TermView2 a)

Ord a => Ord (TermView2 a)

Show a => Show (TermView2 a)

viewTerm2 :: Show a => Term a -> TermView2 a

Returns the TermView2 of the given term.

Standard function

traverseTerm :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Term a -> f (Term b)

fmapTerm :: (Ord a, Ord b) => (a -> b) -> Term a -> Term b

bindTerm :: (Ord a, Ord b) => Term a -> (a -> Term b) -> Term b

Smart constructors

lit :: a -> Term a

lit l creates a term from the literal l.

fApp :: Ord a => FunSym -> [Term a] -> Term a

fApp fsym as creates an application of fsym to as. The function ensures that the resulting term is in AC-normal-form.

fAppAC :: Ord a => ACSym -> [Term a] -> Term a

Smart constructor for AC terms.

fAppC :: Ord a => CSym -> [Term a] -> Term a

Smart constructor for AC terms.

fAppNoEq :: NoEqSym -> [Term a] -> Term a

Smart constructor for non-AC terms.

fAppList :: [Term a] -> Term a

Smart constructor for list terms.

unsafefApp :: FunSym -> [Term a] -> Term a

unsafefApp fsym as creates an application of fsym to as. The caller has to ensure that the resulting term is in AC-normal-form.