tur/logic

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

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

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

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

(defdata Stream :copy (StNil) (StCons) (StInc) (fn))

(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).

Since: lazy-streams

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

a kind-(* -> *) handle over a miniKanren goal `Subst -> Stream`;

Since: stdlib-hkt-consolidation T3

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

-- Solution stream (list / backtracking monad) ─────────────────────────────

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

concatenate two solution streams DEPTH-FIRST.

(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.

(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

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

count the number of solutions in a solution stream.

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

-- Term constructors ────────────────────────────────────────────────────────

(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)

-- Term accessors ───────────────────────────────────────────────────────────

(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)

-- Substitution operations ──────────────────────────────────────────────────

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

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

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

set the fresh-variable counter at the base of a

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

find the term bound to var-id in a substitution.

(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.

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

structurally unify two terms, extending the substitution.

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

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

-- Goal application ─────────────────────────────────────────────────────────

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

-- Goal constructors ────────────────────────────────────────────────────────

(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).

(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).

(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.

(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.

(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.

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

Since: lazy-streams

(disjoined-dfs [A])

(run-logic [A])

-- Runner ───────────────────────────────────────────────────────────────────

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

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

-- Result helpers ───────────────────────────────────────────────────────────

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

extract the first solution substitution from a run-logic

(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))

-- HKT typeclass instances (stdlib-hkt-consolidation T3) ────────────────────

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

worker: map a callback over each solution state.

(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);

Since: stdlib-hkt-consolidation T3

(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

(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