Theoria.Simp.Database (theoria v0.7.0)

Experimental/internal API for 0.2; subject to change before 0.3. Untrusted simplifier database with rule priorities.

Summary

Types

t()

Functions

from_env_all_equations(env, opts \\ [])

Builds a simplifier database from generated definition and matcher equations.

from_env_equations(env, opts \\ [])

Builds a simplifier database from generated environment equations.

from_env_indexed_matcher_equations(env, opts \\ [])

Builds a simplifier database from installed indexed matcher equations.

new(rules \\ [])

Builds a simplifier database sorted by descending priority.

once(database, term)

Applies the first matching simplifier rule.

once_with_step(database, term)

Applies the first matching simplifier rule and returns rewrite-step metadata.

once_with_step(database, env, term, opts \\ [])

Applies the first matching simplifier rule with lazy proof realization support.

Types

t()

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

Functions

from_env_all_equations(env, opts \\ [])

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

Builds a simplifier database from generated definition and matcher equations.

from_env_equations(env, opts \\ [])

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

Builds a simplifier database from generated environment equations.

from_env_indexed_matcher_equations(env, opts \\ [])

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

Builds a simplifier database from installed indexed matcher equations.

new(rules \\ [])

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

Builds a simplifier database sorted by descending priority.

once(database, term)

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

Applies the first matching simplifier rule.

once_with_step(database, term)

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

Applies the first matching simplifier rule and returns rewrite-step metadata.

once_with_step(database, env, term, opts \\ [])

@spec once_with_step(t(), Theoria.Env.t(), Theoria.Term.t(), keyword()) ::
  {:ok, Theoria.Rewrite.Step.t(), Theoria.Simp.Rule.t()} | :not_found

Applies the first matching simplifier rule with lazy proof realization support.