1
1
use derive_where:: derive_where;
2
- use rustc_index:: IndexVec ;
3
2
4
- use super :: { AvailableDepth , Cx , StackDepth , StackEntry } ;
5
- use crate :: data_structures:: { HashMap , HashSet } ;
6
-
7
- #[ derive_where( Debug , Clone , Copy ; X : Cx ) ]
8
- struct QueryData < X : Cx > {
9
- result : X :: Result ,
10
- proof_tree : X :: ProofTree ,
11
- }
3
+ use super :: { AvailableDepth , Cx , NestedGoals } ;
4
+ use crate :: data_structures:: HashMap ;
12
5
13
6
struct Success < X : Cx > {
14
- data : X :: Tracked < QueryData < X > > ,
15
7
additional_depth : usize ,
8
+ nested_goals : NestedGoals < X > ,
9
+ result : X :: Tracked < X :: Result > ,
10
+ }
11
+
12
+ struct WithOverflow < X : Cx > {
13
+ nested_goals : NestedGoals < X > ,
14
+ result : X :: Tracked < X :: Result > ,
16
15
}
17
16
18
17
/// The cache entry for a given input.
@@ -23,24 +22,15 @@ struct Success<X: Cx> {
23
22
#[ derive_where( Default ; X : Cx ) ]
24
23
struct CacheEntry < X : Cx > {
25
24
success : Option < Success < X > > ,
26
- /// We have to be careful when caching roots of cycles.
27
- ///
28
- /// See the doc comment of `StackEntry::cycle_participants` for more
29
- /// details.
30
- nested_goals : HashSet < X :: Input > ,
31
- with_overflow : HashMap < usize , X :: Tracked < QueryData < X > > > ,
25
+ with_overflow : HashMap < usize , WithOverflow < X > > ,
32
26
}
33
27
34
28
#[ derive_where( Debug ; X : Cx ) ]
35
29
pub ( super ) struct CacheData < ' a , X : Cx > {
36
30
pub ( super ) result : X :: Result ,
37
- pub ( super ) proof_tree : X :: ProofTree ,
38
31
pub ( super ) additional_depth : usize ,
39
32
pub ( super ) encountered_overflow : bool ,
40
- // FIXME: This is currently unused, but impacts the design
41
- // by requiring a closure for `Cx::with_global_cache`.
42
- #[ allow( dead_code) ]
43
- pub ( super ) nested_goals : & ' a HashSet < X :: Input > ,
33
+ pub ( super ) nested_goals : & ' a NestedGoals < X > ,
44
34
}
45
35
#[ derive_where( Default ; X : Cx ) ]
46
36
pub struct GlobalCache < X : Cx > {
@@ -55,20 +45,21 @@ impl<X: Cx> GlobalCache<X> {
55
45
input : X :: Input ,
56
46
57
47
result : X :: Result ,
58
- proof_tree : X :: ProofTree ,
59
48
dep_node : X :: DepNodeIndex ,
60
49
61
50
additional_depth : usize ,
62
51
encountered_overflow : bool ,
63
- nested_goals : & HashSet < X :: Input > ,
52
+ nested_goals : NestedGoals < X > ,
64
53
) {
65
- let data = cx. mk_tracked ( QueryData { result, proof_tree } , dep_node) ;
54
+ let result = cx. mk_tracked ( result, dep_node) ;
66
55
let entry = self . map . entry ( input) . or_default ( ) ;
67
- entry. nested_goals . extend ( nested_goals) ;
68
56
if encountered_overflow {
69
- entry. with_overflow . insert ( additional_depth, data) ;
57
+ let with_overflow = WithOverflow { nested_goals, result } ;
58
+ let prev = entry. with_overflow . insert ( additional_depth, with_overflow) ;
59
+ assert ! ( prev. is_none( ) ) ;
70
60
} else {
71
- entry. success = Some ( Success { data, additional_depth } ) ;
61
+ let prev = entry. success . replace ( Success { additional_depth, nested_goals, result } ) ;
62
+ assert ! ( prev. is_none( ) ) ;
72
63
}
73
64
}
74
65
@@ -80,36 +71,37 @@ impl<X: Cx> GlobalCache<X> {
80
71
& ' a self ,
81
72
cx : X ,
82
73
input : X :: Input ,
83
- stack : & IndexVec < StackDepth , StackEntry < X > > ,
84
74
available_depth : AvailableDepth ,
75
+ mut candidate_is_applicable : impl FnMut ( & NestedGoals < X > ) -> bool ,
85
76
) -> Option < CacheData < ' a , X > > {
86
77
let entry = self . map . get ( & input) ?;
87
- if stack. iter ( ) . any ( |e| entry. nested_goals . contains ( & e. input ) ) {
88
- return None ;
89
- }
90
-
91
- if let Some ( ref success) = entry. success {
92
- if available_depth. cache_entry_is_applicable ( success. additional_depth ) {
93
- let QueryData { result, proof_tree } = cx. get_tracked ( & success. data ) ;
78
+ if let Some ( Success { additional_depth, ref nested_goals, ref result } ) = entry. success {
79
+ if available_depth. cache_entry_is_applicable ( additional_depth)
80
+ && candidate_is_applicable ( nested_goals)
81
+ {
94
82
return Some ( CacheData {
95
- result,
96
- proof_tree,
97
- additional_depth : success. additional_depth ,
83
+ result : cx. get_tracked ( & result) ,
84
+ additional_depth,
98
85
encountered_overflow : false ,
99
- nested_goals : & entry . nested_goals ,
86
+ nested_goals,
100
87
} ) ;
101
88
}
102
89
}
103
90
104
- entry. with_overflow . get ( & available_depth. 0 ) . map ( |e| {
105
- let QueryData { result, proof_tree } = cx. get_tracked ( e) ;
106
- CacheData {
107
- result,
108
- proof_tree,
109
- additional_depth : available_depth. 0 ,
110
- encountered_overflow : true ,
111
- nested_goals : & entry. nested_goals ,
91
+ let additional_depth = available_depth. 0 ;
92
+ if let Some ( WithOverflow { nested_goals, result } ) =
93
+ entry. with_overflow . get ( & additional_depth)
94
+ {
95
+ if candidate_is_applicable ( nested_goals) {
96
+ return Some ( CacheData {
97
+ result : cx. get_tracked ( result) ,
98
+ additional_depth,
99
+ encountered_overflow : true ,
100
+ nested_goals,
101
+ } ) ;
112
102
}
113
- } )
103
+ }
104
+
105
+ None
114
106
}
115
107
}
0 commit comments