Ckini v0.1.0

Ckini.Context (Ckini v0.1.0) View Source

An intermediate state of computation.

It contains a substitution of variables and a set of different types of constraints:

  • neq: created using neq goal
  • sym: created using symbolo goal
  • abs: created using absento goal

Link to this section Summary

Types

t()

Functions

add_abs_constraint(ctx, t, u)
add_sym_constraint(ctx, v, t)
constraints(ctx)
disunify(c, v, w)
new()
purify(ctx, r)

Retain only the constraints related to the given term.

purify_abs(abs, r, subst)
purify_neq(cs, r, subst)
purify_sym(vs, r)
unify(c, v, w)
verify(c)
verify_abs(ctx)
verify_neq(ctx)
verify_sym(ctx)
verify_valid_subst(ctx)

Link to this section Types

Link to this type

t()

View Source

Specs

t() :: %Ckini.Context{
  abs: MapSet.t({Ckini.Term.t(), Ckini.Term.t()}),
  neq: [Ckini.Subst.t()],
  subst: Ckini.Subst.t(),
  sym: MapSet.t(Ckini.Var.t())
}

Link to this section Functions

Link to this function

add_abs_constraint(ctx, t, u)

View Source

Specs

add_abs_constraint(t(), Ckini.Term.t(), Ckini.Term.t()) :: t() | nil
Link to this function

add_sym_constraint(ctx, v, t)

View Source

Specs

add_sym_constraint(t(), Ckini.Var.t(), Ckini.Term.t()) :: t() | nil
Link to this function

constraints(ctx)

View Source

Specs

constraints(t()) :: keyword()
Link to this function

disunify(c, v, w)

View Source

Specs

disunify(t(), Ckini.Term.t(), Ckini.Term.t()) :: nil | t()
Link to this function

new()

View Source
Link to this function

purify(ctx, r)

View Source

Specs

purify(t(), Ckini.Subst.t()) :: t()

Retain only the constraints related to the given term.

Link to this function

purify_abs(abs, r, subst)

View Source
Link to this function

purify_neq(cs, r, subst)

View Source

Specs

purify_neq([Ckini.Subst.t()], Ckini.Subst.t(), Ckini.Subst.t()) :: [
  Ckini.Subst.t()
]
Link to this function

purify_sym(vs, r)

View Source
Link to this function

unify(c, v, w)

View Source

Specs

unify(t(), Ckini.Term.t(), Ckini.Term.t()) :: nil | t()
Link to this function

verify(c)

View Source

Specs

verify(t()) :: t() | nil
Link to this function

verify_abs(ctx)

View Source

Specs

verify_abs(t() | nil) :: t() | nil
Link to this function

verify_neq(ctx)

View Source

Specs

verify_neq(t() | nil) :: t() | nil
Link to this function

verify_sym(ctx)

View Source

Specs

verify_sym(t() | nil) :: t() | nil
Link to this function

verify_valid_subst(ctx)

View Source

Specs

verify_valid_subst(t()) :: nil