Theoria.Rewrite.Database (theoria v0.3.0)

Experimental/internal API for 0.2; subject to change before 0.3. A tiny untrusted rewrite-rule database.

Summary

Types

t()

Functions

add(database, rule)

Adds a rule to the database.

from_env_all_equations(env, opts \\ [])

Builds a rewrite database from generated definition and matcher equations in an environment.

from_env_equations(env, opts \\ [])

Builds a rewrite database from generated equation metadata stored in an environment.

from_env_indexed_matcher_equations(env, opts \\ [])

Builds a rewrite database from installed indexed matcher equation metadata.

from_env_matcher_equations(env, opts \\ [])

Builds a rewrite database from generated matcher equations stored in an environment.

from_lemmas(lemmas, equality_type, opts \\ [])

Builds a rewrite database from equation-lemma metadata.

new(rules \\ [])

Builds an empty rewrite database.

once(database, term)

Applies the first rule that rewrites the term.

Types

t()

@type t() :: %Theoria.Rewrite.Database{rules: [Theoria.Rewrite.Rule.t()]}

Functions

add(database, rule)

@spec add(t(), Theoria.Rewrite.Rule.t()) :: t()

Adds a rule to the database.

from_env_all_equations(env, opts \\ [])

@spec from_env_all_equations(
  Theoria.Env.t(),
  keyword()
) :: t()

Builds a rewrite database from generated definition and matcher equations in an environment.

from_env_equations(env, opts \\ [])

@spec from_env_equations(
  Theoria.Env.t(),
  keyword()
) :: t()

Builds a rewrite database from generated equation metadata stored in an environment.

from_env_indexed_matcher_equations(env, opts \\ [])

@spec from_env_indexed_matcher_equations(
  Theoria.Env.t(),
  keyword()
) :: t()

Builds a rewrite database from installed indexed matcher equation metadata.

from_env_matcher_equations(env, opts \\ [])

@spec from_env_matcher_equations(
  Theoria.Env.t(),
  keyword()
) :: t()

Builds a rewrite database from generated matcher equations stored in an environment.

from_lemmas(lemmas, equality_type, opts \\ [])

@spec from_lemmas([Theoria.Equation.Lemma.t()], Theoria.Term.t(), keyword()) :: t()

Builds a rewrite database from equation-lemma metadata.

new(rules \\ [])

@spec new([Theoria.Rewrite.Rule.t()]) :: t()

Builds an empty rewrite database.

once(database, term)

@spec once(t(), Theoria.Term.t()) ::
  {:ok, Theoria.Term.t(), Theoria.Rewrite.Rule.t()} | :not_found

Applies the first rule that rewrites the term.