finish intern-goals-data

Author: yaahc

chalk-integration/src/program.rs

@@ -4,8 +4,8 @@ use chalk_ir::debug::Angle;
 use chalk_ir::interner::ChalkIr;
 use chalk_ir::tls;
 use chalk_ir::{
-    AliasTy, AssocTypeId, Goal, GoalData, ImplId, Lifetime, Parameter, ParameterKind,
-    ProgramClause, StructId, TraitId, Ty, TyData, TypeName,
+    AliasTy, AssocTypeId, Goal, GoalData, Goals, ImplId, Lifetime, Parameter, ParameterKind,
+    ProgramClause, ProgramClauseImplication, StructId, TraitId, Ty, TyData, TypeName,
 };
 use chalk_rust_ir::{
     AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
@@ -176,6 +176,45 @@ impl tls::DebugContext for Program {
             GoalData::CannotProve(()) => write!(fmt, r"¯\_(ツ)_/¯"),
         }
     }
+
+    fn debug_goals(
+        &self,
+        goals: &Goals<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "(")?;
+        for (goal, index) in goals.iter(interner).zip(0..) {
+            if index > 0 {
+                write!(fmt, ", ")?;
+            }
+            write!(fmt, "{:?}", goal)?;
+        }
+        write!(fmt, ")")?;
+        Ok(())
+    }
+
+    fn debug_program_clause_implication(
+        &self,
+        pci: &ProgramClauseImplication<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error> {
+        let interner = self.interner();
+        write!(fmt, "{:?}", pci.consequence)?;
+
+        let conditions = pci.conditions.as_slice(interner);
+
+        let conds = conditions.len();
+        if conds == 0 {
+            return Ok(());
+        }
+
+        write!(fmt, " :- ")?;
+        for cond in &conditions[..conds - 1] {
+            write!(fmt, "{:?}, ", cond)?;
+        }
+        write!(fmt, "{:?}", conditions[conds - 1])
+    }
 }
 
 impl RustIrDatabase<ChalkIr> for Program {

chalk-ir/src/debug.rs

@@ -45,6 +45,18 @@ impl<I: Interner> Debug for Goal<I> {
     }
 }
 
+impl<I: Interner> Debug for Goals<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_goals(self, fmt).unwrap_or_else(|| unimplemented!())
+    }
+}
+
+impl<I: Interner> Debug for ProgramClauseImplication<I> {
+    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
+        I::debug_program_clause_implication(self, fmt).unwrap_or_else(|| unimplemented!())
+    }
+}
+
 impl Display for UniverseIndex {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         write!(fmt, "U{}", self.counter)
@@ -269,20 +281,6 @@ impl<I: Interner> Debug for EqGoal<I> {
     }
 }
 
-impl<I: Interner> Debug for Goals<I> {
-    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        write!(fmt, "(")?;
-        for (goal, index) in self.iter().zip(0..) {
-            if index > 0 {
-                write!(fmt, ", ")?;
-            }
-            write!(fmt, "{:?}", goal)?;
-        }
-        write!(fmt, ")")?;
-        Ok(())
-    }
-}
-
 impl<T: Debug> Debug for Binders<T> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         let Binders {
@@ -315,25 +313,6 @@ impl<I: Interner> Debug for ProgramClause<I> {
     }
 }
 
-impl<I: Interner> Debug for ProgramClauseImplication<I> {
-    fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
-        write!(fmt, "{:?}", self.consequence)?;
-
-        let conditions = self.conditions.as_slice();
-
-        let conds = conditions.len();
-        if conds == 0 {
-            return Ok(());
-        }
-
-        write!(fmt, " :- ")?;
-        for cond in &conditions[..conds - 1] {
-            write!(fmt, "{:?}, ", cond)?;
-        }
-        write!(fmt, "{:?}", conditions[conds - 1])
-    }
-}
-
 impl<I: Interner> Debug for Environment<I> {
     fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
         write!(fmt, "Env({:?})", self.clauses)

chalk-ir/src/fold/boring_impls.rs

@@ -158,9 +158,10 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
         I: 'i,
         TI: 'i,
     {
-        let interner = folder.target_interner();
-        let folded = self.iter().map(|p| p.fold_with(folder, binders));
-        Ok(Goals::from_fallible(interner, folded)?)
+        let interner = folder.interner();
+        let target_interner = folder.target_interner();
+        let folded = self.iter(interner).map(|p| p.fold_with(folder, binders));
+        Ok(Goals::from_fallible(target_interner, folded)?)
     }
 }
 

