Skip to content

Commit 03572a3

Browse files
committed
address nits
1 parent 5839841 commit 03572a3

File tree

3 files changed

+52
-40
lines changed

3 files changed

+52
-40
lines changed
+4-40
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
use std::iter;
2-
31
use super::builder::ClauseBuilder;
42
use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
5-
use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
3+
use chalk_ir::TyData;
4+
5+
mod sized;
66

77
/// For well known traits we have special hard-coded impls, either as an
88
/// optimization or to enforce special rules for correctness.
@@ -18,44 +18,8 @@ pub fn add_builtin_program_clauses<I: Interner>(
1818
}
1919

2020
match well_known {
21-
WellKnownTrait::SizedTrait => add_sized_program_clauses(db, builder, trait_ref, ty),
21+
WellKnownTrait::SizedTrait => sized::add_sized_program_clauses(db, builder, trait_ref, ty),
2222
WellKnownTrait::CopyTrait => { /* TODO */ }
2323
WellKnownTrait::CloneTrait => { /* TODO */ }
2424
}
2525
}
26-
27-
fn add_sized_program_clauses<I: Interner>(
28-
db: &dyn RustIrDatabase<I>,
29-
builder: &mut ClauseBuilder<'_, I>,
30-
trait_ref: &TraitRef<I>,
31-
ty: &TyData<I>,
32-
) {
33-
let interner = db.interner();
34-
35-
let (struct_id, substitution) = match ty {
36-
TyData::Apply(ApplicationTy {
37-
name: TypeName::Struct(struct_id),
38-
substitution,
39-
}) => (*struct_id, substitution),
40-
_ => return,
41-
};
42-
43-
let struct_datum = db.struct_datum(struct_id);
44-
45-
if struct_datum.binders.map_ref(|b| b.fields.is_empty()).value {
46-
builder.push_fact(trait_ref.clone());
47-
return;
48-
}
49-
50-
let last_field_ty = struct_datum
51-
.binders
52-
.map_ref(|b| b.fields.last().unwrap())
53-
.substitute(interner, substitution)
54-
.clone();
55-
56-
let last_field_sized_goal = TraitRef {
57-
trait_id: trait_ref.trait_id,
58-
substitution: Substitution::from1(interner, last_field_ty),
59-
};
60-
builder.push_clause(trait_ref.clone(), iter::once(last_field_sized_goal));
61-
}
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
use std::iter;
2+
3+
use crate::clauses::ClauseBuilder;
4+
use crate::{Interner, RustIrDatabase, TraitRef};
5+
use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
6+
7+
pub fn add_sized_program_clauses<I: Interner>(
8+
db: &dyn RustIrDatabase<I>,
9+
builder: &mut ClauseBuilder<'_, I>,
10+
trait_ref: &TraitRef<I>,
11+
ty: &TyData<I>,
12+
) {
13+
let interner = db.interner();
14+
15+
let (struct_id, substitution) = match ty {
16+
TyData::Apply(ApplicationTy {
17+
name: TypeName::Struct(struct_id),
18+
substitution,
19+
}) => (*struct_id, substitution),
20+
_ => return,
21+
};
22+
23+
let struct_datum = db.struct_datum(struct_id);
24+
25+
// Structs with no fields are always Sized
26+
if struct_datum.binders.map_ref(|b| b.fields.is_empty()).value {
27+
builder.push_fact(trait_ref.clone());
28+
return;
29+
}
30+
31+
// To check if a struct type S<..> is Sized, we only have to look at its last field.
32+
// This is because the WF checks for structs require that all the other fields must be Sized.
33+
let last_field_ty = struct_datum
34+
.binders
35+
.map_ref(|b| b.fields.last().unwrap())
36+
.substitute(interner, substitution)
37+
.clone();
38+
39+
let last_field_sized_goal = TraitRef {
40+
trait_id: trait_ref.trait_id,
41+
substitution: Substitution::from1(interner, last_field_ty),
42+
};
43+
builder.push_clause(trait_ref.clone(), iter::once(last_field_sized_goal));
44+
}

chalk-solve/src/wf.rs

+4
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,7 @@ where
190190
let wg_goal = gb.forall(&struct_data, (), |gb, _, (fields, where_clauses), ()| {
191191
let interner = gb.interner();
192192

193+
// struct is well-formed in terms of Sized
193194
let sized_constraint_goal = compute_struct_sized_constraint(gb.db(), fields);
194195

195196
// (FromEnv(T: Eq) => ...)
@@ -479,6 +480,9 @@ fn compute_assoc_ty_goal<I: Interner>(
479480
))
480481
}
481482

483+
/// Computes a goal to prove Sized constraints on a struct definition.
484+
/// Struct is considered well-formed (in terms of Sized) when it either
485+
/// has no fields or all of it's fields except the last are proven to be Sized.
482486
fn compute_struct_sized_constraint<I: Interner>(
483487
db: &dyn RustIrDatabase<I>,
484488
fields: &[Ty<I>],

0 commit comments

Comments
 (0)