Safe Haskell  SafeInferred 

Language  Haskell2010 
Term rewriting.
Synopsis
 data Rule f = Rule {
 orientation :: Orientation f
 rule_proof :: !(Proof f)
 lhs :: !(Term f)
 rhs :: !(Term f)
 type RuleOf a = Rule (ConstantOf a)
 ruleDerivation :: Rule f > Derivation f
 data Orientation f
 = Oriented
  WeaklyOriented !(Fun f) [Term f]
  Permutative [(Term f, Term f)]
  Unoriented
 oriented :: Orientation f > Bool
 unorient :: Rule f > Equation f
 orient :: Function f => Equation f > Proof f > Rule f
 backwards :: Rule f > Rule f
 simplify :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f
 simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f
 simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f
 simpleRewrite :: (Function f, Has a (Rule f)) => Index f a > Term f > Maybe (Rule f, Subst f)
 type Strategy f = Term f > [Reduction f]
 type Reduction f = [Rule f]
 trans :: Reduction f > Reduction f > Reduction f
 result :: Term f > Reduction f > Term f
 reductionProof :: Function f => Term f > Reduction f > Derivation f
 ruleResult :: Term f > Rule f > Term f
 ruleProof :: Function f => Term f > Rule f > Derivation f
 normaliseWith :: Function f => (Term f > Bool) > Strategy f > Term f > Reduction f
 normalForms :: Function f => Strategy f > Map (Term f) (Reduction f) > Map (Term f) (Term f, Reduction f)
 successors :: Function f => Strategy f > Map (Term f) (Reduction f) > Map (Term f) (Term f, Reduction f)
 successorsAndNormalForms :: Function f => Strategy f > Map (Term f) (Reduction f) > (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f))
 anywhere :: Strategy f > Strategy f
 anywhereOutermost :: Strategy f > Strategy f
 anywhereInnermost :: Strategy f > Strategy f
 rewrite :: (Function f, Has a (Rule f)) => (Rule f > Subst f > Bool) > Index f a > Strategy f
 tryRule :: (Function f, Has a (Rule f)) => (Rule f > Subst f > Bool) > a > Strategy f
 reducesWith :: Function f => (Term f > Term f > Bool) > Rule f > Subst f > Bool
 reduces :: Function f => Rule f > Subst f > Bool
 reducesOriented :: Function f => Rule f > Subst f > Bool
 reducesInModel :: Function f => Model f > Rule f > Subst f > Bool
 reducesSkolem :: Function f => Rule f > Subst f > Bool
Rewrite rules.
A rewrite rule.
Rule  

Instances
(Labelled f, Show f) => Show (Rule f) Source #  
Eq (Rule f) Source #  
Ord (Rule f) Source #  
(Labelled f, PrettyTerm f) => Pretty (Rule f) Source #  
Defined in Twee.Rule pPrintPrec :: PrettyLevel > Rational > Rule f > Doc # pPrintList :: PrettyLevel > [Rule f] > Doc #  
Symbolic (Rule f) Source #  
f ~ g => Has (Active f) (Rule g) Source #  
f ~ g => Has (Rule f) (Rule g) Source #  
f ~ g => Has (Rule f) (Term g) Source #  
type ConstantOf (Rule f) Source #  
Defined in Twee.Rule 
type RuleOf a = Rule (ConstantOf a) Source #
ruleDerivation :: Rule f > Derivation f Source #
data Orientation f Source #
A rule's orientation.
Oriented
and WeaklyOriented
rules are used only lefttoright.
Permutative
and Unoriented
rules are used bidirectionally.
Oriented  An oriented rule. 
WeaklyOriented !(Fun f) [Term f]  A weakly oriented rule. The first argument is the minimal constant, the second argument is a list of terms which are weakly oriented in the rule. A rule with orientation 
Permutative [(Term f, Term f)]  A permutative rule. A rule with orientation 
Unoriented  An unoriented rule. 
Instances
oriented :: Orientation f > Bool Source #
Is a rule oriented or weakly oriented?
orient :: Function f => Equation f > Proof f > Rule f Source #
Turn an equation t :=: u into a rule t > u by computing the orientation info (e.g. oriented, permutative or unoriented).
Crashes if either t < u
, or there is a variable in u
which is
not in t
. To avoid this problem, combine with split
.
Extrafast rewriting, without proof output or unorientable rules.
simplify :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f Source #
Compute the normal form of a term wrt only oriented rules.
simplifyOutermost :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f Source #
Compute the normal form of a term wrt only oriented rules, using outermost reduction.
simplifyInnermost :: (Function f, Has a (Rule f)) => Index f a > Term f > Term f Source #
Compute the normal form of a term wrt only oriented rules, using innermost reduction.
simpleRewrite :: (Function f, Has a (Rule f)) => Index f a > Term f > Maybe (Rule f, Subst f) Source #
Find a simplification step that applies to a term.
Rewriting, with proof output.
type Strategy f = Term f > [Reduction f] Source #
A strategy gives a set of possible reductions for a term.
type Reduction f = [Rule f] Source #
A reduction proof is just a sequence of rewrite steps, stored as a list in reverse order. In each rewrite step, all subterms that are exactly equal to the LHS of the rule are replaced by the RHS, i.e. the rewrite step is performed as a parallel rewrite without matching.
result :: Term f > Reduction f > Term f Source #
Compute the final term resulting from a reduction, given the starting term.
reductionProof :: Function f => Term f > Reduction f > Derivation f Source #
Turn a reduction into a proof.
Normalisation.
normaliseWith :: Function f => (Term f > Bool) > Strategy f > Term f > Reduction f Source #
Normalise a term wrt a particular strategy.
normalForms :: Function f => Strategy f > Map (Term f) (Reduction f) > Map (Term f) (Term f, Reduction f) Source #
Compute all normal forms of a set of terms wrt a particular strategy.
successors :: Function f => Strategy f > Map (Term f) (Reduction f) > Map (Term f) (Term f, Reduction f) Source #
Compute all successors of a set of terms (a successor of a term t
is a term u
such that t >* u
).
successorsAndNormalForms :: Function f => Strategy f > Map (Term f) (Reduction f) > (Map (Term f) (Term f, Reduction f), Map (Term f) (Term f, Reduction f)) Source #
anywhereOutermost :: Strategy f > Strategy f Source #
Apply a strategy anywhere in a term, preferring outermost reductions.
anywhereInnermost :: Strategy f > Strategy f Source #
Apply a strategy anywhere in a term, preferring innermost reductions.
Basic strategies. These only apply at the root of the term.
rewrite :: (Function f, Has a (Rule f)) => (Rule f > Subst f > Bool) > Index f a > Strategy f Source #
A strategy which rewrites using an index.
tryRule :: (Function f, Has a (Rule f)) => (Rule f > Subst f > Bool) > a > Strategy f Source #
A strategy which applies one rule only.
reducesWith :: Function f => (Term f > Term f > Bool) > Rule f > Subst f > Bool Source #
Check if a rule can be applied, given an ordering <= on terms.
reducesOriented :: Function f => Rule f > Subst f > Bool Source #
Check if a rule can be applied and is oriented.