Skip to content

Commit 297aab9

Browse files
basil-cowbasil-cow
committed
first implementation draft
1 parent 154020e commit 297aab9

File tree

13 files changed

+194
-33
lines changed

13 files changed

+194
-33
lines changed

‎chalk-integration/src/db.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ impl RustIrDatabase<ChalkIr> for ChalkDatabase {
138138
.impl_provided_for(auto_trait_id, struct_id)
139139
}
140140

141-
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<ChalkIr> {
141+
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> Option<TraitId<ChalkIr>> {
142142
self.program_ir()
143143
.unwrap()
144144
.well_known_trait_id(well_known_trait)

‎chalk-integration/src/lowering.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1367,6 +1367,9 @@ impl LowerWellKnownTrait for WellKnownTrait {
13671367
fn lower(&self) -> rust_ir::WellKnownTrait {
13681368
match self {
13691369
Self::SizedTrait => rust_ir::WellKnownTrait::SizedTrait,
1370+
Self::CopyTrait => rust_ir::WellKnownTrait::CopyTrait,
1371+
Self::CloneTrait => rust_ir::WellKnownTrait::CloneTrait,
1372+
Self::DropTrait => rust_ir::WellKnownTrait::DropTrait,
13701373
}
13711374
}
13721375
}

‎chalk-integration/src/program.rs

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -321,11 +321,8 @@ impl RustIrDatabase<ChalkIr> for Program {
321321
})
322322
}
323323

