Skip to content

Commit d968d96

Browse files
committed
make the search-graph and cache unaware of chalk types
1 parent 18964c9 commit d968d96

File tree

3 files changed

+90
-48
lines changed

3 files changed

+90
-48
lines changed

chalk-recursive/src/cache.rs

Lines changed: 36 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,45 @@
1-
use crate::UCanonicalGoal;
2-
use chalk_ir::interner::Interner;
3-
use chalk_ir::Fallible;
4-
use chalk_solve::Solution;
51
use rustc_hash::FxHashMap;
2+
use std::fmt::Debug;
3+
use std::hash::Hash;
64
use std::sync::{Arc, Mutex};
75
use tracing::debug;
86
use tracing::instrument;
97
/// The "cache" stores results for goals that we have completely solved.
108
/// Things are added to the cache when we have completely processed their
119
/// result, and it can be shared amongst many solvers.
12-
pub struct Cache<I: Interner> {
13-
data: Arc<Mutex<CacheData<I>>>,
10+
pub struct Cache<K, V>
11+
where
12+
K: Hash + Eq + Debug,
13+
V: Debug + Clone,
14+
{
15+
data: Arc<Mutex<CacheData<K, V>>>,
1416
}
15-
struct CacheData<I: Interner> {
16-
cache: FxHashMap<UCanonicalGoal<I>, Fallible<Solution<I>>>,
17+
struct CacheData<K, V>
18+
where
19+
K: Hash + Eq + Debug,
20+
V: Debug + Clone,
21+
{
22+
cache: FxHashMap<K, V>,
1723
}
1824

19-
impl<I: Interner> Cache<I> {
25+
impl<K, V> Cache<K, V>
26+
where
27+
K: Hash + Eq + Debug,
28+
V: Debug + Clone,
29+
{
2030
pub fn new() -> Self {
2131
Self::default()
2232
}
2333

2434
/// Record a cache result.
2535
#[instrument(skip(self))]
26-
pub fn insert(&self, goal: UCanonicalGoal<I>, result: Fallible<Solution<I>>) {
36+
pub fn insert(&self, goal: K, result: V) {
2737
let mut data = self.data.lock().unwrap();
2838
data.cache.insert(goal, result);
2939
}
3040

3141
/// Record a cache result.
32-
pub fn get(&self, goal: &UCanonicalGoal<I>) -> Option<Fallible<Solution<I>>> {
42+
pub fn get(&self, goal: &K) -> Option<V> {
3343
let data = self.data.lock().unwrap();
3444
if let Some(result) = data.cache.get(&goal) {
3545
debug!(?goal, ?result, "Cache hit");
@@ -41,23 +51,35 @@ impl<I: Interner> Cache<I> {
4151
}
4252
}
4353

44-
impl<I: Interner> Clone for Cache<I> {
54+
impl<K, V> Clone for Cache<K, V>
55+
where
56+
K: Hash + Eq + Debug,
57+
V: Debug + Clone,
58+
{
4559
fn clone(&self) -> Self {
4660
Self {
4761
data: self.data.clone(),
4862
}
4963
}
5064
}
5165

52-
impl<I: Interner> Default for Cache<I> {
66+
impl<K, V> Default for Cache<K, V>
67+
where
68+
K: Hash + Eq + Debug,
69+
V: Debug + Clone,
70+
{
5371
fn default() -> Self {
5472
Self {
5573
data: Default::default(),
5674
}
5775
}
5876
}
5977

60-
impl<I: Interner> Default for CacheData<I> {
78+
impl<K, V> Default for CacheData<K, V>
79+
where
80+
K: Hash + Eq + Debug,
81+
V: Debug + Clone,
82+
{
6183
fn default() -> Self {
6284
Self {
6385
cache: Default::default(),

chalk-recursive/src/recursive.rs

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -17,12 +17,12 @@ struct RecursiveContext<I: Interner> {
1717

1818
/// The "search graph" stores "in-progress results" that are still being
1919
/// solved.
20-
search_graph: SearchGraph<I>,
20+
search_graph: SearchGraph<UCanonicalGoal<I>, Fallible<Solution<I>>>,
2121

2222
/// The "cache" stores results for goals that we have completely solved.
2323
/// Things are added to the cache when we have completely processed their
2424
/// result.
25-
cache: Option<Cache<I>>,
25+
cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
2626

2727
/// The maximum size for goals.
2828
max_size: usize,
@@ -43,7 +43,11 @@ pub struct RecursiveSolver<I: Interner> {
4343
}
4444

4545
impl<I: Interner> RecursiveSolver<I> {
46-
pub fn new(overflow_depth: usize, max_size: usize, cache: Option<Cache<I>>) -> Self {
46+
pub fn new(
47+
overflow_depth: usize,
48+
max_size: usize,
49+
cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
50+
) -> Self {
4751
Self {
4852
ctx: Box::new(RecursiveContext::new(overflow_depth, max_size, cache)),
4953
}
@@ -77,7 +81,11 @@ impl<T> MergeWith<T> for Fallible<T> {
7781
}
7882

7983
impl<I: Interner> RecursiveContext<I> {
80-
pub fn new(overflow_depth: usize, max_size: usize, cache: Option<Cache<I>>) -> Self {
84+
pub fn new(
85+
overflow_depth: usize,
86+
max_size: usize,
87+
cache: Option<Cache<UCanonicalGoal<I>, Fallible<Solution<I>>>>,
88+
) -> Self {
8189
RecursiveContext {
8290
stack: Stack::new(overflow_depth),
8391
search_graph: SearchGraph::new(),
@@ -245,10 +253,10 @@ impl<'me, I: Interner> SolveDatabase<I> for Solver<'me, I> {
245253
} else {
246254
Err(NoSolution)
247255
};
248-
let dfn =
249-
self.context
250-
.search_graph
251-
.insert(&goal, depth, coinductive_goal, initial_solution);
256+
let dfn = self
257+
.context
258+
.search_graph
259+
.insert(&goal, depth, initial_solution);
252260
let subgoal_minimums = self.solve_new_subgoal(goal, depth, dfn);
253261
self.context.search_graph[dfn].links = subgoal_minimums;
254262
self.context.search_graph[dfn].stack_depth = None;

chalk-recursive/src/search_graph.rs

Lines changed: 38 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,35 @@
1+
use super::stack::StackDepth;
2+
use crate::{Cache, Minimums};
3+
use chalk_ir::ClausePriority;
4+
use rustc_hash::FxHashMap;
5+
use std::fmt::Debug;
6+
use std::hash::Hash;
17
use std::ops::Add;
28
use std::ops::Index;
39
use std::ops::IndexMut;
410
use std::usize;
5-
6-
use super::stack::StackDepth;
7-
use crate::{Cache, Minimums, UCanonicalGoal};
8-
use chalk_ir::{
9-
interner::Interner, Canonical, ClausePriority, ConstrainedSubst, Constraints, Fallible,
10-
NoSolution,
11-
};
12-
use chalk_solve::Solution;
13-
use rustc_hash::FxHashMap;
1411
use tracing::{debug, instrument};
1512

1613
/// The "search graph" stores in-progress goals that are still
1714
/// being solved.
18-
pub(super) struct SearchGraph<I: Interner> {
19-
indices: FxHashMap<UCanonicalGoal<I>, DepthFirstNumber>,
20-
nodes: Vec<Node<I>>,
15+
pub(super) struct SearchGraph<K, V>
16+
where
17+
K: Hash + Eq + Debug + Clone,
18+
V: Debug + Clone,
19+
{
20+
indices: FxHashMap<K, DepthFirstNumber>,
21+
nodes: Vec<Node<K, V>>,
2122
}
2223

2324
#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
2425
pub(super) struct DepthFirstNumber {
2526
index: usize,
2627
}
2728

28-
pub(super) struct Node<I: Interner> {
29-
pub(crate) goal: UCanonicalGoal<I>,
29+
pub(super) struct Node<K, V> {
30+
pub(crate) goal: K,
3031

31-
pub(crate) solution: Fallible<Solution<I>>,
32+
pub(crate) solution: V,
3233
pub(crate) solution_priority: ClausePriority,
3334

3435
/// This is `Some(X)` if we are actively exploring this node, or
@@ -42,15 +43,19 @@ pub(super) struct Node<I: Interner> {
4243
pub(crate) links: Minimums,
4344
}
4445

45-
impl<I: Interner> SearchGraph<I> {
46+
impl<K, V> SearchGraph<K, V>
47+
where
48+
K: Hash + Eq + Debug + Clone,
49+
V: Debug + Clone,
50+
{
4651
pub(crate) fn new() -> Self {
4752
SearchGraph {
4853
indices: FxHashMap::default(),
4954
nodes: vec![],
5055
}
5156
}
5257

53-
pub(crate) fn lookup(&self, goal: &UCanonicalGoal<I>) -> Option<DepthFirstNumber> {
58+
pub(crate) fn lookup(&self, goal: &K) -> Option<DepthFirstNumber> {
5459
self.indices.get(goal).cloned()
5560
}
5661

@@ -63,10 +68,9 @@ impl<I: Interner> SearchGraph<I> {
6368
/// or `NoSolution` for other goals
6469
pub(crate) fn insert(
6570
&mut self,
66-
goal: &UCanonicalGoal<I>,
71+
goal: &K,
6772
stack_depth: StackDepth,
68-
coinductive: bool,
69-
solution: Fallible<Solution<I>>,
73+
solution: V,
7074
) -> DepthFirstNumber {
7175
let dfn = DepthFirstNumber {
7276
index: self.nodes.len(),
@@ -94,7 +98,7 @@ impl<I: Interner> SearchGraph<I> {
9498
/// Removes all nodes with a depth-first-number greater than or
9599
/// equal to `dfn`, adding their final solutions into the cache.
96100
#[instrument(level = "debug", skip(self, cache))]
97-
pub(crate) fn move_to_cache(&mut self, dfn: DepthFirstNumber, cache: &Cache<I>) {
101+
pub(crate) fn move_to_cache(&mut self, dfn: DepthFirstNumber, cache: &Cache<K, V>) {
98102
self.indices.retain(|_key, value| *value < dfn);
99103
for node in self.nodes.drain(dfn.index..) {
100104
assert!(node.stack_depth.is_none());
@@ -105,16 +109,24 @@ impl<I: Interner> SearchGraph<I> {
105109
}
106110
}
107111

108-
impl<I: Interner> Index<DepthFirstNumber> for SearchGraph<I> {
109-
type Output = Node<I>;
112+
impl<K, V> Index<DepthFirstNumber> for SearchGraph<K, V>
113+
where
114+
K: Hash + Eq + Debug + Clone,
115+
V: Debug + Clone,
116+
{
117+
type Output = Node<K, V>;
110118

111-
fn index(&self, table_index: DepthFirstNumber) -> &Node<I> {
119+
fn index(&self, table_index: DepthFirstNumber) -> &Node<K, V> {
112120
&self.nodes[table_index.index]
113121
}
114122
}
115123

116-
impl<I: Interner> IndexMut<DepthFirstNumber> for SearchGraph<I> {
117-
fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node<I> {
124+
impl<K, V> IndexMut<DepthFirstNumber> for SearchGraph<K, V>
125+
where
126+
K: Hash + Eq + Debug + Clone,
127+
V: Debug + Clone,
128+
{
129+
fn index_mut(&mut self, table_index: DepthFirstNumber) -> &mut Node<K, V> {
118130
&mut self.nodes[table_index.index]
119131
}
120132
}

0 commit comments

Comments
 (0)