Trait chalk_integration::query::LoweringDatabase
source · pub trait LoweringDatabase: Database + HasQueryGroup<Lowering> + RustIrDatabase<ChalkIr> + Database + Upcast<dyn RustIrDatabase<ChalkIr>> {
// Required methods
fn program_text(&self) -> Arc<String>;
fn set_program_text(&mut self, value__: Arc<String>);
fn set_program_text_with_durability(
&mut self,
value__: Arc<String>,
durability__: Durability,
);
fn solver_choice(&self) -> SolverChoice;
fn set_solver_choice(&mut self, value__: SolverChoice);
fn set_solver_choice_with_durability(
&mut self,
value__: SolverChoice,
durability__: Durability,
);
fn program_ir(&self) -> Result<Arc<Program>, ChalkError>;
fn coherence(
&self,
) -> Result<BTreeMap<TraitId<ChalkIr>, Arc<SpecializationPriorities<ChalkIr>>>, ChalkError>;
fn orphan_check(&self) -> Result<(), ChalkError>;
fn checked_program(&self) -> Result<Arc<Program>, ChalkError>;
fn environment(&self) -> Result<Arc<ProgramEnvironment>, ChalkError>;
fn solver(&self) -> ArcEq<Mutex<Box<dyn Solver<ChalkIr>>>>;
}
Required Methods§
fn program_text(&self) -> Arc<String>
sourcefn set_program_text(&mut self, value__: Arc<String>)
fn set_program_text(&mut self, value__: Arc<String>)
Set the value of the program_text
input.
See program_text
for details.
Note: Setting values will trigger cancellation of any ongoing queries; this method blocks until those queries have been cancelled.
sourcefn set_program_text_with_durability(
&mut self,
value__: Arc<String>,
durability__: Durability,
)
fn set_program_text_with_durability( &mut self, value__: Arc<String>, durability__: Durability, )
Set the value of the program_text
input and promise
that its value will never change again.
See program_text
for details.
Note: Setting values will trigger cancellation of any ongoing queries; this method blocks until those queries have been cancelled.
fn solver_choice(&self) -> SolverChoice
sourcefn set_solver_choice(&mut self, value__: SolverChoice)
fn set_solver_choice(&mut self, value__: SolverChoice)
Set the value of the solver_choice
input.
See solver_choice
for details.
Note: Setting values will trigger cancellation of any ongoing queries; this method blocks until those queries have been cancelled.
sourcefn set_solver_choice_with_durability(
&mut self,
value__: SolverChoice,
durability__: Durability,
)
fn set_solver_choice_with_durability( &mut self, value__: SolverChoice, durability__: Durability, )
Set the value of the solver_choice
input and promise
that its value will never change again.
See solver_choice
for details.
Note: Setting values will trigger cancellation of any ongoing queries; this method blocks until those queries have been cancelled.
fn program_ir(&self) -> Result<Arc<Program>, ChalkError>
sourcefn coherence(
&self,
) -> Result<BTreeMap<TraitId<ChalkIr>, Arc<SpecializationPriorities<ChalkIr>>>, ChalkError>
fn coherence( &self, ) -> Result<BTreeMap<TraitId<ChalkIr>, Arc<SpecializationPriorities<ChalkIr>>>, ChalkError>
Performs coherence check and computes which impls specialize one another (the “specialization priorities”).
fn orphan_check(&self) -> Result<(), ChalkError>
sourcefn checked_program(&self) -> Result<Arc<Program>, ChalkError>
fn checked_program(&self) -> Result<Arc<Program>, ChalkError>
The lowered IR, with coherence, orphan, and WF checks performed.
sourcefn environment(&self) -> Result<Arc<ProgramEnvironment>, ChalkError>
fn environment(&self) -> Result<Arc<ProgramEnvironment>, ChalkError>
The program as logic.
sourcefn solver(&self) -> ArcEq<Mutex<Box<dyn Solver<ChalkIr>>>>
fn solver(&self) -> ArcEq<Mutex<Box<dyn Solver<ChalkIr>>>>
Creates the solver we can use to solve goals. This solver stores intermediate, cached state, which is why it is behind a mutex. Moreover, if the set of program clauses change, that cached state becomes invalid, so the query is marked as volatile, thus ensuring that the solver is recreated in every revision (i.e., each time source program changes).