A unification library for Clojure.
A unification library for Clojure.
(extract-lvars form)(extract-lvars lv-fn form)Takes a datastructure form and returns a distinct set of the logical variables found within. By default, the lvar? predicate is used to detect nested lvars, but the function also accepts a custom predciate lv-fn to use instead.
Takes a datastructure form and returns a distinct set of the logical variables found within. By default, the lvar? predicate is used to detect nested lvars, but the function also accepts a custom predciate lv-fn to use instead.
(flatten-bindings binds)(flatten-bindings variable? binds)Flattens recursive bindings in binds to the same ground, if possible. If a variable cannot be resolved then it is left in place.
Flattens recursive bindings in binds to the same ground, if possible. If a variable cannot be resolved then it is left in place.
Returns true if a symbol represents a core.unify lvar. By default, core.unify expects a symbol starting with ? or just _.
Returns true if a symbol represents a core.unify lvar. By default, core.unify expects a symbol starting with ? or just _.
(make-occurs-subst-fn variable-fn)Given a function to recognize logic variables, returns a function that will attempt to substitute unification bindings between two expressions. This function uses an 'occurs check' to detect cycles.
Given a function to recognize logic variables, returns a function that will attempt to substitute unification bindings between two expressions. This function uses an 'occurs check' to detect cycles.
(make-occurs-unifier-fn variable-fn)Given a function to recognize logic variables, returns a function to perform the unification of two expressions. This function uses an 'occurs check' to detect cycles.
Given a function to recognize logic variables, returns a function to perform the unification of two expressions. This function uses an 'occurs check' to detect cycles.
(make-occurs-unify-fn variable-fn)Given a function to recognize logic variables, returns a function to return a bindings map for two expressions. This function uses an 'occurs check' to detect cycles.
Given a function to recognize logic variables, returns a function to return a bindings map for two expressions. This function uses an 'occurs check' to detect cycles.
(make-subst-fn variable-fn)Given a function to recognize unification variables, returns a function that will attempt to substitute unification bindings between two expressions without an 'occurs check'.
Given a function to recognize unification variables, returns a function that will attempt to substitute unification bindings between two expressions without an 'occurs check'.
(make-unifier-fn variable-fn)Given a function to recognize unification variables, returns a function to perform the unification of two expressions without an 'occurs check'.
Given a function to recognize unification variables, returns a function to perform the unification of two expressions without an 'occurs check'.
(make-unify-fn variable-fn)Given a function to recognize unification variables, returns a function to return a bindings map for two expressions without an 'occurs check'.
Given a function to recognize unification variables, returns a function to return a bindings map for two expressions without an 'occurs check'.
(subst expression bindings)Attempts to substitute the logic variables within an expression with their mapped values in bindings.
Attempts to substitute the logic variables within an expression with their mapped values in bindings.
(unifier expression1 expression2)Attempts the entire unification process from garnering the bindings to substituting the appropriate bindings, using an 'occurs check'.
Attempts the entire unification process from garnering the bindings to substituting the appropriate bindings, using an 'occurs check'.
(unifier- expression1 expression2)Attempts the entire unification process from garnering the bindings to substituting the appropriate bindings. This function is not guranteed to terminate if cyclic logic variables are present.
Attempts the entire unification process from garnering the bindings to substituting the appropriate bindings. This function is not guranteed to terminate if cyclic logic variables are present.
(unify expression1 expression2)Attempts to unify x and y with the given bindings (if any). May return a map of the unifiers (bindings) found. Will throw if an 'occurs check' determines that the expressions contain cyclic bindings or if the sub-expressions clash.
Attempts to unify x and y with the given bindings (if any). May return a map of the unifiers (bindings) found. Will throw if an 'occurs check' determines that the expressions contain cyclic bindings or if the sub-expressions clash.
(unify- expression1 expression2)Attempt to unify x and y with the given bindings (if any). May return a map of the unifiers (bindings) found. Will throw if the sub-expressions clash. This function is not guranteed to terminate if cyclic logic variables are present.
Attempt to unify x and y with the given bindings (if any). May return a map of the unifiers (bindings) found. Will throw if the sub-expressions clash. This function is not guranteed to terminate if cyclic logic variables are present.
(wildcard? form)Returns true if form starts with a core.unify wildcard. By default, core.unify expects the symbol &.
Returns true if form starts with a core.unify wildcard. By default, core.unify expects the symbol &.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |