tur/backtrack

stdlib/backtrack.tur
defn

bt-nil

(bt-nil :int)

-- Helpers ────────────────────────────────────────────────────────────────

0 (null pointer representing the empty list).

defn

bt-cons

(bt-cons [v next] :int)

prepend a value to a backtrack result list.

vthe value to prepend
nextpointer to the existing result list (:int)

Pointer to the new cell (:int).

defn

mzero

(mzero :int)

-- Core monad operations ──────────────────────────────────────────────────

An empty result list (:int null pointer).

  (mzero)  ; => 0
defn

mreturn

(mreturn [x] :int)

lift a single value into the backtrack monad.

xthe value to return
A singleton result list containing x (:int).

  (mreturn 42)  ; => list containing 42
defn

mplus

(mplus [xs ys] :int)

concatenate (union) two backtrack result lists.

xsfirst result list (:int)
yssecond result list (:int)
A new result list with all elements from xs followed by all from ys (:int).

  (mplus (mreturn 1) (mreturn 2))  ; => list [1, 2]
defn

mbind

(mbind [ma fn] :int)

concatMap: apply fn to each result and concatenate all outputs.

maa backtrack result list (:int)
fnfat closure of type (a -> Backtrack b)
The concatenated results of applying fn to each element of ma (:int).

  (mbind (mreturn 3) (fn [x] (mreturn (* x 2))))  ; => list [6]
defn

run-backtrack

(run-backtrack [xs] :int)

-- Run operations ─────────────────────────────────────────────────────────

xsa backtrack result list (:int)
The same result list (the list monad is already eager) (:int).

  (run-backtrack (mreturn 1))  ; => list [1]
defn

run-backtrack-depth

(run-backtrack-depth [xs n] :int)

return at most n results from a backtrack computation.

xsa backtrack result list (:int)
nmaximum number of results to return (:int)
A truncated result list of length at most n (:int).

  (run-backtrack-depth my-results 5)  ; => first 5 results
defn

choice

(choice [xs] :int)

-- Combinators ────────────────────────────────────────────────────────────

xsa backtrack result list (:int)

xs unchanged (:int).

defn

guard

(guard [pred :bool] :int)

succeed with a dummy value when pred is true, fail otherwise.

predboolean condition
(mreturn 0) if pred is true, (mzero) otherwise (:int).

  (guard (> x 0))  ; => mreturn 0 or mzero
defn

fresh

(fresh [f] :int)

apply a fat closure to a fresh variable placeholder (0).

ffat closure of type (a -> Backtrack b)

The result of applying f to the placeholder 0 (:int).

defn

once

(once [xs] :int)

keep only the first result from a backtrack computation.

xsa backtrack result list (:int)
A singleton list containing the first element, or empty if xs is empty (:int).

  (once (mplus (mreturn 1) (mreturn 2)))  ; => list [1]
defn

interleave

(interleave [xs ys] :int)

fair interleaving of two backtrack result lists.

xsfirst result list (:int)
yssecond result list (:int)
A new list that alternates elements from xs and ys (:int).

  (interleave (mreturn 1) (mreturn 2))  ; => list [1, 2] (interleaved)
defn

bt-length

(bt-length [xs] :int)

-- List utilities ─────────────────────────────────────────────────────────

xsa backtrack result list (:int)
The number of elements (:int).

  (bt-length (mplus (mreturn 1) (mreturn 2)))  ; => 2
defn

bt-print

(bt-print [xs])

print each value in a backtrack result list to stdout.

xsa backtrack result list (:int)
defmacro

backtrack-do

(backtrack-do [& forms])

monadic do-notation for the backtracking monad.

formsalternating variable names and monadic expressions, then a body
A backtrack computation (result list) (:int).

  (backtrack-do x (mplus (mreturn 1) (mreturn 2))
                y (mplus (mreturn 10) (mreturn 20))
                (mreturn (+ x y)))  ; => list [11, 21, 12, 22]
Internal definitions
__bt-do-- -- backtrack-do macro ─────────────────────────────────────────────────────