Trait chalk_integration::query::LoweringDatabase

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>

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.

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

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.

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>

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>

fn checked_program(&self) -> Result<Arc<Program>, ChalkError>

The lowered IR, with coherence, orphan, and WF checks performed.

fn environment(&self) -> Result<Arc<ProgramEnvironment>, ChalkError>

The program as logic.

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).

Implementors

impl<DB> LoweringDatabase for DB

where DB: RustIrDatabase<ChalkIr> + Database + Upcast<dyn RustIrDatabase<ChalkIr>> + Database + HasQueryGroup<Lowering>,