Twee.Rule

Term rewriting.

Rewrite rules.

data Rule f

A rewrite rule.

Constructors

Rule

Fields

• orientation :: Orientation f

  Information 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

Eq (Rule f)

Defined in Twee.Rule

Methods

(==) :: Rule f -> Rule f -> Bool

(/=) :: Rule f -> Rule f -> Bool

Ord (Rule f)

Defined in Twee.Rule

Methods

compare :: 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, Show f) => Show (Rule f)

Defined in Twee.Rule

Methods

showsPrec :: Int -> Rule f -> ShowS

show :: Rule f -> String

showList :: [Rule f] -> ShowS

(Labelled f, PrettyTerm f) => Pretty (Rule f)

Defined in Twee.Rule

Methods

pPrintPrec :: PrettyLevel -> Rational -> Rule f -> Doc

pPrint :: Rule f -> Doc

pPrintList :: PrettyLevel -> [Rule f] -> Doc

Symbolic (Rule f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Rule f)

Methods

termsDL :: Rule f -> DList (TermListOf (Rule f))

subst_ :: (Var -> BuilderOf (Rule f)) -> Rule f -> Rule f

f ~ g => Has (Rule f) (Term g)

Defined in Twee.Rule

Methods

the :: Rule f -> Term g

f ~ g => Has (Rule f) (Rule g)

Defined in Twee.Rule

Methods

the :: Rule f -> Rule g

f ~ g => Has (Active f) (Rule g)

Defined in Twee

Methods

the :: Active f -> Rule g

type ConstantOf (Rule f)

Defined in Twee.Rule

type ConstantOf (Rule f) = f

type RuleOf a = Rule (ConstantOf a)

ruleDerivation :: Rule f -> Derivation f

data Orientation f

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

Eq (Orientation f)

Defined in Twee.Rule

Methods

(==) :: Orientation f -> Orientation f -> Bool

(/=) :: Orientation f -> Orientation f -> Bool

Ord (Orientation f)

Defined in Twee.Rule

Methods

compare :: 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

(Labelled f, Show f) => Show (Orientation f)

Defined in Twee.Rule

Methods

showsPrec :: Int -> Orientation f -> ShowS

show :: Orientation f -> String

showList :: [Orientation f] -> ShowS

Symbolic (Orientation f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Orientation f)

Methods

termsDL :: Orientation f -> DList (TermListOf (Orientation f))

subst_ :: (Var -> BuilderOf (Orientation f)) -> Orientation f -> Orientation f

type ConstantOf (Orientation f)

Defined in Twee.Rule

type ConstantOf (Orientation f) = f

oriented :: Orientation f -> Bool

Is a rule oriented or weakly oriented?

unorient :: Rule f -> Equation f

Turn a rule into an equation.

orient :: Function f => Equation f -> Proof f -> Rule f

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

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

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

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

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)

Find a simplification step that applies to a term.

Rewriting, with proof output.

type Strategy f = Term f -> [Reduction f]

A strategy gives a set of possible reductions for a term.

type Reduction f = [Rule f]

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

Transitivity for reduction sequences.

result :: Term f -> Reduction f -> Term f

Compute the final term resulting from a reduction, given the starting term.

reductionProof :: Function f => Term f -> Reduction f -> Derivation f

Turn a reduction into a proof.

ruleResult :: Term f -> Rule f -> Term f

ruleProof :: Function f => Term f -> Rule f -> Derivation f

Normalisation.

normaliseWith :: Function f => (Term f -> Bool) -> Strategy f -> Term f -> Reduction f

Normalise a term wrt a particular strategy.

normalForms :: Function f => Strategy f -> Map (Term f) (Reduction f) -> Map (Term f) (Term f, Reduction f)

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)

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

anywhere :: Strategy f -> Strategy f

Apply a strategy anywhere in a term.

anywhereOutermost :: Strategy f -> Strategy f

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

anywhereInnermost :: Strategy f -> Strategy f

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

A strategy which rewrites using an index.

tryRule :: (Function f, Has a (Rule f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f

A strategy which applies one rule only.

reducesWith :: Function f => (Term f -> Term f -> Bool) -> Rule f -> Subst f -> Bool

Check if a rule can be applied, given an ordering <= on terms.

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

Check if a rule can be applied normally.

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

Check if a rule can be applied and is oriented.

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

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

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

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