tur/logic

(mzero :int)

-- Backtracking monad (inlined) ─────────────────────────────────────────────

(mreturn [x] :int)

wrap a single substitution as a successful result.

(mplus [xs ys] :int)

concatenate two solution lists.

(mbind [ma fn] :int)

apply a fat-closure continuation to each solution and concatenate.

(bt-length [xs] :int)

count the number of solutions in a result list.

(term-int [n] :int)

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

Pointer to a term with tag=0, data1=n (:int).

  (term-int 42)  ; => tagged term pointer for integer 42

(term-var [id] :int)

construct a logic variable term with the given id.

Pointer to a term with tag=1, data1=id (:int).

  (term-var (lvar-next))  ; => fresh logic variable

(term-pair [a b] :int)

construct a logic pair term from two sub-terms.

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 :int)

construct the nil/empty logic term.

Pointer to a term with tag=3 (:int).

  (term-nil)  ; => nil term

(term-tag [t] :int)

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

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

read the integer value from an INT term.

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

read the variable id from a VAR term.

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

read the first sub-term pointer from a PAIR term.

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

read the second sub-term pointer from a PAIR term.

(lvar-next :int)

-- Fresh variable counter ───────────────────────────────────────────────────

A fresh monotonically increasing integer id (:int).

  (term-var (lvar-next))  ; => a unique logic variable

(subs-empty :int)

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

(logic-walk [t subs] :int)

follow variable bindings in a substitution until ground.

The fully walked term pointer (ground or unbound variable) (:int).

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

(logic-unify [t1 t2 subs] :int)

structurally unify two terms, extending the substitution.

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 [f arg] :int)

-- Fat-closure application ──────────────────────────────────────────────────

(apply-goal [g state] :int)

call a goal fat closure with a substitution (UState).

(unify-goal-impl [lt1 lt2 state] :int)

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

(lequal [t1 t2] :ptr<void>)

goal that unifies two terms (miniKanren ==).

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 [dummy state] :int)

implementation helper for the succeed goal.

(succeed :ptr<void>)

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 [dummy state] :int)

implementation helper for the fail goal.

(fail :ptr<void>)

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 [lg22 s] :int)

helper to apply the second goal in a conjunction.

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

implementation helper for conjunction.

(conjoined [g1 g2] :ptr<void>)

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

A goal that succeeds only when both g1 and g2 succeed (:ptr<void>).

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

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

implementation helper for disjunction.

(disjoined [g1 g2] :ptr<void>)

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

A goal whose solutions are the interleaved results of g1 and g2 (:ptr<void>).

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

(fresh-impl [lf state] :int)

implementation helper for fresh variable introduction.

(fresh [f] :ptr<void>)

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

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 [n lst] :int)

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

(run-logic [n g] :int)

run a goal with an empty substitution and return up to n results.

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 [results] :int)

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

(reify-walk [t results] :int)

walk a term through the first result's substitution.

The walked term pointer (ground or unbound variable) (:int).

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