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.

• lhs :: !(Term f)

  The left-hand side of the rule.

• rhs :: !(Term f)

  The right-hand side of the rule.

Instances

Eq (Rule f)

Methods

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

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

Ord (Rule f)

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

Show (Rule f)

Methods

showsPrec :: Int -> Rule f -> ShowS

show :: Rule f -> String

showList :: [Rule f] -> ShowS

PrettyTerm f => Pretty (Rule f)

Methods

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

pPrint :: Rule f -> Doc

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

Symbolic (Rule f)

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)

Methods

the :: Rule f -> Term g

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

Methods

the :: ActiveRule f -> Rule g

type ConstantOf (Rule f)

type ConstantOf (Rule f) = f

type RuleOf a = Rule (ConstantOf a)

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)

Methods

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

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

Ord (Orientation f)

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

Show (Orientation f)

Methods

showsPrec :: Int -> Orientation f -> ShowS

show :: Orientation f -> String

showList :: [Orientation f] -> ShowS

Symbolic (Orientation f)

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)

type ConstantOf (Orientation f) = f

oriented :: Orientation f -> Bool

Is a rule oriented or weakly oriented?

weaklyOriented :: Orientation f -> Bool

Is a rule weakly oriented?

unorient :: Rule f -> Equation f

Turn a rule into an equation.

orient :: Function f => Equation 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 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.

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.

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

Check if a term can be simplified.

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)

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.

data Reduction f

A multi-step rewrite proof t ->* u

Constructors

Step !(Lemma 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)

Methods

showsPrec :: Int -> Reduction f -> ShowS

show :: Reduction f -> String

showList :: [Reduction f] -> ShowS

Function f => Pretty (Reduction f)

Methods

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

pPrint :: Reduction f -> Doc

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

Symbolic (Reduction f)

Associated Types

type ConstantOf (Reduction f) :: *

Methods

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

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

type ConstantOf (Reduction f)

type ConstantOf (Reduction f) = f

trans :: Reduction f -> Reduction f -> Reduction f

A smart constructor for Trans which simplifies Refl.

cong :: Fun f -> [Reduction f] -> Reduction f

A smart constructor for Cong which simplifies Refl.

steps :: Reduction f -> [Reduction f]

The list of all rewrite rules used in a rewrite proof.

reductionProof :: Reduction f -> Derivation f

Turn a reduction into a proof.

step :: (Has a (Rule f), Has a (Lemma f)) => a -> Subst f -> Reduction f

Construct a basic rewrite step.

data Resulting f

A rewrite proof with the final term attached. Has an Ord instance which compares the final term.

Constructors

Resulting

Fields

• result :: !(Term f)
• reduction :: !(Reduction f)

Instances

Eq (Resulting f)

Methods

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

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

Ord (Resulting f)

Methods

compare :: Resulting f -> Resulting f -> Ordering

(<) :: Resulting f -> Resulting f -> Bool

(<=) :: Resulting f -> Resulting f -> Bool

(>) :: Resulting f -> Resulting f -> Bool

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

max :: Resulting f -> Resulting f -> Resulting f

min :: Resulting f -> Resulting f -> Resulting f

Show (Resulting f)

Methods

showsPrec :: Int -> Resulting f -> ShowS

show :: Resulting f -> String

showList :: [Resulting f] -> ShowS

Function f => Pretty (Resulting f)

Methods

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

pPrint :: Resulting f -> Doc

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

Symbolic (Resulting f)

Associated Types

type ConstantOf (Resulting f) :: *

Methods

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

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

type ConstantOf (Resulting f)

type ConstantOf (Resulting f) = f

reduce :: Reduction f -> Resulting f

Construct a Resulting from a Reduction.

Strategy combinators.

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

Normalise a term wrt a particular strategy.

normalForms :: Function f => Strategy f -> [Resulting f] -> Set (Resulting f)

Compute all normal forms of a set of terms wrt a particular strategy.

successors :: Function f => Strategy f -> [Resulting f] -> Set (Resulting 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 -> [Resulting f] -> (Set (Resulting f), Set (Resulting f))

anywhere :: Strategy f -> Strategy f

Apply a strategy anywhere in a term.

nested :: Strategy f -> Strategy f

Apply a strategy to some child of the root function.

parallel :: PrettyTerm f => Strategy f -> Strategy f

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 (Lemma 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), Has a (Lemma 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.