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)

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

Show (Rule f)

Defined in Twee.Rule

Methods

showsPrec :: Int -> Rule f -> ShowS

show :: Rule f -> String

showList :: [Rule f] -> ShowS

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

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 (ActiveRule f) (Rule g)

Defined in Twee

Methods

the :: ActiveRule f -> Rule g

type ConstantOf (Rule f)

Defined in Twee.Rule

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)

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

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

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?

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

Defined in Twee.Rule

Methods

showsPrec :: Int -> Reduction f -> ShowS

show :: Reduction f -> String

showList :: [Reduction f] -> ShowS

Function f => Pretty (Reduction f)

Defined in Twee.Rule

Methods

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

pPrint :: Reduction f -> Doc

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

Symbolic (Reduction f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Reduction f) :: Type

Methods

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

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

type ConstantOf (Reduction f)

Defined in Twee.Rule

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

Defined in Twee.Rule

Methods

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

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

Ord (Resulting f)

Defined in Twee.Rule

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)

Defined in Twee.Rule

Methods

showsPrec :: Int -> Resulting f -> ShowS

show :: Resulting f -> String

showList :: [Resulting f] -> ShowS

Function f => Pretty (Resulting f)

Defined in Twee.Rule

Methods

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

pPrint :: Resulting f -> Doc

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

Symbolic (Resulting f)

Defined in Twee.Rule

Associated Types

type ConstantOf (Resulting f) :: Type

Methods

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

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

type ConstantOf (Resulting f)

Defined in Twee.Rule

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 -> Set (Resulting f) -> Set (Resulting f)

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

successors :: Function f => Strategy f -> Set (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 -> Set (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 (Proof 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 (Proof 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.