Crux.Expression.RewriteRule behaviour (crux v0.1.3)

Behaviour for defining expression rewrite rules.

A rewrite rule defines how to transform boolean expressions during traversal. Rules can be composed together or applied individually depending on their exclusivity requirements.

Summary

Types

acc_id(variable, acc)

acc_map(variable, acc)

rule_options()

rule_spec(variable, acc)

t()

Callbacks

exclusive?()

Returns whether this rule is exclusive.

needs_reapplication?()

Returns whether this rule may need reapplication.

type()

Returns the traversal type for this rule.

walk(t)

Transforms an expression without an accumulator.

walk_stateful(t, acc)

Transforms an expression with an accumulator.

Functions

apply(expression, rules)

Applies a list of rewrite rules to an expression.

Types

acc_id(variable, acc)

@type acc_id(variable, acc) :: t() | Crux.Expression.walker(variable, acc)

acc_map(variable, acc)

@type acc_map(variable, acc) :: %{required(acc_id(variable, acc)) => acc}

rule_options()

@type rule_options() :: [
  exclusive?: boolean(),
  needs_reapplication?: boolean(),
  type: :prewalk | :postwalk
]

rule_spec(variable, acc)

@type rule_spec(variable, acc) ::
  t()
  | Crux.Expression.walker_stateless(variable)
  | {Crux.Expression.walker_stateful(variable, acc), acc}
  | {Crux.Expression.walker_stateful(variable, acc), acc, rule_options()}

t()

@type t() :: module()

Callbacks

exclusive?()

@callback exclusive?() :: boolean()

Returns whether this rule is exclusive.

An exclusive rule cannot be composed with other rules and must be applied in isolation. Non-exclusive rules can be composed together for efficiency.

needs_reapplication?()

@callback needs_reapplication?() :: boolean()

Returns whether this rule may need reapplication.

Rules that return true may be applied multiple times until a fixpoint is reached (no further changes occur). Rules that return false are applied only once.

type()

@callback type() :: :prewalk | :postwalk

Returns the traversal type for this rule.

Must return either :prewalk or :postwalk to indicate when during tree traversal this rule should be applied.

walk(t)

(optional)

@callback walk(Crux.Expression.t(variable)) :: Crux.Expression.t(variable)
when variable: term()

Transforms an expression without an accumulator.

This is the core transformation logic for the rule.

walk_stateful(t, acc)

@callback walk_stateful(Crux.Expression.t(variable), acc) ::
  {Crux.Expression.t(variable), acc}
when variable: term(), acc: term()

Transforms an expression with an accumulator.

This callback is optional - if not implemented, the default implementation will call walk/1 and return {result, acc}.

Functions

apply(expression, rules)

@spec apply(Crux.Expression.t(variable), [rule_spec(variable, acc)]) ::
  {Crux.Expression.t(variable), acc_map(variable, acc)}
when variable: term(), acc: term()

Applies a list of rewrite rules to an expression.

Rules are processed in chunks based on their exclusivity and type while preserving the order they appear in the list. Adjacent rules with the same exclusivity and type are grouped together for efficiency.

Rule Processing

Rules are chunked by adjacency of exclusivity and type
Exclusive rules always get their own chunk
Each chunk is applied sequentially to the result of the previous chunk
If any rule in a chunk has needs_reapplication?() == true, the chunk is reapplied until no changes occur (fixpoint)

Examples

iex> import Crux.Expression, only: [b: 1]
...> expr = b(not not :a)
...>
...> {result, _acc_map} =
...>   RewriteRule.apply(expr, [
...>     Crux.Expression.RewriteRule.NegationLaw
...>   ])
...>
...> result
:a