Skip to content

Commit 4b95a89

Browse files
borsbors
committed
Auto merge of #738 - nrc:well-known, r=nrc
Make DispatchFromDyn a well-known type The first commit is some minor refactoring. The second commit does the 'obvious' work of making DispatchFromDyn well-known. In order to properly enforce the wf-ness constraints on DispatchFromDyn, Chalk needs to know about one-zst types, that is in the next commit. The final commit finishes the DispatchFromDyn work by enforcing the WF-ness constraints and adding tests. r? `@jackh726`
2 parents 82cf22a + e92db1d commit 4b95a89

File tree

16 files changed

+414
-11
lines changed

16 files changed

+414
-11
lines changed

‎chalk-integration/src/db.rs

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,9 +13,9 @@ use chalk_ir::{
1313
UnificationDatabase, Variances,
1414
};
1515
use chalk_solve::rust_ir::{
16-
AdtDatum, AdtRepr, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind,
17-
FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum,
18-
OpaqueTyDatum, TraitDatum, WellKnownTrait,
16+
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
17+
ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
18+
ImplDatum, OpaqueTyDatum, TraitDatum, WellKnownTrait,
1919
};
2020
use chalk_solve::{RustIrDatabase, Solution, SubstitutionResult};
2121
use salsa::Database;
@@ -133,6 +133,10 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
133133
self.program_ir().unwrap().adt_repr(id)
134134
}
135135

136+
fn adt_size_align(&self, id: AdtId<ChalkIr>) -> Arc<AdtSizeAlign> {
137+
self.program_ir().unwrap().adt_size_align(id)
138+
}
139+
136140
fn fn_def_datum(&self, id: FnDefId<ChalkIr>) -> Arc<FnDefDatum<ChalkIr>> {
137141
self.program_ir().unwrap().fn_def_datum(id)
138142
}

‎chalk-integration/src/lowering.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,10 @@ impl LowerWithEnv for (&AdtDefn, chalk_ir::AdtId<ChalkIr>) {
325325
}
326326
}
327327

328+
pub fn lower_adt_size_align(flags: &AdtFlags) -> rust_ir::AdtSizeAlign {
329+
rust_ir::AdtSizeAlign::from_one_zst(flags.one_zst)
330+
}
331+
328332
impl LowerWithEnv for AdtRepr {
329333
type Lowered = rust_ir::AdtRepr<ChalkIr>;
330334

@@ -1138,6 +1142,7 @@ impl Lower for WellKnownTrait {
11381142
WellKnownTrait::CoerceUnsized => rust_ir::WellKnownTrait::CoerceUnsized,
11391143
WellKnownTrait::DiscriminantKind => rust_ir::WellKnownTrait::DiscriminantKind,
11401144
WellKnownTrait::Generator => rust_ir::WellKnownTrait::Generator,
1145+
WellKnownTrait::DispatchFromDyn => rust_ir::WellKnownTrait::DispatchFromDyn,
11411146
}
11421147
}
11431148
}

‎chalk-integration/src/lowering/program_lowerer.rs

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ use std::collections::{BTreeMap, HashSet};
1313
use std::sync::Arc;
1414
use string_cache::DefaultAtom as Atom;
1515

