The easiest way to use Pony-Kanren in your code is via Pony-Stable: run
stable add github kulibali/pony-kanren
to add Pony-Kanren as a dependency to your
bundle.json, and then
in your code to import the library.
You can find library documentation here.
To set up a logic expression and query its results:
- Create an empty
Statevalue, with a functor that can unify the data type that your variables refer to.
- Create a
Goalthat represents a logical expression.
- Use the
Goal.fresh()function to obtain a new state that knows about a variable. That variable will now be visible to subgoals. Note that if you use
Goal.fresh()more than once, the variables will be disjoint. If their scopes intersect, you will get errors.
Goal.conj()for the logical AND operation. This will succeed only if both its subgoals succeed.
Goal.disj()is logical OR. This will succeed if either of its subgoals succeeds.
Goal.unify_vars()will unify two variables, if possible.
Goal.unify_vals()will attempt to structurally unify two values.
Goal.unify_val()will bind a variable to a value, if possible.
- Use the
- A goal is a function that returns a sequence of states. Each state may contain
variable bindings that represent a solution to the logical expression.
- If there is no solution for the expression, the sequence will be empty.
- If an error occurrs when solving, the sequence will contain a solution with
unbound variables and some error messages obtainable via its
- You can query the value of any variable in a particular state using the
The following Pony code initializes and solves the expression
A = B && (B = 123 || B = 456). Running the goal will result in a sequence of
two states, one where
B are bound to
123, and one where
are bound to
use "kanren" let a = Var("A") let b = Var("B") let g = Goals.fresh[USize](a, Goals.fresh[USize](b, Goals.conj[USize]( Goals.unify_vars[USize](b, a), Goals.disj[USize]( Goals.unify_val[USize](b, 123), Goals.unify_val[USize](b, 456) )))) let results = g(State[USize](UnifyEq[USize])) let s1 = results.next()? s1(a) == 123 // true s1(b) == 123 // true let s2 = results.next()? s2(a) == 456 // true s2(b) == 456 // true