Skip to content

Commit a9afe42

Browse files
basil-cowbasil-cow
committed
add Sized well-known impl and wf check
1 parent 30efe09 commit a9afe42

File tree

10 files changed

+197
-15
lines changed

10 files changed

+197
-15
lines changed

‎chalk-integration/src/db.rs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ use chalk_rust_ir::AssociatedTyDatum;
2121
use chalk_rust_ir::AssociatedTyValue;
2222
use chalk_rust_ir::AssociatedTyValueId;
2323
use chalk_rust_ir::ImplDatum;
24+
use chalk_rust_ir::LangItem;
2425
use chalk_rust_ir::StructDatum;
2526
use chalk_rust_ir::TraitDatum;
2627
use chalk_solve::RustIrDatabase;
@@ -137,6 +138,10 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
137138
.impl_provided_for(auto_trait_id, struct_id)
138139
}
139140

141+
fn require_lang_item(&self, lang_item: LangItem) -> TraitId<ChalkIr> {
142+
self.program_ir().unwrap().require_lang_item(lang_item)
143+
}
144+
140145
fn interner(&self) -> &ChalkIr {
141146
&ChalkIr
142147
}

‎chalk-integration/src/lowering.rs

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ use chalk_ir::interner::ChalkIr;
33
use chalk_ir::{self, AssocTypeId, BoundVar, DebruijnIndex, ImplId, StructId, TraitId};
44
use chalk_parse::ast::*;
55
use chalk_rust_ir as rust_ir;
6-
use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, ToParameter};
6+
use chalk_rust_ir::{Anonymize, AssociatedTyValueId, IntoWhereClauses, LangItem, ToParameter};
77
use lalrpop_intern::intern;
88
use std::collections::BTreeMap;
99
use std::sync::Arc;
@@ -246,6 +246,7 @@ impl LowerProgram for Program {
246246

247247
let mut struct_data = BTreeMap::new();
248248
let mut trait_data = BTreeMap::new();
249+
let mut trait_lang_items = BTreeMap::new();
249250
let mut impl_data = BTreeMap::new();
250251
let mut associated_ty_data = BTreeMap::new();
251252
let mut associated_ty_values = BTreeMap::new();
@@ -267,10 +268,24 @@ impl LowerProgram for Program {
267268
}
268269
Item::TraitDefn(ref trait_defn) => {
269270
let trait_id = TraitId(raw_id);
270-
trait_data.insert(
271-
trait_id,
272-
Arc::new(trait_defn.lower_trait(trait_id, &empty_env)?),
273-
);
271+
let trait_datum = trait_defn.lower_trait(trait_id, &empty_env)?;
272+
273+
if let Some(well_known) = trait_datum.well_known {
274+
if let Some(lang_item) = match well_known {
275+
rust_ir::WellKnownTrait::SizedTrait => Some(LangItem::SizedTrait),
276+
_ => None,
277+
} {
278+
use std::collections::btree_map::Entry;
279+
match trait_lang_items.entry(lang_item) {
280+
Entry::Vacant(vacant) => vacant.insert(trait_id),
281+
Entry::Occupied(_) => {
282+
return Err(RustIrError::DuplicateLangItem(lang_item))
283+
}
284+
};
285+
}
286+
}
287+
288+
trait_data.insert(trait_id, Arc::new(trait_datum));
274289

275290
for assoc_ty_defn in &trait_defn.assoc_ty_defns {
276291
let lookup = &associated_ty_lookups[&(trait_id, assoc_ty_defn.name.str)];
@@ -367,6 +382,7 @@ impl LowerProgram for Program {
367382
trait_kinds,
368383
struct_data,
369384
trait_data,
385+
trait_lang_items,
370386
impl_data,
371387
associated_ty_values,
372388
associated_ty_data,

‎chalk-integration/src/program.rs

Lines changed: 12 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ use chalk_ir::{
99
TraitId, Ty, TyData, TypeName,
1010
};
1111
use chalk_rust_ir::{
12-
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, StructDatum,
13-
TraitDatum,
12+
AssociatedTyDatum, AssociatedTyValue, AssociatedTyValueId, ImplDatum, ImplType, LangItem,
13+
StructDatum, TraitDatum,
1414
};
1515
use chalk_solve::split::Split;
1616
use chalk_solve::RustIrDatabase;
@@ -45,6 +45,9 @@ pub struct Program {
4545
/// For each trait:
4646
pub trait_data: BTreeMap<TraitId<ChalkIr>, Arc<TraitDatum<ChalkIr>>>,
4747

48+
/// For each trait lang item
49+
pub trait_lang_items: BTreeMap<LangItem, TraitId<ChalkIr>>,
50+
4851
/// For each associated ty declaration `type Foo` found in a trait:
4952
pub associated_ty_data: BTreeMap<AssocTypeId<ChalkIr>, Arc<AssociatedTyDatum<ChalkIr>>>,
5053

@@ -309,6 +312,13 @@ impl RustIrDatabase<ChalkIr> for Program {
309312
})
310313
}
311314

315+
fn require_lang_item(&self, lang_item: LangItem) -> TraitId<ChalkIr> {
316+
*self
317+
.trait_lang_items
318+
.get(&lang_item)
319+
.unwrap_or_else(|| panic!("No lang item found for {:?}", lang_item))
320+
}
321+
312322
fn interner(&self) -> &ChalkIr {
313323
&ChalkIr
314324
}

‎chalk-integration/src/query.rs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,6 @@ fn checked_program(db: &impl LoweringDatabase) -> Result<Arc<Program>, ChalkErro
100100

101101
let () = tls::set_current_program(&program, || -> Result<(), ChalkError> {
102102
let solver = wf::WfSolver::new(db, db.solver_choice());
103-
104103
for &id in program.struct_data.keys() {
105104
solver.verify_struct_decl(id)?;
106105
}

‎chalk-rust-ir/src/lib.rs

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,10 @@ use chalk_ir::{
1515
};
1616
use std::iter;
1717

18-
#[derive(Clone, Debug, PartialEq, Eq, PartialOrd, Ord)]
19-
pub enum LangItem {}
18+
#[derive(Clone, Copy, Debug, PartialEq, Eq, PartialOrd, Ord)]
19+
pub enum LangItem {
20+
SizedTrait,
21+
}
2022

2123
/// Identifier for an "associated type value" found in some impl.
2224
#[derive(Copy, Clone, Debug, PartialEq, Eq, PartialOrd, Ord, Hash)]
@@ -78,7 +80,7 @@ impl<I: Interner> StructDatum<I> {
7880
}
7981
}
8082

81-
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
83+
#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, HasInterner)]
8284
pub struct StructDatumBound<I: Interner> {
8385
pub fields: Vec<Ty<I>>,
8486
pub where_clauses: Vec<QuantifiedWhereClause<I>>,

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

Lines changed: 40 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,8 @@
1+
use std::iter;
2+
13
use super::builder::ClauseBuilder;
24
use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
3-
use chalk_ir::TyData;
5+
use chalk_ir::{ApplicationTy, Substitution, TyData, TypeName};
46

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

1820
match well_known {
19-
WellKnownTrait::SizedTrait => { /* TODO */ }
21+
WellKnownTrait::SizedTrait => add_sized_program_clauses(db, builder, trait_ref, ty),
2022
WellKnownTrait::CopyTrait => { /* TODO */ }
2123
WellKnownTrait::CloneTrait => { /* TODO */ }
2224
}
2325
}
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+
}

‎chalk-solve/src/lib.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,9 @@ pub trait RustIrDatabase<I: Interner>: Debug {
7676
false
7777
}
7878

79+
/// Returns id of a trait lang item, if found
80+
fn require_lang_item(&self, lang_item: LangItem) -> TraitId<I>;
81+
7982
fn interner(&self) -> &I;
8083
}
8184

‎chalk-solve/src/wf.rs

Lines changed: 33 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -190,6 +190,8 @@ where
190190
let wg_goal = gb.forall(&struct_data, (), |gb, _, (fields, where_clauses), ()| {
191191
let interner = gb.interner();
192192

193+
let sized_constraint_goal = compute_struct_sized_constraint(gb.db(), fields);
194+
193195
// (FromEnv(T: Eq) => ...)
194196
gb.implies(
195197
where_clauses
@@ -203,7 +205,13 @@ where
203205
fields.fold(gb.interner(), &mut input_types);
204206
// ...in a where clause.
205207
where_clauses.fold(gb.interner(), &mut input_types);
206-
gb.all(input_types.into_iter().map(|ty| ty.well_formed()))
208+
209+
gb.all(
210+
input_types
211+
.into_iter()
212+
.map(|ty| ty.well_formed().cast(interner))
213+
.chain(sized_constraint_goal.into_iter()),
214+
)
207215
},
208216
)
209217
});
@@ -464,3 +472,27 @@ fn compute_assoc_ty_goal<I: Interner>(
464472
},
465473
))
466474
}
475+
476+
fn compute_struct_sized_constraint<I: Interner>(
477+
db: &dyn RustIrDatabase<I>,
478+
fields: &[Ty<I>],
479+
) -> Option<Goal<I>> {
480+
if fields.len() <= 1 {
481+
return None;
482+
}
483+
484+
let interner = db.interner();
485+
486+
let sized_trait = db.require_lang_item(LangItem::SizedTrait);
487+
488+
Some(Goal::all(
489+
interner,
490+
fields[..fields.len() - 1].iter().map(|ty| {
491+
TraitRef {
492+
trait_id: sized_trait,
493+
substitution: Substitution::from1(interner, ty.clone()),
494+
}
495+
.cast(interner)
496+
}),
497+
))
498+
}

