Theoria.Equation.Compiler (theoria v0.7.0)

Experimental/internal API for 0.2; subject to change before 0.3. Internal constructor-equation compiler for the initial Bool/Nat/List fragment.

Summary

Types

compiled_result()

result()

Functions

compile(arg1, motive, clauses, major)

Compiles a supported constructor-equation fragment.

compile_bool(motive, clauses, major, context \\ Context.new())

Compiles Bool constructor clauses to a Bool recursor application.

compile_definition(kind, signature, motive, clauses, major, opts \\ [])

Compiles a supported constructor-equation fragment and generated metadata.

compile_list(element_type, motive, clauses, major, levels \\ [1, 1])

Compiles List nil/cons clauses to a List recursor application.

compile_nat(motive, clauses, major)

Compiles Nat zero/succ clauses to a Nat recursor application.

Types

compiled_result()

@type compiled_result() :: {:ok, Theoria.Equation.Compiled.t()} | {:error, term()}

result()

@type result() :: {:ok, Theoria.Term.t()} | {:error, term()}

Functions

compile(arg1, motive, clauses, major)

@spec compile(
  :bool
  | :nat
  | {:list, Theoria.Term.t(), [Theoria.Level.t() | non_neg_integer()]},
  Theoria.Term.t(),
  [Theoria.Equation.Clause.t()],
  Theoria.Term.t()
) :: result()

Compiles a supported constructor-equation fragment.

compile_bool(motive, clauses, major, context \\ Context.new())

@spec compile_bool(
  Theoria.Term.t(),
  [Theoria.Equation.Clause.t()],
  Theoria.Term.t(),
  Theoria.Equation.Context.t()
) :: result()

Compiles Bool constructor clauses to a Bool recursor application.

compile_definition(kind, signature, motive, clauses, major, opts \\ [])

@spec compile_definition(
  :bool
  | :nat
  | {:list, Theoria.Term.t(), [Theoria.Level.t() | non_neg_integer()]},
  Theoria.Equation.Signature.t(),
  Theoria.Term.t(),
  [Theoria.Equation.Clause.t()],
  Theoria.Term.t(),
  keyword()
) :: compiled_result()

Compiles a supported constructor-equation fragment and generated metadata.

compile_list(element_type, motive, clauses, major, levels \\ [1, 1])

@spec compile_list(
  Theoria.Term.t(),
  Theoria.Term.t(),
  [Theoria.Equation.Clause.t()],
  Theoria.Term.t(),
  [Theoria.Level.t() | non_neg_integer()]
) :: result()

Compiles List nil/cons clauses to a List recursor application.

compile_nat(motive, clauses, major)

@spec compile_nat(Theoria.Term.t(), [Theoria.Equation.Clause.t()], Theoria.Term.t()) ::
  result()

Compiles Nat zero/succ clauses to a Nat recursor application.