miniKanren
A Domain Specific Languages for logic programming
logic programming
moon add FlyCloudC/miniKanren@0.1.9
Download zipAuthor
Version
0.1.9
License
Apache-2.0
Repository
Last updated
12 days ago
Downloads
37
README#FlyFloudC/miniKanren
The logic programming language, miniKanren.
More information:
- Daniel P. Friedman, William E. Byrd, Oleg Kiselyov, and Jason Hemann - The Reasoned Schemer
- miniKanren.org
#Example
// find all lists whose 1 and 0 are both in it
let solutions : Iter[Val] = run(v =>
listo(v) &
membero(Int(1), v) &
membero(Int(0), v)
)
solutions.take(10).each(println)The output is
(1 0)
(0 1)
(1 0 _₀)
(1 _₀ 0)
(0 1 _₀)
(_₀ 1 0)
(1 0 _₀ _₁)
(0 _₀ 1)
(1 _₀ 0 _₁)
(1 _₀ _₁ 0)#Goal
type Goal
#Val
#VarId
#appendo
appendo(l1, l2, o) means that the result of appending l1 to l2 is o.
#delay
Creates a lazy goal that delays the evaluation of its body until it is
needed.
Parameters:
- goal_fn : A function that takes no arguments and returns a goal. This function will be evaluated lazily when the resulting goal is applied to a substitution.
Returns a new goal that, when applied to a substitution, creates a suspension
that will evaluate the original goal function only when forced.
Example:
fn manyo(g : Goal) -> Goal {
g | delay(() => manyo(g))
}
inspect(run1(x => manyo(eqo(x, Int(1)))), content="1")#eqo
Creates a goal that unifies two values in a logic programming context. The
goal succeeds if the two values can be unified under some substitution,
producing a stream containing the unified substitution. If unification fails,
produces an empty stream.
Parameters:
- first : First logic value to be unified.
- second : Second logic value to be unified.
Returns a Goal that, when executed with a substitution, attempts to unify
the two values under that substitution.
Example:
inspect(run1(x => eqo(x, Int(42))), content="42")#fresh_var
Creates a new, unique logic variable. Each call to this function returns a
different variable.
#list_from_array
Creates a list from an array of values. The resulting list is represented
as nested pairs terminated by Nil.
Example:
assert_eq(
list_from_array([Int(1), Int(2), Int(3)]),
Pair(Int(1), Pair(Int(2), Pair(Int(3), Nil))),
)#listo
listo(v) means that v is a list.
A list is either an empty list or the cons of a value and another list.
#run
Executes a query and returns an iterator of solutions.
Parameters:
- query : A function that takes a logic variable and returns a goal. This function defines the logic query to be executed.
Returns an iterator that produces the solutions to the query. Each solution
is a concrete value that satisfies the constraints defined in the query.
Example:
inspect(run(x => eqo(x, Int(42))), content="[42]")#run1
Returns the first solution of a logic query.
Parameters:
- query : A function that takes a logic variable and returns a goal. This function defines the logic query to be executed. This query should have at least one solution, otherwise the function will panic.
Returns the first concrete value that satisfies the constraints defined in
the query.
Example:
inspect(run1(x => eqo(x, Int(42))), content="42")Source Files
A Domain Specific Languages for logic programming
logic programming
0.1.9
Apache-2.0
Updated 12 days ago
37 downloads