Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions chalk-engine/src/context.rs
Original file line number Diff line number Diff line change
Expand Up @@ -154,9 +154,6 @@ pub trait Context: Clone + Debug {

fn goal_from_goal_in_environment(goal: &Self::GoalInEnvironment) -> &Self::Goal;

// Used by: simplify
fn add_clauses(env: &Self::Environment, clauses: Self::ProgramClauses) -> Self::Environment;

/// Selects the next appropriate subgoal index for evaluation.
/// Used by: logic
fn next_subgoal_index(ex_clause: &ExClause<Self>) -> usize;
Expand All @@ -180,6 +177,9 @@ pub trait ContextOps<C: Context>: Sized + Clone + Debug + AggregateOps<C> {
infer: &mut C::InferenceTable,
) -> Result<Vec<C::ProgramClause>, Floundered>;

// Used by: simplify
fn add_clauses(&self, env: &C::Environment, clauses: C::ProgramClauses) -> C::Environment;

/// Create an inference table for processing a new goal and instantiate that goal
/// in that context, returning "all the pieces".
///
Expand Down
2 changes: 1 addition & 1 deletion chalk-engine/src/simplify.rs
Original file line number Diff line number Diff line change
Expand Up @@ -41,7 +41,7 @@ impl<C: Context> Forest<C> {
pending_goals.push((environment, context.into_hh_goal(subgoal)))
}
HhGoal::Implies(wc, subgoal) => {
let new_environment = C::add_clauses(&environment, wc);
let new_environment = context.add_clauses(&environment, wc);
pending_goals.push((new_environment, context.into_hh_goal(subgoal)));
}
HhGoal::All(subgoals) => {
Expand Down
9 changes: 5 additions & 4 deletions chalk-integration/src/lowering.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1198,7 +1198,7 @@ impl LowerClause for Clause {
.into_iter()
.map(
|implication: chalk_ir::Binders<chalk_ir::ProgramClauseImplication<ChalkIr>>| {
chalk_ir::ProgramClause::ForAll(implication)
chalk_ir::ProgramClauseData::ForAll(implication).intern(interner)
},
)
.collect();
Expand Down Expand Up @@ -1303,11 +1303,12 @@ impl<'k> LowerGoal<Env<'k>> for Goal {
// `T: Trait<Assoc = U>` to `FromEnv(T: Trait)` and `FromEnv(T: Trait<Assoc = U>)`
// in the assumptions of an `if` goal, e.g. `if (T: Trait) { ... }` lowers to
// `if (FromEnv(T: Trait)) { ... /* this part is untouched */ ... }`.
let where_clauses: LowerResult<Vec<_>> = hyp
let where_clauses = hyp
.into_iter()
.flat_map(|h| h.lower_clause(env).apply_result())
.map(|result| result.map(|h| h.into_from_env_clause(interner)))
.collect();
.map(|result| result.map(|h| h.into_from_env_clause(interner)));
let where_clauses =
chalk_ir::ProgramClauses::from_fallible(interner, where_clauses);
Ok(chalk_ir::GoalData::Implies(where_clauses?, g.lower(env)?).intern(interner))
}
Goal::And(g1, g2s) => {
Expand Down
22 changes: 20 additions & 2 deletions chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,8 @@ use chalk_ir::interner::ChalkIr;
use chalk_ir::tls;
use chalk_ir::{
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, ImplId, Lifetime,
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
TyData, TypeName,
Parameter, ProgramClause, ProgramClauseImplication, ProgramClauses, StructId, Substitution,
TraitId, Ty, TyData, TypeName,
};
use chalk_rust_ir::{
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
Expand Down Expand Up @@ -173,6 +173,24 @@ impl tls::DebugContext for Program {
write!(fmt, "{:?}", pci.debug(interner))
}

fn debug_program_clause(
&self,
clause: &ProgramClause<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error> {
let interner = self.interner();
write!(fmt, "{:?}", clause.data(interner))
}

fn debug_program_clauses(
&self,
clauses: &ProgramClauses<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error> {
let interner = self.interner();
write!(fmt, "{:?}", clauses.as_slice(interner))
}

fn debug_application_ty(
&self,
application_ty: &ApplicationTy<ChalkIr>,
Expand Down
14 changes: 8 additions & 6 deletions chalk-ir/src/cast.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,10 +183,11 @@ where
I: Interner,
{
fn cast_to(self, interner: &I) -> ProgramClause<I> {
ProgramClause::Implies(ProgramClauseImplication {
ProgramClauseData::Implies(ProgramClauseImplication {
consequence: self.cast(interner),
conditions: Goals::new(interner),
})
.intern(interner)
}
}

Expand All @@ -196,22 +197,23 @@ where
I: Interner,
{
fn cast_to(self, interner: &I) -> ProgramClause<I> {
ProgramClause::ForAll(self.map(|bound| ProgramClauseImplication {
ProgramClauseData::ForAll(self.map(|bound| ProgramClauseImplication {
consequence: bound.cast(interner),
conditions: Goals::new(interner),
}))
.intern(interner)
}
}

impl<I: Interner> CastTo<ProgramClause<I>> for ProgramClauseImplication<I> {
fn cast_to(self, _interner: &I) -> ProgramClause<I> {
ProgramClause::Implies(self)
fn cast_to(self, interner: &I) -> ProgramClause<I> {
ProgramClauseData::Implies(self).intern(interner)
}
}

impl<I: Interner> CastTo<ProgramClause<I>> for Binders<ProgramClauseImplication<I>> {
fn cast_to(self, _interner: &I) -> ProgramClause<I> {
ProgramClause::ForAll(self)
fn cast_to(self, interner: &I) -> ProgramClause<I> {
ProgramClauseData::ForAll(self).intern(interner)
}
}

Expand Down
14 changes: 11 additions & 3 deletions chalk-ir/src/could_match.rs
Original file line number Diff line number Diff line change
Expand Up @@ -62,14 +62,22 @@ where
}
}

impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClauseData<I> {
fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
match self {
ProgramClause::Implies(implication) => {
ProgramClauseData::Implies(implication) => {
implication.consequence.could_match(interner, other)
}

ProgramClause::ForAll(clause) => clause.value.consequence.could_match(interner, other),
ProgramClauseData::ForAll(clause) => {
clause.value.consequence.could_match(interner, other)
}
}
}
}

impl<I: Interner> CouldMatch<DomainGoal<I>> for ProgramClause<I> {
fn could_match(&self, interner: &I, other: &DomainGoal<I>) -> bool {
self.data(interner).could_match(interner, other)
}
}
18 changes: 15 additions & 3 deletions chalk-ir/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,18 @@ impl<I: Interner> Debug for ProgramClauseImplication<I> {
}
}

impl<I: Interner> Debug for ProgramClause<I> {
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
I::debug_program_clause(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
}
}

impl<I: Interner> Debug for ProgramClauses<I> {
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
I::debug_program_clauses(self, fmt).unwrap_or_else(|| write!(fmt, "{:?}", self.interned))
}
}

impl<I: Interner> Debug for ApplicationTy<I> {
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
I::debug_application_ty(self, fmt).unwrap_or_else(|| write!(fmt, "ApplicationTy(?)"))
Expand Down Expand Up @@ -520,11 +532,11 @@ impl<T: Debug> Debug for Binders<T> {
}
}

impl<I: Interner> Debug for ProgramClause<I> {
impl<I: Interner> Debug for ProgramClauseData<I> {
fn fmt(&self, fmt: &mut Formatter<'_>) -> Result<(), Error> {
match self {
ProgramClause::Implies(pc) => write!(fmt, "{:?}", pc),
ProgramClause::ForAll(pc) => write!(fmt, "{:?}", pc),
ProgramClauseData::Implies(pc) => write!(fmt, "{:?}", pc),
ProgramClauseData::ForAll(pc) => write!(fmt, "{:?}", pc),
}
}
}
Expand Down
51 changes: 44 additions & 7 deletions chalk-ir/src/fold/boring_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -172,6 +172,26 @@ impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for Goals<I> {
}
}

impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for ProgramClauses<I> {
type Result = ProgramClauses<TI>;
fn fold_with<'i>(
&self,
folder: &mut dyn Folder<'i, I, TI>,
outer_binder: DebruijnIndex,
) -> Fallible<Self::Result>
where
I: 'i,
TI: 'i,
{
let interner = folder.interner();
let target_interner = folder.target_interner();
let folded = self
.iter(interner)
.map(|p| p.fold_with(folder, outer_binder));
Ok(ProgramClauses::from_fallible(target_interner, folded)?)
}
}

#[macro_export]
macro_rules! copy_fold {
($t:ty) => {
Expand Down Expand Up @@ -228,7 +248,7 @@ id_fold!(StructId);
id_fold!(TraitId);
id_fold!(AssocTypeId);

impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClauseData<I> {
fn super_fold_with<'i>(
&self,
folder: &mut dyn Folder<'i, I, TI>,
Expand All @@ -239,16 +259,33 @@ impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
TI: 'i,
{
match self {
ProgramClause::Implies(pci) => {
Ok(ProgramClause::Implies(pci.fold_with(folder, outer_binder)?))
}
ProgramClause::ForAll(pci) => {
Ok(ProgramClause::ForAll(pci.fold_with(folder, outer_binder)?))
}
ProgramClauseData::Implies(pci) => Ok(ProgramClauseData::Implies(
pci.fold_with(folder, outer_binder)?,
)),
ProgramClauseData::ForAll(pci) => Ok(ProgramClauseData::ForAll(
pci.fold_with(folder, outer_binder)?,
)),
}
}
}

impl<I: Interner, TI: TargetInterner<I>> SuperFold<I, TI> for ProgramClause<I> {
fn super_fold_with<'i>(
&self,
folder: &mut dyn Folder<'i, I, TI>,
outer_binder: DebruijnIndex,
) -> ::chalk_engine::fallible::Fallible<Self::Result>
where
I: 'i,
TI: 'i,
{
let clause = self.data(folder.interner());
Ok(clause
.super_fold_with(folder, outer_binder)?
.intern(folder.target_interner()))
}
}

impl<I: Interner, TI: TargetInterner<I>> Fold<I, TI> for PhantomData<I> {
type Result = PhantomData<TI>;

Expand Down
Loading