twee-lib-2.4.2: An equational theorem prover

Twee.Rule

Description

Term rewriting.

Synopsis

# Rewrite rules.

data Rule f Source #

A rewrite rule.

Constructors

 Rule Fieldsorientation :: Orientation fInformation about whether and how the rule is oriented.rule_proof :: !(Proof f)A proof that the rule holds.lhs :: !(Term f)The left-hand side of the rule.rhs :: !(Term f)The right-hand side of the rule.

#### Instances

Instances details
 (Labelled f, Show f) => Show (Rule f) Source # Instance detailsDefined in Twee.Rule MethodsshowsPrec :: Int -> Rule f -> ShowS #show :: Rule f -> String #showList :: [Rule f] -> ShowS # Eq (Rule f) Source # Instance detailsDefined in Twee.Rule Methods(==) :: Rule f -> Rule f -> Bool #(/=) :: Rule f -> Rule f -> Bool # Ord (Rule f) Source # Instance detailsDefined in Twee.Rule Methodscompare :: Rule f -> Rule f -> Ordering #(<) :: Rule f -> Rule f -> Bool #(<=) :: Rule f -> Rule f -> Bool #(>) :: Rule f -> Rule f -> Bool #(>=) :: Rule f -> Rule f -> Bool #max :: Rule f -> Rule f -> Rule f #min :: Rule f -> Rule f -> Rule f # (Labelled f, PrettyTerm f) => Pretty (Rule f) Source # Instance detailsDefined in Twee.Rule MethodspPrintPrec :: PrettyLevel -> Rational -> Rule f -> Doc #pPrint :: Rule f -> Doc #pPrintList :: PrettyLevel -> [Rule f] -> Doc # Symbolic (Rule f) Source # Instance detailsDefined in Twee.Rule Associated Typestype ConstantOf (Rule f) Source # MethodstermsDL :: Rule f -> DList (TermListOf (Rule f)) Source #subst_ :: (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f Source # f ~ g => Has (Active f) (Rule g) Source # Instance detailsDefined in Twee Methodsthe :: Active f -> Rule g Source # f ~ g => Has (Rule f) (Rule g) Source # Instance detailsDefined in Twee.Rule Methodsthe :: Rule f -> Rule g Source # f ~ g => Has (Rule f) (Term g) Source # Instance detailsDefined in Twee.Rule Methodsthe :: Rule f -> Term g Source # type ConstantOf (Rule f) Source # Instance detailsDefined in Twee.Rule type ConstantOf (Rule f) = f

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.

Constructors

 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 WeaklyOriented k ts can be used unless all terms in ts are equal to k. Permutative [(Term f, Term f)] A permutative rule.A rule with orientation Permutative ts can be used if map fst ts is lexicographically greater than map snd ts. Unoriented An unoriented rule.

#### Instances

Instances details
 (Labelled f, Show f) => Show (Orientation f) Source # Instance detailsDefined in Twee.Rule MethodsshowsPrec :: Int -> Orientation f -> ShowS #show :: Orientation f -> String #showList :: [Orientation f] -> ShowS # Source # Instance detailsDefined in Twee.Rule Methods(==) :: Orientation f -> Orientation f -> Bool #(/=) :: Orientation f -> Orientation f -> Bool # Source # Instance detailsDefined in Twee.Rule Methodscompare :: Orientation f -> Orientation f -> Ordering #(<) :: Orientation f -> Orientation f -> Bool #(<=) :: Orientation f -> Orientation f -> Bool #(>) :: Orientation f -> Orientation f -> Bool #(>=) :: Orientation f -> Orientation f -> Bool #max :: Orientation f -> Orientation f -> Orientation f #min :: Orientation f -> Orientation f -> Orientation f # Source # Instance detailsDefined in Twee.Rule Associated Typestype ConstantOf (Orientation f) Source # Methodssubst_ :: (Var -> BuilderOf (Orientation f)) -> Orientation f -> Orientation f Source # type ConstantOf (Orientation f) Source # Instance detailsDefined in Twee.Rule type ConstantOf (Orientation f) = f

Is a rule oriented or weakly oriented?

unorient :: Rule f -> Equation f Source #

Turn a rule into an equation.

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.

backwards :: Rule f -> Rule f Source #

Flip an unoriented rule so that it goes right-to-left.

# 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.

trans :: Reduction f -> Reduction f -> Reduction f Source #

Transitivity for reduction sequences.

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.

ruleResult :: Term f -> Rule f -> Term f Source #

# 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).

Apply a strategy anywhere in a term.

Apply a strategy anywhere in a term, preferring outermost reductions.

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.

reduces :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied normally.

reducesOriented :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied and is oriented.

reducesInModel :: Function f => Model f -> Rule f -> Subst f -> Bool Source #

Check if a rule can be applied in a particular model.

reducesSkolem :: Function f => Rule f -> Subst f -> Bool Source #

Check if a rule can be applied to the Skolemised version of a term.