Skip to content

Commit 8ce0360

Browse files
committed
collect fixed-point iteration code into fixed-point module
1 parent 09103b2 commit 8ce0360

File tree

8 files changed

+44
-45
lines changed

8 files changed

+44
-45
lines changed

chalk-recursive/src/fixed_point.rs

Lines changed: 27 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,16 @@
1-
use crate::cache::Cache;
2-
use crate::search_graph::DepthFirstNumber;
3-
use crate::search_graph::SearchGraph;
4-
use crate::stack::{Stack, StackDepth};
5-
use crate::Minimums;
61
use std::fmt::Debug;
72
use std::hash::Hash;
83
use tracing::debug;
94
use tracing::{info, instrument};
105

6+
mod cache;
7+
mod search_graph;
8+
mod stack;
9+
10+
pub use cache::Cache;
11+
use search_graph::{DepthFirstNumber, SearchGraph};
12+
use stack::{Stack, StackDepth};
13+
1114
pub(super) struct RecursiveContext<K, V>
1215
where
1316
K: Hash + Eq + Debug + Clone,
@@ -45,6 +48,25 @@ where
4548
fn error_value(self) -> V;
4649
}
4750

51+
/// The `minimums` struct is used while solving to track whether we encountered
52+
/// any cycles in the process.
53+
#[derive(Copy, Clone, Debug)]
54+
pub(super) struct Minimums {
55+
positive: DepthFirstNumber,
56+
}
57+
58+
impl Minimums {
59+
pub fn new() -> Self {
60+
Minimums {
61+
positive: DepthFirstNumber::MAX,
62+
}
63+
}
64+
65+
pub fn update_from(&mut self, minimums: Minimums) {
66+
self.positive = ::std::cmp::min(self.positive, minimums.positive);
67+
}
68+
}
69+
4870
impl<K, V> RecursiveContext<K, V>
4971
where
5072
K: Hash + Eq + Debug + Clone,

chalk-recursive/src/search_graph.rs renamed to chalk-recursive/src/fixed_point/search_graph.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
use super::stack::StackDepth;
2-
use crate::{Cache, Minimums};
2+
use super::{Cache, Minimums};
33
use rustc_hash::FxHashMap;
44
use std::fmt::Debug;
55
use std::hash::Hash;

chalk-recursive/src/stack.rs renamed to chalk-recursive/src/fixed_point/stack.rs

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,19 +3,19 @@ use std::ops::Index;
33
use std::ops::IndexMut;
44
use std::usize;
55

