1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206
use crate::RustIrDatabase; use chalk_derive::HasInterner; use chalk_ir::interner::Interner; use chalk_ir::*; use std::fmt; pub mod truncate; /// A (possible) solution for a proposed goal. #[derive(Clone, Debug, PartialEq, Eq, HasInterner)] pub enum Solution<I: Interner> { /// The goal indeed holds, and there is a unique value for all existential /// variables. In this case, we also record a set of lifetime constraints /// which must also hold for the goal to be valid. Unique(Canonical<ConstrainedSubst<I>>), /// The goal may be provable in multiple ways, but regardless we may have some guidance /// for type inference. In this case, we don't return any lifetime /// constraints, since we have not "committed" to any particular solution /// yet. Ambig(Guidance<I>), } /// When a goal holds ambiguously (e.g., because there are multiple possible /// solutions), we issue a set of *guidance* back to type inference. #[derive(Clone, Debug, PartialEq, Eq)] pub enum Guidance<I: Interner> { /// The existential variables *must* have the given values if the goal is /// ever to hold, but that alone isn't enough to guarantee the goal will /// actually hold. Definite(Canonical<Substitution<I>>), /// There are multiple plausible values for the existentials, but the ones /// here are suggested as the preferred choice heuristically. These should /// be used for inference fallback only. Suggested(Canonical<Substitution<I>>), /// There's no useful information to feed back to type inference Unknown, } impl<I: Interner> Solution<I> { pub fn is_unique(&self) -> bool { match *self { Solution::Unique(..) => true, _ => false, } } pub fn display<'a>(&'a self, interner: &'a I) -> SolutionDisplay<'a, I> { SolutionDisplay { solution: self, interner, } } } pub struct SolutionDisplay<'a, I: Interner> { solution: &'a Solution<I>, interner: &'a I, } impl<'a, I: Interner> fmt::Display for SolutionDisplay<'a, I> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> Result<(), fmt::Error> { let SolutionDisplay { solution, interner } = self; match solution { Solution::Unique(constrained) => write!(f, "Unique; {}", constrained.display(interner)), Solution::Ambig(Guidance::Definite(subst)) => write!( f, "Ambiguous; definite substitution {}", subst.display(interner) ), Solution::Ambig(Guidance::Suggested(subst)) => write!( f, "Ambiguous; suggested substitution {}", subst.display(interner) ), Solution::Ambig(Guidance::Unknown) => write!(f, "Ambiguous; no inference guidance"), } } } #[derive(Debug)] pub enum SubstitutionResult<S> { Definite(S), Ambiguous(S), Floundered, } impl<S> SubstitutionResult<S> { pub fn as_ref(&self) -> SubstitutionResult<&S> { match self { SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(subst), SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(subst), SubstitutionResult::Floundered => SubstitutionResult::Floundered, } } pub fn map<U, F: FnOnce(S) -> U>(self, f: F) -> SubstitutionResult<U> { match self { SubstitutionResult::Definite(subst) => SubstitutionResult::Definite(f(subst)), SubstitutionResult::Ambiguous(subst) => SubstitutionResult::Ambiguous(f(subst)), SubstitutionResult::Floundered => SubstitutionResult::Floundered, } } } impl<S: fmt::Display> fmt::Display for SubstitutionResult<S> { fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { match self { SubstitutionResult::Definite(subst) => write!(fmt, "{}", subst), SubstitutionResult::Ambiguous(subst) => write!(fmt, "Ambiguous({})", subst), SubstitutionResult::Floundered => write!(fmt, "Floundered"), } } } /// Finds the solution to "goals", or trait queries -- i.e., figures /// out what sets of types implement which traits. Also, between /// queries, this struct stores the cached state from previous solver /// attempts, which can then be re-used later. pub trait Solver<I: Interner> where Self: fmt::Debug, { /// Attempts to solve the given goal, which must be in canonical /// form. Returns a unique solution (if one exists). This will do /// only as much work towards `goal` as it has to (and that work /// is cached for future attempts). /// /// # Parameters /// /// - `program` -- defines the program clauses in scope. /// - **Important:** You must supply the same set of program clauses /// each time you invoke `solve`, as otherwise the cached data may be /// invalid. /// - `goal` the goal to solve /// /// # Returns /// /// - `None` is the goal cannot be proven. /// - `Some(solution)` if we succeeded in finding *some* answers, /// although `solution` may reflect ambiguity and unknowns. fn solve( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, ) -> Option<Solution<I>>; /// Attempts to solve the given goal, which must be in canonical /// form. Returns a unique solution (if one exists). This will do /// only as much work towards `goal` as it has to (and that work /// is cached for future attempts). In addition, the solving of the /// goal can be limited by returning `false` from `should_continue`. /// /// # Parameters /// /// - `program` -- defines the program clauses in scope. /// - **Important:** You must supply the same set of program clauses /// each time you invoke `solve`, as otherwise the cached data may be /// invalid. /// - `goal` the goal to solve /// - `should_continue` if `false` is returned, the no further solving /// will be done. A `Guidance(Suggested(...))` will be returned a /// `Solution`, using any answers that were generated up to that point. /// /// # Returns /// /// - `None` is the goal cannot be proven. /// - `Some(solution)` if we succeeded in finding *some* answers, /// although `solution` may reflect ambiguity and unknowns. fn solve_limited( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, should_continue: &dyn std::ops::Fn() -> bool, ) -> Option<Solution<I>>; /// Attempts to solve the given goal, which must be in canonical /// form. Provides multiple solutions to function `f`. This will do /// only as much work towards `goal` as it has to (and that work /// is cached for future attempts). /// /// # Parameters /// /// - `program` -- defines the program clauses in scope. /// - **Important:** You must supply the same set of program clauses /// each time you invoke `solve`, as otherwise the cached data may be /// invalid. /// - `goal` the goal to solve /// - `f` -- function to proceed solution. New solutions will be generated /// while function returns `true`. /// - first argument is solution found /// - second argument is ther next solution present /// - returns true if next solution should be handled /// /// # Returns /// /// - `true` all solutions were processed with the function. /// - `false` the function returned `false` and solutions were interrupted. fn solve_multiple( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, f: &mut dyn FnMut(SubstitutionResult<Canonical<ConstrainedSubst<I>>>, bool) -> bool, ) -> bool; }