@@ -278,6 +278,8 @@ pub type TraitObligations<'tcx> = Vec<TraitObligation<'tcx>>;
278
278
/// * `DomainGoal`
279
279
/// * `Goal`
280
280
/// * `Clause`
281
+ /// * `Environment`
282
+ /// * `InEnvironment`
281
283
/// are used for representing the trait system in the form of
282
284
/// logic programming clauses. They are part of the interface
283
285
/// for the chalk SLG solver.
@@ -335,6 +337,14 @@ impl<'tcx> DomainGoal<'tcx> {
335
337
pub fn into_goal ( self ) -> GoalKind < ' tcx > {
336
338
GoalKind :: DomainGoal ( self )
337
339
}
340
+
341
+ pub fn into_program_clause ( self ) -> ProgramClause < ' tcx > {
342
+ ProgramClause {
343
+ goal : self ,
344
+ hypotheses : ty:: List :: empty ( ) ,
345
+ category : ProgramClauseCategory :: Other ,
346
+ }
347
+ }
338
348
}
339
349
340
350
impl < ' tcx > GoalKind < ' tcx > {
@@ -360,6 +370,15 @@ pub enum Clause<'tcx> {
360
370
ForAll ( ty:: Binder < ProgramClause < ' tcx > > ) ,
361
371
}
362
372
373
+ impl Clause < ' tcx > {
374
+ pub fn category ( self ) -> ProgramClauseCategory {
375
+ match self {
376
+ Clause :: Implies ( clause) => clause. category ,
377
+ Clause :: ForAll ( clause) => clause. skip_binder ( ) . category ,
378
+ }
379
+ }
380
+ }
381
+
363
382
/// Multiple clauses.
364
383
pub type Clauses < ' tcx > = & ' tcx List < Clause < ' tcx > > ;
365
384
@@ -376,6 +395,38 @@ pub struct ProgramClause<'tcx> {
376
395
377
396
/// ...if we can prove these hypotheses (there may be no hypotheses at all):
378
397
pub hypotheses : Goals < ' tcx > ,
398
+
399
+ /// Useful for filtering clauses.
400
+ pub category : ProgramClauseCategory ,
401
+ }
402
+
403
+ #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug ) ]
404
+ pub enum ProgramClauseCategory {
405
+ ImpliedBound ,
406
+ WellFormed ,
407
+ Other ,
408
+ }
409
+
410
+ /// A set of clauses that we assume to be true.
411
+ #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug ) ]
412
+ pub struct Environment < ' tcx > {
413
+ pub clauses : Clauses < ' tcx > ,
414
+ }
415
+
416
+ impl Environment < ' tcx > {
417
+ pub fn with < G > ( self , goal : G ) -> InEnvironment < ' tcx , G > {
418
+ InEnvironment {
419
+ environment : self ,
420
+ goal,
421
+ }
422
+ }
423
+ }
424
+
425
+ /// Something (usually a goal), along with an environment.
426
+ #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug ) ]
427
+ pub struct InEnvironment < ' tcx , G > {
428
+ pub environment : Environment < ' tcx > ,
429
+ pub goal : G ,
379
430
}
380
431
381
432
pub type Selection < ' tcx > = Vtable < ' tcx , PredicateObligation < ' tcx > > ;
0 commit comments