RFC: Arithmetics

examples/arithmetic.rs

@@ -13,12 +13,7 @@ fn main() {
         println!("SOLUTION:");
         for (var, term) in solution.iter_vars() {
             if let Some(term) = term {
-                println!(
-                    "  ${} = {}",
-                    var.ord(),
-                    u.pretty()
-                        .term_to_string(term, query.query().scope.as_ref())
-                );
+                println!("  ${} = {}", var.ord(), query.pretty().term_to_string(term));
             } else {
                 println!("<bug: no solution>");
             }

examples/repl.rs

@@ -171,13 +171,7 @@ fn query(state: &mut AppState, args: &str) {
                                 print!("  _{} = ", var.ord());
                             }
                             if let Some(term) = term {
-                                println!(
-                                    "{}",
-                                    state
-                                        .universe
-                                        .pretty()
-                                        .term_to_string(term, query.query().scope.as_ref())
-                                );
+                                println!("{}", query.pretty().term_to_string(term));
                             } else {
                                 println!("<any>");
                             }

examples/zebra.rs

@@ -20,11 +20,7 @@ fn main() {
             if i == 0 {
                 for var in solution.vars() {
                     if let Some(term) = var {
-                        println!(
-                            "{}",
-                            u.pretty()
-                                .term_to_string(term, query.query().scope.as_ref())
-                        );
+                        println!("{}", query.pretty().term_to_string(term));
                     } else {
                         println!("<bug: no solution>");
                     }

src/resolve/arithmetic.rs

@@ -1,7 +1,7 @@
 use std::collections::HashMap;
 use std::convert::TryInto;
 
-use crate::ast::Sym;
+use crate::ast::{Sym, Var};
 use crate::search::{Resolved, Resolver, SolutionState};
 use crate::term_arena::{AppTerm, ArgRange, Term, TermId};
 use crate::universe::SymbolStorage;
@@ -55,7 +55,15 @@ impl ArithmeticResolver {
             ("rem", Exp::Rem),
             ("pow", Exp::Pow),
         ];
-        let preds = [("is", Pred::Is)];
+        let preds = [
+            ("is", Pred::Is),
+            ("isLess", Pred::IsLess),
+            ("isGreater", Pred::IsGreater),
+            ("isLessEq", Pred::IsLessEq),
+            ("isGreaterEq", Pred::IsGreaterEq),
+            ("isDivider", Pred::IsDivider),
+            ("isNeg", Pred::IsNeg),
+        ];
         Self {
             exp_map: symbols.build_sym_map(exps),
             pred_map: symbols.build_sym_map(preds),
@@ -93,7 +101,7 @@ impl ArithmeticResolver {
         &mut self,
         args: ArgRange,
         context: &mut crate::search::ResolveContext,
-    ) -> Option<Resolved<()>> {
+    ) -> Option<Resolved<(Var, i64)>> {
         let [left, right] = context.solution().terms().get_args_fixed(args)?;
         // Right must be fully instantiated and evaluate to integer formula
         let right_val = self.eval_exp(context.solution(), right)?;
@@ -114,6 +122,60 @@ impl ArithmeticResolver {
             _ => None,
         }
     }
+
+    fn resolve_neg(
+        &mut self,
+        args: ArgRange,
+        context: &mut crate::search::ResolveContext,
+    ) -> Option<Resolved<(Var, i64)>> {
+        let [left, right] = context.solution().terms().get_args_fixed(args)?;
+        // Right must be fully instantiated and evaluate to integer formula
+        let right_val = self.eval_exp(context.solution(), right)?;
+
+        // Left must be variable or integer
+        let (_left_id, left_term) = context.solution().follow_vars(left);
+        match left_term {
+            Term::Var(var) => {
+                match right_val.checked_neg() {
+                    None => None,
+                    Some(value) => {
+                        // Allocate result and assign to unbound variable
+                        let result_term = context.solution_mut().terms_mut().int(value);
+                        context
+                            .solution_mut()
+                            .set_var(var, result_term)
+                            .then_some(Resolved::Success)
+                    },
+                }
+            }
+            Term::Int(left_val) => (left_val == -right_val).then_some(Resolved::Success),
+            // TODO: log invalid terms
+            _ => None,
+        }
+    }
+
+    fn resolve_instantiated_op2(
+        &mut self,
+        args: ArgRange,
+        context: &mut crate::search::ResolveContext,
+        op: fn(i64, i64) -> bool,
+    ) -> Option<Resolved<(Var, i64)>> {
+        let [left, right] = context.solution().terms().get_args_fixed(args)?;
+        // Right must be fully instantiated and evaluate to integer formula
+        let right_val = self.eval_exp(context.solution(), right)?;
+        // Left can be fully instantiated and evaluate to integer formula
+        if let Some(left_val) = self.eval_exp(context.solution(), left) {
+            op(left_val, right_val).then_some(Resolved::Success)
+        } else {
+            // Left must be variable or integer
+            let (_left_id, left_term) = context.solution().follow_vars(left);
+            match left_term {
+                Term::Int(left_val) => op(left_val, right_val).then_some(Resolved::Success),
+                // TODO: log invalid terms
+                _ => None,
+            }
+        }
+    }
 }
 
 enum Exp {
@@ -127,11 +189,16 @@ enum Exp {
 
 enum Pred {
     Is,
+    IsLess,
+    IsGreater,
+    IsLessEq,
+    IsGreaterEq,
+    IsDivider,
+    IsNeg,
 }
 
 impl Resolver for ArithmeticResolver {
-    /// The arithmetic resolver provides no choice.
-    type Choice = ();
+    type Choice = (Var, i64); // the largest number
 
     fn resolve(
         &mut self,
@@ -142,6 +209,12 @@ impl Resolver for ArithmeticResolver {
         let pred = self.pred_map.get(&sym)?;
         match pred {
             Pred::Is => self.resolve_is(args, context),
+            Pred::IsLess => self.resolve_instantiated_op2(args, context, |a, b| a < b),
+            Pred::IsGreater => self.resolve_instantiated_op2(args, context, |a, b| a > b),
+            Pred::IsLessEq => self.resolve_instantiated_op2(args, context, |a, b| a <= b),
+            Pred::IsGreaterEq => self.resolve_instantiated_op2(args, context, |a, b| a >= b),
+            Pred::IsDivider => self.resolve_instantiated_op2(args, context, |a, b| a % b == 0),
+            Pred::IsNeg => self.resolve_neg(args, context),
         }
     }
 

src/search/test.rs

@@ -243,12 +243,7 @@ fn cut() {
             .map(|sol| {
                 sol.vars()
                     .iter()
-                    .map(|var| {
-                        var.as_ref().map(|term| {
-                            tu.pretty()
-                                .term_to_string(term, query.query().scope.as_ref())
-                        })
-                    })
+                    .map(|var| var.as_ref().map(|term| query.pretty().term_to_string(term)))
                     .collect::<Vec<_>>()
             })
             .collect();

src/textual.rs

@@ -8,6 +8,7 @@ mod parser;
 mod pretty;
 
 pub use parser::{ParseError, ParseErrorKind};
+use pretty::ScopedPrettifier;
 
 use crate::{
     ast::Query,
@@ -69,7 +70,7 @@ pub use self::{parser::Parser, pretty::Prettifier};
 ///     println!("SOLUTION:");
 ///     for (var, term) in solution.iter_vars() {
 ///         if let Some(term) = term {
-///             println!("  ${} = {}", var.ord(), u.pretty().term_to_string(&term, query.query().scope.as_ref()));
+///             println!("  ${} = {}", var.ord(), query.pretty().term_to_string(&term));
 ///         } else {
 ///             println!("<bug: no solution>");
 ///         }
@@ -170,4 +171,10 @@ impl<'a> UniverseQuery<'a> {
     pub fn symbols_mut(&mut self) -> &mut SymbolOverlay<'a> {
         &mut self.symbols
     }
+
+    /// Return a pretty-printer using the symbols defined in this query.
+    /// As opposed to TextualUniverse::pretty, this one won't allow any mixups between the sources of the universe and the variables.
+    pub fn pretty(&self) -> ScopedPrettifier<SymbolOverlay> {
+        ScopedPrettifier::new(&self.symbols, self.query().scope.as_ref())
+    }
 }

src/textual/pretty.rs

@@ -2,9 +2,12 @@ use crate::{
     ast::{AppTerm, Query, Rule, Term, VarScope},
     universe::Symbols,
 };
+use std::ops::Deref;
 
 /// A pretty-printer for terms using the Prolog-like syntax of the
 /// [TextualUniverse](super::TextualUniverse).
+///
+/// This type takes an explicit scope in many methods, making it possible to use the wrong variable scope for the given universe. A version where mixups are impossible is ScopedPrettifier.
 pub struct Prettifier<'u, T: Symbols> {
     universe: &'u T,
 }
@@ -116,3 +119,50 @@ impl<'a, T: Symbols> Prettifier<'a, T> {
         Ok(())
     }
 }
+
+/// A prettifier for showing terms relating to a query.
+pub struct ScopedPrettifier<'u, T: Symbols> {
+    pretty: Prettifier<'u, T>,
+    // The scope is meant to reference the same query as the symbols in the base prettifier, so it shares the lifetime
+    scope: Option<&'u VarScope>,
+}
+
+impl<'u, T: Symbols> ScopedPrettifier<'u, T> {
+    pub fn new(universe: &'u T, scope: Option<&'u VarScope>) -> Self {
+        Self {
+            pretty: Prettifier::new(universe),
+            scope,
+        }
+    }
+
+    pub fn term_to_string(&self, term: &Term) -> String {
+        self.pretty.term_to_string(term, self.scope)
+    }
+
+    pub fn pretty<W: std::fmt::Write>(&self, writer: &mut W, term: &Term) -> std::fmt::Result {
+        self.pretty.pretty(writer, term, self.scope)
+    }
+
+    pub fn pretty_app<W: std::fmt::Write>(
+        &self,
+        writer: &mut W,
+        term: &AppTerm,
+    ) -> std::fmt::Result {
+        self.pretty.pretty_app(writer, term, self.scope)
+    }
+
+    pub fn pretty_conjunction<W: std::fmt::Write>(
+        &self,
+        writer: &mut W,
+        goals: &[Term],
+    ) -> std::fmt::Result {
+        self.pretty.pretty_conjunction(writer, goals, self.scope)
+    }
+}
+
+impl<'u, T: Symbols> Deref for ScopedPrettifier<'u, T> {
+    type Target = Prettifier<'u, T>;
+    fn deref(&self) -> &Self::Target {
+        &self.pretty
+    }
+}

src/universe.rs

@@ -143,7 +143,7 @@ impl Default for SymbolStore {
 }
 
 /// Stores and allocates unique symbols on top of a symbol store, without modifying it.
-#[derive(Debug)]
+#[derive(Debug, Clone)]
 pub struct SymbolOverlay<'a> {
     symbols: &'a SymbolStore,
     // Sym entries stored here start at 0, but get translated on the API boundary to start at symbols.num_symbols().