tur/logic

(defdata Term :copy (TInt :int) (TVar :int) (TPair :Term :Term) (TNil))

(defdata Subst :copy (SNil :int) (SBind :int :Term :Subst))

(defdata UnifyResult :copy (UFail) (UOk :Subst))

(defdata Lookup :copy (LMissing) (LFound :Term))

(defdata Stream :copy)

(st-force [th :(fn [] Stream)] :Stream)

run a delayed stream one step.

(st-pull [xs :Stream] :Stream)

force a stream until it is mature (StNil or StCons).

This is where laziness is cashed in: every consumer that needs to look at the head of a stream pulls first, and only that much of the search runs.

Since: lazy-streams

(defopaque Goal [A] :ptr<void>)

a kind-(* -> *) handle over a miniKanren goal Subst -> Stream; carrier is the fat-closure pointer.

Since: stdlib-hkt-consolidation T3

(st-append [xs :Stream ys :Stream] :Stream)

concatenate two solution streams.

(st-append-dfs [xs :Stream ys :Stream] :Stream)

concatenate two solution streams DEPTH-FIRST.

Same as st-append but WITHOUT the swap, so the left branch is exhausted before the right is touched. Still lazy -- it defers through an immature stream rather than forcing it -- so run-logic n still costs n solutions.

Use when a goal's left branch is known to terminate and you want the leftmost solution cheaply. st-append reaches a solution at depth d breadth-first, which is what makes it complete on infinite relations and what makes it slower on a goal whose only solutions are deep.

Prefer st-append unless you have measured. Depth-first is faster on the goals it terminates on and diverges on the ones it does not, which is the whole reason the default swaps.

(st-length (st-append-dfs (mreturn s) (mreturn s)))  ; => 2

Since: lazy-streams

(st-bind [xs :Stream f :(fn [Subst] Stream)] :Stream)

concatMap: apply f to each state and concatenate the streams. f is a Subst -> Stream callback (arrives as a first-class :fn value).

(st-length [xs :Stream] :int)

count the states in a solution stream.

(st-take [n :int xs :Stream] :Stream)

keep at most n states from the front of a solution stream.

(mzero :Stream)

the empty solution stream (no solutions).

(mreturn [s :Subst] :Stream)

wrap a single substitution as a one-solution stream.

(mplus [xs :Stream ys :Stream] :Stream)

concatenate (union) two solution streams.

(mbind [ma :Stream fn :(fn [Subst] Stream)] :Stream)

apply a Subst -> Stream continuation to each solution and concatenate the results.

(bt-length [xs :Stream] :int)

count the number of solutions in a solution stream.

(term-int [n :int] :Term)

construct a logic term representing an integer value.

(term-int 42)  ; => integer term 42

(term-var [id :int] :Term)

construct a logic variable term with the given id.

(term-var 0)  ; => logic variable 0

(term-pair [a :Term b :Term] :Term)

construct a logic pair term from two sub-terms.

(term-pair (term-int 1) (term-int 2))  ; => pair term (1 . 2)

(term-nil :Term)

construct the nil/empty logic term.

(term-nil)  ; => nil term

(term-int-val [t :Term] :int)

read the integer value from an INT term (0 otherwise).

(term-var-id [t :Term] :int)

read the variable id from a VAR term (0 otherwise).

(term-pair-fst [t :Term] :Term)

read the first sub-term of a PAIR term (TNil otherwise).

(term-pair-snd [t :Term] :Term)

read the second sub-term of a PAIR term (TNil otherwise).

(subs-empty :Subst)

return the empty substitution (fresh counter at 0).

(subst-next [s :Subst] :int)

read the next unused fresh-variable id from the base of a substitution.

(subst-set-next [s :Subst n :int] :Subst)

set the fresh-variable counter at the base of a substitution, preserving all bindings.

(subst-lookup [vid :int subs :Subst] :Lookup)

find the term bound to var-id in a substitution. Returns (LFound term) when var-id is bound, (LMissing) otherwise.

(logic-walk [t :Term subs :Subst] :Term)

follow variable bindings in a substitution until ground.

(logic-walk (term-var 0) subs)  ; => bound term or the variable itself

(unify-walked [a :Term b :Term subs :Subst] :UnifyResult)

structural unification of two already-walked terms. No occurs check (matching standard miniKanren).

(logic-unify [t1 :Term t2 :Term subs :Subst] :UnifyResult)

structurally unify two terms, extending the substitution.

No occurs check is performed. Returns a tagged UnifyResult.

(logic-unify (term-var 0) (term-int 5) (subs-empty))  ; => (UOk {x0=5})

(apply-goal [g :(Goal int) state :Subst] :Stream)

run a goal against a search state, yielding a solution stream.

(unify-goal-impl [lt1 :Term lt2 :Term state :Subst] :Stream)

implementation helper: unify two terms against a state.

(lequal [t1 :Term t2 :Term] :(Goal int))

goal that unifies two terms (miniKanren ==).

(run-logic 1 (lequal (term-int 5) (term-int 5)))  ; => one solution

(succeed :(Goal int))

goal that always succeeds without changing the substitution.

(run-logic 1 (succeed))  ; => one solution

(fail :(Goal int))

goal that always fails, producing no solutions.

