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
113
114
115
116
117
118

use rustc_index::IndexVec;

use super::{AvailableDepth, Cx, StackDepth, StackEntry};
use crate::data_structures::{HashMap, HashSet};

#[derive(derivative::Derivative)]
#[derivative(Debug(bound = ""), Clone(bound = ""), Copy(bound = ""))]
struct QueryData<X: Cx> {
    result: X::Result,
    proof_tree: X::ProofTree,
}

struct Success<X: Cx> {
    data: X::Tracked<QueryData<X>>,
    additional_depth: usize,
}

/// The cache entry for a given input.
///
/// This contains results whose computation never hit the
/// recursion limit in `success`, and all results which hit
/// the recursion limit in `with_overflow`.
#[derive(derivative::Derivative)]
#[derivative(Default(bound = ""))]
struct CacheEntry<X: Cx> {
    success: Option<Success<X>>,
    /// We have to be careful when caching roots of cycles.
    ///
    /// See the doc comment of `StackEntry::cycle_participants` for more
    /// details.
    nested_goals: HashSet<X::Input>,
    with_overflow: HashMap<usize, X::Tracked<QueryData<X>>>,
}

#[derive(derivative::Derivative)]
#[derivative(Debug(bound = ""))]
pub(super) struct CacheData<'a, X: Cx> {
    pub(super) result: X::Result,
    pub(super) proof_tree: X::ProofTree,
    pub(super) additional_depth: usize,
    pub(super) encountered_overflow: bool,
    // FIXME: This is currently unused, but impacts the design
    // by requiring a closure for `Cx::with_global_cache`.
    pub(super) nested_goals: &'a HashSet<X::Input>,
}

#[derive(derivative::Derivative)]
#[derivative(Default(bound = ""))]
pub struct GlobalCache<X: Cx> {
    map: HashMap<X::Input, CacheEntry<X>>,
}

impl<X: Cx> GlobalCache<X> {
    /// Insert a final result into the global cache.
    pub(super) fn insert(
        &mut self,
        cx: X,
        input: X::Input,

        result: X::Result,
        proof_tree: X::ProofTree,
        dep_node: X::DepNodeIndex,

        additional_depth: usize,
        encountered_overflow: bool,
        nested_goals: &HashSet<X::Input>,
    ) {
        let data = cx.mk_tracked(QueryData { result, proof_tree }, dep_node);
        let entry = self.map.entry(input).or_default();
        entry.nested_goals.extend(nested_goals);
        if encountered_overflow {
            entry.with_overflow.insert(additional_depth, data);
        } else {
            entry.success = Some(Success { data, additional_depth });
        }
    }

    /// Try to fetch a cached result, checking the recursion limit
    /// and handling root goals of coinductive cycles.
    ///
    /// If this returns `Some` the cache result can be used.
    pub(super) fn get<'a>(
        &'a self,
        cx: X,
        input: X::Input,
        stack: &IndexVec<StackDepth, StackEntry<X>>,
        available_depth: AvailableDepth,
    ) -> Option<CacheData<'a, X>> {
        let entry = self.map.get(&input)?;
        if stack.iter().any(|e| entry.nested_goals.contains(&e.input)) {
            return None;
        }

        if let Some(ref success) = entry.success {
            if available_depth.cache_entry_is_applicable(success.additional_depth) {
                let QueryData { result, proof_tree } = cx.get_tracked(&success.data);
                return Some(CacheData {
                    result,
                    proof_tree,
                    additional_depth: success.additional_depth,
                    encountered_overflow: false,
                    nested_goals: &entry.nested_goals,
                });
            }
        }

        entry.with_overflow.get(&available_depth.0).map(|e| {
            let QueryData { result, proof_tree } = cx.get_tracked(e);
            CacheData {
                result,
                proof_tree,
                additional_depth: available_depth.0,
                encountered_overflow: true,
                nested_goals: &entry.nested_goals,
            }
        })
    }
}