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

use std::marker::PhantomData;

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

use super::inspect::{self, ProofTreeBuilder};
use super::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 FIXPOINT_STEP_LIMIT: usize = FIXPOINT_STEP_LIMIT;

    type ProofTreeBuilder = ProofTreeBuilder<D>;

    fn recursion_limit(cx: I) -> usize {
        cx.recursion_limit()
    }

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

    fn reached_fixpoint(
        cx: I,
        kind: UsageKind,
        input: CanonicalInput<I>,
        provisional_result: Option<QueryResult<I>>,
        result: QueryResult<I>,
    ) -> bool {
        if let Some(r) = provisional_result {
            r == result
        } else {
            match kind {
                UsageKind::Single(CycleKind::Coinductive) => {
                    response_no_constraints(cx, input, Certainty::Yes) == result
                }
                UsageKind::Single(CycleKind::Inductive) => {
                    response_no_constraints(cx, input, Certainty::overflow(false)) == result
                }
                UsageKind::Mixed => false,
            }
        }
    }

    fn on_stack_overflow(
        cx: I,
        inspect: &mut ProofTreeBuilder<D>,
        input: CanonicalInput<I>,
    ) -> QueryResult<I> {
        inspect.canonical_goal_evaluation_kind(inspect::WipCanonicalGoalEvaluationKind::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 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))
}