6-
pub(crate) struct Stack {
6+
pub(super) struct Stack {
77
// program: Arc<ProgramEnvironment>,
88
entries: Vec<StackEntry>,
99
overflow_depth: usize,
1010
}
1111

1212
#[derive(Copy, Clone, Debug, PartialOrd, Ord, PartialEq, Eq, Hash)]
13-
pub(crate) struct StackDepth {
13+
pub(super) struct StackDepth {
1414
depth: usize,
1515
}
1616

1717
/// The data we actively keep for each goal on the stack.
18-
pub(crate) struct StackEntry {
18+
pub(super) struct StackEntry {
1919
/// Was this a coinductive goal?
2020
coinductive_goal: bool,
2121

@@ -24,7 +24,7 @@ pub(crate) struct StackEntry {
2424
}
2525

2626
impl Stack {
27-
pub(crate) fn new(
27+
pub(super) fn new(
2828
// program: &Arc<ProgramEnvironment>,
2929
overflow_depth: usize,
3030
) -> Self {
@@ -35,11 +35,11 @@ impl Stack {
3535
}
3636
}
3737

38-
pub(crate) fn is_empty(&self) -> bool {
38+
pub(super) fn is_empty(&self) -> bool {
3939
self.entries.is_empty()
4040
}
4141

42-
pub(crate) fn push(&mut self, coinductive_goal: bool) -> StackDepth {
42+
pub(super) fn push(&mut self, coinductive_goal: bool) -> StackDepth {
4343
let depth = StackDepth {
4444
depth: self.entries.len(),
4545
};
@@ -58,7 +58,7 @@ impl Stack {
5858
depth
5959
}
6060

61-
pub(crate) fn pop(&mut self, depth: StackDepth) {
61+
pub(super) fn pop(&mut self, depth: StackDepth) {
6262
assert_eq!(
6363
depth.depth + 1,
6464
self.entries.len(),
@@ -70,7 +70,7 @@ impl Stack {
7070
/// True iff there exist at least one coinductive goal
7171
/// and one inductive goal each from the top of the stack
7272
/// down to (and including) the given depth.
73-
pub(crate) fn mixed_inductive_coinductive_cycle_from(&self, depth: StackDepth) -> bool {
73+
pub(super) fn mixed_inductive_coinductive_cycle_from(&self, depth: StackDepth) -> bool {
7474
let coinductive_count = self.entries[depth.depth..]
7575
.iter()
7676
.filter(|entry| entry.coinductive_goal)
@@ -83,11 +83,11 @@ impl Stack {
8383
}
8484

8585
impl StackEntry {
86-
pub(crate) fn flag_cycle(&mut self) {
86+
pub(super) fn flag_cycle(&mut self) {
8787
self.cycle = true;
8888
}
8989

90-
pub(crate) fn read_and_reset_cycle_flag(&mut self) -> bool {
90+
pub(super) fn read_and_reset_cycle_flag(&mut self) -> bool {
9191
mem::replace(&mut self.cycle, false)
9292
}
9393
}

chalk-recursive/src/fulfill.rs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
1+
use crate::fixed_point::Minimums;
12
use crate::solve::SolveDatabase;
2-
use crate::Minimums;
33
use chalk_ir::cast::Cast;
44
use chalk_ir::fold::Fold;
55
use chalk_ir::interner::{HasInterner, Interner};

chalk-recursive/src/lib.rs

Lines changed: 1 addition & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,12 @@
1-
use crate::search_graph::DepthFirstNumber;
21
use chalk_ir::{Goal, InEnvironment, UCanonical};
32

43
pub type UCanonicalGoal<I> = UCanonical<InEnvironment<Goal<I>>>;
54

6-
mod cache;
75
mod combine;
86
mod fixed_point;
97
mod fulfill;
108
mod recursive;
11-
mod search_graph;
129
pub mod solve;
13-
mod stack;
1410

15-
pub use cache::Cache;
11+
pub use fixed_point::Cache;
1612
pub use recursive::RecursiveSolver;
17-
18-
/// The `minimums` struct is used while solving to track whether we encountered
19-
/// any cycles in the process.
20-
#[derive(Copy, Clone, Debug)]
21-
pub(crate) struct Minimums {
22-
pub(crate) positive: DepthFirstNumber,
23-
}
24-
25-
impl Minimums {
26-
pub fn new() -> Self {
27-
Minimums {
28-
positive: DepthFirstNumber::MAX,
29-
}
30-
}
31-
32-
pub fn update_from(&mut self, minimums: Minimums) {
33-
self.positive = ::std::cmp::min(self.positive, minimums.positive);
34-
}
35-
}

chalk-recursive/src/recursive.rs

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
1-
use super::fixed_point::{RecursiveContext, SolverStuff};
2-
use crate::cache::Cache;
1+
use crate::fixed_point::{Cache, Minimums, RecursiveContext, SolverStuff};
32
use crate::solve::{SolveDatabase, SolveIteration};
4-
use crate::{Minimums, UCanonicalGoal};
3+
use crate::UCanonicalGoal;
54
use chalk_ir::{interner::Interner, NoSolution};
65
use chalk_ir::{Canonical, ConstrainedSubst, Goal, InEnvironment, UCanonical};
76
use chalk_ir::{Constraints, Fallible};

chalk-recursive/src/solve.rs

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
use super::combine;
22
use super::fulfill::Fulfill;
3-
use crate::{Minimums, UCanonicalGoal};
3+
use crate::fixed_point::Minimums;
4+
use crate::UCanonicalGoal;
45
use chalk_ir::could_match::CouldMatch;
56
use chalk_ir::fold::Fold;
67
use chalk_ir::interner::{HasInterner, Interner};

0 commit comments

Comments
 (0)