File tree Expand file tree Collapse file tree 2 files changed +8
-8
lines changed Expand file tree Collapse file tree 2 files changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -7,10 +7,10 @@ actually implement this? That's where the [`SearchGraph`] comes into play.
7
7
[ cycles ] : ./inductive_cycles.md
8
8
[ coinduction ] : ./coinduction.md
9
9
[ stack ] : ./stack.md
10
- [ `SearchGraph` ] : https://rust-lang.github.io/chalk/chalk_recursive/search_graph/struct.SearchGraph.html
11
- [ `DepthFirstNumber` ] : https://rust-lang.github.io/chalk/chalk_recursive/search_graph/struct.DepthFirstNumber.html
12
- [ `Node` ] : https://rust-lang.github.io/chalk/chalk_recursive/search_graph/struct.Node.html
13
- [ `stack_depth` ] : https://rust-lang.github.io/chalk/chalk_recursive/search_graph/struct.Node.html#structfield.stack_depth
10
+ [ `SearchGraph` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ search_graph/struct.SearchGraph.html
11
+ [ `DepthFirstNumber` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ search_graph/struct.DepthFirstNumber.html
12
+ [ `Node` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ search_graph/struct.Node.html
13
+ [ `stack_depth` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ search_graph/struct.Node.html#structfield.stack_depth
14
14
15
15
The role of the [ ` SearchGraph ` ] is to store information about each goal that we
16
16
are currently solving. Typically, these are goals on the stack -- but other
@@ -183,7 +183,7 @@ recursively invoking some goal G2 that is in the search graph but *not* present
183
183
on the stack, then we update the current [ ` Minimums ` ] with the values stored in
184
184
the search graph.
185
185
186
- [ `Minimums` ] : https://rust-lang.github.io/chalk/chalk_recursive/struct.Minimums.html
186
+ [ `Minimums` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ struct.Minimums.html
187
187
188
188
## Removing nodes from the graph
189
189
Original file line number Diff line number Diff line change @@ -5,13 +5,13 @@ what it sounds like: a stack that stores each thing that the recursive solver is
5
5
solving. Initially, it contains only one item, the root goal that was given by
6
6
the user.
7
7
8
- [ `Stack` ] : https://rust-lang.github.io/chalk/chalk_recursive/stack/struct.Stack.html
8
+ [ `Stack` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ stack/struct.Stack.html
9
9
10
10
Each frame on the stack has an associated [ ` StackDepth ` ] , which is basically an
11
11
index that increases (so 0 is the top of the stack, 1 is the next thing pushed,
12
12
etc).
13
13
14
- [ `StackDepth` ] : https://rust-lang.github.io/chalk/chalk_recursive/stack/struct.StackDepth.html
14
+ [ `StackDepth` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ stack/struct.StackDepth.html
15
15
16
16
## How the recursive solver works at the highest level
17
17
@@ -74,4 +74,4 @@ detect a cycle by checking in the [search graph] to see whether G has an associa
74
74
to learn more about that).
75
75
76
76
[ search graph ] : ./search_graph.md
77
- [ `cycle` ] : https://rust-lang.github.io/chalk/chalk_recursive/stack/struct.StackEntry.html#structfield.cycle
77
+ [ `cycle` ] : https://rust-lang.github.io/chalk/chalk_recursive/fixed_point/ stack/struct.StackEntry.html#structfield.cycle
You can’t perform that action at this time.
0 commit comments