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;
            }
        }
    }
}