tur/logic
miniKanren-style logic programming (unification, goals, streams).
Since: Phase B1
Goal
(Goal [A] :ptr<void>))
a kind-(* -> *) handle over a miniKanren goal `UState -> list
Since: stdlib-hkt-consolidation T3
mzero
(mzero :)
-- Backtracking monad (inlined) ─────────────────────────────────────────────
0 (null pointer, empty solution list).
mreturn
(mreturn [x] :)
wrap a single substitution as a successful result.
| x | substitution pointer (:int) |
A singleton solution list (:int).
mplus
(mplus [xs ys] :)
concatenate two solution lists.
| xs | first solution list (:int) | |
| ys | second solution list (:int) |
A new list with all solutions from xs followed by those from ys (:int).
mbind
(mbind [ma fn] :)
apply a fat-closure continuation to each solution and concatenate.
| ma | solution list (:int) | |
| fn | fat closure of type (UState -> list UState) |
Concatenated solutions (:int).
bt-length
(bt-length [xs] :)
count the number of solutions in a result list.
| xs | solution list (:int) |
Number of solutions (:int).
term-int
(term-int [n] :)
-- Term constructors ────────────────────────────────────────────────────────
| n | integer value |
Pointer to a term with tag=0, data1=n (:int).
(term-int 42) ; => tagged term pointer for integer 42
term-var
(term-var [id] :)
construct a logic variable term with the given id.
| id | unique variable identifier (:int) |
Pointer to a term with tag=1, data1=id (:int).
(term-var (lvar-next)) ; => fresh logic variable
term-pair
(term-pair [a b] :)
construct a logic pair term from two sub-terms.
| a | first sub-term pointer (:int) | |
| b | second sub-term pointer (:int) |
Pointer to a term with tag=2, data1=a, data2=b (:int).
(term-pair (term-int 1) (term-int 2)) ; => pair term (1 . 2)
term-nil
(term-nil :)
construct the nil/empty logic term.
Pointer to a term with tag=3 (:int).
(term-nil) ; => nil term
term-tag
(term-tag [t] :)
-- Term accessors ───────────────────────────────────────────────────────────
| t | term pointer (:int) |
0=INT, 1=VAR, 2=PAIR, 3=NIL (:int).
term-int-val
(term-int-val [t] :)
read the integer value from an INT term.
| t | term pointer with tag=0 (:int) |
The integer value stored in data1 (:int).
term-var-id
(term-var-id [t] :)
read the variable id from a VAR term.
| t | term pointer with tag=1 (:int) |
The variable id stored in data1 (:int).
term-pair-fst
(term-pair-fst [t] :)
read the first sub-term pointer from a PAIR term.
| t | term pointer with tag=2 (:int) |
data1 (first sub-term pointer) (:int).
term-pair-snd
(term-pair-snd [t] :)
read the second sub-term pointer from a PAIR term.
| t | term pointer with tag=2 (:int) |
data2 (second sub-term pointer) (:int).
lvar-next
(lvar-next :)
-- Fresh variable counter ───────────────────────────────────────────────────
A fresh monotonically increasing integer id (:int).
(term-var (lvar-next)) ; => a unique logic variable
subs-empty
(subs-empty :)
-- Substitution operations ──────────────────────────────────────────────────
0 (null pointer representing an empty alist) (:int).
logic-walk
(logic-walk [t subs] :)
follow variable bindings in a substitution until ground.
| t | term pointer to walk (:int) | |
| subs | substitution alist pointer (:int) |
The fully walked term pointer (ground or unbound variable) (:int).
(logic-walk (term-var 0) subs) ; => bound term or the variable itself
logic-unify
(logic-unify [t1 t2 subs] :)
structurally unify two terms, extending the substitution.
| t1 | first term pointer (:int) | |
| t2 | second term pointer (:int) | |
| subs | current substitution alist (:int) |
Extended substitution on success, or -1 on unification failure (:int).
(logic-unify (term-var 0) (term-int 5) (subs-empty)) ; => subs with x0=5
apply-fat
(apply-fat [f : int arg : int] :)
-- Fat-closure application ──────────────────────────────────────────────────
| f | fat closure pointer (:int) | |
| arg | argument to pass (:int) |
Return value of the closure (:int).
apply-goal
(apply-goal [g : int state : int] :)
call a goal fat closure with a substitution (UState).
| g | goal fat closure pointer (:int) | |
| state | current substitution (:int) |
Solution list (list of substitutions) (:int).
unify-goal-impl
(unify-goal-impl [lt1 lt2 state] :)
-- Goal constructors ────────────────────────────────────────────────────────
lequal
(lequal [t1 t2] :)
goal that unifies two terms (miniKanren ==).
| t1 | first term pointer (:int) | |
| t2 | second term pointer (:int) |
A goal (:ptr<void>) that succeeds iff t1 and t2 unify.
(run-logic 1 (lequal (term-int 5) (term-int 5))) ; => one solution
succeed-impl
(succeed-impl [dummy state] :)
implementation helper for the succeed goal.
succeed
(succeed :)
goal that always succeeds without changing the substitution.
A goal (:ptr<void>) that adds the current state unchanged to the solutions.
(run-logic 1 (succeed)) ; => one solution (empty substitution)
fail-impl
(fail-impl [dummy state] :)
implementation helper for the fail goal.
fail
(fail :)
goal that always fails, producing no solutions.
A goal (:ptr<void>) that produces an empty solution list.
(run-logic 1 (fail)) ; => empty list
conjoined-inner
(conjoined-inner [lg22 s] :)
helper to apply the second goal in a conjunction.
conjoined-impl
(conjoined-impl [lg1 lg2 state] :)
implementation helper for conjunction.
conjoined-raw
(conjoined-raw [g1 g2] :)
int worker behind conjoined / Monad bind sequencing.
conjoined
(conjoined [A B])
goal that applies g1 then g2 to each result (conjunction).
| g1 | first goal (Goal A) | |
| g2 | second goal (Goal B) |
A goal (Goal B) that succeeds only when both g1 and g2 succeed.
(run-logic 1 (conjoined (lequal x (term-int 1)) (succeed))) ; => [x=1]
Since: Phase B1
disjoined-impl
(disjoined-impl [lg1 lg2 state] :)
implementation helper for disjunction.
disjoined-raw
(disjoined-raw [g1 g2] :)
int worker behind disjoined / Alternative alt-or.
disjoined
(disjoined [A])
goal that combines results from g1 and g2 (disjunction).
| g1 | first goal (Goal A) | |
| g2 | second goal (Goal A) |
A goal (Goal A) whose solutions are the union of g1's and g2's.
(run-logic 2 (disjoined (lequal x (term-int 1)) (lequal x (term-int 2)))) ; => [x=1, x=2]
Since: Phase B1
fresh-impl
(fresh-impl [lf state] :)
implementation helper for fresh variable introduction.
fresh
(fresh [f] :)
create a new logic variable and pass it to a goal-building function.
| f | fat closure of type (term -> goal) |
A goal (:ptr<void>) that introduces a fresh variable and runs (f var).
(run-logic 1 (fresh (fn [x] (lequal x (term-int 7))))) ; => [x=7]
take-n
(take-n [n lst] :)
-- Runner ───────────────────────────────────────────────────────────────────
| n | maximum number of solutions (:int) | |
| lst | solution list (:int) |
A truncated solution list of length at most n (:int).
run-logic
(run-logic [A])
run a goal with an empty substitution and return up to n results.
| n | maximum number of solutions (:int) | |
| g | goal to run (:ptr<void>) |
A list of at most n substitutions (solution list) (:int).
(run-logic 1 (fresh (fn [x] (lequal x (term-int 3))))) ; => one solution
first-state
(first-state [results] :)
-- Result helpers ───────────────────────────────────────────────────────────
| results | solution list from run-logic (:int) |
The first substitution pointer, or 0 if the list is empty (:int).
reify-walk
(reify-walk [t results] :)
walk a term through the first result's substitution.
| t | term pointer to reify (:int) | |
| results | solution list from run-logic (:int) |
The walked term pointer (ground or unbound variable) (:int).
(reify-walk my-var (run-logic 1 my-goal)) ; => ground term or variable
bind-goal-raw
(bind-goal-raw [g k : fn] :)
-- HKT typeclass instances (stdlib-hkt-consolidation T3) ────────────────────
fmap-goal-raw
(fmap-goal-raw [g f : fn] :)
worker: map a `:fn` callback over each solution
Functor[Goal]
(definstance Functor [Goal])
map a function over each solution substitution.
Since: stdlib-hkt-consolidation T3
Applicative[Goal]
(definstance Applicative [Goal])
pure is the always-succeeding goal (state preserved);
Since: stdlib-hkt-consolidation T3
Monad[Goal]
(definstance Monad [Goal])
bind is conjunction: run the goal, then feed each resulting
(do-m _ (lequal x (term-int 1)) (lequal y (term-int 2)))
Since: stdlib-hkt-consolidation T3
Alternative[Goal]
(definstance Alternative [Goal])
empty is the failing goal; alt-or is disjunction (the
(alt-or (lequal x (term-int 1)) (lequal x (term-int 2)))
Since: stdlib-hkt-consolidation T3