tur/backtrack
backtracking monad (list monad) for non-deterministic search.
Backtrack T = list T. Each "result" is a list of all possible values.
Since: Phase CA0
Backtrack
(defopaque Backtrack [A] :int)
a kind-(* -> *) handle over the list/non-determinism monad; carrier is the int result-list (Cell) pointer.
Since: stdlib-hkt-consolidation T3
bt-nil
(bt-nil :int)
return the empty backtrack list (null pointer sentinel).
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)
the empty backtrack computation (no results).
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 :int ^fat f :(fn [int] int)] :int)
concatMap: apply fn to each result and concatenate all outputs.
fn MUST be a fat closure (struct { int64_t __fn; ... }). Use the backtrack-do macro which guarantees fat closures via forced capture.
| 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)
return all results from a backtrack computation (identity).
| 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)
identity combinator; xs is already a list of alternatives.
| 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 [^fat f :(fn [int] int)] :int)
apply a fat closure to a fresh (unbound) logic variable.
The fresh variable is represented by the sentinel INT64_MIN, which is outside the practical range of logic values and distinct from 0.
f MUST be a fat closure.
| 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)
count the number of results in a backtrack result list.
| 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.
Syntax: (backtrack-do var1 ma1 var2 ma2 ... body)
Each (var ma) pair binds var to each element of the backtrack computation ma. The final form is the body expression, which should return a backtrack value. All generated lambdas are guaranteed to be fat closures.
| 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]
bt-apply-fat
(bt-apply-fat [f x] :int)
invoke a fat-closure box with a single argument.
fmap-backtrack-raw
(fmap-backtrack-raw [xs f :fn] :int)
worker: map a :fn callback over every result.
ap-backtrack-raw
(ap-backtrack-raw [fs xs] :int)
int worker: cartesian application of fns to arguments.
Functor[Backtrack]
(definstance Functor [Backtrack])
map a function over every result value.
(fmap (mreturn 21) (fn [x] (* x 2))) ; => [42]
Since: stdlib-hkt-consolidation T3
Applicative[Backtrack]
(definstance Applicative [Backtrack])
pure is a singleton result; ap forms the cartesian product, applying each function result to each argument result.
(ap (mreturn (fn [x] (+ x 1))) (mreturn 41)) ; => [42]
Since: stdlib-hkt-consolidation T3
Monad[Backtrack]
(definstance Monad [Backtrack])
bind is concatMap: feed every result into the continuation and union the outputs. This is what do-m / for lower onto.
(do-m x (mplus (mreturn 1) (mreturn 2)) (mreturn (* x 10))) ; => [10 20]
Since: stdlib-hkt-consolidation T3
Alternative[Backtrack]
(definstance Alternative [Backtrack])
empty is the failing search; alt-or unions the results of both searches (the backtracking choice).
(alt-or (mreturn 1) (mreturn 2)) ; => [1 2]
Since: stdlib-hkt-consolidation T3
Internal definitions
__bt-do-- -- backtrack-do macro ─────────────────────────────────────────────────────