Safe Haskell | None |
---|---|
Language | Haskell2010 |
- module Twee.Term
- module Twee.Pretty
- class Symbolic a where
- type ConstantOf a
- subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a
- terms :: Symbolic a => a -> [TermListOf a]
- type TermOf a = Term (ConstantOf a)
- type TermListOf a = TermList (ConstantOf a)
- type SubstOf a = Subst (ConstantOf a)
- type TriangleSubstOf a = TriangleSubst (ConstantOf a)
- type BuilderOf a = Builder (ConstantOf a)
- type FunOf a = Fun (ConstantOf a)
- vars :: Symbolic a => a -> [Var]
- isGround :: Symbolic a => a -> Bool
- funs :: Symbolic a => a -> [FunOf a]
- occ :: Symbolic a => FunOf a -> a -> Int
- occVar :: Symbolic a => Var -> a -> Int
- canonicalise :: Symbolic a => a -> a
- renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b
- newtype Id = Id {}
- class Has a b where
- class Minimal f where
- minimalTerm :: Minimal f => Term f
- isMinimal :: Minimal f => Term f -> Bool
- erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a
- class Skolem f where
- class Arity f where
- class Sized a where
- class Ord f => Ordered f where
- lessThan :: Ordered f => Term f -> Term f -> Bool
- orientTerms :: Ordered f => Term f -> Term f -> Maybe Ordering
- class EqualsBonus f where
- data Strictness
- type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, EqualsBonus f)
- data Extended f
Re-exported functionality
module Twee.Term
module Twee.Pretty
The Symbolic
typeclass
class Symbolic a where Source #
Generalisation of term functionality to things that contain terms (e.g., rewrite rules and equations).
type ConstantOf a Source #
termsDL :: a -> DList (TermListOf a) Source #
Symbolic a => Symbolic [a] Source # | |
Symbolic a => Symbolic (Maybe a) Source # | |
Symbolic (Term f) Source # | |
Symbolic (TermList f) Source # | |
Symbolic (Subst f) Source # | |
Symbolic (Equation f) Source # | |
Symbolic (Derivation f) Source # | |
Symbolic (Resulting f) Source # | |
Symbolic (Reduction f) Source # | |
Symbolic (Orientation f) Source # | |
Symbolic (Rule f) Source # | |
Symbolic (CriticalPair f) Source # | |
PrettyTerm f => Symbolic (ActiveRule f) Source # | |
((~) * (ConstantOf a) (ConstantOf b), Symbolic a, Symbolic b) => Symbolic (a, b) Source # | |
((~) * (ConstantOf a) (ConstantOf b), (~) * (ConstantOf a) (ConstantOf c), Symbolic a, Symbolic b, Symbolic c) => Symbolic (a, b, c) Source # | |
subst :: (Symbolic a, Substitution s, SubstFun s ~ ConstantOf a) => s -> a -> a Source #
Apply a substitution.
terms :: Symbolic a => a -> [TermListOf a] Source #
Find all terms occuring in the argument.
type TermListOf a = TermList (ConstantOf a) Source #
A termlist compatible with a given Symbolic
.
type TriangleSubstOf a = TriangleSubst (ConstantOf a) Source #
A triangle substitution compatible with a given Symbolic
.
type FunOf a = Fun (ConstantOf a) Source #
The underlying type of function symbols of a given Symbolic
.
occ :: Symbolic a => FunOf a -> a -> Int Source #
Count how many times a function symbol occurs in the argument.
occVar :: Symbolic a => Var -> a -> Int Source #
Count how many times a variable occurs in the argument.
canonicalise :: Symbolic a => a -> a Source #
Rename the argument so that variables are introduced in a canonical order (starting with V0, then V1 and so on).
renameAvoiding :: (Symbolic a, Symbolic b) => a -> b -> b Source #
Rename the second argument so that it does not mention any variable which occurs in the first.
General-purpose functionality
Represents a unique identifier (e.g., for a rule).
An instance
indicates that a value of type Has
a ba
contains a value
of type b
which is somehow part of the meaning of the a
.
A number of functions use Has
constraints to work in a more general setting.
For example, the functions in CP
operate on rewrite rules, but actually
accept any a
satisfying
.Has
a (Rule
f)
Use taste when definining Has
instances; don't do it willy-nilly.
Has a a Source # | |
Has (ActiveRule f) Depth Source # | |
Has (ActiveRule f) RuleId Source # | |
Has (ActiveRule f) Id Source # | |
(~) * f g => Has (Rule f) (Term g) Source # | |
(~) * f g => Has (ActiveRule f) (Positions g) Source # | |
(~) * f g => Has (ActiveRule f) (Lemma g) Source # | |
(~) * f g => Has (ActiveRule f) (Proof g) Source # | |
(~) * f g => Has (ActiveRule f) (Rule g) Source # | |
Typeclasses
minimalTerm :: Minimal f => Term f Source #
Build the minimal constant as a term.
erase :: (Symbolic a, ConstantOf a ~ f, Minimal f) => [Var] -> a -> a Source #
Erase a given set of variables from the argument, replacing them with the minimal constant.
Construction of Skolem constants.
For types which have a notion of arity.
For types which have a notion of size.
class Ord f => Ordered f where Source #
lessEq :: Term f -> Term f -> Bool Source #
Return True
if the first term is less than or equal to the second,
in the term ordering.
lessIn :: Model f -> Term f -> Term f -> Maybe Strictness Source #
Check if the first term is less than or equal to the second in the given model, and decide whether the inequality is strict or nonstrict.
lessThan :: Ordered f => Term f -> Term f -> Bool Source #
Return True
if the first argument is strictly less than the second,
in the term ordering.
class EqualsBonus f where Source #
A hack for encoding Horn clauses. See Score
.
The default implementation of hasEqualsBonus
should work OK.
EqualsBonus f => EqualsBonus (Fun f) Source # | |
EqualsBonus f => EqualsBonus (Extended f) Source # | |
data Strictness Source #
Describes whether an inequality is strict or nonstrict.
type Function f = (Ordered f, Arity f, Sized f, Minimal f, Skolem f, PrettyTerm f, EqualsBonus f) Source #
The collection of constraints which the type of function symbols must satisfy in order to be used by twee.
A function symbol extended with a minimal constant and Skolem functions.
Comes equipped with Minimal
and Skolem
instances.
Functor Extended Source # | |
Eq f => Eq (Extended f) Source # | |
Ord f => Ord (Extended f) Source # | |
Show f => Show (Extended f) Source # | |
Pretty f => Pretty (Extended f) Source # | |
PrettyTerm f => PrettyTerm (Extended f) Source # | |
(Typeable * f, Ord f) => Minimal (Extended f) Source # | |
EqualsBonus f => EqualsBonus (Extended f) Source # | |
Sized f => Sized (Extended f) Source # | |
Arity f => Arity (Extended f) Source # | |
(Typeable * f, Ord f) => Skolem (Extended f) Source # | |