Skip to content

Commit 7ca82d1

Browse files
nathanwhitnathanwhit
committed
Refactor/clean up program clause generation
Simplifies creation of `FnDefDatum` and `StructDatum` program clauses
1 parent e05efd9 commit 7ca82d1

File tree

1 file changed

+120
-90
lines changed

1 file changed

+120
-90
lines changed

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

Lines changed: 120 additions & 90 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
use crate::clauses::builder::ClauseBuilder;
22
use crate::split::Split;
3-
use chalk_ir::cast::{Cast, Caster};
3+
use chalk_ir::cast::{Cast, CastTo, Caster};
44
use chalk_ir::interner::Interner;
55
use chalk_ir::*;
66
use chalk_rust_ir::*;
@@ -180,6 +180,95 @@ impl<I: Interner> ToProgramClauses<I> for OpaqueTyDatum<I> {
180180
}
181181
}
182182

183+
fn application_ty<I: Interner>(
184+
builder: &mut ClauseBuilder<'_, I>,
185+
id: impl CastTo<TypeName<I>>,
186+
) -> ApplicationTy<I> {
187+
let interner = builder.interner();
188+
ApplicationTy {
189+
name: id.cast(interner),
190+
substitution: builder.substitution_in_scope(),
191+
}
192+
}
193+
194+
fn interned_application_ty<I: Interner>(interner: &I, appl_ty: &ApplicationTy<I>) -> Ty<I> {
195+
appl_ty.clone().intern(interner)
196+
}
197+
198+
fn well_formed_program_clauses<'a, I, Wc>(
199+
builder: &'a mut ClauseBuilder<'_, I>,
200+
id: impl CastTo<TypeName<I>>,
201+
where_clauses: Wc,
202+
) where
203+
I: Interner,
204+
Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>,
205+
{
206+
// Given a type definition `struct Foo<T: Eq> { }` generate the clause
207+
// forall<T> {
208+
// WF(Foo<T>) :- WF(T: Eq).
209+
// }
210+
let interner = builder.interner();
211+
let appl_ty = application_ty(builder, id);
212+
let ty = appl_ty.clone().intern(interner);
213+
builder.push_clause(
214+
WellFormed::Ty(ty.clone()),
215+
where_clauses
216+
.cloned()
217+
.map(|qwc| qwc.into_well_formed_goal(interner)),
218+
);
219+
}
220+
221+
fn fully_visible_program_clauses<'a, I>(
222+
builder: &'a mut ClauseBuilder<'_, I>,
223+
id: impl CastTo<TypeName<I>>,
224+
) where
225+
I: Interner,
226+
{
227+
// Given a type definition `struct Foo<T: Eq> { }` generate the clause
228+
// forall<T> {
229+
// IsFullyVisible(Foo<T>) :- IsFullyVisible(T).
230+
// }
231+
let interner = builder.interner();
232+
let appl_ty = application_ty(builder, id);
233+
let ty = interned_application_ty(interner, &appl_ty);
234+
builder.push_clause(
235+
DomainGoal::IsFullyVisible(ty.clone()),
236+
appl_ty
237+
.type_parameters(interner)
238+
.map(|typ| DomainGoal::IsFullyVisible(typ).cast::<Goal<_>>(interner)),
239+
);
240+
}
241+
242+
fn implied_bounds_program_clauses<'a, I, Wc>(
243+
builder: &'a mut ClauseBuilder<'_, I>,
244+
id: impl CastTo<TypeName<I>>,
245+
where_clauses: Wc,
246+
) where
247+
I: Interner,
248+
Wc: Iterator<Item = &'a QuantifiedWhereClause<I>>,
249+
{
250+
let interner = builder.interner();
251+
let appl_ty = application_ty(builder, id);
252+
let ty = interned_application_ty(interner, &appl_ty);
253+
254+
for qwc in where_clauses {
255+
// Generate implied bounds rules. We have to push the binders from the where-clauses
256+
// too -- e.g., if we had `struct Foo<T: for<'a> Bar<&'a i32>>`, we would
257+
// create a reverse rule like:
258+
//
259+
// ```notrust
260+
// forall<T, 'a> { FromEnv(T: Bar<&'a i32>) :- FromEnv(Foo<T>) }
261+
// ```
262+
//
263+
// In other words, you can assume `T: Bar<&'a i32>`
264+
// for any `'a` *if* you are assuming that `Foo<T>` is
265+
// well formed.
266+
builder.push_binders(&qwc, |builder, wc| {
267+
builder.push_clause(wc.into_from_env_goal(interner), Some(ty.clone().from_env()));
268+
});
269+
}
270+
}
271+
183272
impl<I: Interner> ToProgramClauses<I> for StructDatum<I> {
184273
/// Given the following type definition: `struct Foo<T: Eq> { }`, generate:
185274
///
@@ -234,33 +323,17 @@ impl<I: Interner> ToProgramClauses<I> for StructDatum<I> {
234323

235324
let interner = builder.interner();
236325
let binders = self.binders.map_ref(|b| &b.where_clauses);
326+
let id = self.id;
327+
237328
builder.push_binders(&binders, |builder, where_clauses| {
238-
let self_appl_ty = &ApplicationTy {
239-
name: self.id.cast(interner),
240-
substitution: builder.substitution_in_scope(),
241-
};
242-
let self_ty = self_appl_ty.clone().intern(interner);
329+
well_formed_program_clauses(builder, id, where_clauses.iter());
243330

244-
// forall<T> {
245-
// WF(Foo<T>) :- WF(T: Eq).
246-
// }
247-
builder.push_clause(
248-
WellFormed::Ty(self_ty.clone()),
249-
where_clauses
250-
.iter()
251-
.cloned()
252-
.map(|qwc| qwc.into_well_formed_goal(interner)),
253-
);
331+
implied_bounds_program_clauses(builder, id, where_clauses.iter());
254332

255-
// forall<T> {
256-
// IsFullyVisible(Foo<T>) :- IsFullyVisible(T).
257-
// }
258-
builder.push_clause(
259-
DomainGoal::IsFullyVisible(self_ty.clone()),
260-
self_appl_ty
261-
.type_parameters(interner)
262-
.map(|ty| DomainGoal::IsFullyVisible(ty).cast::<Goal<_>>(interner)),
263-
);
333+
fully_visible_program_clauses(builder, id);
334+
335+
let self_appl_ty = application_ty(builder, id);
336+
let self_ty = interned_application_ty(interner, &self_appl_ty);
264337

265338
// Fundamental types often have rules in the form of:
266339
// Goal(FundamentalType<T>) :- Goal(T)
@@ -313,83 +386,40 @@ impl<I: Interner> ToProgramClauses<I> for StructDatum<I> {
313386
if self.flags.fundamental {
314387
fundamental_rule!(DownstreamType);
315388
}
316-
317-
for qwc in where_clauses {
318-
// Generate implied bounds rules. We have to push the binders from the where-clauses
319-
// too -- e.g., if we had `struct Foo<T: for<'a> Bar<&'a i32>>`, we would
320-
// create a reverse rule like:
321-
//
322-
// ```notrust
323-
// forall<T, 'a> { FromEnv(T: Bar<&'a i32>) :- FromEnv(Foo<T>) }
324-
// ```
325-
//
326-
// In other words, you can assume `T: Bar<&'a i32>`
327-
// for any `'a` *if* you are assuming that `Foo<T>` is
328-
// well formed.
329-
builder.push_binders(&qwc, |builder, wc| {
330-
builder.push_clause(
331-
wc.into_from_env_goal(interner),
332-
Some(self_ty.clone().from_env()),
333-
);
334-
});
335-
}
336389
});
337390
}
338391
}
339392

340393
impl<I: Interner> ToProgramClauses<I> for FnDefDatum<I> {
394+
/// Given the following function definition: `fn bar<T>() where T: Eq`, generate:
395+
///
396+
/// ```notrust
397+
/// -- Rule WellFormed-Type
398+
/// forall<T> {
399+
/// WF(bar<T>) :- WF(T: Eq)
400+
/// }
401+
///
402+
/// -- Rule Implied-Bound-From-Type
403+
/// forall<T> {
404+
/// FromEnv(T: Eq) :- FromEnv(bar<T>).
405+
/// }
406+
///
407+
/// forall<T> {
408+
/// IsFullyVisible(bar<T>) :- IsFullyVisible(T).
409+
/// }
410+
/// ```
341411
fn to_program_clauses(&self, builder: &mut ClauseBuilder<'_, I>) {
342412
debug_heading!("FnDatum::to_program_clauses(self={:?})", self);
343413

344-
let interner = builder.interner();
345414
let binders = self.binders.map_ref(|b| &b.where_clauses);
346-
builder.push_binders(&binders, |builder, where_clauses| {
347-
let self_appl_ty = &ApplicationTy {
348-
name: self.id.cast(interner),
349-
substitution: builder.substitution_in_scope(),
350-
};
351-
let self_ty = self_appl_ty.clone().intern(interner);
415+
let id = self.id;
352416

353-
// forall<T> {
354-
// WF(foo<T>) :- WF(T: Eq).
355-
// }
356-
builder.push_clause(
357-
WellFormed::Ty(self_ty.clone()),
358-
where_clauses
359-
.iter()
360-
.cloned()
361-
.map(|qwc| qwc.into_well_formed_goal(interner)),
362-
);
417+
builder.push_binders(&binders, |builder, where_clauses| {
418+
well_formed_program_clauses(builder, id, where_clauses.iter());
363419

364-
// forall<T> {
365-
// IsFullyVisible(foo<T>) :- IsFullyVisible(T).
366-
// }
367-
builder.push_clause(
368-
DomainGoal::IsFullyVisible(self_ty.clone()),
369-
self_appl_ty
370-
.type_parameters(interner)
371-
.map(|ty| DomainGoal::IsFullyVisible(ty).cast::<Goal<_>>(interner)),
372-
);
420+
implied_bounds_program_clauses(builder, id, where_clauses.iter());
373421

374-
for qwc in where_clauses {
375-
// Generate implied bounds rules. We have to push the binders from the where-clauses
376-
// too -- e.g., if we had `fn foo<T: for<'a> Bar<&'a i32>>()`, we would
377-
// create a reverse rule like:
378-
//
379-
// ```notrust
380-
// forall<T, 'a> { FromEnv(T: Bar<&'a i32>) :- FromEnv(foo<T>) }
381-
// ```
382-
//
383-
// In other words, you can assume `T: Bar<&'a i32>`
384-
// for any `'a` *if* you are assuming that `foo<T>` is
385-
// well formed.
386-
builder.push_binders(&qwc, |builder, wc| {
387-
builder.push_clause(
388-
wc.into_from_env_goal(interner),
389-
Some(self_ty.clone().from_env()),
390-
);
391-
});
392-
}
422+
fully_visible_program_clauses(builder, id);
393423
});
394424
}
395425
}

0 commit comments

Comments
 (0)