Theoria.Simp (theoria v0.3.0)

Copy Markdown View Source

Experimental/internal API for 0.2; subject to change before 0.3. Tiny untrusted simplification groundwork backed by generated equation rules.

Summary

Types

result()

Functions

normalize(env, term, opts \\ [])

Repeatedly applies generated equation simplifications until normal form or fuel exhaustion.

once(env, term, opts \\ [])

Applies one generated equation simplification, if possible.

Types

result()

@type result() :: %{
  term: Theoria.Term.t(),
  steps: [Theoria.Simp.Step.t()],
  stopped: :normal | :fuel
}

Functions

normalize(env, term, opts \\ [])

@spec normalize(Theoria.Env.t(), Theoria.Term.t(), keyword()) :: result()

Repeatedly applies generated equation simplifications until normal form or fuel exhaustion.

once(env, term, opts \\ [])

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

Applies one generated equation simplification, if possible.