Implement Cut

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(),

src/ast.rs

@@ -78,6 +78,10 @@ pub enum Term {
     App(AppTerm),
     /// A signed 64-bit integer
     Int(i64),
+    /// The special built-in cut predicate.
+    ///
+    /// Evaluating it prunes all further choices for the currently active rule.
+    Cut,
 }
 
 impl Term {
@@ -91,6 +95,7 @@ impl Term {
             Term::Var(v) => v.0 + 1,
             Term::App(app) => app.count_var_slots(),
             Term::Int(_) => 0,
+            Term::Cut => 0,
         }
     }
 }
@@ -182,7 +187,7 @@ pub struct Rule {
     pub head: AppTerm,
     /// The terms that need to hold for the `head` to become true. If the tail is empty, then the
     /// head is always true. The rule is then called a fact.
-    pub tail: Vec<AppTerm>,
+    pub tail: Vec<Term>,
     /// Names of the variables used in this rule
     pub scope: Option<VarScope>,
 }
@@ -208,7 +213,7 @@ impl Rule {
             functor: pred,
             args,
         };
-        self.tail.push(app_term);
+        self.tail.push(Term::App(app_term));
         self
     }
 }
@@ -227,14 +232,14 @@ impl Rule {
 /// let female = Sym::from_ord(1);
 /// let bob = Sym::from_ord(2);
 /// let rule = exists(|[x]|
-///     Query::single(grandparent, vec![bob.into(), x.into()])
-///     .and(female, vec![x.into()])
+///     Query::single_app(grandparent, vec![bob.into(), x.into()])
+///     .and_app(female, vec![x.into()])
 /// );
 /// ```
 #[derive(Debug, Clone, PartialEq, Eq)]
 pub struct Query {
     /// The conunctive goals that need to be proven as part of this query.
-    pub goals: Vec<AppTerm>,
+    pub goals: Vec<Term>,
     /// Names of the variables used in this query
     pub scope: Option<VarScope>,
 }
@@ -246,22 +251,30 @@ impl Query {
     }
 
     /// A query consisting of a set of goals.
-    pub fn new(goals: Vec<AppTerm>, scope: Option<VarScope>) -> Query {
+    pub fn new(goals: Vec<Term>, scope: Option<VarScope>) -> Query {
         Query { goals, scope }
     }
 
     /// A query with just a single goal.
-    pub fn single(pred: Sym, args: Vec<Term>) -> Query {
-        Query::new(vec![AppTerm::new(pred, args)], None)
+    pub fn single_app(pred: Sym, args: Vec<Term>) -> Query {
+        Query::single(Term::App(AppTerm::new(pred, args)))
+    }
+
+    /// A query with just a single goal.
+    pub fn single(pred: Term) -> Query {
+        Query::new(vec![pred], None)
     }
 
     /// Add another goal to this query.
-    pub fn and(mut self, pred: Sym, args: Vec<Term>) -> Self {
-        let app_term = AppTerm {
+    pub fn and_app(self, pred: Sym, args: Vec<Term>) -> Self {
+        self.and(Term::App(AppTerm {
             functor: pred,
             args,
-        };
-        self.goals.push(app_term);
+        }))
+    }
+
+    pub fn and(mut self, pred: Term) -> Self {
+        self.goals.push(pred);
         self
     }
 

src/lib.rs

@@ -111,7 +111,7 @@
 //! #     .when(add, vec![p.into(), q.into(), r.into()])
 //! # }));
 //! let query = ast::exists(|[x]| {
-//!     ast::Query::single(
+//!     ast::Query::single_app(
 //!         add,
 //!         vec![
 //!             x.into(),

src/resolve/arithmetic.rs

@@ -84,6 +84,8 @@ impl ArithmeticResolver {
                 Some(ret)
             }
             Term::Int(i) => Some(i),
+            // TODO: log: any other term is an error
+            _ => None,
         }
     }
 
@@ -108,7 +110,8 @@ impl ArithmeticResolver {
                     .then_some(Resolved::Success)
             }
             Term::Int(left_val) => (left_val == right_val).then_some(Resolved::Success),
-            Term::App(_) => None,
+            // TODO: log invalid terms
+            _ => None,
         }
     }
 }