16-
use super::{env::*, Lower, LowerParameterMap, LowerWithEnv, FIXME_SELF};
16+
use super::{env::*, lower_adt_size_align, Lower, LowerParameterMap, LowerWithEnv, FIXME_SELF};
1717
use crate::error::RustIrError;
1818
use crate::program::Program as LoweredProgram;
1919
use crate::RawId;
@@ -143,6 +143,7 @@ impl ProgramLowerer {
143143
pub fn lower(self, program: &Program, raw_ids: &[RawId]) -> LowerResult<LoweredProgram> {
144144
let mut adt_data = BTreeMap::new();
145145
let mut adt_reprs = BTreeMap::new();
146+
let mut adt_size_aligns = BTreeMap::new();
146147
let mut adt_variances = BTreeMap::new();
147148
let mut fn_def_data = BTreeMap::new();
148149
let mut fn_def_variances = BTreeMap::new();
@@ -186,6 +187,7 @@ impl ProgramLowerer {
186187
let adt_id = AdtId(raw_id);
187188
adt_data.insert(adt_id, Arc::new((d, adt_id).lower(&empty_env)?));
188189
adt_reprs.insert(adt_id, Arc::new(d.repr.lower(&empty_env)?));
190+
adt_size_aligns.insert(adt_id, Arc::new(lower_adt_size_align(&d.flags)));
189191
let n_params = d.all_parameters().len();
190192
let variances = match d.variances.clone() {
191193
Some(v) => {
@@ -480,6 +482,7 @@ impl ProgramLowerer {
480482
trait_kinds: self.trait_kinds,
481483
adt_data,
482484
adt_reprs,
485+
adt_size_aligns,
483486
adt_variances,
484487
fn_def_data,
485488
fn_def_variances,

‎chalk-integration/src/program.rs

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,9 @@ use chalk_ir::{
99
Substitution, TraitId, Ty, TyKind, UintTy, Variances,
1010
};
1111
use chalk_solve::rust_ir::{
12-
AdtDatum, AdtRepr, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ClosureKind,
13-
FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum, ImplDatum,
14-
ImplType, OpaqueTyDatum, TraitDatum, WellKnownTrait,
12+
AdtDatum, AdtRepr, AdtSizeAlign, AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId,
13+
ClosureKind, FnDefDatum, FnDefInputsAndOutputDatum, GeneratorDatum, GeneratorWitnessDatum,
14+
ImplDatum, ImplType, OpaqueTyDatum, TraitDatum, WellKnownTrait,
1515
};
1616
use chalk_solve::split::Split;
1717
use chalk_solve::RustIrDatabase;
@@ -61,6 +61,8 @@ pub struct Program {
6161

6262
pub adt_reprs: BTreeMap<AdtId<ChalkIr>, Arc<AdtRepr<ChalkIr>>>,
6363

64+
pub adt_size_aligns: BTreeMap<AdtId<ChalkIr>, Arc<AdtSizeAlign>>,
65+
6466
pub fn_def_data: BTreeMap<FnDefId<ChalkIr>, Arc<FnDefDatum<ChalkIr>>>,
6567

6668
pub closure_inputs_and_output:
@@ -430,6 +432,10 @@ impl RustIrDatabase<ChalkIr> for Program {
430432
self.adt_reprs[&id].clone()
431433
}
432434

435+
fn adt_size_align(&self, id: AdtId<ChalkIr>) -> Arc<AdtSizeAlign> {
436+
self.adt_size_aligns[&id].clone()
437+
}
438+
433439
fn fn_def_datum(&self, id: FnDefId<ChalkIr>) -> Arc<FnDefDatum<ChalkIr>> {
434440
self.fn_def_data[&id].clone()
435441
}

‎chalk-parse/src/ast.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ pub struct AdtFlags {
7474
pub upstream: bool,
7575
pub fundamental: bool,
7676
pub phantom_data: bool,
77+
pub one_zst: bool,
7778
pub kind: AdtKind,
7879
}
7980

@@ -159,6 +160,7 @@ pub enum WellKnownTrait {
159160
CoerceUnsized,
160161
DiscriminantKind,
161162
Generator,
163+
DispatchFromDyn,
162164
}
163165

164166
#[derive(Clone, PartialEq, Eq, Debug)]

‎chalk-parse/src/parser.lalrpop

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,7 @@ NonEnumerableKeyword: () = "#" "[" "non_enumerable" "]";
5353
CoinductiveKeyword: () = "#" "[" "coinductive" "]";
5454
ObjectSafeKeyword: () = "#" "[" "object_safe" "]";
5555
PhantomDataKeyword: () = "#" "[" "phantom_data" "]";
56+
OneZstKeyword: () = "#" "[" "one_zst" "]";
5657

5758
WellKnownTrait: WellKnownTrait = {
5859
"#" "[" "lang" "(" "sized" ")" "]" => WellKnownTrait::Sized,
@@ -67,6 +68,7 @@ WellKnownTrait: WellKnownTrait = {
6768
"#" "[" "lang" "(" "coerce_unsized" ")" "]" => WellKnownTrait::CoerceUnsized,
6869
"#" "[" "lang" "(" "discriminant_kind" ")" "]" => WellKnownTrait::DiscriminantKind,
6970
"#" "[" "lang" "(" "generator" ")" "]" => WellKnownTrait::Generator,
71+
"#" "[" "lang" "(" "dispatch_from_dyn" ")" "]" => WellKnownTrait::DispatchFromDyn,
7072
};
7173

7274
AdtReprAttr: AdtReprAttr = {
@@ -90,7 +92,7 @@ ReprIntTy: Ty = {
9092
}
9193

9294
AdtDefn: AdtDefn = {
93-
<variances:Variances?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <phantom_data:PhantomDataKeyword?> <repr:AdtReprAttr*>
95+
<variances:Variances?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <phantom_data:PhantomDataKeyword?> <one_zst:OneZstKeyword?> <repr:AdtReprAttr*>
9496
"enum" <n:Id><p:Angle<VariableKind>>
9597
<w:QuantifiedWhereClauses> "{" <v:Variants> "}" => AdtDefn
9698
{
@@ -102,6 +104,7 @@ AdtDefn: AdtDefn = {
102104
upstream: upstream.is_some(),
103105
fundamental: fundamental.is_some(),
104106
phantom_data: phantom_data.is_some(),
107+
one_zst: one_zst.is_some(),
105108
kind: AdtKind::Enum,
106109
},
107110
repr: AdtRepr {
@@ -115,7 +118,7 @@ AdtDefn: AdtDefn = {
115118
},
116119
variances,
117120
},
118-
<variances:Variances?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <phantom_data:PhantomDataKeyword?> <repr:AdtReprAttr*>
121+
<variances:Variances?> <upstream:UpstreamKeyword?> <fundamental:FundamentalKeyword?> <phantom_data:PhantomDataKeyword?> <one_zst:OneZstKeyword?> <repr:AdtReprAttr*>
119122
"struct" <n:Id><p:Angle<VariableKind>>
120123
<w:QuantifiedWhereClauses> "{" <f:Fields> "}" => AdtDefn
121124
{
@@ -134,6 +137,7 @@ AdtDefn: AdtDefn = {
134137
upstream: upstream.is_some(),
135138
fundamental: fundamental.is_some(),
136139
phantom_data: phantom_data.is_some(),
140+
one_zst: one_zst.is_some(),
137141
kind: AdtKind::Struct,
138142
},
139143
repr: AdtRepr {

‎chalk-solve/src/clauses/builtin_traits.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ pub fn add_builtin_program_clauses<I: Interner>(
2828
let ty = self_ty.kind(db.interner()).clone();
2929

3030
match well_known {
31-
// There are no builtin impls provided for the following traits:
32-
WellKnownTrait::Unpin | WellKnownTrait::Drop | WellKnownTrait::CoerceUnsized => (),
3331
// Built-in traits are non-enumerable.
3432
_ if self_ty.is_general_var(db.interner(), binders) => return Err(Floundered),
3533
WellKnownTrait::Sized => {
@@ -52,6 +50,11 @@ pub fn add_builtin_program_clauses<I: Interner>(
5250
WellKnownTrait::Generator => {
5351
generator::add_generator_program_clauses(db, builder, self_ty)?;
5452
}
53+
// There are no builtin impls provided for the following traits:
54+
WellKnownTrait::Unpin
55+
| WellKnownTrait::Drop
56+
| WellKnownTrait::CoerceUnsized
57+
| WellKnownTrait::DispatchFromDyn => (),
5558
}
5659
Ok(())
5760
})

‎chalk-solve/src/display/items.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,7 @@ impl<I: Interner> RenderAsRust<I> for TraitDatum<I> {
204204
WellKnownTrait::CoerceUnsized => "coerce_unsized",
205205
WellKnownTrait::DiscriminantKind => "discriminant_kind",
206206
WellKnownTrait::Generator => "generator",
207+
WellKnownTrait::DispatchFromDyn => "dispatch_from_dyn",
207208
};
208209
writeln!(f, "#[lang({})]", name)?;
209210
}

‎chalk-solve/src/display/stub.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -90,6 +90,10 @@ impl<I: Interner, DB: RustIrDatabase<I>> RustIrDatabase<I> for StubWrapper<'_, D
9090
self.db.adt_repr(id)
9191
}
9292

93+
fn adt_size_align(&self, id: chalk_ir::AdtId<I>) -> Arc<crate::rust_ir::AdtSizeAlign> {
94+
self.db.adt_size_align(id)
95+
}
96+
9397
fn fn_def_datum(
9498
&self,
9599
fn_def_id: chalk_ir::FnDefId<I>,

‎chalk-solve/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
6767
/// Returns the representation for the ADT definition with the given id.
6868
fn adt_repr(&self, id: AdtId<I>) -> Arc<AdtRepr<I>>;
6969

70+
/// Returns the siza and alignment of the ADT definition with the given id.
71+
fn adt_size_align(&self, id: AdtId<I>) -> Arc<AdtSizeAlign>;
72+
7073
/// Returns the datum for the fn definition with the given id.
7174
fn fn_def_datum(&self, fn_def_id: FnDefId<I>) -> Arc<FnDefDatum<I>>;
7275

0 commit comments

Comments
 (0)