Skip to content
Merged
Show file tree
Hide file tree
Changes from 1 commit
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
2 changes: 1 addition & 1 deletion 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
9 changes: 9 additions & 0 deletions chalk-integration/src/program.rs
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,15 @@ 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_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
12 changes: 9 additions & 3 deletions chalk-ir/src/could_match.rs
Original file line number Diff line number Diff line change
Expand Up @@ -62,14 +62,20 @@ 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)
}
}
13 changes: 10 additions & 3 deletions chalk-ir/src/debug.rs
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,13 @@ 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.clause))
}
}

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 +527,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
25 changes: 20 additions & 5 deletions chalk-ir/src/fold/boring_impls.rs
Original file line number Diff line number Diff line change
Expand Up @@ -228,7 +228,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 +239,31 @@ 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)?))
ProgramClauseData::Implies(pci) => {
Ok(ProgramClauseData::Implies(pci.fold_with(folder, outer_binder)?))
}
ProgramClause::ForAll(pci) => {
Ok(ProgramClause::ForAll(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
59 changes: 59 additions & 0 deletions chalk-ir/src/interner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,8 @@ use crate::Lifetime;
use crate::LifetimeData;
use crate::Parameter;
use crate::ParameterData;
use crate::ProgramClause;
use crate::ProgramClauseData;
use crate::ProgramClauseImplication;
use crate::SeparatorTraitRef;
use crate::StructId;
Expand Down Expand Up @@ -94,6 +96,14 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
/// converted back to its underlying data via `substitution_data`.
type InternedSubstitution: Debug + Clone + Eq + Hash;

/// "Interned" representation of a "program clause". In normal user code,
/// `Self::InternedProgramClause` is not referenced. Instead, we refer to
/// `ProgramClause<Self>`, which wraps this type.
///
/// An `InternedProgramClause` is created by `intern_program_clause` and can be
/// converted back to its underlying data via `program_clause_data`.
type InternedProgramClause: Debug + Clone + Eq + Hash;

/// The core "id" type used for struct-ids and the like.
type DefId: Debug + Copy + Eq + Ord + Hash;

Expand Down Expand Up @@ -234,6 +244,21 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
None
}

/// Prints the debug representation of a ProgramClause. 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).
#[allow(unused_variables)]
fn debug_program_clause(
clause: &ProgramClause<Self>,
fmt: &mut fmt::Formatter<'_>,
) -> Option<fmt::Result> {
None
}

/// Prints the debug representation of an ApplicationTy. To get good
/// results, this requires inspecting TLS, and is difficult to
/// code without reference to a specific interner (and hence
Expand Down Expand Up @@ -337,6 +362,18 @@ pub trait Interner: Debug + Copy + Eq + Ord + Hash {
&self,
substitution: &'a Self::InternedSubstitution,
) -> &'a [Parameter<Self>];

/// Create an "interned" program clause from `data`. This is not
/// normally invoked directly; instead, you invoke
/// `ProgramClauseData::intern` (which will ultimately call this
/// method).
fn intern_program_clause(&self, data: ProgramClauseData<Self>) -> Self::InternedProgramClause;

/// Lookup the `ProgramClauseData` that was interned to create a `ProgramClause`.
fn program_clause_data<'a>(
&self,
clause: &'a Self::InternedProgramClause,
) -> &'a ProgramClauseData<Self>;
}

pub trait TargetInterner<I: Interner>: Interner {
Expand Down Expand Up @@ -391,6 +428,7 @@ mod default {
type InternedGoal = Arc<GoalData<ChalkIr>>;
type InternedGoals = Vec<Goal<ChalkIr>>;
type InternedSubstitution = Vec<Parameter<ChalkIr>>;
type InternedProgramClause = ProgramClauseData<ChalkIr>;
type DefId = RawId;
type Identifier = Identifier;

Expand Down Expand Up @@ -459,6 +497,13 @@ mod default {
tls::with_current_program(|prog| Some(prog?.debug_program_clause_implication(pci, fmt)))
}

fn debug_program_clause(
clause: &ProgramClause<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Option<fmt::Result> {
tls::with_current_program(|prog| Some(prog?.debug_program_clause(clause, fmt)))
}

fn debug_application_ty(
application_ty: &ApplicationTy<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
Expand Down Expand Up @@ -544,6 +589,20 @@ mod default {
) -> &'a [Parameter<ChalkIr>] {
substitution
}

fn intern_program_clause(
&self,
data: ProgramClauseData<Self>,
) -> ProgramClauseData<Self> {
data
}

fn program_clause_data<'a>(
&self,
clause: &'a ProgramClauseData<Self>,
) -> &'a ProgramClauseData<Self> {
clause
}
}

