Merge pull request #211 from nikomatsakis/queryify

decompose chalk logic for query-ification and re-use

Author: nikomatsakis

.dir-locals.el

@@ -0,0 +1 @@
+((rust-mode (rust-format-on-save . t)))

Cargo.lock

@@ -13,12 +13,12 @@ edition = "2018"
 bench = []
 
 [dependencies]
+derive-new = "0.5.6"
 diff = "0.1.11"
 docopt = "1.0.0"
 failure = "0.1"
 itertools = "0.7.8"
 lalrpop-intern = "0.15.1"
-petgraph = "0.4.13"
 rustyline = "1.0"
 salsa = "0.10.0"
 serde = "1.0"
@@ -45,4 +45,12 @@ path = "chalk-macros"
 version = "0.9.0"
 path = "chalk-engine"
 
+[dependencies.chalk-rust-ir]
+version = "0.1.0"
+path = "chalk-rust-ir"
+
+[dependencies.chalk-rules]
+version = "0.1.0"
+path = "chalk-rules"
+
 [workspace]

Cargo.toml

@@ -125,6 +125,45 @@ pub trait Context: Clone + Debug {
         environment: &Self::Environment,
         goal: Self::Goal,
     ) -> Self::GoalInEnvironment;
+
+    /// Extracts the inner normalized substitution from a canonical ex-clause.
+    fn inference_normalized_subst_from_ex_clause(
+        canon_ex_clause: &Self::CanonicalExClause,
+    ) -> &Self::InferenceNormalizedSubst;
+
+    /// Extracts the inner normalized substitution from a canonical constraint subst.
+    fn inference_normalized_subst_from_subst(
+        canon_ex_clause: &Self::CanonicalConstrainedSubst,
+    ) -> &Self::InferenceNormalizedSubst;
+
+    /// True if this solution has no region constraints.
+    fn empty_constraints(ccs: &Self::CanonicalConstrainedSubst) -> bool;
+
+    fn canonical(u_canon: &Self::UCanonicalGoalInEnvironment) -> &Self::CanonicalGoalInEnvironment;
+
+    fn is_trivial_substitution(
+        u_canon: &Self::UCanonicalGoalInEnvironment,
+        canonical_subst: &Self::CanonicalConstrainedSubst,
+    ) -> bool;
+
+    fn num_universes(_: &Self::UCanonicalGoalInEnvironment) -> usize;
+
+    /// Convert a goal G *from* the canonical universes *into* our
+    /// local universes. This will yield a goal G' that is the same
+    /// but for the universes of universally quantified names.
+    fn map_goal_from_canonical(
+        _: &Self::UniverseMap,
+        value: &Self::CanonicalGoalInEnvironment,
+    ) -> Self::CanonicalGoalInEnvironment;
+
+    /// Convert a substitution *from* the canonical universes *into*
+    /// our local universes. This will yield a substitution S' that is
+    /// the same but for the universes of universally quantified
+    /// names.
+    fn map_subst_from_canonical(
+        _: &Self::UniverseMap,
+        value: &Self::CanonicalConstrainedSubst,
+    ) -> Self::CanonicalConstrainedSubst;
 }
 
 pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
@@ -155,43 +194,6 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
         canonical_ex_clause: &C::CanonicalExClause,
         op: impl WithInstantiatedExClause<C, Output = R>,
     ) -> R;
-
-    /// Extracts the inner normalized substitution from a canonical ex-clause.
-    fn inference_normalized_subst_from_ex_clause(
-        canon_ex_clause: &C::CanonicalExClause,
-    ) -> &C::InferenceNormalizedSubst;
-
-    /// Extracts the inner normalized substitution from a canonical constraint subst.
-    fn inference_normalized_subst_from_subst(
-        canon_ex_clause: &C::CanonicalConstrainedSubst,
-    ) -> &C::InferenceNormalizedSubst;
-
-    /// True if this solution has no region constraints.
-    fn empty_constraints(ccs: &C::CanonicalConstrainedSubst) -> bool;
-
-    fn canonical(u_canon: &C::UCanonicalGoalInEnvironment) -> &C::CanonicalGoalInEnvironment;
-    fn is_trivial_substitution(
-        u_canon: &C::UCanonicalGoalInEnvironment,
-        canonical_subst: &C::CanonicalConstrainedSubst,
-    ) -> bool;
-    fn num_universes(_: &C::UCanonicalGoalInEnvironment) -> usize;
-
-    /// Convert a goal G *from* the canonical universes *into* our
-    /// local universes. This will yield a goal G' that is the same
-    /// but for the universes of universally quantified names.
-    fn map_goal_from_canonical(
-        _: &C::UniverseMap,
-        value: &C::CanonicalGoalInEnvironment,
-    ) -> C::CanonicalGoalInEnvironment;
-
-    /// Convert a substitution *from* the canonical universes *into*
-    /// our local universes. This will yield a substitution S' that is
-    /// the same but for the universes of universally quantified
-    /// names.
-    fn map_subst_from_canonical(
-        _: &C::UniverseMap,
-        value: &C::CanonicalConstrainedSubst,
-    ) -> C::CanonicalConstrainedSubst;
 }
 
 /// Callback trait for `instantiate_ucanonical_goal`. Unlike the other

