Safe Haskell | None |
---|---|
Language | Haskell2010 |
Term rewriting.
Synopsis
- data Rule f = Rule {
- orientation :: !(Orientation f)
- lhs :: !(Term f)
- rhs :: !(Term f)
- type RuleOf a = Rule (ConstantOf a)
- data Orientation f
- = Oriented
- | WeaklyOriented !(Fun f) [Term f]
- | Permutative [(Term f, Term f)]
- | Unoriented
- oriented :: Orientation f -> Bool
- weaklyOriented :: Orientation f -> Bool
- unorient :: Rule f -> Equation f
- orient :: Function f => Equation f -> Rule f
- backwards :: Rule f -> Rule f
- simplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
- simplify1 :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Term f
- canSimplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Bool
- canSimplifyList :: (Function f, Has a (Rule f)) => Index f a -> TermList f -> Bool
- simpleRewrite :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Maybe (Rule f, Subst f)
- type Strategy f = Term f -> [Reduction f]
- data Reduction f
- trans :: Reduction f -> Reduction f -> Reduction f
- cong :: Fun f -> [Reduction f] -> Reduction f
- steps :: Reduction f -> [Reduction f]
- reductionProof :: Reduction f -> Derivation f
- step :: (Has a (Rule f), Has a (Proof f)) => a -> Subst f -> Reduction f
- data Resulting f = Resulting {}
- reduce :: Reduction f -> Resulting f
- normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Resulting f
- normalForms :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f)
- successors :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f)
- successorsAndNormalForms :: Function f => Strategy f -> Set (Resulting f) -> (Set (Resulting f), Set (Resulting f))
- anywhere :: Strategy f -> Strategy f
- nested :: Strategy f -> Strategy f
- parallel :: PrettyTerm f => Strategy f -> Strategy f
- rewrite :: (Function f, Has a (Rule f), Has a (Proof f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
- tryRule :: (Function f, Has a (Rule f), Has a (Proof 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 # | |
Show (Rule f) Source # | |
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 (ActiveRule f) (Rule g) Source # | |
type ConstantOf (Rule f) Source # | |
Defined in Twee.Rule |
type RuleOf a = Rule (ConstantOf a) 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?
weaklyOriented :: Orientation f -> Bool Source #
Is a rule weakly oriented?
orient :: Function f => Equation 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 t -> u is not a valid rule, for example if there is
a variable in u
which is not in t
. To prevent this happening,
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.
canSimplify :: (Function f, Has a (Rule f)) => Index f a -> Term f -> Bool Source #
Check if a term can be simplified.
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.
A multi-step rewrite proof t ->* u
Step !(Proof f) !(Rule f) !(Subst f) | Apply a single rewrite rule to the root of a term |
Refl !(Term f) | Reflexivity |
Trans !(Reduction f) !(Reduction f) | Transivitity |
Cong !(Fun f) ![Reduction f] | Congruence |
Instances
Show (Reduction f) Source # | |
Function f => Pretty (Reduction f) Source # | |
Defined in Twee.Rule pPrintPrec :: PrettyLevel -> Rational -> Reduction f -> Doc # pPrint :: Reduction f -> Doc # pPrintList :: PrettyLevel -> [Reduction f] -> Doc # | |
Symbolic (Reduction f) Source # | |
type ConstantOf (Reduction f) Source # | |
Defined in Twee.Rule |
trans :: Reduction f -> Reduction f -> Reduction f Source #
A smart constructor for Trans which simplifies Refl.
cong :: Fun f -> [Reduction f] -> Reduction f Source #
A smart constructor for Cong which simplifies Refl.
steps :: Reduction f -> [Reduction f] Source #
The list of all rewrite rules used in a rewrite proof.
reductionProof :: Reduction f -> Derivation f Source #
Turn a reduction into a proof.
step :: (Has a (Rule f), Has a (Proof f)) => a -> Subst f -> Reduction f Source #
Construct a basic rewrite step.
A rewrite proof with the final term attached.
Has an Ord
instance which compares the final term.
Instances
Eq (Resulting f) Source # | |
Ord (Resulting f) Source # | |
Show (Resulting f) Source # | |
Function f => Pretty (Resulting f) Source # | |
Defined in Twee.Rule pPrintPrec :: PrettyLevel -> Rational -> Resulting f -> Doc # pPrint :: Resulting f -> Doc # pPrintList :: PrettyLevel -> [Resulting f] -> Doc # | |
Symbolic (Resulting f) Source # | |
type ConstantOf (Resulting f) Source # | |
Defined in Twee.Rule |
Strategy combinators.
normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Resulting f Source #
Normalise a term wrt a particular strategy.
normalForms :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting f) Source #
Compute all normal forms of a set of terms wrt a particular strategy.
successors :: Function f => Strategy f -> Set (Resulting f) -> Set (Resulting 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 -> Set (Resulting f) -> (Set (Resulting f), Set (Resulting f)) Source #
parallel :: PrettyTerm f => Strategy f -> Strategy f Source #
Apply a strategy in parallel in as many places as possible. Takes only the first rewrite of each strategy.
Basic strategies. These only apply at the root of the term.
rewrite :: (Function f, Has a (Rule f), Has a (Proof 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), Has a (Proof 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.