vendor/chalk-engine/src/simplify.rs

   1 use crate::forest::Forest;
   2 use crate::slg::SlgContextOps;
   3 use crate::{ExClause, Literal, TimeStamp};
   4
   5 use chalk_ir::cast::{Cast, Caster};
   6 use chalk_ir::interner::Interner;
   7 use chalk_ir::{
   8     Environment, FallibleOrFloundered, Goal, GoalData, InEnvironment, QuantifierKind, Substitution,
   9     TyKind, TyVariableKind, Variance,
  10 };
  11 use chalk_solve::infer::InferenceTable;
  12 use tracing::debug;
  13
  14 impl<I: Interner> Forest<I> {
  15     /// Simplifies a goal into a series of positive domain goals
  16     /// and negative goals. This operation may fail if the goal
  17     /// includes unifications that cannot be completed.
  18     pub(super) fn simplify_goal(
  19         context: &SlgContextOps<I>,
  20         infer: &mut InferenceTable<I>,
  21         subst: Substitution<I>,
  22         initial_environment: Environment<I>,
  23         initial_goal: Goal<I>,
  24     ) -> FallibleOrFloundered<ExClause<I>> {
  25         let mut ex_clause = ExClause {
  26             subst,
  27             ambiguous: false,
  28             constraints: vec![],
  29             subgoals: vec![],
  30             delayed_subgoals: vec![],
  31             answer_time: TimeStamp::default(),
  32             floundered_subgoals: vec![],
  33         };
  34
  35         // A stack of higher-level goals to process.
  36         let mut pending_goals = vec![(initial_environment, initial_goal)];
  37
  38         while let Some((environment, goal)) = pending_goals.pop() {
  39             match goal.data(context.program().interner()) {
  40                 GoalData::Quantified(QuantifierKind::ForAll, subgoal) => {
  41                     let subgoal = infer.instantiate_binders_universally(
  42                         context.program().interner(),
  43                         subgoal.clone(),
  44                     );
  45                     pending_goals.push((environment, subgoal.clone()));
  46                 }
  47                 GoalData::Quantified(QuantifierKind::Exists, subgoal) => {
  48                     let subgoal = infer.instantiate_binders_existentially(
  49                         context.program().interner(),
  50                         subgoal.clone(),
  51                     );
  52                     pending_goals.push((environment, subgoal.clone()));
  53                 }
  54                 GoalData::Implies(wc, subgoal) => {
  55                     let new_environment = environment.add_clauses(
  56                         context.program().interner(),
  57                         wc.iter(context.program().interner()).cloned(),
  58                     );
  59                     pending_goals.push((new_environment, subgoal.clone()));
  60                 }
  61                 GoalData::All(subgoals) => {
  62                     for subgoal in subgoals.iter(context.program().interner()) {
  63                         pending_goals.push((environment.clone(), subgoal.clone()));
  64                     }
  65                 }
  66                 GoalData::Not(subgoal) => {
  67                     ex_clause
  68                         .subgoals
  69                         .push(Literal::Negative(InEnvironment::new(
  70                             &environment,
  71                             subgoal.clone(),
  72                         )));
  73                 }
  74                 GoalData::EqGoal(goal) => {
  75                     let interner = context.program().interner();
  76                     let db = context.unification_database();
  77                     let a = &goal.a;
  78                     let b = &goal.b;
  79
  80                     let result =
  81                         match infer.relate(interner, db, &environment, Variance::Invariant, a, b) {
  82                             Ok(r) => r,
  83                             Err(_) => return FallibleOrFloundered::NoSolution,
  84                         };
  85                     ex_clause.subgoals.extend(
  86                         result
  87                             .goals
  88                             .into_iter()
  89                             .casted(interner)
  90                             .map(Literal::Positive),
  91                     );
  92                 }
  93                 GoalData::SubtypeGoal(goal) => {
  94                     let interner = context.program().interner();
  95                     let db = context.unification_database();
  96                     let a_norm = infer.normalize_ty_shallow(interner, &goal.a);
  97                     let a = a_norm.as_ref().unwrap_or(&goal.a);
  98                     let b_norm = infer.normalize_ty_shallow(interner, &goal.b);
  99                     let b = b_norm.as_ref().unwrap_or(&goal.b);
 100
 101                     if matches!(
 102                         a.kind(interner),
 103                         TyKind::InferenceVar(_, TyVariableKind::General)
 104                     ) && matches!(
 105                         b.kind(interner),
 106                         TyKind::InferenceVar(_, TyVariableKind::General)
 107                     ) {
 108                         return FallibleOrFloundered::Floundered;
 109                     }
 110
 111                     let result =
 112                         match infer.relate(interner, db, &environment, Variance::Covariant, a, b) {
 113                             Ok(r) => r,
 114                             Err(_) => return FallibleOrFloundered::Floundered,
 115                         };
 116                     ex_clause.subgoals.extend(
 117                         result
 118                             .goals
 119                             .into_iter()
 120                             .casted(interner)
 121                             .map(Literal::Positive),
 122                     );
 123                 }
 124                 GoalData::DomainGoal(domain_goal) => {
 125                     ex_clause
 126                         .subgoals
 127                         .push(Literal::Positive(InEnvironment::new(
 128                             &environment,
 129                             domain_goal.clone().cast(context.program().interner()),
 130                         )));
 131                 }
 132                 GoalData::CannotProve => {
 133                     debug!("Marking Strand as ambiguous because of a `CannotProve` subgoal");
 134                     ex_clause.ambiguous = true;
 135                 }
 136             }
 137         }
 138
 139         FallibleOrFloundered::Ok(ex_clause)
 140     }
 141 }