chalk-engine/src/context.rs

@@ -6,17 +6,16 @@ use crate::table::{Answer, AnswerIndex};
 use crate::tables::Tables;
 use crate::{DepthFirstNumber, SimplifiedAnswer, TableIndex};
 
-pub struct Forest<C: Context, CO: ContextOps<C>> {
-    #[allow(dead_code)]
-    pub(crate) context: CO,
+pub struct Forest<C: Context> {
+    context: C,
     pub(crate) tables: Tables<C>,
     pub(crate) stack: Stack,
 
     dfn: DepthFirstNumber,
 }
 
-impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
-    pub fn new(context: CO) -> Self {
+impl<C: Context> Forest<C> {
+    pub fn new(context: C) -> Self {
         Forest {
             context,
             tables: Tables::new(),
@@ -25,6 +24,16 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
         }
     }
 
+    /// Gives access to `self.context`. In fact, the SLG solver
+    /// doesn't ever use `self.context` for anything, and only cares
+    /// about the associated types and methods defined on it.  But the
+    /// creator of the forest can use the context field to store
+    /// configuration info (e.g., in chalk, we store the max size of a
+    /// term in here).
+    pub fn context(&self) -> &C {
+        &self.context
+    }
+
     // Gets the next depth-first number. This number never decreases.
     pub(super) fn next_dfn(&mut self) -> DepthFirstNumber {
         self.dfn.next()
@@ -37,15 +46,16 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// terminate.
     pub fn force_answers(
         &mut self,
+        context: &impl ContextOps<C>,
         goal: C::UCanonicalGoalInEnvironment,
         num_answers: usize,
     ) -> Vec<Answer<C>> {
-        let table = self.get_or_create_table_for_ucanonical_goal(goal);
+        let table = self.get_or_create_table_for_ucanonical_goal(context, goal);
         let mut answers = Vec::with_capacity(num_answers);
         for i in 0..num_answers {
             let i = AnswerIndex::from(i);
             loop {
-                match self.ensure_root_answer(table, i) {
+                match self.ensure_root_answer(context, table, i) {
                     Ok(()) => break,
                     Err(RootSearchFail::QuantumExceeded) => continue,
                     Err(RootSearchFail::NoMoreSolutions) => return answers,
@@ -64,12 +74,14 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// invocations. Invoking `next` fewer times is preferable =)
     fn iter_answers<'f>(
         &'f mut self,
+        context: &'f impl ContextOps<C>,
         goal: &C::UCanonicalGoalInEnvironment,
     ) -> impl AnswerStream<C> + 'f {
-        let table = self.get_or_create_table_for_ucanonical_goal(goal.clone());
+        let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone());
         let answer = AnswerIndex::ZERO;
         ForestSolver {
             forest: self,
+            context,
             table,
             answer,
         }
@@ -78,10 +90,12 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     /// Solves a given goal, producing the solution. This will do only
     /// as much work towards `goal` as it has to (and that works is
     /// cached for future attempts).
-    pub fn solve(&mut self, goal: &C::UCanonicalGoalInEnvironment) -> Option<C::Solution> {
-        self.context
-            .clone()
-            .make_solution(CO::canonical(&goal), self.iter_answers(goal))
+    pub fn solve(
+        &mut self,
+        context: &impl ContextOps<C>,
+        goal: &C::UCanonicalGoalInEnvironment,
+    ) -> Option<C::Solution> {
+        context.make_solution(C::canonical(&goal), self.iter_answers(context, goal))
     }
 
     /// True if all the tables on the stack starting from `depth` and
@@ -118,25 +132,34 @@ impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
     }
 
     /// Useful for testing.
-    pub fn num_cached_answers_for_goal(&mut self, goal: &C::UCanonicalGoalInEnvironment) -> usize {
-        let table = self.get_or_create_table_for_ucanonical_goal(goal.clone());
+    pub fn num_cached_answers_for_goal(
+        &mut self,
+        context: &impl ContextOps<C>,
+        goal: &C::UCanonicalGoalInEnvironment,
+    ) -> usize {
+        let table = self.get_or_create_table_for_ucanonical_goal(context, goal.clone());
         self.tables[table].num_cached_answers()
     }
 }
 
-struct ForestSolver<'forest, C: Context + 'forest, CO: ContextOps<C> + 'forest> {
-    forest: &'forest mut Forest<C, CO>,
+struct ForestSolver<'me, C: Context + 'me, CO: ContextOps<C> + 'me> {
+    forest: &'me mut Forest<C>,
+    context: &'me CO,
     table: TableIndex,
     answer: AnswerIndex,
 }
 
-impl<'forest, C, CO: ContextOps<C>> AnswerStream<C> for ForestSolver<'forest, C, CO>
+impl<'me, C, CO> AnswerStream<C> for ForestSolver<'me, C, CO>
 where
     C: Context,
+    CO: ContextOps<C>,
 {
     fn peek_answer(&mut self) -> Option<SimplifiedAnswer<C>> {
         loop {
-            match self.forest.ensure_root_answer(self.table, self.answer) {
+            match self
+                .forest
+                .ensure_root_answer(self.context, self.table, self.answer)
+            {
                 Ok(()) => {
                     let answer = self.forest.answer(self.table, self.answer);