impl HasInterner for ChalkIr {
Expand Down
41 changes: 33 additions & 8 deletions chalk-ir/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1208,8 +1208,8 @@ pub struct ProgramClauseImplication<I: Interner> {
pub conditions: Goals<I>,
}

#[derive(Clone, PartialEq, Eq, Hash, HasInterner)]
pub enum ProgramClause<I: Interner> {
#[derive(Clone, PartialEq, Eq, Hash, Fold, HasInterner)]
pub enum ProgramClauseData<I: Interner> {
Implies(ProgramClauseImplication<I>),
ForAll(Binders<ProgramClauseImplication<I>>),
}
Expand All @@ -1227,17 +1227,42 @@ impl<I: Interner> ProgramClauseImplication<I> {
}
}

impl<I: Interner> ProgramClause<I> {
pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
impl<I: Interner> ProgramClauseData<I> {
pub fn into_from_env_clause(self, interner: &I) -> ProgramClauseData<I> {
match self {
ProgramClause::Implies(implication) => {
ProgramClause::Implies(implication.into_from_env_clause(interner))
ProgramClauseData::Implies(implication) => {
ProgramClauseData::Implies(implication.into_from_env_clause(interner))
}
ProgramClause::ForAll(binders_implication) => {
ProgramClause::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
ProgramClauseData::ForAll(binders_implication) => {
ProgramClauseData::ForAll(binders_implication.map(|i| i.into_from_env_clause(interner)))
}
}
}

pub fn intern(self, interner: &I) -> ProgramClause<I> {
ProgramClause {
clause: interner.intern_program_clause(self),
}
}
}

#[derive(Clone, PartialEq, Eq, Hash, PartialOrd, Ord, HasInterner)]
pub struct ProgramClause<I: Interner> {
clause: I::InternedProgramClause,
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: I think we we call this interned in all the other structs

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We call it interned except in Goal and Goals IIRC. I think those should be renamed and everything should be interned.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looks like @tirr-c fixed the new cases in this PR, we can create an issue for the others

}

impl<I: Interner> ProgramClause<I> {
pub fn into_from_env_clause(self, interner: &I) -> ProgramClause<I> {
let program_clause_data = self.data(interner);
let new_clause = program_clause_data.clone().into_from_env_clause(interner);
ProgramClause {
clause: interner.intern_program_clause(new_clause),
}
}

pub fn data(&self, interner: &I) -> &ProgramClauseData<I> {
interner.program_clause_data(&self.clause)
}
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Also I think we should add an interned(&self) -> &I::InternedProgramClause accessor


/// Wraps a "canonicalized item". Items are canonicalized as follows:
Expand Down
8 changes: 7 additions & 1 deletion chalk-ir/src/tls.rs
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
use crate::interner::ChalkIr;
use crate::{
debug::SeparatorTraitRef, AliasTy, ApplicationTy, AssocTypeId, Goal, Goals, Lifetime,
Parameter, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
Parameter, ProgramClause, ProgramClauseImplication, StructId, Substitution, TraitId, Ty,
};
use std::cell::RefCell;
use std::fmt;
Expand Down Expand Up @@ -68,6 +68,12 @@ pub trait DebugContext {
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error>;

fn debug_program_clause(
&self,
clause: &ProgramClause<ChalkIr>,
fmt: &mut fmt::Formatter<'_>,
) -> Result<(), fmt::Error>;

fn debug_application_ty(
&self,
application_ty: &ApplicationTy<ChalkIr>,
Expand Down
12 changes: 11 additions & 1 deletion chalk-ir/src/zip.rs
Original file line number Diff line number Diff line change
Expand Up @@ -309,7 +309,7 @@ enum_zip!(impl<I> for DomainGoal<I> {
Compatible,
DownstreamType
});
enum_zip!(impl<I> for ProgramClause<I> { Implies, ForAll });
enum_zip!(impl<I> for ProgramClauseData<I> { Implies, ForAll });

impl<I: Interner> Zip<I> for Substitution<I> {
fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
Expand Down Expand Up @@ -396,3 +396,13 @@ impl<I: Interner> Zip<I> for Parameter<I> {
Zip::zip_with(zipper, a.data(interner), b.data(interner))
}
}

impl<I: Interner> Zip<I> for ProgramClause<I> {
fn zip_with<'i, Z: Zipper<'i, I>>(zipper: &mut Z, a: &Self, b: &Self) -> Fallible<()>
where
I: 'i,
{
let interner = zipper.interner();
Zip::zip_with(zipper, a.data(interner), b.data(interner))
}
}
Loading