11//! Trait solving using Chalk.
2- use std:: {
3- panic,
4- sync:: { Arc , Mutex } ,
5- } ;
2+ use std:: { panic, sync:: Arc } ;
63
74use chalk_ir:: cast:: Cast ;
85use 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 } ;
107use ra_prof:: profile;
118use rustc_hash:: FxHashSet ;
129
@@ -19,74 +16,6 @@ use self::chalk::{from_chalk, Interner, ToChalk};
1916pub ( crate ) mod chalk;
2017mod builtin;
2118
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-
9019/// This controls the maximum size of types Chalk considers. If we set this too
9120/// high, we can run into slow edge cases; if we set it too low, Chalk won't
9221/// find some solutions.
@@ -100,16 +29,6 @@ struct ChalkContext<'a, DB> {
10029 krate : CrateId ,
10130}
10231
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-
11332fn create_chalk_solver ( ) -> chalk_solve:: Solver < Interner > {
11433 let solver_choice =
11534 chalk_solve:: SolverChoice :: SLG { max_size : CHALK_SOLVER_MAX_SIZE , expected_answers : None } ;
@@ -239,10 +158,35 @@ pub(crate) fn trait_solve_query(
239158 // We currently don't deal with universes (I think / hope they're not yet
240159 // relevant for our use cases?)
241160 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) ;
243162 solution. map ( |solution| solution_from_chalk ( db, solution) )
244163}
245164
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+
246190fn solution_from_chalk (
247191 db : & impl HirDatabase ,
248192 solution : chalk_solve:: Solution < Interner > ,
0 commit comments