From 04eac265ee998420ed3d4627ef83c62c23d4b2d5 Mon Sep 17 00:00:00 2001 From: Fabian Thorand Date: Sun, 24 Nov 2024 20:23:31 +0100 Subject: [PATCH] Update readme and add example --- README.md | 45 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 38 insertions(+), 7 deletions(-) diff --git a/README.md b/README.md index 540d917..3012d0a 100644 --- a/README.md +++ b/README.md @@ -7,20 +7,19 @@ ## Overview At the heart of this project is a small, efficient Rust library for solving first-order predicate -logic expressions like they can be found in e.g. Prolog. +logic expressions like they can be found in e.g. Prolog. Compare to the latter, this library is much +more simplistic, though extensible. Additionally, there is a [REPL example](examples/repl.rs) for interactively playing around with the implementation. -Compared to Prolog, it currently lacks some features though. Most notable, there are -- no negation or cut, -- no special built-in types (like integers) - Features that are implemented: - Standard (compound) terms - Named variables & wildcards - DFS-based inference -- Custom predicate resolvers (e.g. with side effects) +- A "cut" operation for pruning the search space +- Integer arithmetic +- Extensibility through custom predicate resolvers (e.g. predicates with side effects) ## Showcase @@ -70,6 +69,38 @@ Found solution: No more solutions. ``` +While there is no standard library, using the cut operation, it is possible to build many of the +common combinators, such as `once`: + +``` +?- :define once(X) :- X, !. +Defined! +``` + +Given a predicate producing multiple choices... + +``` +?- :define foo(hello). foo(world). +Defined! +?- foo(X). +Found solution: + X = hello +Found solution: + X = world +No more solutions. +``` + +..., we can now restrict it to produce only the first choice: + +``` +?- once(foo(X)). +Found solution: + X = hello +No more solutions. +``` + +Other combiantors, like negation, can also be implemented using cut. + ## Rust API The core of the API doesn't work with a textual representation of terms like the REPL does, but @@ -139,7 +170,7 @@ this answer: let solutions = query_dfs( &r, &exists(|[x]| { - Query::single( + Query::single_app( add, vec![ x.into(),