tur/backtrack
backtracking monad (list monad) for non-deterministic search.
Since: Phase CA0
bt-nil
(bt-nil :int)
-- Helpers ────────────────────────────────────────────────────────────────
0 (null pointer representing the empty list).
bt-cons
(bt-cons [v next] :int)
prepend a value to a backtrack result list.
| v | the value to prepend | |
| next | pointer to the existing result list (:int) |
Pointer to the new cell (:int).
mzero
(mzero :int)
-- Core monad operations ──────────────────────────────────────────────────
An empty result list (:int null pointer).
(mzero) ; => 0
mreturn
(mreturn [x] :int)
lift a single value into the backtrack monad.
| x | the value to return |
A singleton result list containing x (:int).
(mreturn 42) ; => list containing 42
mplus
(mplus [xs ys] :int)
concatenate (union) two backtrack result lists.
| xs | first result list (:int) | |
| ys | second 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]
mbind
(mbind [ma fn] :int)
concatMap: apply fn to each result and concatenate all outputs.
| ma | a backtrack result list (:int) | |
| fn | fat 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]
run-backtrack
(run-backtrack [xs] :int)
-- Run operations ─────────────────────────────────────────────────────────
| xs | a backtrack result list (:int) |
The same result list (the list monad is already eager) (:int).
(run-backtrack (mreturn 1)) ; => list [1]
run-backtrack-depth
(run-backtrack-depth [xs n] :int)
return at most n results from a backtrack computation.
| xs | a backtrack result list (:int) | |
| n | maximum 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
choice
(choice [xs] :int)
-- Combinators ────────────────────────────────────────────────────────────
| xs | a backtrack result list (:int) |
xs unchanged (:int).
guard
(guard [pred :bool] :int)
succeed with a dummy value when pred is true, fail otherwise.
| pred | boolean condition |
(mreturn 0) if pred is true, (mzero) otherwise (:int).
(guard (> x 0)) ; => mreturn 0 or mzero
fresh
(fresh [f] :int)
apply a fat closure to a fresh (unbound) logic variable.
| f | fat closure of type (a -> Backtrack b) |
The result of applying f to the unbound sentinel (:int).
once
(once [xs] :int)
keep only the first result from a backtrack computation.
| xs | a 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]
interleave
(interleave [xs ys] :int)
fair interleaving of two backtrack result lists.
| xs | first result list (:int) | |
| ys | second result list (:int) |
A new list that alternates elements from xs and ys (:int).
(interleave (mreturn 1) (mreturn 2)) ; => list [1, 2] (interleaved)
bt-length
(bt-length [xs] :int)
-- List utilities ─────────────────────────────────────────────────────────
| xs | a backtrack result list (:int) |
The number of elements (:int).
(bt-length (mplus (mreturn 1) (mreturn 2))) ; => 2
bt-print
(bt-print [xs])
print each value in a backtrack result list to stdout.
| xs | a backtrack result list (:int) |
backtrack-do
(backtrack-do [& forms])
monadic do-notation for the backtracking monad.
| forms | alternating 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 ─────────────────────────────────────────────────────