Universe can be queried while immutable

Added SymbolOverlay which contains changes needed to execute a particular query.

examples/arithmetic.rs

@@ -7,7 +7,7 @@ fn main() {
         .unwrap();
 
     let query = u.prepare_query("mul(A,A,B).").unwrap();
-    let solutions = query_dfs(u.resolver(), &query);
+    let solutions = query_dfs(u.resolver(), query.query());
 
     for solution in solutions.take(10) {
         println!("SOLUTION:");
@@ -16,7 +16,8 @@ fn main() {
                 println!(
                     "  ${} = {}",
                     var.ord(),
-                    u.pretty().term_to_string(&term, query.scope.as_ref())
+                    u.pretty()
+                        .term_to_string(&term, query.query().scope.as_ref())
                 );
             } else {
                 println!("<bug: no solution>");

examples/repl.rs

@@ -9,7 +9,7 @@ use logru::resolve::{ArithmeticResolver, ResolverExt};
 use logru::search::{query_dfs, Resolved, Resolver};
 use logru::term_arena::{AppTerm, ArgRange};
 use logru::textual::{Prettifier, TextualUniverse};
-use logru::SymbolStore;
+use logru::{SymbolStorage, SymbolStore};
 use rustyline::completion::Completer;
 use rustyline::error::ReadlineError;
 use rustyline::highlight::Highlighter;
@@ -148,11 +148,11 @@ fn query(state: &mut AppState, args: &str) {
         Ok(query) => {
             let builtins = state
                 .commands
-                .as_resolver(&state.universe.symbols, query.scope.as_ref());
+                .as_resolver(&state.universe.symbols, query.query().scope.as_ref());
             let resolver = builtins
                 .or_else(&mut state.arithmetic)
                 .or_else(state.universe.resolver());
-            let mut solutions = query_dfs(resolver, &query);
+            let mut solutions = query_dfs(resolver, query.query());
             loop {
                 if state.interrupted.load(atomic::Ordering::SeqCst) {
                     println!("Interrupted!");
@@ -163,7 +163,9 @@ fn query(state: &mut AppState, args: &str) {
                         let solution = solutions.get_solution();
                         println!("Found solution:");
                         for (var, term) in solution.iter_vars() {
-                            if let Some(name) = query.scope.as_ref().and_then(|s| s.get_name(var)) {
+                            if let Some(name) =
+                                query.query().scope.as_ref().and_then(|s| s.get_name(var))
+                            {
                                 print!("  {} = ", name);
                             } else {
                                 print!("  _{} = ", var.ord());
@@ -174,7 +176,7 @@ fn query(state: &mut AppState, args: &str) {
                                     state
                                         .universe
                                         .pretty()
-                                        .term_to_string(&term, query.scope.as_ref())
+                                        .term_to_string(&term, query.query().scope.as_ref())
                                 );
                             } else {
                                 println!("<any>");

examples/zebra.rs

@@ -11,7 +11,7 @@ fn main() {
 
     let query = u.prepare_query("puzzle(Houses).").unwrap();
     for i in 0..repeats {
-        let search = logru::query_dfs(u.resolver(), &query);
+        let search = logru::query_dfs(u.resolver(), query.query());
         let before = Instant::now();
         let solutions = search.collect::<Vec<_>>();
         let duration = before.elapsed();
@@ -20,7 +20,11 @@ fn main() {
             if i == 0 {
                 for var in solution.vars() {
                     if let Some(term) = var {
-                        println!("{}", u.pretty().term_to_string(term, query.scope.as_ref()));
+                        println!(
+                            "{}",
+                            u.pretty()
+                                .term_to_string(term, query.query().scope.as_ref())
+                        );
                     } else {
                         println!("<bug: no solution>");
                     }

src/lib.rs

@@ -35,6 +35,7 @@
 //!
 //! ```
 //! use logru::ast::{self, Rule};
+//! use logru::SymbolStorage;
 //!
 //! let mut syms = logru::SymbolStore::new();
 //! let mut r = logru::RuleSet::new();
@@ -84,6 +85,7 @@
 //! # use logru::ast::{self, Rule};
 //! # use logru::resolve::RuleResolver;
 //! # use logru::search::Solution;
+//! # use logru::SymbolStorage;
 //! # let mut syms = logru::SymbolStore::new();
 //! # let mut r = logru::RuleSet::new();
 //! # let s = syms.get_or_insert_named("s");
@@ -154,4 +156,4 @@ pub mod universe;
 
 pub use resolve::RuleResolver;
 pub use search::query_dfs;
-pub use universe::{RuleSet, SymbolStore};
+pub use universe::{RuleSet, SymbolStorage, SymbolStore, Symbols};

src/resolve/arithmetic.rs

@@ -4,7 +4,7 @@ use std::convert::TryInto;
 use crate::ast::Sym;
 use crate::search::{Resolved, Resolver, SolutionState};
 use crate::term_arena::{AppTerm, ArgRange, Term, TermId};
-use crate::SymbolStore;
+use crate::universe::SymbolStorage;
 
 /// A special resolver for integer arithmetic. It provides a special predicate `is/2` which
 /// evaluates integer expressions.
@@ -46,7 +46,7 @@ pub struct ArithmeticResolver {
 }
 
 impl ArithmeticResolver {
-    pub fn new(symbols: &mut SymbolStore) -> Self {
+    pub fn new<T: SymbolStorage>(symbols: &mut T) -> Self {
         let exps = [
             ("add", Exp::Add),
             ("sub", Exp::Sub),
@@ -167,14 +167,12 @@ mod tests {
 
     #[test]
     fn simple() {
-        let mut tu = TextualUniverse::new();
-        let query = tu
+        let tu = TextualUniverse::new();
+        let mut query = tu
             .prepare_query("is(X, add(3, mul(3, sub(6, div(10, rem(10, pow(2,3))))))).")
             .unwrap();
-        let mut results = query_dfs(
-            ArithmeticResolver::new(&mut tu.symbols).or_else(tu.resolver()),
-            &query,
-        );
+        let resolver = ArithmeticResolver::new(&mut query.symbols_mut());
+        let mut results = query_dfs(resolver.or_else(tu.resolver()), query.query());
         assert_eq!(results.next(), Some(Solution(vec![Some(Term::Int(6))])));
         assert!(results.next().is_none());
     }
@@ -193,25 +191,25 @@ mod tests {
         .unwrap();
         {
             let query = tu.prepare_query("eq(add(2, 2), pow(2, 2)).").unwrap();
-            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), &query);
+            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), query.query());
             assert_eq!(results.next(), Some(Solution(vec![])));
             assert!(results.next().is_none());
         }
         {
             let query = tu.prepare_query("eq(X, pow(2, 2)).").unwrap();
-            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), &query);
+            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), query.query());
             assert_eq!(results.next(), Some(Solution(vec![Some(Term::Int(4))])));
             assert!(results.next().is_none());
         }
         {
             let query = tu.prepare_query("eq(add(2, 2), X).").unwrap();
-            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), &query);
+            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), query.query());
             assert_eq!(results.next(), Some(Solution(vec![Some(Term::Int(4))])));
             assert!(results.next().is_none());
         }
         {
             let query = tu.prepare_query("eq(2, 2).").unwrap();
-            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), &query);
+            let mut results = query_dfs(arith.by_ref().or_else(tu.resolver()), query.query());
             assert_eq!(results.next(), Some(Solution(vec![])));
             assert!(results.next().is_none());
         }

src/search.rs

@@ -113,6 +113,7 @@ impl<'c> ResolveContext<'c> {
     }
 }
 
+#[derive(Debug)]
 pub enum Resolved<C> {
     /// The goal resolved to a single choice that was successfully applied to the state.
     Success,
@@ -284,6 +285,7 @@ impl<R: Resolver> SolutionIter<R> {
     /// # use logru::ast::{self, Rule};
     /// # use logru::resolve::RuleResolver;
     /// # use logru::search::Step;
+    /// # use logru::SymbolStorage;
     /// # let mut syms = logru::SymbolStore::new();
     /// # let mut r = logru::RuleSet::new();
     /// # let s = syms.get_or_insert_named("s");

src/search/test.rs

@@ -1,6 +1,6 @@
 use super::*;
 use crate::textual::TextualUniverse;
-use crate::{ast::*, RuleResolver, RuleSet, SymbolStore};
+use crate::{ast::*, RuleResolver, RuleSet, SymbolStorage, SymbolStore};
 
 #[test]
 fn genealogy() {
@@ -237,15 +237,17 @@ fn cut() {
     #[track_caller]
     fn assert_solutions(tu: &mut TextualUniverse, query: &str, solutions: &[&[Option<&str>]]) {
         let query = tu.prepare_query(query).unwrap();
-        let rets: Vec<_> = query_dfs(tu.resolver(), &query).collect();
+        let rets: Vec<_> = query_dfs(tu.resolver(), query.query()).collect();
         let pretty_solutions: Vec<_> = rets
             .into_iter()
             .map(|sol| {
                 sol.vars()
                     .iter()
                     .map(|var| {
-                        var.as_ref()
-                            .map(|term| tu.pretty().term_to_string(&term, query.scope.as_ref()))
+                        var.as_ref().map(|term| {
+                            tu.pretty()
+                                .term_to_string(&term, query.query().scope.as_ref())
+                        })
                     })
                     .collect::<Vec<_>>()
             })

src/textual.rs

@@ -13,7 +13,7 @@ use crate::{
     ast::Query,
     resolve::RuleResolver,
     search::{self, SolutionIter},
-    universe::{RuleSet, SymbolStore},
+    universe::{RuleSet, SymbolOverlay, SymbolStore},
 };
 
 pub use self::{parser::Parser, pretty::Prettifier};
@@ -64,12 +64,12 @@ pub use self::{parser::Parser, pretty::Prettifier};
 /// .unwrap();
 ///
 /// let query = u.prepare_query("mul(X,X,Y).").unwrap();
-/// let solutions = query_dfs(u.resolver(), &query);
+/// let solutions = query_dfs(u.resolver(), query.query());
 /// for solution in solutions.take(5) {
 ///     println!("SOLUTION:");
 ///     for (var, term) in solution.iter_vars() {
 ///         if let Some(term) = term {
-///             println!("  ${} = {}", var.ord(), u.pretty().term_to_string(&term, query.scope.as_ref()));
+///             println!("  ${} = {}", var.ord(), u.pretty().term_to_string(&term, query.query().scope.as_ref()));
 ///         } else {
 ///             println!("<bug: no solution>");
 ///         }
@@ -100,8 +100,11 @@ impl TextualUniverse {
     }
 
     /// Parse a query, but do not run it.
-    pub fn prepare_query(&mut self, query: &str) -> Result<Query, ParseError> {
-        Parser::new(&mut self.symbols).parse_query_str(query)
+    pub fn prepare_query(&self, query: &str) -> Result<UniverseQuery<'_>, ParseError> {
+        let symbols = SymbolOverlay::new(&self.symbols);
+        let mut parser = Parser::new(symbols);
+        let query = parser.parse_query_str(query)?;
+        Ok(UniverseQuery::new(parser.into_symbols(), query))
     }
 
     /// Run a query against the universe using the DFS solver.
@@ -115,18 +118,21 @@ impl TextualUniverse {
     /// thus the pretty-printer is still accessible.
     pub fn query_dfs(&mut self, query: &str) -> Result<SolutionIter<RuleResolver>, ParseError> {
         let query = self.prepare_query(query)?;
-        Ok(search::query_dfs(RuleResolver::new(&self.rules), &query))
+        Ok(search::query_dfs(
+            RuleResolver::new(&self.rules),
+            query.query(),
+        ))
     }
 
     // //////////////////////////////// OTHER ACCESSORS ////////////////////////////////
 
     /// Return a pretty-printer using the symbols defined in this universe.
-    pub fn pretty(&self) -> Prettifier {
+    pub fn pretty(&self) -> Prettifier<SymbolStore> {
         Prettifier::new(&self.symbols)
     }
 
     /// Return a term parser that uses the name mapping of this universe for parsing terms.
-    pub fn parse(&mut self) -> Parser {
+    pub fn parse(&mut self) -> Parser<&mut SymbolStore> {
         Parser::new(&mut self.symbols)
     }
 
@@ -141,3 +147,27 @@ impl Default for TextualUniverse {
         Self::new()
     }
 }
+
+/// A query tied to a particular universe through symbols
+pub struct UniverseQuery<'a> {
+    symbols: SymbolOverlay<'a>,
+    query: Query,
+}
+
+impl<'a> UniverseQuery<'a> {
+    pub fn new(symbols: SymbolOverlay<'a>, query: Query) -> Self {
+        Self { symbols, query }
+    }
+
+    pub fn query(&self) -> &Query {
+        &self.query
+    }
+
+    pub fn symbols(&self) -> &SymbolOverlay<'a> {
+        &self.symbols
+    }
+
+    pub fn symbols_mut(&mut self) -> &mut SymbolOverlay<'a> {
+        &mut self.symbols
+    }
+}

src/textual/parser.rs

@@ -3,7 +3,7 @@ use std::iter::Peekable;
 use logos::{Logos, Span, SpannedIter};
 
 use crate::ast::{AppTerm, Query, Rule, Sym, Term, Var, VarScope};
-use crate::universe::SymbolStore;
+use crate::universe::SymbolStorage;
 
 use super::lexer::Token;
 
@@ -91,17 +91,21 @@ impl ParseErrorKind {
 
 /// A parser for terms using the Prolog-like syntax of the
 /// [TextualUniverse](super::TextualUniverse).
-pub struct Parser<'u> {
-    symbols: &'u mut SymbolStore,
+pub struct Parser<T: SymbolStorage> {
+    symbols: T,
 }
 
-impl<'a> Parser<'a> {
-    pub fn new(symbols: &'a mut SymbolStore) -> Self {
+impl<'a, T: SymbolStorage> Parser<T> {
+    pub fn new(symbols: T) -> Self {
         Self { symbols }
     }
 
-    // //////////////////////////////// PUBLIC PARSER ////////////////////////////////
+    /// The act of parsing creates a new set of symbols which correspond to the parsed queries. This extracts those symbols.
+    pub fn into_symbols(self) -> T {
+        self.symbols
+    }
 
+    // //////////////////////////////// PUBLIC PARSER ////////////////////////////////
     pub fn parse_query_str(&mut self, query: &str) -> Result<Query, ParseError> {
         let mut tokens = TokenStream::new(query);
         let mut scope = VarScope::new();
@@ -279,13 +283,17 @@ impl<'a> Parser<'a> {
 mod test {
     use super::super::pretty;
     use super::*;
+    use crate::universe::{SymbolOverlay, SymbolStore};
+
     fn query_roundtrip_test(input: &str) {
-        let mut nu = SymbolStore::new();
-        let mut p = Parser::new(&mut nu);
+        let mut ss = SymbolStore::new();
+        let nu = SymbolOverlay::new(&mut ss);
+        let mut p = Parser::new(nu);
 
         let q = p.parse_query_str(input).unwrap();
 
-        let pretty = pretty::Prettifier::new(&nu);
+        let symbols = p.into_symbols();
+        let pretty = pretty::Prettifier::new(&symbols);
         let qs = pretty.query_to_string(&q);
         assert_eq!(qs, input);
     }

src/textual/pretty.rs

@@ -1,15 +1,16 @@
-use crate::ast::{AppTerm, Query, Rule, Term, VarScope};
-
-use super::SymbolStore;
+use crate::{
+    ast::{AppTerm, Query, Rule, Term, VarScope},
+    universe::Symbols,
+};
 
 /// A pretty-printer for terms using the Prolog-like syntax of the
 /// [TextualUniverse](super::TextualUniverse).
-pub struct Prettifier<'u> {
-    universe: &'u SymbolStore,
+pub struct Prettifier<'u, T: Symbols> {
+    universe: &'u T,
 }
 
-impl<'a> Prettifier<'a> {
-    pub fn new(universe: &'a SymbolStore) -> Self {
+impl<'a, T: Symbols> Prettifier<'a, T> {
+    pub fn new(universe: &'a T) -> Self {
         Self { universe }
     }