‎tests/test/auto_traits.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,15 @@ use super::*;
66
fn auto_semantics() {
77
test! {
88
program {
9+
#[lang(sized)] trait Sized { }
910
#[auto] trait Send { }
1011

1112
struct i32 { }
1213

1314
struct Ptr<T> { }
1415
impl<T> Send for Ptr<T> where T: Send { }
1516

16-
struct List<T> {
17+
struct List<T> where T: Sized {
1718
data: T,
1819
next: Ptr<List<T>>
1920
}

‎tests/test/wf_lowering.rs

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -636,3 +636,79 @@ fn assoc_type_recursive_bound() {
636636
}
637637
}
638638
}
639+
640+
#[test]
641+
fn duplicate_lang_item() {
642+
lowering_error! {
643+
program {
644+
#[lang(sized)]
645+
trait Sized { }
646+
647+
#[lang(sized)]
648+
trait Sized2 { }
649+
} error_msg {
650+
"duplicate lang item `SizedTrait`"
651+
}
652+
}
653+
}
654+
655+
#[test]
656+
fn struct_sized_constraints() {
657+
lowering_error! {
658+
program {
659+
#[lang(sized)]
660+
trait Sized { }
661+
662+
struct S<T> {
663+
t1: T,
664+
t2: T
665+
}
666+
} error_msg {
667+
"type declaration `S` does not meet well-formedness requirements"
668+
}
669+
}
670+
671+
lowering_success! {
672+
program {
673+
#[lang(sized)]
674+
trait Sized { }
675+
676+
struct Foo { }
677+
678+
struct S<T> {
679+
t1: Foo,
680+
t2: T
681+
}
682+
}
683+
}
684+
685+
lowering_success! {
686+
program {
687+
#[lang(sized)]
688+
trait Sized { }
689+
690+
struct S<T> where T: Sized {
691+
t1: T,
692+
t2: T
693+
}
694+
}
695+
}
696+
697+
lowering_success! {
698+
program {
699+
#[lang(sized)]
700+
trait Sized { }
701+
702+
struct Foo {}
703+
704+
struct G<T> {
705+
foo: S<S<Foo>>,
706+
s: S<S<S<T>>>
707+
}
708+
709+
struct S<T> {
710+
t1: T
711+
}
712+
}
713+
}
714+
}

0 commit comments

Comments
 (0)