Theoria.Equation.Branch (theoria v0.4.0)

Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-specific branch descriptors for equation compilation.

Summary

binder()

t()

Builds a generic branch descriptor from recursor-rule metadata.

Builds the List cons branch descriptor.

nat_succ(clause)

Builds the Nat successor branch descriptor.

Builds a Vec cons branch metadata descriptor for indexed-equation planning.

Wraps a body in the branch binders.

@type binder() :: {atom(), Theoria.Term.t()}

@type t() :: %Theoria.Equation.Branch{
  binders: [binder()],
  context: Theoria.Equation.Context.t()
}

@spec from_recursor_rule(
  Theoria.Equation.Clause.t(),
  Theoria.Env.RecursorRule.t(),
  [Theoria.Term.t()],
  map()
) :: t()

Builds a generic branch descriptor from recursor-rule metadata.

@spec list_cons(Theoria.Equation.Clause.t(), Theoria.Term.t(), Theoria.Term.t()) ::
  t()

Builds the List cons branch descriptor.

@spec nat_succ(Theoria.Equation.Clause.t()) :: t()

Builds the Nat successor branch descriptor.

@spec vec_cons(
  Theoria.Equation.Clause.t(),
  Theoria.Term.t(),
  Theoria.Term.t(),
  Theoria.Term.t()
) :: t()

Builds a Vec cons branch metadata descriptor for indexed-equation planning.

@spec wrap(t(), Theoria.Term.t()) :: Theoria.Term.t()

Wraps a body in the branch binders.