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
use crate::context::{AnswerResult, AnswerStream}; use crate::forest::Forest; use crate::slg::aggregate::AggregateOps; use crate::slg::SlgContextOps; use chalk_ir::interner::Interner; use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical}; use chalk_solve::{RustIrDatabase, Solution, Solver, SubstitutionResult}; use std::fmt; pub struct SLGSolver<I: Interner> { pub(crate) forest: Forest<I>, pub(crate) max_size: usize, pub(crate) expected_answers: Option<usize>, } impl<I: Interner> SLGSolver<I> { pub fn new(max_size: usize, expected_answers: Option<usize>) -> Self { Self { forest: Forest::new(), max_size, expected_answers, } } } impl<I: Interner> fmt::Debug for SLGSolver<I> { fn fmt(&self, fmt: &mut fmt::Formatter<'_>) -> fmt::Result { write!(fmt, "SLGSolver") } } impl<I: Interner> Solver<I> for SLGSolver<I> { fn solve( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, ) -> Option<Solution<I>> { let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); ops.make_solution(goal, self.forest.iter_answers(&ops, goal), || true) } fn solve_limited( &mut self, program: &dyn RustIrDatabase<I>, goal: &UCanonical<InEnvironment<Goal<I>>>, should_continue: &dyn std::ops::Fn() -> bool, ) -> Option<Solution<I>> { let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); ops.make_solution(goal, self.forest.iter_answers(&ops, goal), should_continue) } 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 { let ops = SlgContextOps::new(program, self.max_size, self.expected_answers); let mut answers = self.forest.iter_answers(&ops, goal); loop { let subst = match answers.next_answer(|| true) { AnswerResult::Answer(answer) => { if !answer.ambiguous { SubstitutionResult::Definite(answer.subst) } else if answer .subst .value .subst .is_identity_subst(ops.program().interner()) { SubstitutionResult::Floundered } else { SubstitutionResult::Ambiguous(answer.subst) } } AnswerResult::Floundered => SubstitutionResult::Floundered, AnswerResult::NoMoreSolutions => { return true; } AnswerResult::QuantumExceeded => continue, }; if !f(subst, !answers.peek_answer(|| true).is_no_more_solutions()) { return false; } } } }