tur/logic
miniKanren-style logic programming (unification, goals, streams).
Since: Phase B1
Term
(defdata Term :copy (TInt) (TVar) (TPair) (TNil))
Subst
(defdata Subst :copy (SNil) (SBind))
UnifyResult
(defdata UnifyResult :copy (UFail) (UOk))
Lookup
(defdata Lookup :copy (LMissing) (LFound))
Stream
(defdata Stream :copy (StNil) (StCons) (StInc) (fn))
st-force
(st-force [th : (fn [])
run a delayed stream one step.
st-pull
(st-pull [xs : Stream] :)
force a stream until it is mature (StNil or StCons).
| xs | a possibly-delayed stream |
The same stream forced to StNil or StCons.
Since: lazy-streams
Goal
(Goal [A] :ptr<void>))
a kind-(* -> *) handle over a miniKanren goal `Subst -> Stream`;
Since: stdlib-hkt-consolidation T3
st-append
(st-append [xs : Stream ys : Stream] :)
-- Solution stream (list / backtracking monad) ─────────────────────────────
st-append-dfs
(st-append-dfs [xs : Stream ys : Stream] :)
concatenate two solution streams DEPTH-FIRST.
| xs | first solution stream | |
| ys | second solution stream |
xs's solutions, then ys's.
(st-length (st-append-dfs (mreturn s) (mreturn s))) ; => 2
Since: lazy-streams
st-bind
(st-bind [xs : Stream f : (fn [Subst])
concatMap: apply f to each state and concatenate the streams.
st-length
(st-length [xs : Stream] :)
count the states in a solution stream.
st-take
(st-take [n : int xs : Stream] :)
keep at most n states from the front of a solution stream.
mzero
(mzero :)
the empty solution stream (no solutions).
An empty Stream.
mreturn
(mreturn [s : Subst] :)
wrap a single substitution as a one-solution stream.
| s | the search state (Subst) |
A singleton Stream containing s.
mplus
(mplus [xs : Stream ys : Stream] :)
concatenate (union) two solution streams.
| xs | first solution stream | |
| ys | second solution stream |
A Stream with all of xs's solutions followed by all of ys's.
mbind
(mbind [ma : Stream fn : (fn [Subst])
apply a `Subst -> Stream` continuation to each solution and
| ma | a solution stream | |
| fn | a `Subst -> Stream` callback |
The concatenated solution stream.
bt-length
(bt-length [xs : Stream] :)
count the number of solutions in a solution stream.
| xs | solution stream |
Number of solutions.
term-int
(term-int [n : int] :)
-- Term constructors ────────────────────────────────────────────────────────
| n | integer value |
A TInt term.
(term-int 42) ; => integer term 42
term-var
(term-var [id : int] :)
construct a logic variable term with the given id.
| id | unique variable identifier |
A TVar term.
(term-var 0) ; => logic variable 0
term-pair
(term-pair [a : Term b : Term] :)
construct a logic pair term from two sub-terms.
| a | first sub-term | |
| b | second sub-term |
A TPair term.
(term-pair (term-int 1) (term-int 2)) ; => pair term (1 . 2)
term-nil
(term-nil :)
construct the nil/empty logic term.
A TNil term.
(term-nil) ; => nil term
term-int-val
(term-int-val [t : Term] :)
-- Term accessors ───────────────────────────────────────────────────────────
| t | a Term |
The integer payload of a TInt, or 0 for any other term.
term-var-id
(term-var-id [t : Term] :)
read the variable id from a VAR term (0 otherwise).
| t | a Term |
The id of a TVar, or 0 for any other term.
term-pair-fst
(term-pair-fst [t : Term] :)
read the first sub-term of a PAIR term (TNil otherwise).
| t | a Term |
The first component of a TPair, or TNil for any other term.
term-pair-snd
(term-pair-snd [t : Term] :)
read the second sub-term of a PAIR term (TNil otherwise).
| t | a Term |
The second component of a TPair, or TNil for any other term.
subs-empty
(subs-empty :)
-- Substitution operations ──────────────────────────────────────────────────
An empty Subst with next fresh-var id 0.
subst-next
(subst-next [s : Subst] :)
read the next unused fresh-variable id from the base of a
subst-set-next
(subst-set-next [s : Subst n : int] :)
set the fresh-variable counter at the base of a
subst-lookup
(subst-lookup [vid : int subs : Subst] :)
find the term bound to var-id in a substitution.
logic-walk
(logic-walk [t : Term subs : Subst] :)
follow variable bindings in a substitution until ground.
| t | the term to walk | |
| subs | the substitution |
The fully walked term (a ground term or an unbound variable).
(logic-walk (term-var 0) subs) ; => bound term or the variable itself
unify-walked
(unify-walked [a : Term b : Term subs : Subst] :)
structural unification of two already-walked terms.
logic-unify
(logic-unify [t1 : Term t2 : Term subs : Subst] :)
structurally unify two terms, extending the substitution.
| t1 | first term | |
| t2 | second term | |
| subs | current substitution |
(UOk subs') on success, or (UFail) on unification failure.
(logic-unify (term-var 0) (term-int 5) (subs-empty)) ; => (UOk {x0=5})
apply-goal
(apply-goal [g : (Goal int) state : Subst] :)
-- Goal application ─────────────────────────────────────────────────────────
| g | a goal | |
| state | the current search state (Subst) |
The solution Stream.
unify-goal-impl
(unify-goal-impl [lt1 : Term lt2 : Term state : Subst] :)
-- Goal constructors ────────────────────────────────────────────────────────
lequal
(lequal [t1 : Term t2 : Term] :)
goal that unifies two terms (miniKanren ==).
| t1 | first term | |
| t2 | second term |
A goal (Goal int) that succeeds iff t1 and t2 unify.
(run-logic 1 (lequal (term-int 5) (term-int 5))) ; => one solution
succeed
(succeed :)
goal that always succeeds without changing the substitution.
A goal (Goal int) that adds the current state unchanged to the solutions.
(run-logic 1 (succeed)) ; => one solution
fail
(fail :)
goal that always fails, producing no solutions.
A goal (Goal int) that produces an empty solution stream.
(run-logic 1 (fail)) ; => empty stream
conjoined-impl
(conjoined-impl [lg1 : (Goal int) lg2 : (Goal int) state : Subst] :)
implementation helper for conjunction.
conjoined-raw
(conjoined-raw [g1 : (Goal int) g2 : (Goal 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 : (Goal int) lg2 : (Goal int) state : Subst] :)
implementation helper for disjunction.
disjoined-raw
(disjoined-raw [g1 : (Goal int) g2 : (Goal 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 [^fat lf : (fn [Term])
implementation helper for fresh variable introduction.
fresh
(fresh [^fat f : (fn [Term])
create a new logic variable and pass it to a goal-building function.
| f | a (Term -> Goal) callback |
A goal (Goal int) that introduces a fresh variable and runs (f var).
(run-logic 1 (fresh (fn [x] (lequal x (term-int 7))))) ; => [x=7]
zzz
(zzz [g])
delay a goal so a recursive relation can be written at all.
| g | a goal EXPRESSION, not evaluated until the stream is pulled |
A goal that yields an immature stream.
(run-logic 1 (zzz (nats))) ; terminates
Since: lazy-streams
disjoined-dfs-impl
(disjoined-dfs-impl [lg1 : (Goal int) lg2 : (Goal int) state : Subst] :)
disjunction that searches DEPTH-FIRST.
| g1 | first goal | |
| g2 | second goal |
A goal yielding g1's solutions then g2's.
(run-logic 1 (disjoined-dfs (lequal x (term-int 1)) (lequal x (term-int 2))))
Since: lazy-streams
disjoined-dfs
(disjoined-dfs [A])
run-logic
(run-logic [A])
-- Runner ───────────────────────────────────────────────────────────────────
| n | maximum number of solutions | |
| g | goal to run (Goal A) |
A Stream of at most n solution states.
(run-logic 1 (fresh (fn [x] (lequal x (term-int 3))))) ; => one solution
stream-empty?
(stream-empty? [xs : Stream] :)
-- Result helpers ───────────────────────────────────────────────────────────
first-state
(first-state [results : Stream] :)
extract the first solution substitution from a run-logic
| results | solution stream from run-logic |
The first Subst, or the empty substitution if the stream is empty.
reify-walk
(reify-walk [t : Term results : Stream] :)
walk a term through the first solution's substitution.
| t | the term to reify | |
| results | solution stream from run-logic |
The walked term (ground term or unbound variable); t itself if there are no solutions.
(reify-walk my-var (run-logic 1 my-goal)) ; => ground term or variable
bind-goal-raw
(bind-goal-raw [g : (Goal int) k : fn] :)
-- HKT typeclass instances (stdlib-hkt-consolidation T3) ────────────────────
fmap-goal-raw
(fmap-goal-raw [g : (Goal int) f : (fn [Subst])
worker: map a callback over each solution state.
Functor[Goal]
(definstance Functor [Goal])
map a function over each solution state.
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