324-
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<ChalkIr> {
325-
*self
326-
.well_known_traits
327-
.get(&well_known_trait)
328-
.unwrap_or_else(|| panic!("No lang item found for {:?}", well_known_trait))
324+
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> Option<TraitId<ChalkIr>> {
325+
self.well_known_traits.get(&well_known_trait).map(|x| *x)
329326
}
330327

331328
fn interner(&self) -> &ChalkIr {

‎chalk-parse/src/ast.rs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,9 @@ pub struct TraitDefn {
5454
#[derive(Copy, Clone, PartialEq, Eq, Debug)]
5555
pub enum WellKnownTrait {
5656
SizedTrait,
57+
CopyTrait,
58+
CloneTrait,
59+
DropTrait,
5760
}
5861

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

‎chalk-parse/src/parser.lalrpop

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,9 @@ CoinductiveKeyword: () = "#" "[" "coinductive" "]";
4545

4646
WellKnownTrait: WellKnownTrait = {
4747
"#" "[" "lang" "(" "sized" ")" "]" => WellKnownTrait::SizedTrait,
48+
"#" "[" "lang" "(" "copy" ")" "]" => WellKnownTrait::CopyTrait,
49+
"#" "[" "lang" "(" "clone" ")" "]" => WellKnownTrait::CloneTrait,
50+
"#" "[" "lang" "(" "drop" ")" "]" => WellKnownTrait::DropTrait,
4851
};
4952

5053
StructDefn: StructDefn = {

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -136,6 +136,7 @@ pub enum WellKnownTrait {
136136
SizedTrait,
137137
CopyTrait,
138138
CloneTrait,
139+
DropTrait,
139140
}
140141

141142
impl<I: Interner> TraitDatum<I> {

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

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ use super::builder::ClauseBuilder;
22
use crate::{Interner, RustIrDatabase, TraitRef, WellKnownTrait};
33
use chalk_ir::TyData;
44

5+
mod copy;
56
mod sized;
67

78
/// For well known traits we have special hard-coded impls, either as an
@@ -22,7 +23,8 @@ pub fn add_builtin_program_clauses<I: Interner>(
2223

2324
match well_known {
2425
WellKnownTrait::SizedTrait => sized::add_sized_program_clauses(db, builder, trait_ref, ty),
25-
WellKnownTrait::CopyTrait => { /* TODO */ }
26-
WellKnownTrait::CloneTrait => { /* TODO */ }
26+
WellKnownTrait::CopyTrait => copy::add_copy_program_clauses(db, builder, trait_ref, ty),
27+
// Drop and Clone impls are provided explicitly
28+
WellKnownTrait::CloneTrait | WellKnownTrait::DropTrait => (),
2729
}
2830
}

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
use crate::clauses::ClauseBuilder;
2+
use crate::{Interner, RustIrDatabase, TraitRef};
3+
use chalk_ir::TyData;
4+
5+
pub fn add_copy_program_clauses<I: Interner>(
6+
db: &dyn RustIrDatabase<I>,
7+
builder: &mut ClauseBuilder<'_, I>,
8+
trait_ref: &TraitRef<I>,
9+
ty: &TyData<I>,
10+
) {
11+
let _interner = db.interner();
12+
13+
match ty {
14+
TyData::Function(_) => builder.push_fact(trait_ref.clone()),
15+
// TODO(areredify)
16+
// when #368 lands, extend this to handle everything accordingly
17+
_ => return,
18+
};
19+
}

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

Lines changed: 26 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -415,23 +415,32 @@ impl<I: Interner> ToProgramClauses<I> for TraitDatum<I> {
415415
// conditions.
416416
let type_parameters: Vec<_> = trait_ref.type_parameters(interner).collect();
417417

418-
// Add all cases for potential downstream impls that could exist
419-
for i in 0..type_parameters.len() {
420-
builder.push_clause(
421-
trait_ref.clone(),
422-
where_clauses
423-
.iter()
424-
.cloned()
425-
.casted(interner)
426-
.chain(iter::once(DomainGoal::Compatible(()).cast(interner)))
427-
.chain((0..i).map(|j| {
428-
DomainGoal::IsFullyVisible(type_parameters[j].clone()).cast(interner)
429-
}))
430-
.chain(iter::once(
431-
DomainGoal::DownstreamType(type_parameters[i].clone()).cast(interner),
432-
))
433-
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
434-
);
418+
// Drop trait can't have downstream implementation because it can only
419+
// be implemented with the same genericity as the struct definition,
420+
// i.e. Drop implementation for `struct S<T: Eq> {}` is forced to be
421+
// `impl Drop<T: Eq> for S<T> { ... }`. That means that orphan rules
422+
// prevent Drop from being implemented in downstream crates.
423+
if self.well_known != Some(WellKnownTrait::DropTrait) {
424+
// Add all cases for potential downstream impls that could exist
425+
for i in 0..type_parameters.len() {
426+
builder.push_clause(
427+
trait_ref.clone(),
428+
where_clauses
429+
.iter()
430+
.cloned()
431+
.casted(interner)
432+
.chain(iter::once(DomainGoal::Compatible(()).cast(interner)))
433+
.chain((0..i).map(|j| {
434+
DomainGoal::IsFullyVisible(type_parameters[j].clone())
435+
.cast(interner)
436+
}))
437+
.chain(iter::once(
438+
DomainGoal::DownstreamType(type_parameters[i].clone())
439+
.cast(interner),
440+
))
441+
.chain(iter::once(GoalData::CannotProve(()).intern(interner))),
442+
);
443+
}
435444
}
436445

437446
// Orphan rules:

‎chalk-solve/src/lib.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ pub trait RustIrDatabase<I: Interner>: Debug {
8181
}
8282

8383
/// Returns id of a trait lang item, if found
84-
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> TraitId<I>;
84+
fn well_known_trait_id(&self, well_known_trait: WellKnownTrait) -> Option<TraitId<I>>;
8585

8686
fn interner(&self) -> &I;
8787
}

‎chalk-solve/src/wf.rs

Lines changed: 83 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -207,11 +207,6 @@ where
207207
let impl_datum = self.db.impl_datum(impl_id);
208208
let trait_id = impl_datum.trait_id();
209209

210-
// You can't manually implement Sized
211-
if let Some(WellKnownTrait::SizedTrait) = self.db.trait_datum(trait_id).well_known {
212-
return Err(WfError::IllFormedTraitImpl(trait_id));
213-
}
214-
215210
let impl_goal = Goal::all(
216211
interner,
217212
impl_header_wf_goal(self.db, impl_id).into_iter().chain(
@@ -261,6 +256,8 @@ fn impl_header_wf_goal<I: Interner>(
261256
gb.forall(&impl_fields, (), |gb, _, (trait_ref, where_clauses), ()| {
262257
let interner = gb.interner();
263258

259+
let trait_constraint_goal = compute_well_known_impl_constraint(gb.db(), &trait_ref, where_clauses);
260+
264261
// if (WC && input types are well formed) { ... }
265262
let impl_wf = impl_wf_environment(interner, &where_clauses, &trait_ref);
266263
gb.implies(impl_wf, |gb| {
@@ -280,7 +277,8 @@ fn impl_header_wf_goal<I: Interner>(
280277
let goals = types
281278
.into_iter()
282279
.map(|ty| ty.well_formed().cast(interner))
283-
.chain(Some((*trait_ref).clone().well_formed().cast(interner)));
280+
.chain(Some((*trait_ref).clone().well_formed().cast(interner)))
281+
.chain(trait_constraint_goal.into_iter());
284282

285283
gb.all::<_, Goal<I>>(goals)
286284
})
@@ -447,6 +445,18 @@ fn compute_assoc_ty_goal<I: Interner>(
447445
))
448446
}
449447

448+
fn compute_well_known_impl_constraint<I: Interner>(db: &dyn RustIrDatabase<I>, trait_ref: &TraitRef<I>, where_clause: &[Binders<WhereClause<I>>]) -> Option<Goal<I>> {
449+
let interner = db.interner();
450+
451+
match db.trait_datum(trait_ref.trait_id).well_known? {
452+
// You can't add a manual implementation of Sized
453+
WellKnownTrait::SizedTrait => Some(GoalData::CannotProve(()).intern(interner)),
454+
WellKnownTrait::CopyTrait => compute_copy_impl_constraint(db, trait_ref, where_clause),
455+
WellKnownTrait::DropTrait => compute_drop_impl_constraint(db, trait_ref, where_clause),
456+
WellKnownTrait::CloneTrait => None,
457+
}
458+
}
459+
450460
/// Computes a goal to prove Sized constraints on a struct definition.
451461
/// Struct is considered well-formed (in terms of Sized) when it either
452462
/// has no fields or all of it's fields except the last are proven to be Sized.
@@ -460,7 +470,7 @@ fn compute_struct_sized_constraint<I: Interner>(
460470

461471
let interner = db.interner();
462472

463-
let sized_trait = db.well_known_trait_id(WellKnownTrait::SizedTrait);
473+
let sized_trait = db.well_known_trait_id(WellKnownTrait::SizedTrait)?;
464474

465475
Some(Goal::all(
466476
interner,
@@ -473,3 +483,69 @@ fn compute_struct_sized_constraint<I: Interner>(
473483
}),
474484
))
475485
}
486+
487+
/// Computes a goal to prove constraints on a Copy implementation.
488+
/// Copy impl is considered well-formed for
489+
/// a) certain builtin types (scalar values, shared ref, etc..)
490+
/// b) structs which
491+
/// 1) have all Copy fields
492+
/// 2) don't have a Drop impl
493+
fn compute_copy_impl_constraint<I: Interner>(
494+
db: &dyn RustIrDatabase<I>,
495+
trait_ref: &TraitRef<I>,
496+
_where_clause: &[Binders<WhereClause<I>>],
497+
) -> Option<Goal<I>> {
498+
let interner = db.interner();
499+
500+
let ty = trait_ref.self_type_parameter(interner);
501+
502+
let copy_trait = db.well_known_trait_id(WellKnownTrait::CopyTrait)?;
503+
let ty_data = ty.data(interner);
504+
505+
let (struct_id, substitution) = match ty_data {
506+
TyData::Apply(ApplicationTy {
507+
name: TypeName::Struct(struct_id),
508+
substitution,
509+
}) => (*struct_id, substitution),
510+
// TODO(areredify)
511+
// when #368 lands, extend this to handle everything accordingly
512+
_ => return None,
513+
};
514+
515+
let neg_drop_goal = db
516+
.well_known_trait_id(WellKnownTrait::DropTrait)
517+
.map(|drop_trait_id| {
518+
TraitRef {
519+
trait_id: drop_trait_id,
520+
substitution: Substitution::from1(interner, ty.clone()),
521+
}
522+
.cast::<Goal<I>>(interner)
523+
.negate(interner)
524+
});
525+
526+
let struct_datum = db.struct_datum(struct_id);
527+
528+
let goals = struct_datum
529+
.binders
530+
.map_ref(|b| &b.fields)
531+
.substitute(interner, substitution)
532+
.into_iter()
533+
.map(|f| {
534+
TraitRef {
535+
trait_id: copy_trait,
536+
substitution: Substitution::from1(interner, f),
537+
}
538+
.cast(interner)
539+
})
540+
.chain(neg_drop_goal.into_iter());
541+
542+
Some(Goal::all(interner, goals))
543+
}
544+
545+
fn compute_drop_impl_constraint<I: Interner>(
546+
db: &dyn RustIrDatabase<I>,
547+
trait_ref: &TraitRef<I>,
548+
where_clauses: &[Binders<WhereClause<I>>]
549+
) -> Option<Goal<I>> {
550+
None
551+
}

‎tests/test/wf_goals.rs

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,3 +55,29 @@ fn recursive_where_clause_on_type() {
5555
}
5656
}
5757
}
58+
59+
#[test]
60+
fn my_test() {
61+
test! {
62+
program {
63+
#[lang(copy)]
64+
trait Copy { }
65+
66+
#[lang(drop)]
67+
trait Drop { }
68+
69+
struct S<T1, T2> where T1: Copy, T2: Copy {
70+
t1: T1,
71+
t2: T2
72+
}
73+
74+
impl<T1, T2> Copy for S<T1, T2> { }
75+
}
76+
77+
goal {
78+
compatible { not { exists<T1, T2> { S<T1, T2>: Drop } } }
79+
} yields {
80+
"No possible solution"
81+
}
82+
}
83+
}

‎tests/test/wf_lowering.rs

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -710,3 +710,25 @@ fn struct_sized_constraints() {
710710
}
711711
}
712712
}
713+
714+
#[test]
715+
fn copy_constraints() {
716+
lowering_error! {
717+
program {
718+
#[lang(copy)]
719+
trait Copy { }
720+
721+
#[lang(drop)]
722+
trait Drop { }
723+
724+
struct S<T1, T2> where T1: Copy, T2: Copy {
725+
t1: T1,
726+
t2: T2
727+
}
728+
729+
impl<T1, T2> Copy for S<T1, T2> { }
730+
} error_msg {
731+
""
732+
}
733+
}
734+
}

0 commit comments

Comments
 (0)