1
1
//! Trait solving using Chalk.
2
- use std:: {
3
- panic,
4
- sync:: { Arc , Mutex } ,
5
- } ;
2
+ use std:: { panic, sync:: Arc } ;
6
3
7
4
use chalk_ir:: cast:: Cast ;
8
5
use hir_def:: { expr:: ExprId , DefWithBodyId , ImplId , TraitId , TypeAliasId } ;
9
- use ra_db:: { impl_intern_key, salsa, Canceled , CrateId } ;
6
+ use ra_db:: { impl_intern_key, salsa, CrateId } ;
10
7
use ra_prof:: profile;
11
8
use rustc_hash:: FxHashSet ;
12
9
@@ -19,74 +16,6 @@ use self::chalk::{from_chalk, Interner, ToChalk};
19
16
pub ( crate ) mod chalk;
20
17
mod builtin;
21
18
22
- #[ derive( Debug , Clone ) ]
23
- pub struct TraitSolver {
24
- krate : CrateId ,
25
- inner : Arc < Mutex < chalk_solve:: Solver < Interner > > > ,
26
- }
27
-
28
- /// We need eq for salsa
29
- impl PartialEq for TraitSolver {
30
- fn eq ( & self , other : & TraitSolver ) -> bool {
31
- Arc :: ptr_eq ( & self . inner , & other. inner )
32
- }
33
- }
34
-
35
- impl Eq for TraitSolver { }
36
-
37
- impl TraitSolver {
38
- fn solve (
39
- & self ,
40
- db : & impl HirDatabase ,
41
- goal : & chalk_ir:: UCanonical < chalk_ir:: InEnvironment < chalk_ir:: Goal < Interner > > > ,
42
- ) -> Option < chalk_solve:: Solution < Interner > > {
43
- let context = ChalkContext { db, krate : self . krate } ;
44
- log:: debug!( "solve goal: {:?}" , goal) ;
45
- let mut solver = match self . inner . lock ( ) {
46
- Ok ( it) => it,
47
- // Our cancellation works via unwinding, but, as chalk is not
48
- // panic-safe, we need to make sure to propagate the cancellation.
49
- // Ideally, we should also make chalk panic-safe.
50
- Err ( _) => ra_db:: Canceled :: throw ( ) ,
51
- } ;
52
-
53
- let fuel = std:: cell:: Cell :: new ( CHALK_SOLVER_FUEL ) ;
54
-
55
- let solution = panic:: catch_unwind ( {
56
- let solver = panic:: AssertUnwindSafe ( & mut solver) ;
57
- let context = panic:: AssertUnwindSafe ( & context) ;
58
- move || {
59
- solver. 0 . solve_limited ( context. 0 , goal, || {
60
- context. 0 . db . check_canceled ( ) ;
61
- let remaining = fuel. get ( ) ;
62
- fuel. set ( remaining - 1 ) ;
63
- if remaining == 0 {
64
- log:: debug!( "fuel exhausted" ) ;
65
- }
66
- remaining > 0
67
- } )
68
- }
69
- } ) ;
70
-
71
- let solution = match solution {
72
- Ok ( it) => it,
73
- Err ( err) => {
74
- if err. downcast_ref :: < Canceled > ( ) . is_some ( ) {
75
- panic:: resume_unwind ( err)
76
- } else {
77
- log:: error!( "chalk panicked :-(" ) ;
78
- // Reset the solver, as it is not panic-safe.
79
- * solver = create_chalk_solver ( ) ;
80
- None
81
- }
82
- }
83
- } ;
84
-
85
- log:: debug!( "solve({:?}) => {:?}" , goal, solution) ;
86
- solution
87
- }
88
- }
89
-
90
19
/// This controls the maximum size of types Chalk considers. If we set this too
91
20
/// high, we can run into slow edge cases; if we set it too low, Chalk won't
92
21
/// find some solutions.
@@ -100,16 +29,6 @@ struct ChalkContext<'a, DB> {
100
29
krate : CrateId ,
101
30
}
102
31
103
- pub ( crate ) fn trait_solver_query (
104
- db : & ( impl HirDatabase + salsa:: Database ) ,
105
- krate : CrateId ,
106
- ) -> TraitSolver {
107
- db. salsa_runtime ( ) . report_untracked_read ( ) ;
108
- // krate parameter is just so we cache a unique solver per crate
109
- log:: debug!( "Creating new solver for crate {:?}" , krate) ;
110
- TraitSolver { krate, inner : Arc :: new ( Mutex :: new ( create_chalk_solver ( ) ) ) }
111
- }
112
-
113
32
fn create_chalk_solver ( ) -> chalk_solve:: Solver < Interner > {
114
33
let solver_choice =
115
34
chalk_solve:: SolverChoice :: SLG { max_size : CHALK_SOLVER_MAX_SIZE , expected_answers : None } ;
@@ -239,10 +158,35 @@ pub(crate) fn trait_solve_query(
239
158
// We currently don't deal with universes (I think / hope they're not yet
240
159
// relevant for our use cases?)
241
160
let u_canonical = chalk_ir:: UCanonical { canonical, universes : 1 } ;
242
- let solution = db . trait_solver ( krate ) . solve ( db, & u_canonical) ;
161
+ let solution = solve ( db, krate , & u_canonical) ;
243
162
solution. map ( |solution| solution_from_chalk ( db, solution) )
244
163
}
245
164
165
+ fn solve (
166
+ db : & impl HirDatabase ,
167
+ krate : CrateId ,
168
+ goal : & chalk_ir:: UCanonical < chalk_ir:: InEnvironment < chalk_ir:: Goal < Interner > > > ,
169
+ ) -> Option < chalk_solve:: Solution < Interner > > {
170
+ let context = ChalkContext { db, krate } ;
171
+ log:: debug!( "solve goal: {:?}" , goal) ;
172
+ let mut solver = create_chalk_solver ( ) ;
173
+
174
+ let fuel = std:: cell:: Cell :: new ( CHALK_SOLVER_FUEL ) ;
175
+
176
+ let solution = solver. solve_limited ( & context, goal, || {
177
+ context. db . check_canceled ( ) ;
178
+ let remaining = fuel. get ( ) ;
179
+ fuel. set ( remaining - 1 ) ;
180
+ if remaining == 0 {
181
+ log:: debug!( "fuel exhausted" ) ;
182
+ }
183
+ remaining > 0
184
+ } ) ;
185
+
186
+ log:: debug!( "solve({:?}) => {:?}" , goal, solution) ;
187
+ solution
188
+ }
189
+
246
190
fn solution_from_chalk (
247
191
db : & impl HirDatabase ,
248
192
solution : chalk_solve:: Solution < Interner > ,
0 commit comments