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
- data FunSym
- data ACSym
- type NonACSym = (ByteString, Int)
- type FunSig = Set NonACSym
- dhFunSig :: FunSig
- xorFunSig :: FunSig
- msetFunSig :: FunSig
- pairFunSig :: FunSig
- dhReducibleFunSig :: FunSig
- implicitFunSig :: FunSig
- 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
- lits :: Ord a => Term a -> [a]
- prettyTerm :: Document d => (l -> d) -> Term l -> d
- lit :: a -> Term a
- fApp :: Ord a => FunSym -> [Term a] -> Term a
- fAppAC :: Ord a => ACSym -> [Term a] -> Term a
- fAppNonAC :: NonACSym -> [Term a] -> Term a
- fAppList :: [Term a] -> Term a
- unsafefApp :: FunSym -> [Term a] -> Term a
- fAppMult, fAppXor, fAppUnion :: Ord a => [Term a] -> Term a
- fAppOne, fAppEmpty, fAppZero :: Term a
- fAppPair, fAppExp :: (Term a, Term a) -> Term a
- fAppInv, fAppSnd, fAppFst :: Term a -> Term a
- expSymString :: ByteString
- invSymString :: ByteString
- destPair :: Term a -> Maybe (Term a, Term a)
- destInverse :: Term a -> Maybe (Term a)
- destProduct :: Term a -> Maybe [Term a]
- destXor :: Term a -> Maybe [Term a]
- destUnion :: Term a -> Maybe [Term a]
- isPair :: Term a -> Bool
- isInverse :: Term a -> Bool
- isProduct :: Term a -> Bool
- isXor :: Term a -> Bool
- isUnion :: Term a -> Bool
- class Sized a where
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_1627456989, Binary v_1627456990) => Binary (Lit c_1627456989 v_1627456990) | |
(NFData c_1627456989, NFData v_1627456990) => NFData (Lit c_1627456989 v_1627456990) | |
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.
Signatures and function symbols
Function symbols
AC function symbols.
type NonACSym = (ByteString, Int)Source
non-AC function symbols
The signature for then non-AC multiset function symbols.
The signature for pairing.
dhReducibleFunSig :: FunSigSource
Reducible non-AC symbols for DH.
implicitFunSig :: FunSigSource
Implicit non-AC 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_1627404171 => Binary (Term a_1627404171) | |
NFData a_1627404171 => NFData (Term a_1627404171) | |
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.
traverseTerm :: (Applicative f, Ord a, Ord b) => (a -> f b) -> Term a -> f (Term b)Source
lits :: Ord a => Term a -> [a]Source
lits t
returns all literals that occur in term t
. List can contain duplicates.
prettyTerm :: Document d => (l -> d) -> Term l -> dSource
Pretty print a term.
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.
fAppMult, fAppXor, fAppUnion :: Ord a => [Term a] -> Term aSource
Smart constructors for mult, union, and xor.
exp symbol
Destructors and classifiers
destInverse :: Term a -> Maybe (Term a)Source
Destruct a top-level inverse in the group of exponents.
destProduct :: Term a -> Maybe [Term a]Source
Destruct a top-level product.