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 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_1627456936, Binary v_1627456937) => Binary (Lit c_1627456936 v_1627456937)

(NFData c_1627456936, NFData v_1627456937) => NFData (Lit c_1627456936 v_1627456937)

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

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

Signatures and function symbols

data FunSym

Function symbols

Constructors

NonAC NonACSym

a non-AC function function symbol of a given arity

AC ACSym

an AC function symbol, can be used n-ary

List

a non-AC 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

Xor

Mult

Instances

Eq ACSym

Data ACSym

Ord ACSym

Show ACSym

Typeable ACSym

Binary ACSym

NFData ACSym

type NonACSym = (ByteString, Int)

non-AC function symbols

type FunSig = Set NonACSym

Function signatures.

dhFunSig :: FunSig

The signature for the non-AC Diffie-Hellman function symbols.

xorFunSig :: FunSig

The signature for the non-AC Xor function symbols.

msetFunSig :: FunSig

The signature for then non-AC multiset function symbols.

pairFunSig :: FunSig

The signature for pairing.

dhReducibleFunSig :: FunSig

Reducible non-AC symbols for DH.

implicitFunSig :: FunSig

Implicit non-AC symbols.

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 LNTerm

Eq a => Eq (Term a)

Data a => Data (Term a)

Ord a => Ord (Term a)

Show a => Show (Term a)

Binary a_1627404145 => Binary (Term a_1627404145)

NFData a_1627404145 => NFData (Term a_1627404145)

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

FXor [Term a]

Zero

FUnion [Term a]

Empty

FPair (Term a) (Term a)

FAppNonAC NonACSym [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.

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

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

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

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

Pretty print a term.

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.

fAppNonAC :: NonACSym -> [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.

fAppMult, fAppXor, fAppUnion :: Ord a => [Term a] -> Term a

Smart constructors for mult, union, and xor.

fAppOne, fAppEmpty, fAppZero :: Term a

Smart constructors for one, zero, and empty.

fAppPair, fAppExp :: (Term a, Term a) -> Term a

Smart constructors for pair and exp.

fAppInv, fAppSnd, fAppFst :: Term a -> Term a

Smart constructors for inv, fst, and snd.

Destructors and classifiers

destPair :: Term a -> Maybe (Term a, Term a)

Destruct a top-level pair.

destInverse :: Term a -> Maybe (Term a)

Destruct a top-level inverse in the group of exponents.

destProduct :: Term a -> Maybe [Term a]

Destruct a top-level product.

destXor :: Term a -> Maybe [Term a]

Destruct a top-level product.

destUnion :: Term a -> Maybe [Term a]

Destruct a top-level multiset union.

isPair :: Term a -> Bool

True iff the term is a well-formed pair.

isInverse :: Term a -> Bool

True iff the term is a well-formed inverse.

isProduct :: Term a -> Bool

True iff the term is a well-formed product.

isXor :: Term a -> Bool

True iff the term is a well-formed xor'ing.

isUnion :: Term a -> Bool

True iff the term is a well-formed xor'ing.

class Sized a where

Methods

size :: a -> Int

Instances

Sized Variant

Sized a => Sized [a]

Sized a => Sized (Term a)

Sized (Lit c v)

Sized (SubstVFresh c v)

Sized (Subst c v)