Safe Haskell | None |
---|---|
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
Eq (Rule f) Source # | |
Ord (Rule f) Source # | |
(Labelled f, Show f) => Show (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 (Rule f) (Term g) Source # | |
f ~ g => Has (Rule f) (Rule g) Source # | |
f ~ g => Has (Active f) (Rule 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 left-to-right.
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
.
Extra-fast 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.