chalk-ir/src/interner.rs

@@ -2,10 +2,12 @@ use crate::AliasTy;
 use crate::AssocTypeId;
 use crate::Goal;
 use crate::GoalData;
+use crate::Goals;
 use crate::Lifetime;
 use crate::LifetimeData;
 use crate::Parameter;
 use crate::ParameterData;
+use crate::ProgramClauseImplication;
 use crate::StructId;
 use crate::TraitId;
 use crate::Ty;
@@ -176,6 +178,27 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     /// if no info about current program is available from TLS).
     fn debug_goal(goal: &Goal<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result>;
 
+    /// Prints the debug representation of a list of goals. To get good
+    /// results, this requires inspecting TLS, and is difficult to
+    /// code without reference to a specific interner (and hence
+    /// fully known types).
+    ///
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    fn debug_goals(goals: &Goals<Self>, fmt: &mut fmt::Formatter<'_>) -> Option<fmt::Result>;
+
+    /// Prints the debug representation of a ProgramClauseImplication. To get good
+    /// results, this requires inspecting TLS, and is difficult to
+    /// code without reference to a specific interner (and hence
+    /// fully known types).
+    ///
+    /// Returns `None` to fallback to the default debug output (e.g.,
+    /// if no info about current program is available from TLS).
+    fn debug_program_clause_implication(
+        pci: &ProgramClauseImplication<Self>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Option<fmt::Result>;
+
     /// Create an "interned" type from `ty`. This is not normally
     /// invoked directly; instead, you invoke `TyData::intern` (which
     /// will ultimately call this method).
@@ -218,7 +241,7 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
     fn intern_goals(&self, data: impl IntoIterator<Item = Goal<Self>>) -> Self::InternedGoals;
 
     /// Lookup the `GoalsData` that was interned to create a `InternedGoals`.
-    fn goals_data(goals: &Self::InternedGoals) -> &[Goal<Self>];
+    fn goals_data<'a>(&self, goals: &'a Self::InternedGoals) -> &'a [Goal<Self>];
 
     /// Create an "interned" substitution from `data`. This is not
     /// normally invoked directly; instead, you invoke
@@ -339,6 +362,20 @@ mod default {
             tls::with_current_program(|prog| Some(prog?.debug_goal(goal, fmt)))
         }
 
+        fn debug_goals(
+            goals: &Goals<ChalkIr>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| Some(prog?.debug_goals(goals, fmt)))
+        }
+
+        fn debug_program_clause_implication(
+            pci: &ProgramClauseImplication<ChalkIr>,
+            fmt: &mut fmt::Formatter<'_>,
+        ) -> Option<fmt::Result> {
+            tls::with_current_program(|prog| Some(prog?.debug_program_clause_implication(pci, fmt)))
+        }
+
         fn intern_ty(&self, ty: TyData<ChalkIr>) -> Arc<TyData<ChalkIr>> {
             Arc::new(ty)
         }
@@ -384,7 +421,7 @@ mod default {
             data.into_iter().collect()
         }
 
-        fn goals_data(goals: &Vec<Goal<ChalkIr>>) -> &[Goal<ChalkIr>] {
+        fn goals_data<'a>(&self, goals: &'a Vec<Goal<ChalkIr>>) -> &'a [Goal<ChalkIr>] {
             goals
         }
 

chalk-ir/src/lib.rs

