flux_middle/
cstore.rs

1use std::rc::Rc;
2
3use rustc_data_structures::unord::{UnordMap, UnordSet};
4use rustc_hir::def_id::CrateNum;
5use rustc_span::def_id::DefId;
6
7use crate::{PanicSpec, def_id::FluxDefId, queries::QueryResult, rty};
8
9pub type OptResult<T> = Option<QueryResult<T>>;
10
11pub trait CrateStore {
12    fn fn_sig(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::PolyFnSig>>;
13    fn adt_def(&self, def_id: DefId) -> OptResult<rty::AdtDef>;
14    fn adt_sort_def(&self, def_id: DefId) -> OptResult<rty::AdtSortDef>;
15    fn generics_of(&self, def_id: DefId) -> OptResult<rty::Generics>;
16    fn refinement_generics_of(
17        &self,
18        def_id: DefId,
19    ) -> OptResult<rty::EarlyBinder<rty::RefinementGenerics>>;
20    fn item_bounds(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::Clauses>>;
21    fn predicates_of(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::GenericPredicates>>;
22    fn assoc_refinements_of(&self, def_id: DefId) -> OptResult<rty::AssocRefinements>;
23    fn constant_info(&self, def_id: DefId) -> OptResult<rty::ConstantInfo>;
24    fn static_info(&self, def_id: DefId) -> OptResult<rty::StaticInfo>;
25    fn assoc_refinements_def(&self, key: FluxDefId) -> OptResult<rty::EarlyBinder<rty::Lambda>>;
26    fn default_assoc_refinements_def(
27        &self,
28        key: FluxDefId,
29    ) -> OptResult<Option<rty::EarlyBinder<rty::Lambda>>>;
30    fn sort_of_assoc_reft(&self, key: FluxDefId) -> OptResult<rty::EarlyBinder<rty::FuncSort>>;
31    fn variants_of(
32        &self,
33        def_id: DefId,
34    ) -> OptResult<rty::Opaqueness<rty::EarlyBinder<rty::PolyVariants>>>;
35    fn type_of(&self, def_id: DefId) -> OptResult<rty::EarlyBinder<rty::TyOrCtor>>;
36    fn normalized_defns(&self, krate: CrateNum) -> Rc<rty::NormalizedDefns>;
37    fn func_sort(&self, def_id: FluxDefId) -> Option<rty::PolyFuncSort>;
38    fn func_span(&self, def_id: FluxDefId) -> Option<rustc_span::Span>;
39    fn sort_decl_param_count(&self, def_id: FluxDefId) -> Option<usize>;
40    fn no_panic(&self, def_id: DefId) -> Option<bool>;
41    fn assume_parametric_params(&self, def_id: DefId) -> Option<UnordSet<u32>>;
42    fn inferred_no_panic(&self, krate: CrateNum) -> Rc<UnordMap<DefId, PanicSpec>>;
43    fn has_crate(&self, krate: CrateNum) -> bool;
44}
45
46pub type CrateStoreDyn = dyn CrateStore;
flux_middle/cstore.rs

flux_middle/
cstore.rs
