chalk_recursive/
recursive.rs

1use crate::fixed_point::{Cache, Minimums, RecursiveContext, SolverStuff};
2use crate::solve::{SolveDatabase, SolveIteration};
3use crate::UCanonicalGoal;
4use chalk_ir::{interner::Interner, NoSolution};
5use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
6use chalk_ir::{Constraints, Fallible};
7use chalk_solve::{coinductive_goal::IsCoinductive, RustIrDatabase, Solution};
8use std::fmt;
9
10/// A Solver is the basic context in which you can propose goals for a given
11/// program. **All questions posed to the solver are in canonical, closed form,
12/// so that each question is answered with effectively a "clean slate"**. This
13/// allows for better caching, and simplifies management of the inference
14/// context.
15struct Solver<'me, I: Interner> {
16    program: &'me dyn RustIrDatabase<I>,
17    context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>,
18}
19
20pub struct RecursiveSolver<I: Interner> {
21    ctx: Box<RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
22}
23
24impl<I: Interner> RecursiveSolver<I> {
25    pub fn new(
26        overflow_depth: usize,
27        max_size: usize,
28        cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
29    ) -> Self {
30        Self {
31            ctx: Box::new(RecursiveContext::new(overflow_depth, max_size, cache)),
32        }
33    }
34}
35
36impl<I: Interner> fmt::Debug for RecursiveSolver<I> {
37    fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result {
38        write!(fmt, "RecursiveSolver")
39    }
40}
41
42impl<'me, I: Interner> Solver<'me, I> {
43    pub(crate) fn new(
44        context: &'me mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>,
45        program: &'me dyn RustIrDatabase<I>,
46    ) -> Self {
47        Self { program, context }
48    }
49}
50
51impl<I: Interner> SolverStuff<UCanonicalGoal<I>, Fallible<Solution<I>>> for &dyn RustIrDatabase<I> {
52    fn is_coinductive_goal(self, goal: &UCanonicalGoal<I>) -> bool {
53        goal.is_coinductive(self)
54    }
55
56    fn initial_value(
57        self,
58        goal: &UCanonicalGoal<I>,
59        coinductive_goal: bool,
60    ) -> Fallible<Solution<I>> {
61        if coinductive_goal {
62            Ok(Solution::Unique(Canonical {
63                value: ConstrainedSubst {
64                    subst: goal.trivial_substitution(self.interner()),
65                    constraints: Constraints::empty(self.interner()),
66                },
67                binders: goal.canonical.binders.clone(),
68            }))
69        } else {
70            Err(NoSolution)
71        }
72    }
73
74    fn solve_iteration(
75        self,
76        context: &mut RecursiveContext<UCanonicalGoal<I>, Fallible<Solution<I>>>,
77        goal: &UCanonicalGoal<I>,
78        minimums: &mut Minimums,
79        should_continue: impl std::ops::Fn() -> bool + Clone,
80    ) -> Fallible<Solution<I>> {
81        Solver::new(context, self).solve_iteration(goal, minimums, should_continue)
82    }
83
84    fn reached_fixed_point(
85        self,
86        old_answer: &Fallible<Solution<I>>,
87        current_answer: &Fallible<Solution<I>>,
88    ) -> bool {
89        // Some of our subgoals depended on us. We need to re-run
90        // with the current answer.
91        old_answer == current_answer || {
92            // Subtle: if our current answer is ambiguous, we can just stop, and
93            // in fact we *must* -- otherwise, we sometimes fail to reach a
94            // fixed point. See `multiple_ambiguous_cycles` for more.
95            match &current_answer {
96                Ok(s) => s.is_ambig(),
97                Err(_) => false,
98            }
99        }
100    }
101
102    fn error_value(self) -> Fallible<Solution<I>> {
103        Err(NoSolution)
104    }
105}
106
107impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
108    fn solve_goal(
109        &mut self,
110        goal: UCanonicalGoal<I>,
111        minimums: &mut Minimums,
112        should_continue: impl std::ops::Fn() -> bool + Clone,
113    ) -> Fallible<Solution<I>> {
114        self.context
115            .solve_goal(&goal, minimums, self.program, should_continue)
116    }
117
118    fn interner(&self) -> I {
119        self.program.interner()
120    }
121
122    fn db(&self) -> &dyn RustIrDatabase<I> {
123        self.program
124    }
125
126    fn max_size(&self) -> usize {
127        self.context.max_size()
128    }
129}
130
131impl<I: Interner> chalk_solve::Solver<I> for RecursiveSolver<I> {
132    fn solve(
133        &mut self,
134        program: &dyn RustIrDatabase<I>,
135        goal: &UCanonical<InEnvironment<Goal<I>>>,
136    ) -> Option<chalk_solve::Solution<I>> {
137        self.ctx.solve_root_goal(goal, program, || true).ok()
138    }
139
140    fn solve_limited(
141        &mut self,
142        program: &dyn RustIrDatabase<I>,
143        goal: &UCanonical<InEnvironment<Goal<I>>>,
144        should_continue: &dyn std::ops::Fn() -> bool,
145    ) -> Option<chalk_solve::Solution<I>> {
146        self.ctx
147            .solve_root_goal(goal, program, should_continue)
148            .ok()
149    }
150
151    fn solve_multiple(
152        &mut self,
153        _program: &dyn RustIrDatabase<I>,
154        _goal: &UCanonical<InEnvironment<Goal<I>>>,
155        _f: &mut dyn FnMut(
156            chalk_solve::SubstitutionResult<Canonical<ConstrainedSubst<I>>>,
157            bool,
158        ) -> bool,
159    ) -> bool {
160        unimplemented!("Recursive solver doesn't support multiple answers")
161    }
162}
chalk_recursive/recursive.rs

chalk_recursive/
recursive.rs
