vendor/chalk-engine/src/simplify.rs

   1 use fallible::Fallible;
   2 use {ExClause, Literal};
   3 use forest::Forest;
   4 use hh::HhGoal;
   5 use context::prelude::*;
   6
   7 impl<C: Context, CO: ContextOps<C>> Forest<C, CO> {
   8     /// Simplifies an HH goal into a series of positive domain goals
   9     /// and negative HH goals. This operation may fail if the HH goal
  10     /// includes unifications that cannot be completed.
  11     pub(super) fn simplify_hh_goal<I: Context>(
  12         infer: &mut dyn InferenceTable<C, I>,
  13         subst: I::Substitution,
  14         initial_environment: &I::Environment,
  15         initial_hh_goal: HhGoal<I>,
  16     ) -> Fallible<ExClause<I>> {
  17         let mut ex_clause = ExClause {
  18             subst,
  19             delayed_literals: vec![],
  20             constraints: vec![],
  21             subgoals: vec![],
  22         };
  23
  24         // A stack of higher-level goals to process.
  25         let mut pending_goals = vec![(initial_environment.clone(), initial_hh_goal)];
  26
  27         while let Some((environment, hh_goal)) = pending_goals.pop() {
  28             match hh_goal {
  29                 HhGoal::ForAll(subgoal) => {
  30                     let subgoal = infer.instantiate_binders_universally(&subgoal);
  31                     pending_goals.push((environment, infer.into_hh_goal(subgoal)));
  32                 }
  33                 HhGoal::Exists(subgoal) => {
  34                     let subgoal = infer.instantiate_binders_existentially(&subgoal);
  35                     pending_goals.push((environment, infer.into_hh_goal(subgoal)))
  36                 }
  37                 HhGoal::Implies(wc, subgoal) => {
  38                     let new_environment = infer.add_clauses(&environment, wc);
  39                     pending_goals.push((new_environment, infer.into_hh_goal(subgoal)));
  40                 }
  41                 HhGoal::And(subgoal1, subgoal2) => {
  42                     pending_goals.push((environment.clone(), infer.into_hh_goal(subgoal1)));
  43                     pending_goals.push((environment, infer.into_hh_goal(subgoal2)));
  44                 }
  45                 HhGoal::Not(subgoal) => {
  46                     ex_clause
  47                         .subgoals
  48                         .push(Literal::Negative(I::goal_in_environment(&environment, subgoal)));
  49                 }
  50                 HhGoal::Unify(variance, a, b) => {
  51                     let result = infer.unify_parameters(&environment, variance, &a, &b)?;
  52                     infer.into_ex_clause(result, &mut ex_clause)
  53                 }
  54                 HhGoal::DomainGoal(domain_goal) => {
  55                     ex_clause
  56                         .subgoals
  57                         .push(Literal::Positive(I::goal_in_environment(
  58                             &environment,
  59                             infer.into_goal(domain_goal),
  60                         )));
  61                 }
  62                 HhGoal::CannotProve => {
  63                     // You can think of `CannotProve` as a special
  64                     // goal that is only provable if `not {
  65                     // CannotProve }`. Trying to prove this, of
  66                     // course, will always create a negative cycle and
  67                     // hence a delayed literal that cannot be
  68                     // resolved.
  69                     let goal = infer.cannot_prove();
  70                     ex_clause
  71                         .subgoals
  72                         .push(Literal::Negative(I::goal_in_environment(&environment, goal)));
  73                 }
  74             }
  75         }
  76
  77         Ok(ex_clause)
  78     }
  79 }