Maintainer | Benedikt Schmidt <beschmi@gmail.com> |
---|---|
Safe Haskell | None |
Terms with variables and constants.
- data Lit c v
- type VTerm c v = Term (Lit c v)
- varTerm :: v -> VTerm c v
- constTerm :: c -> VTerm c v
- varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]
- occursVTerm :: Eq v => v -> VTerm c v -> Bool
- constsVTerm :: IsConst c => VTerm c v -> [c]
- isVar :: VTerm c v -> Bool
- termVar :: VTerm c v -> Maybe v
- termVar' :: (Show c, Show v) => VTerm c v -> v
- class (Ord v, Eq v, Show v) => IsVar v
- class (Ord c, Eq c, Show c, Data c) => IsConst c
- prettyTerm :: (Document d, Show l) => (l -> d) -> Term l -> d
- showFunSymName :: FunSym -> String
- lits :: Ord a => Term a -> [a]
- fAppOne :: Term a
- fAppExp :: Ord a => (Term a, Term a) -> Term a
- fAppInv :: Term a -> Term a
- fAppPMult :: Ord a => (Term a, Term a) -> Term a
- fAppEMap :: Ord a => (Term a, Term a) -> Term a
- fAppPair :: Ord a => (Term a, Term a) -> Term a
- fAppFst :: Term a -> Term a
- fAppSnd :: Term a -> Term a
- isPair :: Show a => Term a -> Bool
- isInverse :: Show a => Term a -> Bool
- isProduct :: Show a => Term a -> Bool
- isUnion :: Show a => Term a -> Bool
- isEMap :: Show a => Term a -> Bool
- isNullaryPublicFunction :: Term a -> Bool
- isPrivateFunction :: Term a -> Bool
- data FunSym
- data ACSym
- data CSym = EMap
- data Privacy
- type NoEqSym = (ByteString, (Int, Privacy))
- type FunSig = Set FunSym
- type NoEqFunSig = Set NoEqSym
- expSymString :: ByteString
- invSymString :: ByteString
- pmultSymString :: ByteString
- emapSymString :: ByteString
- unionSymString :: ByteString
- expSym :: NoEqSym
- pmultSym :: NoEqSym
- dhFunSig :: FunSig
- bpFunSig :: FunSig
- msetFunSig :: FunSig
- pairFunSig :: NoEqFunSig
- dhReducibleFunSig :: FunSig
- bpReducibleFunSig :: FunSig
- implicitFunSig :: FunSig
- class Sized a where
- data Term a
- data TermView a
- viewTerm :: Term a -> TermView a
- data TermView2 a
- viewTerm2 :: Show a => Term a -> TermView2 a
- 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
- lit :: a -> Term a
- fApp :: Ord a => FunSym -> [Term a] -> Term a
- fAppAC :: Ord a => ACSym -> [Term a] -> Term a
- fAppC :: Ord a => CSym -> [Term a] -> Term a
- fAppNoEq :: NoEqSym -> [Term a] -> Term a
- fAppList :: [Term a] -> Term a
- unsafefApp :: FunSym -> [Term a] -> Term a
Terms with constants and variables
A Lit is either a constant or a variable. (Const
is taken by Control.Applicative)
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) |
varsVTerm :: (Eq v, Ord v) => VTerm c v -> [v]Source
vars t
returns a duplicate-free list of variables that occur in t
.
occursVTerm :: Eq v => v -> VTerm c v -> BoolSource
occurs v t
returns True
if v
occurs in t
constsVTerm :: IsConst c => VTerm c v -> [c]Source
constsVTerm t
returns a duplicate-free list of constants that occur in t
.
Destructors
termVar' :: (Show c, Show v) => VTerm c v -> vSource
Extract just the variable from a term that must be variable, throw an error if this fails.
Pretty printing and query functions.
prettyTerm :: (Document d, Show l) => (l -> d) -> Term l -> dSource
Pretty print a term.
showFunSymName :: FunSym -> StringSource
Convert a function symbol to its name.
lits :: Ord a => Term a -> [a]Source
lits t
returns all literals that occur in term t
. List can contain duplicates.
Smart constructors
fAppExp :: Ord a => (Term a, Term a) -> Term aSource
Smart constructors for pair, exp, pmult, and emap.
fAppPMult :: Ord a => (Term a, Term a) -> Term aSource
Smart constructors for pair, exp, pmult, and emap.
fAppEMap :: Ord a => (Term a, Term a) -> Term aSource
Smart constructors for pair, exp, pmult, and emap.
fAppPair :: Ord a => (Term a, Term a) -> Term aSource
Smart constructors for pair, exp, pmult, and emap.
Destructors and classifiers
isNullaryPublicFunction :: Term a -> BoolSource
True
iff the term is a nullary, public function.
isPrivateFunction :: Term a -> BoolSource
AC, C, and NonAC funcion symbols
Function symbols
AC function symbols.
C(ommutative) function symbols
A function symbol can be either Private (unknown to adversary) or Public.
= (ByteString, (Int, Privacy)) | operator name, arity, private |
NoEq function symbols (with respect to the background theory).
Signatures
type NoEqFunSig = Set NoEqSymSource
NoEq function signatures.
concrete symbols strings
Function symbols
concrete signatures
The signature for the multiset function symbols.
pairFunSig :: NoEqFunSigSource
The signature for pairing.
dhReducibleFunSig :: FunSigSource
Reducible function symbols for DH.
bpReducibleFunSig :: FunSigSource
Reducible function symbols for BP.
implicitFunSig :: FunSigSource
Implicit function symbols.
Terms
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) |
View on terms that corresponds to representation.
View on terms that distinguishes function application of builtin symbols like exp.
Standard function
traverseTerm :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Term a -> f (Term b)Source
Smart constructors
fApp :: Ord a => FunSym -> [Term a] -> Term aSource
fApp fsym as
creates an application of fsym
to as
. The function
ensures that the resulting term is in AC-normal-form.
unsafefApp :: FunSym -> [Term a] -> Term aSource
unsafefApp fsym as
creates an application of fsym
to as. The
caller has to ensure that the resulting term is in AC-normal-form.