@@ -968,7 +968,7 @@ impl<I: Interner> ProgramClause<I> {
     pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
         match self {
             ProgramClause::Implies(implication) => {
-                if implication.conditions.is_empty() {
+                if implication.conditions.is_empty(interner) {
                     ProgramClause::Implies(ProgramClauseImplication {
                         consequence: implication.consequence.into_from_env_goal(interner),
                         conditions: Goals::new(interner),
@@ -1054,20 +1054,20 @@ impl<I: Interner> Goals<I> {
         Ok(Goals::from(interner, goals))
     }
 
-    pub fn iter(&self) -> std::slice::Iter<'_, Goal<I>> {
-        self.as_slice().iter()
+    pub fn iter(&self, interner: &I) -> std::slice::Iter<'_, Goal<I>> {
+        self.as_slice(interner).iter()
     }
 
-    pub fn is_empty(&self) -> bool {
-        self.as_slice().is_empty()
+    pub fn is_empty(&self, interner: &I) -> bool {
+        self.as_slice(interner).is_empty()
     }
 
-    pub fn len(&self) -> usize {
-        self.as_slice().len()
+    pub fn len(&self, interner: &I) -> usize {
+        self.as_slice(interner).len()
     }
 
-    pub fn as_slice(&self) -> &[Goal<I>] {
-        I::goals_data(&self.goals)
+    pub fn as_slice(&self, interner: &I) -> &[Goal<I>] {
+        interner.goals_data(&self.goals)
     }
 }
 
@@ -1140,7 +1140,7 @@ impl<I: Interner> Goal<I> {
     /// required to prove it.
     pub fn is_trivially_true(&self, interner: &I) -> bool {
         match self.data(interner) {
-            GoalData::All(goals) => goals.is_empty(),
+            GoalData::All(goals) => goals.is_empty(interner),
             _ => false,
         }
     }

chalk-ir/src/tls.rs

@@ -1,5 +1,8 @@
 use crate::interner::ChalkIr;
-use crate::{AliasTy, AssocTypeId, Goal, Lifetime, Parameter, StructId, TraitId, Ty};
+use crate::{
+    AliasTy, AssocTypeId, Goal, Goals, Lifetime, Parameter, ProgramClauseImplication, StructId,
+    TraitId, Ty,
+};
 use std::cell::RefCell;
 use std::fmt;
 use std::sync::Arc;
@@ -52,6 +55,18 @@ pub trait DebugContext {
         goal: &Goal<ChalkIr>,
         fmt: &mut fmt::Formatter<'_>,
     ) -> Result<(), fmt::Error>;
+
+    fn debug_goals(
+        &self,
+        goals: &Goals<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
+
+    fn debug_program_clause_implication(
+        &self,
+        pci: &ProgramClauseImplication<ChalkIr>,
+        fmt: &mut fmt::Formatter<'_>,
+    ) -> Result<(), fmt::Error>;
 }
 
 pub fn with_current_program<R>(op: impl FnOnce(Option<&Arc<dyn DebugContext>>) -> R) -> R {

chalk-ir/src/zip.rs

@@ -261,7 +261,8 @@ impl<I: Interner> Zip<I> for Goals<I> {
     where
         I: 'i,
     {
-        Zip::zip_with(zipper, a.as_slice(), b.as_slice())?;
+        let interner = zipper.interner();
+        Zip::zip_with(zipper, a.as_slice(interner), b.as_slice(interner))?;
         Ok(())
     }
 }

chalk-solve/src/solve/slg.rs

@@ -331,7 +331,7 @@ impl<'me, I: Interner> context::ContextOps<SlgContext<I>> for SlgContextOps<'me,
                 HhGoal::Exists(binders_goal)
             }
             GoalData::Implies(dg, subgoal) => HhGoal::Implies(dg, subgoal),
-            GoalData::All(goals) => HhGoal::All(goals.iter().cloned().collect()),
+            GoalData::All(goals) => HhGoal::All(goals.iter(interner).cloned().collect()),
             GoalData::Not(g1) => HhGoal::Not(g1),
             GoalData::EqGoal(EqGoal { a, b }) => HhGoal::Unify((), a, b),
             GoalData::DomainGoal(domain_goal) => HhGoal::DomainGoal(domain_goal),

chalk-solve/src/solve/slg/resolvent.rs

@@ -114,7 +114,7 @@ impl<I: Interner> context::ResolventOps<SlgContext<I>> for TruncatingInferenceTa
         // Add the `conditions` from the program clause into the result too.
         ex_clause
             .subgoals
-            .extend(conditions.iter().map(|c| match c.data(interner) {
+            .extend(conditions.iter(interner).map(|c| match c.data(interner) {
                 GoalData::Not(c1) => {
                     Literal::Negative(InEnvironment::new(environment, Goal::clone(c1)))
                 }