Specs

absento(Ckini.Term.t(), Ckini.Term.t()) :: goal()

Assert term t never contains term u.

Examples

iex> use Ckini
iex> run(q, do: absento(q, 42))
[{:_0, [abs: [_0: 42]]}]
iex> run(q) do
...>   eq(q, 42)
...>   absento(q, 42)
...> end
[]
iex> run(q) do
...>   eq(q, [:the, :answer, :is, [42]])
...>   absento(q, 42)
...> end
[]

Anyo runs the goal for indefinitely number of times.

Examples

iex> use Ckini
iex> run(5, x, do: anyo(eq(x, 1)))
[1, 1, 1, 1, 1]

copy_termo creates a copy of its first argument, replacing logic variables with new variables.

Examples

iex> use Ckini
iex> [x, y] = Var.new_many(2)
iex> run({w, z}) do
...>   eq([:a, x, 5, y, x], w)
...>   copy_termo(w, z)
...>   eq(x, 1)
...> end
[{[:a,   1, 5, :_0,   1],
  [:a, :_1, 5, :_2, :_1]}]

Specs

eq(Ckini.Term.t(), Ckini.Term.t()) :: goal()

eq is the same as the == operator in TRS and other miniKanren literature.

Examples

iex> use Ckini
iex> run(x, do: eq(3, x))
[3]
iex> run(x, do: eq([x], x))
[]

Specs

fail() :: goal()

fail is a goal that always fails.

Examples

iex> use Ckini
iex> run(x) do
...>   conde do
...>     _ ->
...>        fail()
...>        eq(x, 1)
...>     _ ->
...>        succ()
...>        eq(x, 2)
...>   end
...> end
[2]

The =/= operator.

Examples

iex> use Ckini
iex> run(x) do
...>   neq(3, x)
...>   eq(x, 3)
...> end
[]
iex> run(x) do
...>   eq(3, x)
...>   neq(x, 3)
...> end
[]
iex> run(x) do
...>   eq(4, x)
...>   neq(x, 3)
...> end
[4]
iex> [y, z] = Var.new_many(2)
iex> run(x) do
...>   neq(x, [y,z])
...>   eq(y, 999)
...>   eq(z, 998)
...> end
[{:_0, [neq: [[_0: [999, 998]]]]}]
iex> run(x) do
...>   neq(x, [:hello, :world])
...>   neq(x, :hello)
...> end
[{:_0, [neq: [[_0: :hello], [_0: [:hello, :world]]]]}]
iex> run(x) do
...>   neq(x, [y,z])
...>   neq(x, :hello)
...>   eq(x, [1,2,3])
...> end
[[1,2,3]]

onceo succeeds at most once.

Examples

iex> use Ckini
iex> run(x, do: onceo(anyo(eq(x, 1))))
[1]

Print the current value of a logic variable. You can peek into multiple variables by enclosing them with a tuple.

peek/1 comes handy for debugging purposes.

Examples

iex> use Ckini
iex> log = ExUnit.CaptureLog.capture_log(fn ->
...>   run q do
...>     conde do
...>       z ->
...>         eq(q, 1)
...>         eq(z, q)
...>         peek({z, q})
...>       z ->
...>         eq(q, 2)
...>         peek({z, q})
...>         eq(z, q)
...>     end
...>   end
...> end)
iex> String.contains?(log, "{1, 1}")
true
iex> String.match?(log, ~r/{z<\d+>, 2}/)
true

Project a logic variable to Elixir variable.

Normally, you cannot perform native Elixir operations on logic variables. For example, you cannot run not x if x is a logic variable that happens to bind to a boolean value.

Project/2 provides a way to access to the current value of a logic variable. Note that if the variable is not currently bound to a ground term, you may still get a logic variable back.

Examples

iex> use Ckini
iex> run q do
...>   fresh x do
...>     eq(x, false)
...>     project(x, fn x ->
...>       eq(q, not x)
...>     end)
...>   end
...> end
[true]

Specs

succ() :: goal()

succ is a goal that always succeeds.

Examples

iex> use Ckini
iex> run(x) do
...>   succ()
...>   eq(x, 1)
...> end
[1]

Specs

symbolo(Ckini.Term.t()) :: goal()

Assert a variable to be a symbol.

Examples

iex> use Ckini
iex> run(q) do
...>   eq(q, :hello)
...>   symbolo(q)
...> end
[:hello]
iex> run(q) do
...>   eq(q, [])
...>   symbolo(q)
...> end
[]
iex> run(q) do
...>   symbolo(q)
...>   conde do
...>     _ -> eq(q, 1)
...>     _ -> eq(q, :a)
...>     _ -> eq(q, [])
...>   end
...> end
[:a]
iex> v = Var.new()
iex> run q do
...>   symbolo(q)
...>   symbolo(v)
...> end
[{:_0, sym: [:_0]}]