1
- /// An infrastructure to mechanically analyse proof trees.
2
- ///
3
- /// It is unavoidable that this representation is somewhat
4
- /// lossy as it should hide quite a few semantically relevant things,
5
- /// e.g. canonicalization and the order of nested goals.
6
- ///
7
- /// @lcnr: However, a lot of the weirdness here is not strictly necessary
8
- /// and could be improved in the future. This is mostly good enough for
9
- /// coherence right now and was annoying to implement, so I am leaving it
10
- /// as is until we start using it for something else.
11
- use std:: ops:: ControlFlow ;
12
-
1
+ //! An infrastructure to mechanically analyse proof trees.
2
+ //!
3
+ //! It is unavoidable that this representation is somewhat
4
+ //! lossy as it should hide quite a few semantically relevant things,
5
+ //! e.g. canonicalization and the order of nested goals.
6
+ //!
7
+ //! @lcnr: However, a lot of the weirdness here is not strictly necessary
8
+ //! and could be improved in the future. This is mostly good enough for
9
+ //! coherence right now and was annoying to implement, so I am leaving it
10
+ //! as is until we start using it for something else.
11
+
12
+ use rustc_ast_ir:: try_visit;
13
+ use rustc_ast_ir:: visit:: VisitorResult ;
13
14
use rustc_infer:: infer:: InferCtxt ;
14
15
use rustc_middle:: traits:: query:: NoSolution ;
15
16
use rustc_middle:: traits:: solve:: { inspect, QueryResult } ;
@@ -53,10 +54,7 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
53
54
/// to also use it to compute the most relevant goal
54
55
/// for fulfillment errors. Will do that once we actually
55
56
/// need it.
56
- pub fn visit_nested < V : ProofTreeVisitor < ' tcx > > (
57
- & self ,
58
- visitor : & mut V ,
59
- ) -> ControlFlow < V :: BreakTy > {
57
+ pub fn visit_nested < V : ProofTreeVisitor < ' tcx > > ( & self , visitor : & mut V ) -> V :: Result {
60
58
// HACK: An arbitrary cutoff to avoid dealing with overflow and cycles.
61
59
if self . goal . depth <= 10 {
62
60
let infcx = self . goal . infcx ;
@@ -75,17 +73,18 @@ impl<'a, 'tcx> InspectCandidate<'a, 'tcx> {
75
73
for & goal in & instantiated_goals {
76
74
let ( _, proof_tree) = infcx. evaluate_root_goal ( goal, GenerateProofTree :: Yes ) ;
77
75
let proof_tree = proof_tree. unwrap ( ) ;
78
- visitor. visit_goal ( & InspectGoal :: new (
76
+ try_visit ! ( visitor. visit_goal( & InspectGoal :: new(
79
77
infcx,
80
78
self . goal. depth + 1 ,
81
79
& proof_tree,
82
- ) ) ? ;
80
+ ) ) ) ;
83
81
}
84
82
85
- ControlFlow :: Continue ( ( ) )
86
- } ) ?;
83
+ V :: Result :: output ( )
84
+ } )
85
+ } else {
86
+ V :: Result :: output ( )
87
87
}
88
- ControlFlow :: Continue ( ( ) )
89
88
}
90
89
}
91
90
@@ -202,9 +201,9 @@ impl<'a, 'tcx> InspectGoal<'a, 'tcx> {
202
201
203
202
/// The public API to interact with proof trees.
204
203
pub trait ProofTreeVisitor < ' tcx > {
205
- type BreakTy ;
204
+ type Result : VisitorResult = ( ) ;
206
205
207
- fn visit_goal ( & mut self , goal : & InspectGoal < ' _ , ' tcx > ) -> ControlFlow < Self :: BreakTy > ;
206
+ fn visit_goal ( & mut self , goal : & InspectGoal < ' _ , ' tcx > ) -> Self :: Result ;
208
207
}
209
208
210
209
#[ extension( pub trait ProofTreeInferCtxtExt <' tcx>) ]
@@ -213,7 +212,7 @@ impl<'tcx> InferCtxt<'tcx> {
213
212
& self ,
214
213
goal : Goal < ' tcx , ty:: Predicate < ' tcx > > ,
215
214
visitor : & mut V ,
216
- ) -> ControlFlow < V :: BreakTy > {
215
+ ) -> V :: Result {
217
216
self . probe ( |_| {
218
217
let ( _, proof_tree) = self . evaluate_root_goal ( goal, GenerateProofTree :: Yes ) ;
219
218
let proof_tree = proof_tree. unwrap ( ) ;
0 commit comments