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

use std::convert::Infallible;
use std::marker::PhantomData;

use rustc_type_ir::inherent::*;
use rustc_type_ir::search_graph::{self, PathKind};
use rustc_type_ir::solve::{CanonicalInput, Certainty, QueryResult};
use rustc_type_ir::Interner;

use super::inspect::ProofTreeBuilder;
use super::{has_no_inference_or_external_constraints, FIXPOINT_STEP_LIMIT};
use crate::delegate::SolverDelegate;

/// This type is never constructed. We only use it to implement `search_graph::Delegate`
/// for all types which impl `SolverDelegate` and doing it directly fails in coherence.
pub(super) struct SearchGraphDelegate<D: SolverDelegate> {
    _marker: PhantomData<D>,
}
pub(super) type SearchGraph<D> = search_graph::SearchGraph<SearchGraphDelegate<D>>;
impl<D, I> search_graph::Delegate for SearchGraphDelegate<D>
where
    D: SolverDelegate<Interner = I>,
    I: Interner,
{
    type Cx = D::Interner;

    const ENABLE_PROVISIONAL_CACHE: bool = true;
    type ValidationScope = Infallible;
    fn enter_validation_scope(
        _cx: Self::Cx,
        _input: CanonicalInput<I>,
    ) -> Option<Self::ValidationScope> {
        None
    }

    const FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;

    type ProofTreeBuilder = ProofTreeBuilder<D>;
    fn inspect_is_noop(inspect: &mut Self::ProofTreeBuilder) -> bool {
        inspect.is_noop()
    }

    const DIVIDE_AVAILABLE_DEPTH_ON_OVERFLOW: usize = 4;
    fn recursion_limit(cx: I) -> usize {
        cx.recursion_limit()
    }

    fn initial_provisional_result(
        cx: I,
        kind: PathKind,
        input: CanonicalInput<I>,
    ) -> QueryResult<I> {
        match kind {
            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes),
            PathKind::Inductive => response_no_constraints(cx, input, Certainty::overflow(false)),
        }
    }

    fn is_initial_provisional_result(
        cx: Self::Cx,
        kind: PathKind,
        input: CanonicalInput<I>,
        result: QueryResult<I>,
    ) -> bool {
        match kind {
            PathKind::Coinductive => response_no_constraints(cx, input, Certainty::Yes) == result,
            PathKind::Inductive => {
                response_no_constraints(cx, input, Certainty::overflow(false)) == result
            }
        }
    }

    fn on_stack_overflow(
        cx: I,
        inspect: &mut ProofTreeBuilder<D>,
        input: CanonicalInput<I>,
    ) -> QueryResult<I> {
        inspect.canonical_goal_evaluation_overflow();
        response_no_constraints(cx, input, Certainty::overflow(true))
    }

    fn on_fixpoint_overflow(cx: I, input: CanonicalInput<I>) -> QueryResult<I> {
        response_no_constraints(cx, input, Certainty::overflow(false))
    }

    fn is_ambiguous_result(result: QueryResult<I>) -> bool {
        result.is_ok_and(|response| {
            has_no_inference_or_external_constraints(response)
                && matches!(response.value.certainty, Certainty::Maybe(_))
        })
    }

    fn propagate_ambiguity(
        cx: I,
        for_input: CanonicalInput<I>,
        from_result: QueryResult<I>,
    ) -> QueryResult<I> {
        let certainty = from_result.unwrap().value.certainty;
        response_no_constraints(cx, for_input, certainty)
    }

    fn step_is_coinductive(cx: I, input: CanonicalInput<I>) -> bool {
        input.value.goal.predicate.is_coinductive(cx)
    }
}

fn response_no_constraints<I: Interner>(
    cx: I,
    goal: CanonicalInput<I>,
    certainty: Certainty,
) -> QueryResult<I> {
    Ok(super::response_no_constraints_raw(cx, goal.max_universe, goal.variables, certainty))
}