Struct flux_driver::callbacks::CrateChecker
source · struct CrateChecker<'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
cache: QueryCache,
- checker_config: CheckerConfig,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§cache: QueryCache
§checker_config: CheckerConfig
Implementations§
source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
fn matches_check_def(&self, def_id: LocalDefId) -> bool
fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
Auto Trait Implementations§
impl<'genv, 'tcx> !DynSend for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !DynSync for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+ checker_config: CheckerConfig,
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§cache: QueryCache
§checker_config: CheckerConfig
Implementations§
source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
sourcefn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
sourcefn matches_check_def(&self, def_id: LocalDefId) -> bool
sourcefn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
Auto Trait Implementations§
§impl<'genv, 'tcx> !DynSend for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !DynSync for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§impl<T, R> CollectAndApply<T, R> for T
§fn collect_and_apply<I, F>(iter: I, f: F) -> Rwhere
diff --git a/doc/flux_fixpoint/struct.Task.html b/doc/flux_fixpoint/struct.Task.html
index cda68229e0..3ddc229b21 100644
--- a/doc/flux_fixpoint/struct.Task.html
+++ b/doc/flux_fixpoint/struct.Task.html
@@ -9,7 +9,7 @@
}Fields§
§comments: Vec<String>
§constants: Vec<ConstInfo<T>>
§data_decls: Vec<DataDecl<T>>
§kvars: Vec<KVar<T>>
§constraint: Constraint<T>
§qualifiers: Vec<Qualifier<T>>
§scrape_quals: bool
Implementations§
source§impl<T: Types> Task<T>
sourcepub fn hash_with_default(&self) -> u64
sourcepub fn check_with_cache(
&self,
key: String,
- cache: &mut QueryCache
+ cache: &mut QueryCache
) -> Result<FixpointResult<T::Tag>>
sourcepub(crate) fn check(&self) -> Result<FixpointResult<T::Tag>>
Trait Implementations§
Auto Trait Implementations§
source§impl PartialEq for InferMode
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
§impl<T> AnyEq for T
source§impl<'tcx, T> ArenaAllocatable<'tcx, IsCopy> for Twhere
T: Copy,
source§fn allocate_on<'a>(self, arena: &'a Arena<'tcx>) -> &'a mut T
source§fn allocate_from_iter<'a>(
diff --git a/doc/flux_middle/intern/struct.Interned.html b/doc/flux_middle/intern/struct.Interned.html
index 591366e249..49b5d4e0ce 100644
--- a/doc/flux_middle/intern/struct.Interned.html
+++ b/doc/flux_middle/intern/struct.Interned.html
@@ -44,28 +44,28 @@
reductions for tuples and abstractions.
sourcepub fn to_loc(&self) -> Option<Loc>
sourcepub fn to_path(&self) -> Option<Path>
sourcepub fn is_abs(&self) -> bool
sourcepub fn eta_expand_abs(&self, inputs: &[Sort], output: Sort) -> Lambda
sourcepub fn fold_sort(sort: &Sort, f: impl FnMut(&Sort) -> Expr) -> Expr
sourcepub fn proj_and_reduce(&self, proj: FieldProj) -> Expr
Applies a projection to an expression and optimistically try to beta reduce it if possible.
-sourcepub fn flatten_conjs(&self) -> Vec<&Expr>
sourcepub fn flatten_conjs(&self) -> Vec<&Expr>
source§impl Interned<TyS>
sourcepub fn alias(kind: AliasKind, alias_ty: AliasTy) -> Ty
sourcepub fn opaque(
def_id: impl Into<DefId>,
args: GenericArgs,
refine_args: RefineArgs
-) -> Ty
sourcepub fn projection(alias_ty: AliasTy) -> Ty
sourcepub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
sourcepub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
sourcepub fn uninit() -> Ty
sourcepub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
sourcepub fn exists(ty: Binder<Ty>) -> Ty
sourcepub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
sourcepub fn discr(adt_def: AdtDef, place: Place) -> Ty
sourcepub fn unit() -> Ty
sourcepub fn bool() -> Ty
sourcepub fn int(int_ty: IntTy) -> Ty
sourcepub fn uint(uint_ty: UintTy) -> Ty
sourcepub fn param(param_ty: ParamTy) -> Ty
sourcepub fn downcast(
+) -> Ty
sourcepub fn projection(alias_ty: AliasTy) -> Ty
sourcepub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
sourcepub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
sourcepub fn uninit() -> Ty
sourcepub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
sourcepub fn exists(ty: Binder<Ty>) -> Ty
sourcepub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
sourcepub fn discr(adt_def: AdtDef, place: Place) -> Ty
sourcepub fn unit() -> Ty
sourcepub fn bool() -> Ty
sourcepub fn int(int_ty: IntTy) -> Ty
sourcepub fn uint(uint_ty: UintTy) -> Ty
sourcepub fn param(param_ty: ParamTy) -> Ty
sourcepub fn downcast(
adt: AdtDef,
args: GenericArgs,
ty: Ty,
variant: VariantIdx,
fields: List<Ty>
-) -> Ty
sourcepub fn blocked(ty: Ty) -> Ty
sourcepub fn str() -> Ty
sourcepub fn char() -> Ty
sourcepub fn float(float_ty: FloatTy) -> Ty
sourcepub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
sourcepub fn mk_slice(ty: Ty) -> Ty
sourcepub fn tuple(tys: impl Into<List<Ty>>) -> Ty
sourcepub fn array(ty: Ty, c: Const) -> Ty
sourcepub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
sourcepub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
sourcepub fn never() -> Ty
sourcepub fn unconstr(&self) -> (Ty, Expr)
sourcepub fn unblocked(&self) -> Ty
sourcepub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
-sourcepub fn is_uninit(&self) -> bool
sourcepub fn is_box(&self) -> bool
sourcepub fn is_struct(&self) -> bool
sourcepub fn is_array(&self) -> bool
sourcepub fn is_slice(&self) -> bool
sourcepub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
sourcepub fn identity_for_item(
+) -> Ty
sourcepub fn blocked(ty: Ty) -> Ty
sourcepub fn str() -> Ty
sourcepub fn char() -> Ty
sourcepub fn float(float_ty: FloatTy) -> Ty
sourcepub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
sourcepub fn mk_slice(ty: Ty) -> Ty
sourcepub fn tuple(tys: impl Into<List<Ty>>) -> Ty
sourcepub fn array(ty: Ty, c: Const) -> Ty
sourcepub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
sourcepub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
sourcepub fn never() -> Ty
sourcepub fn unconstr(&self) -> (Ty, Expr)
sourcepub fn unblocked(&self) -> Ty
sourcepub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
+sourcepub fn is_uninit(&self) -> bool
sourcepub fn is_box(&self) -> bool
sourcepub fn is_struct(&self) -> bool
sourcepub fn is_array(&self) -> bool
sourcepub fn is_slice(&self) -> bool
sourcepub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
sourcepub fn identity_for_item(
genv: GlobalEnv<'_, '_>,
def_id: impl Into<DefId>
-) -> QueryResult<Self>
sourcefn fill_item<F>(
+) -> QueryResult<Self>
sourcefn fill_item<F>(
genv: GlobalEnv<'_, '_>,
args: &mut Vec<GenericArg>,
generics: &Generics,
mk_kind: &mut F
) -> QueryResult<()>
sourcefn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> GenericArgsRef<'tcx>
source§impl Interned<[BoundVariableKind]>
sourcepub fn to_sort_list(&self) -> List<Sort>
source§impl Interned<[GenericArg]>
sourcepub fn as_closure(&self) -> ClosureArgs
sourcepub fn as_coroutine(&self) -> CoroutineArgs
Trait Implementations§
impl<T> Any for Twhere
+ checker_config: CheckerConfig,
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§cache: QueryCache
§checker_config: CheckerConfig
Implementations§
source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
sourcefn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
sourcefn matches_check_def(&self, def_id: LocalDefId) -> bool
sourcefn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
Auto Trait Implementations§
§impl<'genv, 'tcx> !DynSend for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !DynSync for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§impl<T, R> CollectAndApply<T, R> for T
§fn collect_and_apply<I, F>(iter: I, f: F) -> Rwhere
diff --git a/doc/flux_fixpoint/struct.Task.html b/doc/flux_fixpoint/struct.Task.html
index cda68229e0..3ddc229b21 100644
--- a/doc/flux_fixpoint/struct.Task.html
+++ b/doc/flux_fixpoint/struct.Task.html
@@ -9,7 +9,7 @@
}Fields§
§comments: Vec<String>
§constants: Vec<ConstInfo<T>>
§data_decls: Vec<DataDecl<T>>
§kvars: Vec<KVar<T>>
§constraint: Constraint<T>
§qualifiers: Vec<Qualifier<T>>
§scrape_quals: bool
Implementations§
source§impl<T: Types> Task<T>
sourcepub fn hash_with_default(&self) -> u64
sourcepub fn check_with_cache(
&self,
key: String,
- cache: &mut QueryCache
+ cache: &mut QueryCache
) -> Result<FixpointResult<T::Tag>>
sourcepub(crate) fn check(&self) -> Result<FixpointResult<T::Tag>>
Trait Implementations§
Auto Trait Implementations§
source§impl PartialEq for InferMode
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
§impl<T> AnyEq for T
source§impl<'tcx, T> ArenaAllocatable<'tcx, IsCopy> for Twhere
T: Copy,
source§fn allocate_on<'a>(self, arena: &'a Arena<'tcx>) -> &'a mut T
source§fn allocate_from_iter<'a>(
diff --git a/doc/flux_middle/intern/struct.Interned.html b/doc/flux_middle/intern/struct.Interned.html
index 591366e249..49b5d4e0ce 100644
--- a/doc/flux_middle/intern/struct.Interned.html
+++ b/doc/flux_middle/intern/struct.Interned.html
@@ -44,28 +44,28 @@
reductions for tuples and abstractions.
sourcepub fn to_loc(&self) -> Option<Loc>
sourcepub fn to_path(&self) -> Option<Path>
sourcepub fn is_abs(&self) -> bool
sourcepub fn eta_expand_abs(&self, inputs: &[Sort], output: Sort) -> Lambda
sourcepub fn fold_sort(sort: &Sort, f: impl FnMut(&Sort) -> Expr) -> Expr
sourcepub fn proj_and_reduce(&self, proj: FieldProj) -> Expr
Applies a projection to an expression and optimistically try to beta reduce it if possible.
-sourcepub fn flatten_conjs(&self) -> Vec<&Expr>
sourcepub fn flatten_conjs(&self) -> Vec<&Expr>
source§impl Interned<TyS>
sourcepub fn alias(kind: AliasKind, alias_ty: AliasTy) -> Ty
sourcepub fn opaque(
def_id: impl Into<DefId>,
args: GenericArgs,
refine_args: RefineArgs
-) -> Ty
sourcepub fn projection(alias_ty: AliasTy) -> Ty
sourcepub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
sourcepub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
sourcepub fn uninit() -> Ty
sourcepub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
sourcepub fn exists(ty: Binder<Ty>) -> Ty
sourcepub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
sourcepub fn discr(adt_def: AdtDef, place: Place) -> Ty
sourcepub fn unit() -> Ty
sourcepub fn bool() -> Ty
sourcepub fn int(int_ty: IntTy) -> Ty
sourcepub fn uint(uint_ty: UintTy) -> Ty
sourcepub fn param(param_ty: ParamTy) -> Ty
sourcepub fn downcast(
+) -> Ty
sourcepub fn projection(alias_ty: AliasTy) -> Ty
sourcepub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
sourcepub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
sourcepub fn uninit() -> Ty
sourcepub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
sourcepub fn exists(ty: Binder<Ty>) -> Ty
sourcepub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
sourcepub fn discr(adt_def: AdtDef, place: Place) -> Ty
sourcepub fn unit() -> Ty
sourcepub fn bool() -> Ty
sourcepub fn int(int_ty: IntTy) -> Ty
sourcepub fn uint(uint_ty: UintTy) -> Ty
sourcepub fn param(param_ty: ParamTy) -> Ty
sourcepub fn downcast(
adt: AdtDef,
args: GenericArgs,
ty: Ty,
variant: VariantIdx,
fields: List<Ty>
-) -> Ty
sourcepub fn blocked(ty: Ty) -> Ty
sourcepub fn str() -> Ty
sourcepub fn char() -> Ty
sourcepub fn float(float_ty: FloatTy) -> Ty
sourcepub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
sourcepub fn mk_slice(ty: Ty) -> Ty
sourcepub fn tuple(tys: impl Into<List<Ty>>) -> Ty
sourcepub fn array(ty: Ty, c: Const) -> Ty
sourcepub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
sourcepub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
sourcepub fn never() -> Ty
sourcepub fn unconstr(&self) -> (Ty, Expr)
sourcepub fn unblocked(&self) -> Ty
sourcepub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
-sourcepub fn is_uninit(&self) -> bool
sourcepub fn is_box(&self) -> bool
sourcepub fn is_struct(&self) -> bool
sourcepub fn is_array(&self) -> bool
sourcepub fn is_slice(&self) -> bool
sourcepub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
sourcepub fn identity_for_item(
+) -> Ty
sourcepub fn blocked(ty: Ty) -> Ty
sourcepub fn str() -> Ty
sourcepub fn char() -> Ty
sourcepub fn float(float_ty: FloatTy) -> Ty
sourcepub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
sourcepub fn mk_slice(ty: Ty) -> Ty
sourcepub fn tuple(tys: impl Into<List<Ty>>) -> Ty
sourcepub fn array(ty: Ty, c: Const) -> Ty
sourcepub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
sourcepub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
sourcepub fn never() -> Ty
sourcepub fn unconstr(&self) -> (Ty, Expr)
sourcepub fn unblocked(&self) -> Ty
sourcepub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
+sourcepub fn is_uninit(&self) -> bool
sourcepub fn is_box(&self) -> bool
sourcepub fn is_struct(&self) -> bool
sourcepub fn is_array(&self) -> bool
sourcepub fn is_slice(&self) -> bool
sourcepub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
sourcepub fn identity_for_item(
genv: GlobalEnv<'_, '_>,
def_id: impl Into<DefId>
-) -> QueryResult<Self>
sourcefn fill_item<F>(
+) -> QueryResult<Self>
sourcefn fill_item<F>(
genv: GlobalEnv<'_, '_>,
args: &mut Vec<GenericArg>,
generics: &Generics,
mk_kind: &mut F
) -> QueryResult<()>
sourcefn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> GenericArgsRef<'tcx>
source§impl Interned<[BoundVariableKind]>
sourcepub fn to_sort_list(&self) -> List<Sort>
source§impl Interned<[GenericArg]>
sourcepub fn as_closure(&self) -> ClosureArgs
sourcepub fn as_coroutine(&self) -> CoroutineArgs
Trait Implementations§
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§cache: QueryCache
§checker_config: CheckerConfig
Implementations§
source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
fn matches_check_def(&self, def_id: LocalDefId) -> bool
fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
Auto Trait Implementations§
impl<'genv, 'tcx> !DynSend for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !DynSync for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Blanket Implementations§
source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
§impl<T, R> CollectAndApply<T, R> for T
impl<T, R> CollectAndApply<T, R> for T
§fn collect_and_apply<I, F>(iter: I, f: F) -> Rwhere
diff --git a/doc/flux_fixpoint/struct.Task.html b/doc/flux_fixpoint/struct.Task.html
index cda68229e0..3ddc229b21 100644
--- a/doc/flux_fixpoint/struct.Task.html
+++ b/doc/flux_fixpoint/struct.Task.html
@@ -9,7 +9,7 @@
}Fields§
§comments: Vec<String>
§constants: Vec<ConstInfo<T>>
§data_decls: Vec<DataDecl<T>>
§kvars: Vec<KVar<T>>
§constraint: Constraint<T>
§qualifiers: Vec<Qualifier<T>>
§scrape_quals: bool
Implementations§
source§impl<T: Types> Task<T>
sourcepub fn hash_with_default(&self) -> u64
sourcepub fn check_with_cache(
&self,
key: String,
- cache: &mut QueryCache
+ cache: &mut QueryCache
) -> Result<FixpointResult<T::Tag>>
sourcepub(crate) fn check(&self) -> Result<FixpointResult<T::Tag>>
Trait Implementations§
Auto Trait Implementations§
source§impl PartialEq for InferMode
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
fn collect_and_apply<I, F>(iter: I, f: F) -> Rwhere
diff --git a/doc/flux_fixpoint/struct.Task.html b/doc/flux_fixpoint/struct.Task.html
index cda68229e0..3ddc229b21 100644
--- a/doc/flux_fixpoint/struct.Task.html
+++ b/doc/flux_fixpoint/struct.Task.html
@@ -9,7 +9,7 @@
}Fields§
§comments: Vec<String>
§constants: Vec<ConstInfo<T>>
§data_decls: Vec<DataDecl<T>>
§kvars: Vec<KVar<T>>
§constraint: Constraint<T>
§qualifiers: Vec<Qualifier<T>>
§scrape_quals: bool
Implementations§
source§impl<T: Types> Task<T>
sourcepub fn hash_with_default(&self) -> u64
sourcepub fn check_with_cache(
&self,
key: String,
- cache: &mut QueryCache
+ cache: &mut QueryCache
) -> Result<FixpointResult<T::Tag>>
sourcepub(crate) fn check(&self) -> Result<FixpointResult<T::Tag>>
Trait Implementations§
Auto Trait Implementations§
source§impl PartialEq for InferMode
source§impl SliceInternable for InferMode
source§fn storage() -> &'static InternStorage<[Self]>
source§impl Copy for InferMode
source§impl Eq for InferMode
source§impl StructuralPartialEq for InferMode
Auto Trait Implementations§
§impl DynSend for InferMode
§impl DynSync for InferMode
§impl Freeze for InferMode
§impl RefUnwindSafe for InferMode
§impl Send for InferMode
§impl Sync for InferMode
§impl Unpin for InferMode
§impl UnwindSafe for InferMode
Blanket Implementations§
Fields§
§comments: Vec<String>
§constants: Vec<ConstInfo<T>>
§data_decls: Vec<DataDecl<T>>
§kvars: Vec<KVar<T>>
§constraint: Constraint<T>
§qualifiers: Vec<Qualifier<T>>
§scrape_quals: bool
Implementations§
source§impl<T: Types> Task<T>
impl<T: Types> Task<T>
pub fn hash_with_default(&self) -> u64
pub fn check_with_cache( &self, key: String, - cache: &mut QueryCache + cache: &mut QueryCache ) -> Result<FixpointResult<T::Tag>>
pub(crate) fn check(&self) -> Result<FixpointResult<T::Tag>>
Trait Implementations§
Auto Trait Implementations§
source§impl PartialEq for InferMode
impl PartialEq for InferMode
source§impl SliceInternable for InferMode
impl SliceInternable for InferMode
fn storage() -> &'static InternStorage<[Self]>
impl Copy for InferMode
impl Eq for InferMode
impl StructuralPartialEq for InferMode
impl DynSend for InferMode
impl DynSync for InferMode
impl Freeze for InferMode
impl RefUnwindSafe for InferMode
impl Send for InferMode
impl Sync for InferMode
impl Unpin for InferMode
impl UnwindSafe for InferMode
source§impl SliceInternable for InferMode
impl SliceInternable for InferMode
fn storage() -> &'static InternStorage<[Self]>
impl Copy for InferMode
impl Eq for InferMode
impl StructuralPartialEq for InferMode
Auto Trait Implementations§
impl DynSend for InferMode
impl DynSync for InferMode
impl Freeze for InferMode
impl RefUnwindSafe for InferMode
impl Send for InferMode
impl Sync for InferMode
impl Unpin for InferMode
impl UnwindSafe for InferMode
Blanket Implementations§
§impl<T> AnyEq for T
impl<T> AnyEq for T
source§impl<'tcx, T> ArenaAllocatable<'tcx, IsCopy> for Twhere
T: Copy,
impl<'tcx, T> ArenaAllocatable<'tcx, IsCopy> for Twhere
T: Copy,
fn allocate_on<'a>(self, arena: &'a Arena<'tcx>) -> &'a mut T
fn allocate_from_iter<'a>( diff --git a/doc/flux_middle/intern/struct.Interned.html b/doc/flux_middle/intern/struct.Interned.html index 591366e249..49b5d4e0ce 100644 --- a/doc/flux_middle/intern/struct.Interned.html +++ b/doc/flux_middle/intern/struct.Interned.html @@ -44,28 +44,28 @@ reductions for tuples and abstractions.
pub fn to_loc(&self) -> Option<Loc>
pub fn to_path(&self) -> Option<Path>
pub fn is_abs(&self) -> bool
pub fn eta_expand_abs(&self, inputs: &[Sort], output: Sort) -> Lambda
pub fn fold_sort(sort: &Sort, f: impl FnMut(&Sort) -> Expr) -> Expr
sourcepub fn proj_and_reduce(&self, proj: FieldProj) -> Expr
pub fn proj_and_reduce(&self, proj: FieldProj) -> Expr
Applies a projection to an expression and optimistically try to beta reduce it if possible.
-pub fn flatten_conjs(&self) -> Vec<&Expr>
pub fn flatten_conjs(&self) -> Vec<&Expr>
source§impl Interned<TyS>
impl Interned<TyS>
pub fn alias(kind: AliasKind, alias_ty: AliasTy) -> Ty
pub fn opaque( def_id: impl Into<DefId>, args: GenericArgs, refine_args: RefineArgs -) -> Ty
pub fn projection(alias_ty: AliasTy) -> Ty
pub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
pub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
pub fn uninit() -> Ty
pub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
pub fn exists(ty: Binder<Ty>) -> Ty
pub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
pub fn discr(adt_def: AdtDef, place: Place) -> Ty
pub fn unit() -> Ty
pub fn bool() -> Ty
pub fn int(int_ty: IntTy) -> Ty
pub fn uint(uint_ty: UintTy) -> Ty
pub fn param(param_ty: ParamTy) -> Ty
pub fn downcast( +) -> Ty
pub fn projection(alias_ty: AliasTy) -> Ty
pub fn ptr(pk: impl Into<PtrKind>, path: impl Into<Path>) -> Ty
pub fn constr(p: impl Into<Expr>, ty: Ty) -> Ty
pub fn uninit() -> Ty
pub fn indexed(bty: BaseTy, idx: impl Into<Expr>) -> Ty
pub fn exists(ty: Binder<Ty>) -> Ty
pub fn exists_with_constr(bty: BaseTy, pred: Expr) -> Ty
pub fn discr(adt_def: AdtDef, place: Place) -> Ty
pub fn unit() -> Ty
pub fn bool() -> Ty
pub fn int(int_ty: IntTy) -> Ty
pub fn uint(uint_ty: UintTy) -> Ty
pub fn param(param_ty: ParamTy) -> Ty
pub fn downcast( adt: AdtDef, args: GenericArgs, ty: Ty, variant: VariantIdx, fields: List<Ty> -) -> Ty
pub fn blocked(ty: Ty) -> Ty
pub fn str() -> Ty
pub fn char() -> Ty
pub fn float(float_ty: FloatTy) -> Ty
pub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
pub fn mk_slice(ty: Ty) -> Ty
pub fn tuple(tys: impl Into<List<Ty>>) -> Ty
pub fn array(ty: Ty, c: Const) -> Ty
pub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
pub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
pub fn never() -> Ty
pub fn unconstr(&self) -> (Ty, Expr)
pub fn unblocked(&self) -> Ty
pub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
pub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
pub fn is_uninit(&self) -> bool
pub fn is_box(&self) -> bool
pub fn is_struct(&self) -> bool
pub fn is_array(&self) -> bool
pub fn is_slice(&self) -> bool
pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
impl Interned<[GenericArg]>
pub fn identity_for_item( +) -> Ty
pub fn blocked(ty: Ty) -> Ty
pub fn str() -> Ty
pub fn char() -> Ty
pub fn float(float_ty: FloatTy) -> Ty
pub fn mk_ref(region: Region, ty: Ty, mutbl: Mutability) -> Ty
pub fn mk_slice(ty: Ty) -> Ty
pub fn tuple(tys: impl Into<List<Ty>>) -> Ty
pub fn array(ty: Ty, c: Const) -> Ty
pub fn closure(did: DefId, tys: impl Into<List<Ty>>) -> Ty
pub fn coroutine(did: DefId, resume_ty: Ty, upvar_tys: List<Ty>) -> Ty
pub fn never() -> Ty
pub fn unconstr(&self) -> (Ty, Expr)
pub fn unblocked(&self) -> Ty
pub fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> Ty<'tcx>
sourcepub fn is_integral(&self) -> bool
pub fn is_integral(&self) -> bool
Whether the type is an int
or a uint
pub fn is_uninit(&self) -> bool
pub fn is_box(&self) -> bool
pub fn is_struct(&self) -> bool
pub fn is_array(&self) -> bool
pub fn is_slice(&self) -> bool
pub fn as_bty_skipping_existentials(&self) -> Option<&BaseTy>
source§impl Interned<[GenericArg]>
impl Interned<[GenericArg]>
pub fn identity_for_item( genv: GlobalEnv<'_, '_>, def_id: impl Into<DefId> -) -> QueryResult<Self>
fn fill_item<F>( +) -> QueryResult<Self>
fn fill_item<F>( genv: GlobalEnv<'_, '_>, args: &mut Vec<GenericArg>, generics: &Generics, mk_kind: &mut F ) -> QueryResult<()>
fn to_rustc<'tcx>(&self, tcx: TyCtxt<'tcx>) -> GenericArgsRef<'tcx>
source§impl Interned<[BoundVariableKind]>
impl Interned<[BoundVariableKind]>
pub fn to_sort_list(&self) -> List<Sort>
source§impl Interned<[GenericArg]>
impl Interned<[GenericArg]>
pub fn as_closure(&self) -> ClosureArgs
pub fn as_coroutine(&self) -> CoroutineArgs
source§impl Interned<[BoundVariableKind]>
impl Interned<[BoundVariableKind]>
pub fn to_sort_list(&self) -> List<Sort>
source§impl Interned<[GenericArg]>
impl Interned<[GenericArg]>
pub fn as_closure(&self) -> ClosureArgs
pub fn as_coroutine(&self) -> CoroutineArgs
Trait Implementations§
source§impl<D, T> Decodable<D> for Interned<T>where
diff --git a/doc/flux_middle/intern/trait.Internable.html b/doc/flux_middle/intern/trait.Internable.html
index 1672b71849..ae418e9ad2 100644
--- a/doc/flux_middle/intern/trait.Internable.html
+++ b/doc/flux_middle/intern/trait.Internable.html
@@ -2,4 +2,4 @@
// Required method
fn storage() -> &'static InternStorage<Self>;
}Required Methods§
sourcefn storage() -> &'static InternStorage<Self>
Object Safety§
This trait is not object safe.Implementations on Foreign Types§
source§impl<T> Internable for [T]where
- T: SliceInternable,
source§fn storage() -> &'static InternStorage<Self>
Implementors§
source§impl Internable for ExprS
source§impl Internable for flux_middle::rty::AdtDefData
source§impl Internable for AdtSortDefData
source§impl Internable for flux_middle::rty::TyS
source§impl Internable for flux_middle::rustc::ty::AdtDefData
source§impl Internable for flux_middle::rustc::ty::TyS
\ No newline at end of file
+ T: SliceInternable,
impl<D, T> Decodable<D> for Interned<T>where
diff --git a/doc/flux_middle/intern/trait.Internable.html b/doc/flux_middle/intern/trait.Internable.html
index 1672b71849..ae418e9ad2 100644
--- a/doc/flux_middle/intern/trait.Internable.html
+++ b/doc/flux_middle/intern/trait.Internable.html
@@ -2,4 +2,4 @@
// Required method
fn storage() -> &'static InternStorage<Self>;
}Required Methods§
sourcefn storage() -> &'static InternStorage<Self>
Object Safety§
This trait is not object safe.Implementations on Foreign Types§
source§impl<T> Internable for [T]where
- T: SliceInternable,
source§fn storage() -> &'static InternStorage<Self>
Implementors§
source§impl Internable for ExprS
source§impl Internable for flux_middle::rty::AdtDefData
source§impl Internable for AdtSortDefData
source§impl Internable for flux_middle::rty::TyS
source§impl Internable for flux_middle::rustc::ty::AdtDefData
source§impl Internable for flux_middle::rustc::ty::TyS
\ No newline at end of file
+ T: SliceInternable,
Required Methods§
fn storage() -> &'static InternStorage<Self>
Object Safety§
This trait is not object safe.