(run-logic 1 (fail))  ; => empty stream

(conjoined-impl [lg1 :(Goal int) lg2 :(Goal int) state :Subst] :Stream)

implementation helper for conjunction.

(conjoined-raw [g1 :(Goal int) g2 :(Goal int)] :(Goal int))

worker behind conjoined / Monad bind sequencing.

(conjoined [A B])

goal that applies g1 then g2 to each result (conjunction).

Equivalent to sequencing the two goals with do-m against the Monad [Goal] instance.

(run-logic 1 (conjoined (lequal x (term-int 1)) (succeed)))  ; => [x=1]

Since: Phase B1

(disjoined-impl [lg1 :(Goal int) lg2 :(Goal int) state :Subst] :Stream)

implementation helper for disjunction.

(disjoined-raw [g1 :(Goal int) g2 :(Goal int)] :(Goal int))

worker behind disjoined / Alternative alt-or.

(disjoined [A])

goal that combines results from g1 and g2 (disjunction).

This is the worker behind Alternative [Goal]'s alt-or method.

(run-logic 2 (disjoined (lequal x (term-int 1)) (lequal x (term-int 2))))
; => [x=1, x=2]

Since: Phase B1

(fresh-impl [^fat lf :(fn [Term] (Goal int)) state :Subst] :Stream)

implementation helper for fresh variable introduction.

(fresh [^fat f :(fn [Term] (Goal int))] :(Goal int))

create a new logic variable and pass it to a goal-building function.

The callback is taken ^fat, so a capturing lambda -- e.g. the inner goal of a nested fresh that closes over the outer variable -- dispatches correctly. A caller's lambda parameter type is inferred, so (fresh (fn [x] ...)) needs no annotation on x.

(run-logic 1 (fresh (fn [x] (lequal x (term-int 7)))))  ; => [x=7]

(zzz [g])

delay a goal so a recursive relation can be written at all.

Without this, a self-recursive relation diverges while the goal is being BUILT, before any search runs:

(defn nats [] : (Goal int) (disjoined (succeed) (nats)))   ; SIGSEGV

disjoined takes its goals strictly, so (nats) calls itself forever. zzz wraps the goal EXPRESSION unevaluated, so nothing recurses until the resulting stream is pulled -- and then only one step at a time:

(defn nats [] : (Goal int) (disjoined (succeed) (zzz (nats))))

This is the Zzz of the miniKanren literature. It is a macro and has to be: a function would evaluate its argument at the call site, which is the divergence it exists to prevent.

(run-logic 1 (zzz (nats)))   ; terminates

Since: lazy-streams

(disjoined-dfs-impl [lg1 :(Goal int) lg2 :(Goal int) state :Subst] :Stream)

disjunction that searches DEPTH-FIRST.

disjoined interleaves, which is what makes it complete on relations with infinitely many solutions. That costs more to reach a solution that sits deep in the left branch, because interleaving gets there breadth-first. This variant keeps the old depth-first order.

It is NOT complete: on a goal whose left branch has infinitely many solutions it never reaches the right one. Reach for it only when the left branch is known finite.

(run-logic 1 (disjoined-dfs (lequal x (term-int 1)) (lequal x (term-int 2))))

Since: lazy-streams

(disjoined-dfs [A])

(run-logic [A])

run a goal with an empty state and return up to n solutions.

(run-logic 1 (fresh (fn [x] (lequal x (term-int 3)))))  ; => one solution

(stream-empty? [xs :Stream] :bool)

is a solution stream empty?

(first-state [results :Stream] :Subst)

extract the first solution substitution from a run-logic stream.

(reify-walk [t :Term results :Stream] :Term)

walk a term through the first solution's substitution.

(reify-walk my-var (run-logic 1 my-goal))  ; => ground term or variable

(bind-goal-raw [g :(Goal int) k :fn] :(Goal int))

worker: conjunction that threads the state into the :fn continuation, which returns the next goal.

(fmap-goal-raw [g :(Goal int) f :(fn [Subst] Subst)] :(Goal int))

worker: map a callback over each solution state.

The callback is typed (fn [Subst] Subst) rather than a bare :fn. That is not just hygiene: a bare :fn result is an erased carrier word, so the body had to ascribe it back with (:: (f s) :Subst) -- a no-op cast while Subst rides the int64 carrier, and a real representation change the moment it does not (SR4). Spelling the signature deletes the reinterpret.

(definstance Functor [Goal])

map a function over each solution state.

Since: stdlib-hkt-consolidation T3

(definstance Applicative [Goal])

pure is the always-succeeding goal (state preserved); ap sequences the two goals (conjunction) keeping the second's states.

Since: stdlib-hkt-consolidation T3

(definstance Monad [Goal])

bind is conjunction: run the goal, then feed each resulting state into the continuation (which returns the next goal). This is what do-m / for lower onto for goal-conjunction chains.

(do-m _ (lequal x (term-int 1)) (lequal y (term-int 2)))

Since: stdlib-hkt-consolidation T3

(definstance Alternative [Goal])

empty is the failing goal; alt-or is disjunction (the miniKanren disj): it unions the solutions of both goals.

(alt-or (lequal x (term-int 1)) (lequal x (term-int 2)))

Since: stdlib-hkt-consolidation T3