@@ -9,7 +9,7 @@ mod structural_impls;
99
1010use crate :: mir:: interpret:: ErrorHandled ;
1111use crate :: ty:: subst:: SubstsRef ;
12- use crate :: ty:: { self , AdtKind , List , Ty , TyCtxt } ;
12+ use crate :: ty:: { self , AdtKind , Ty , TyCtxt } ;
1313
1414use rustc_ast:: ast;
1515use rustc_hir as hir;
@@ -307,162 +307,6 @@ pub struct DerivedObligationCause<'tcx> {
307307pub parent_code : Rc < ObligationCauseCode < ' tcx > > ,
308308}
309309
310- /// The following types:
311- /// * `WhereClause`,
312- /// * `WellFormed`,
313- /// * `FromEnv`,
314- /// * `DomainGoal`,
315- /// * `Goal`,
316- /// * `Clause`,
317- /// * `Environment`,
318- /// * `InEnvironment`,
319- /// are used for representing the trait system in the form of
320- /// logic programming clauses. They are part of the interface
321- /// for the chalk SLG solver.
322- #[ derive( Clone , Copy , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable , Lift ) ]
323- pub enum WhereClause < ' tcx > {
324- Implemented ( ty:: TraitPredicate < ' tcx > ) ,
325- ProjectionEq ( ty:: ProjectionPredicate < ' tcx > ) ,
326- RegionOutlives ( ty:: RegionOutlivesPredicate < ' tcx > ) ,
327- TypeOutlives ( ty:: TypeOutlivesPredicate < ' tcx > ) ,
328- }
329-
330- #[ derive( Clone , Copy , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable , Lift ) ]
331- pub enum WellFormed < ' tcx > {
332- Trait ( ty:: TraitPredicate < ' tcx > ) ,
333- Ty ( Ty < ' tcx > ) ,
334- }
335-
336- #[ derive( Clone , Copy , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable , Lift ) ]
337- pub enum FromEnv < ' tcx > {
338- Trait ( ty:: TraitPredicate < ' tcx > ) ,
339- Ty ( Ty < ' tcx > ) ,
340- }
341-
342- #[ derive( Clone , Copy , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable , Lift ) ]
343- pub enum DomainGoal < ' tcx > {
344- Holds ( WhereClause < ' tcx > ) ,
345- WellFormed ( WellFormed < ' tcx > ) ,
346- FromEnv ( FromEnv < ' tcx > ) ,
347- Normalize ( ty:: ProjectionPredicate < ' tcx > ) ,
348- }
349-
350- pub type PolyDomainGoal < ' tcx > = ty:: Binder < DomainGoal < ' tcx > > ;
351-
352- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable ) ]
353- pub enum QuantifierKind {
354- Universal ,
355- Existential ,
356- }
357-
358- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable , Lift ) ]
359- pub enum GoalKind < ' tcx > {
360- Implies ( Clauses < ' tcx > , Goal < ' tcx > ) ,
361- And ( Goal < ' tcx > , Goal < ' tcx > ) ,
362- Not ( Goal < ' tcx > ) ,
363- DomainGoal ( DomainGoal < ' tcx > ) ,
364- Quantified ( QuantifierKind , ty:: Binder < Goal < ' tcx > > ) ,
365- Subtype ( Ty < ' tcx > , Ty < ' tcx > ) ,
366- CannotProve ,
367- }
368-
369- pub type Goal < ' tcx > = & ' tcx GoalKind < ' tcx > ;
370-
371- pub type Goals < ' tcx > = & ' tcx List < Goal < ' tcx > > ;
372-
373- impl < ' tcx > DomainGoal < ' tcx > {
374- pub fn into_goal ( self ) -> GoalKind < ' tcx > {
375- GoalKind :: DomainGoal ( self )
376- }
377-
378- pub fn into_program_clause ( self ) -> ProgramClause < ' tcx > {
379- ProgramClause {
380- goal : self ,
381- hypotheses : ty:: List :: empty ( ) ,
382- category : ProgramClauseCategory :: Other ,
383- }
384- }
385- }
386-
387- impl < ' tcx > GoalKind < ' tcx > {
388- pub fn from_poly_domain_goal (
389- domain_goal : PolyDomainGoal < ' tcx > ,
390- tcx : TyCtxt < ' tcx > ,
391- ) -> GoalKind < ' tcx > {
392- match domain_goal. no_bound_vars ( ) {
393- Some ( p) => p. into_goal ( ) ,
394- None => GoalKind :: Quantified (
395- QuantifierKind :: Universal ,
396- domain_goal. map_bound ( |p| tcx. mk_goal ( p. into_goal ( ) ) ) ,
397- ) ,
398- }
399- }
400- }
401-
402- /// This matches the definition from Page 7 of "A Proof Procedure for the Logic of Hereditary
403- /// Harrop Formulas".
404- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable ) ]
405- pub enum Clause < ' tcx > {
406- Implies ( ProgramClause < ' tcx > ) ,
407- ForAll ( ty:: Binder < ProgramClause < ' tcx > > ) ,
408- }
409-
410- impl Clause < ' tcx > {
411- pub fn category ( self ) -> ProgramClauseCategory {
412- match self {
413- Clause :: Implies ( clause) => clause. category ,
414- Clause :: ForAll ( clause) => clause. skip_binder ( ) . category ,
415- }
416- }
417- }
418-
419- /// Multiple clauses.
420- pub type Clauses < ' tcx > = & ' tcx List < Clause < ' tcx > > ;
421-
422- /// A "program clause" has the form `D :- G1, ..., Gn`. It is saying
423- /// that the domain goal `D` is true if `G1...Gn` are provable. This
424- /// is equivalent to the implication `G1..Gn => D`; we usually write
425- /// it with the reverse implication operator `:-` to emphasize the way
426- /// that programs are actually solved (via backchaining, which starts
427- /// with the goal to solve and proceeds from there).
428- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable ) ]
429- pub struct ProgramClause < ' tcx > {
430- /// This goal will be considered true ...
431- pub goal : DomainGoal < ' tcx > ,
432-
433- /// ... if we can prove these hypotheses (there may be no hypotheses at all):
434- pub hypotheses : Goals < ' tcx > ,
435-
436- /// Useful for filtering clauses.
437- pub category : ProgramClauseCategory ,
438- }
439-
440- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable ) ]
441- pub enum ProgramClauseCategory {
442- ImpliedBound ,
443- WellFormed ,
444- Other ,
445- }
446-
447- /// A set of clauses that we assume to be true.
448- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable ) ]
449- pub struct Environment < ' tcx > {
450- pub clauses : Clauses < ' tcx > ,
451- }
452-
453- impl Environment < ' tcx > {
454- pub fn with < G > ( self , goal : G ) -> InEnvironment < ' tcx , G > {
455- InEnvironment { environment : self , goal }
456- }
457- }
458-
459- /// Something (usually a goal), along with an environment.
460- #[ derive( Copy , Clone , PartialEq , Eq , Hash , Debug , HashStable , TypeFoldable ) ]
461- pub struct InEnvironment < ' tcx , G > {
462- pub environment : Environment < ' tcx > ,
463- pub goal : G ,
464- }
465-
466310#[ derive( Clone , Debug , TypeFoldable ) ]
467311pub enum SelectionError < ' tcx > {
468312 Unimplemented ,
0 commit comments