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_fhir_analysis/conv/errors/index.html b/doc/flux_fhir_analysis/conv/errors/index.html
index 3b608aa7ff..40c805915f 100644
--- a/doc/flux_fhir_analysis/conv/errors/index.html
+++ b/doc/flux_fhir_analysis/conv/errors/index.html
@@ -1 +1 @@
-flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
+flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
index 1a42b647fc..865cb8a773 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
@@ -1,8 +1,8 @@
-AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
+AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
span: Span,
name: Ident,
-}
Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
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_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
index c639ddebbc..0efdde4d5e 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
@@ -1,7 +1,7 @@
-AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
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_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
index bacb14b497..c19df9e3c8 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
@@ -1,7 +1,7 @@
-InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
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_fhir_analysis/conv/fn.bug_on_infer_sort.html b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
index 598ac05698..b52fede725 100644
--- a/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
@@ -1 +1 @@
-bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
+bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
index 6a867e86a2..e34d184e52 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
@@ -1,4 +1,4 @@
-conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
+conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
genv: GlobalEnv<'_, '_>,
func: &SpecFunc<'_>
) -> QueryResult<SpecFuncDecl>
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
index fe32db2a97..b557ca174d 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
@@ -1,4 +1,4 @@
-conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
+conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
genv: GlobalEnv<'_, '_>,
fsort: &FuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
index 710c51a3b7..b70c272bcc 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_lit.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
@@ -1 +1 @@
-conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
+conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
index bff8c4fd4b..d71f87000c 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
@@ -1,4 +1,4 @@
-conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
+conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
genv: GlobalEnv<'_, '_>,
sort: &PolyFuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
index d15979ee29..7ac1428109 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
@@ -1,4 +1,4 @@
-conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
+conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
index f1e2ef2f52..977b51cb9b 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
@@ -1,4 +1,4 @@
-conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
+conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
genv: GlobalEnv<'_, '_>,
sort: &Sort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
index 20cd1ac129..7030b959ab 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
@@ -1,4 +1,4 @@
-conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
+conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
genv: GlobalEnv<'_, '_>,
path: &SortPath<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
index 082cab288f..8c81f6cf98 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
@@ -1,4 +1,4 @@
-conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
+conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
genv: GlobalEnv<'_, '_>,
sorts: &[Sort<'_>],
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
index 27eeab02a3..82d056f8fd 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
@@ -1 +1 @@
-conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
+conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
index 002de1a000..ae912c0675 100644
--- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
@@ -1,4 +1,4 @@
-resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
+resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html
index df109044a8..fcaa02a9bb 100644
--- a/doc/flux_fhir_analysis/conv/index.html
+++ b/doc/flux_fhir_analysis/conv/index.html
@@ -1,4 +1,4 @@
-flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
+flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
well-formedness implies:
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
index 4bf3ced369..638f2a67dd 100644
--- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
+++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
@@ -1,7 +1,7 @@
ConvCtxt in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::ConvCtxt
source · pub struct ConvCtxt<'a, 'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>
) -> Self
sourcefn conv_generic_bounds(
@@ -63,74 +63,73 @@
&self,
env: &mut Env,
constr: &Constraint<'_>
-) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
+) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
&self,
env: &mut Env,
- alias: &AliasReft<'_>,
- func_args: &[Expr<'_>]
-) -> QueryResult<Expr>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
+ alias: &AliasReft<'_>
+) -> QueryResult<AliasReft>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
&self,
env: &mut Env,
qself: &Ty<'_>,
assoc_segment: &PathSegment<'_>
-) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
-sourcefn probe_type_param_bounds(
+) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
+sourcefn probe_type_param_bounds(
&self,
param_did: LocalDefId,
assoc_ident: Ident
-) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
+) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
&self,
all_candidates: impl Fn() -> I,
assoc_ident: Ident
) -> Result<TraitRef<'tcx>, ErrorGuaranteed>where
- I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
+ I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
&self,
item_generics: &Generics,
trait_ref: TraitRef<'tcx>
-) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
+) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
&self,
env: &mut Env,
arg: &RefineArg<'_>
-) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
+) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>]
-) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
+) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>],
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn fill_generic_args_defaults(
+) -> QueryResult
sourcefn fill_generic_args_defaults(
&self,
def_id: DefId,
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn conv_ty_to_generic_arg(
+) -> QueryResult
sourcefn conv_ty_to_generic_arg(
&self,
env: &mut Env,
kind: GenericParamDefKind,
ty: &Ty<'_>
-) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
+) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
&self,
kind: GenericParamDefKind,
ty_span: Span,
ty: &Ty
-) -> QueryResult<GenericArg>
sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
+) -> QueryResult<GenericArg>sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
if the type cannot be converted into a rty::SubsetTy
.
-sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
+
sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
&self,
env: &mut Env,
exprs: &[Expr<'_>]
-) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
+) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
&self,
env: &mut Env,
invariants: &[Expr<'_>]
-) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
+) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
&self,
env: &mut Env,
invariant: &Expr<'_>
-) -> QueryResult<Invariant>
sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<Invariant>sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, '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_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html
index 00b4c9449e..533f2f4f30 100644
--- a/doc/flux_fhir_analysis/conv/struct.Env.html
+++ b/doc/flux_fhir_analysis/conv/struct.Env.html
@@ -1,11 +1,11 @@
Env in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Env
source · pub(crate) struct Env {
layers: Vec<Layer>,
early_bound: FxIndexMap<ParamId, (Symbol, Sort)>,
-}
Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
+}Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
genv: GlobalEnv<'_, '_>,
early_bound: &[RefineParam<'_>],
wfckresults: &WfckResults<'_>
-) -> QueryResult<Self>
sourcefn depth(&self) -> usize
sourcefn push_layer(&mut self, layer: Layer)
sourcefn pop_layer(&mut self) -> Layer
sourcefn top_layer(&self) -> &Layer
sourcefn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>
sourcefn to_early_bound_vars(&self) -> List<Expr>
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
Blanket Implementations§
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
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_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html
index 11204b4cea..262d0e7c41 100644
--- a/doc/flux_fhir_analysis/conv/struct.Layer.html
+++ b/doc/flux_fhir_analysis/conv/struct.Layer.html
@@ -1,25 +1,25 @@
Layer in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Layer
source · struct Layer {
map: FxIndexMap<ParamId, ParamEntry>,
kind: LayerKind,
-}
Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
+}Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
cx: &ConvCtxt<'_, '_, '_>,
params: &[RefineParam<'_>],
kind: LayerKind
-) -> QueryResult<Self>
sourcefn list(
+) -> QueryResult<Self>
sourcefn list(
cx: &ConvCtxt<'_, '_, '_>,
bound_regions: u32,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn coalesce(
+) -> QueryResult<Self>
sourcefn coalesce(
cx: &ConvCtxt<'_, '_, '_>,
def_id: DefId,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
+) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
+) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
&self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<List<BoundVariableKind>>sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
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_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
index 4c69f4b5ac..783ca37a9c 100644
--- a/doc/flux_fhir_analysis/conv/struct.LookupResult.html
+++ b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
@@ -2,7 +2,7 @@
kind: LookupResultKind<'a>,
span: Span,
}Fields§
§kind: LookupResultKind<'a>
§span: Span
The span of the variable that originated the lookup. Used to report bugs.
-Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
Blanket Implementations§
source§impl<T> Any for Twhere
+Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
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_fhir_analysis/conv/struct.ParamEntry.html b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
index 51baaa0039..8352b066e6 100644
--- a/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
+++ b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
@@ -2,7 +2,7 @@
name: Symbol,
sort: Sort,
mode: InferMode,
-}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
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_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
index 3ba1eed611..fa04e67bc8 100644
--- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
+++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
@@ -11,7 +11,7 @@
self,
f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>)
) -> Result<(), ErrorGuaranteed>sourcefn check_func_params_uses(&mut self, expr: &Expr<'_>, is_top_level_conj: bool)
Checks that refinement parameters of function sort are used in allowed positions.
-sourcefn check_params_are_value_determined(&mut self, params: &[RefineParam<'_>])
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
Blanket Implementations§
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, '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_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
index 76e6dea020..ec167a3d6e 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
@@ -4,7 +4,7 @@
}Fields§
§infcx: &'a mut InferCtxt<'genv, 'tcx>
§errors: Errors<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> Result<(), ErrorGuaranteed>sourcefn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, '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_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
index 8ce074b905..a5811de32d 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
@@ -1,6 +1,6 @@
InferCtxt in flux_fhir_analysis::wf::sortck - Rust Struct flux_fhir_analysis::
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_fhir_analysis/conv/errors/index.html b/doc/flux_fhir_analysis/conv/errors/index.html
index 3b608aa7ff..40c805915f 100644
--- a/doc/flux_fhir_analysis/conv/errors/index.html
+++ b/doc/flux_fhir_analysis/conv/errors/index.html
@@ -1 +1 @@
-flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
+flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
index 1a42b647fc..865cb8a773 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
@@ -1,8 +1,8 @@
-AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
+AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
span: Span,
name: Ident,
-}
Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
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_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
index c639ddebbc..0efdde4d5e 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
@@ -1,7 +1,7 @@
-AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
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_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
index bacb14b497..c19df9e3c8 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
@@ -1,7 +1,7 @@
-InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
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_fhir_analysis/conv/fn.bug_on_infer_sort.html b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
index 598ac05698..b52fede725 100644
--- a/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
@@ -1 +1 @@
-bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
+bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
index 6a867e86a2..e34d184e52 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
@@ -1,4 +1,4 @@
-conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
+conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
genv: GlobalEnv<'_, '_>,
func: &SpecFunc<'_>
) -> QueryResult<SpecFuncDecl>
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
index fe32db2a97..b557ca174d 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
@@ -1,4 +1,4 @@
-conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
+conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
genv: GlobalEnv<'_, '_>,
fsort: &FuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
index 710c51a3b7..b70c272bcc 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_lit.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
@@ -1 +1 @@
-conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
+conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
index bff8c4fd4b..d71f87000c 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
@@ -1,4 +1,4 @@
-conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
+conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
genv: GlobalEnv<'_, '_>,
sort: &PolyFuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
index d15979ee29..7ac1428109 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
@@ -1,4 +1,4 @@
-conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
+conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
index f1e2ef2f52..977b51cb9b 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
@@ -1,4 +1,4 @@
-conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
+conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
genv: GlobalEnv<'_, '_>,
sort: &Sort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
index 20cd1ac129..7030b959ab 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
@@ -1,4 +1,4 @@
-conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
+conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
genv: GlobalEnv<'_, '_>,
path: &SortPath<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
index 082cab288f..8c81f6cf98 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
@@ -1,4 +1,4 @@
-conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
+conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
genv: GlobalEnv<'_, '_>,
sorts: &[Sort<'_>],
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
index 27eeab02a3..82d056f8fd 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
@@ -1 +1 @@
-conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
+conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
index 002de1a000..ae912c0675 100644
--- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
@@ -1,4 +1,4 @@
-resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
+resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html
index df109044a8..fcaa02a9bb 100644
--- a/doc/flux_fhir_analysis/conv/index.html
+++ b/doc/flux_fhir_analysis/conv/index.html
@@ -1,4 +1,4 @@
-flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
+flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
well-formedness implies:
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
index 4bf3ced369..638f2a67dd 100644
--- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
+++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
@@ -1,7 +1,7 @@
ConvCtxt in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::ConvCtxt
source · pub struct ConvCtxt<'a, 'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>
) -> Self
sourcefn conv_generic_bounds(
@@ -63,74 +63,73 @@
&self,
env: &mut Env,
constr: &Constraint<'_>
-) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
+) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
&self,
env: &mut Env,
- alias: &AliasReft<'_>,
- func_args: &[Expr<'_>]
-) -> QueryResult<Expr>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
+ alias: &AliasReft<'_>
+) -> QueryResult<AliasReft>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
&self,
env: &mut Env,
qself: &Ty<'_>,
assoc_segment: &PathSegment<'_>
-) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
-sourcefn probe_type_param_bounds(
+) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
+sourcefn probe_type_param_bounds(
&self,
param_did: LocalDefId,
assoc_ident: Ident
-) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
+) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
&self,
all_candidates: impl Fn() -> I,
assoc_ident: Ident
) -> Result<TraitRef<'tcx>, ErrorGuaranteed>where
- I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
+ I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
&self,
item_generics: &Generics,
trait_ref: TraitRef<'tcx>
-) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
+) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
&self,
env: &mut Env,
arg: &RefineArg<'_>
-) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
+) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>]
-) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
+) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>],
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn fill_generic_args_defaults(
+) -> QueryResult
sourcefn fill_generic_args_defaults(
&self,
def_id: DefId,
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn conv_ty_to_generic_arg(
+) -> QueryResult
sourcefn conv_ty_to_generic_arg(
&self,
env: &mut Env,
kind: GenericParamDefKind,
ty: &Ty<'_>
-) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
+) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
&self,
kind: GenericParamDefKind,
ty_span: Span,
ty: &Ty
-) -> QueryResult<GenericArg>
sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
+) -> QueryResult<GenericArg>sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
if the type cannot be converted into a rty::SubsetTy
.
-sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
+
sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
&self,
env: &mut Env,
exprs: &[Expr<'_>]
-) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
+) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
&self,
env: &mut Env,
invariants: &[Expr<'_>]
-) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
+) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
&self,
env: &mut Env,
invariant: &Expr<'_>
-) -> QueryResult<Invariant>
sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<Invariant>sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, '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_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html
index 00b4c9449e..533f2f4f30 100644
--- a/doc/flux_fhir_analysis/conv/struct.Env.html
+++ b/doc/flux_fhir_analysis/conv/struct.Env.html
@@ -1,11 +1,11 @@
Env in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Env
source · pub(crate) struct Env {
layers: Vec<Layer>,
early_bound: FxIndexMap<ParamId, (Symbol, Sort)>,
-}
Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
+}Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
genv: GlobalEnv<'_, '_>,
early_bound: &[RefineParam<'_>],
wfckresults: &WfckResults<'_>
-) -> QueryResult<Self>
sourcefn depth(&self) -> usize
sourcefn push_layer(&mut self, layer: Layer)
sourcefn pop_layer(&mut self) -> Layer
sourcefn top_layer(&self) -> &Layer
sourcefn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>
sourcefn to_early_bound_vars(&self) -> List<Expr>
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
Blanket Implementations§
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
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_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html
index 11204b4cea..262d0e7c41 100644
--- a/doc/flux_fhir_analysis/conv/struct.Layer.html
+++ b/doc/flux_fhir_analysis/conv/struct.Layer.html
@@ -1,25 +1,25 @@
Layer in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Layer
source · struct Layer {
map: FxIndexMap<ParamId, ParamEntry>,
kind: LayerKind,
-}
Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
+}Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
cx: &ConvCtxt<'_, '_, '_>,
params: &[RefineParam<'_>],
kind: LayerKind
-) -> QueryResult<Self>
sourcefn list(
+) -> QueryResult<Self>
sourcefn list(
cx: &ConvCtxt<'_, '_, '_>,
bound_regions: u32,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn coalesce(
+) -> QueryResult<Self>
sourcefn coalesce(
cx: &ConvCtxt<'_, '_, '_>,
def_id: DefId,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
+) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
+) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
&self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<List<BoundVariableKind>>sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
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_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
index 4c69f4b5ac..783ca37a9c 100644
--- a/doc/flux_fhir_analysis/conv/struct.LookupResult.html
+++ b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
@@ -2,7 +2,7 @@
kind: LookupResultKind<'a>,
span: Span,
}Fields§
§kind: LookupResultKind<'a>
§span: Span
The span of the variable that originated the lookup. Used to report bugs.
-Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
Blanket Implementations§
source§impl<T> Any for Twhere
+Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
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_fhir_analysis/conv/struct.ParamEntry.html b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
index 51baaa0039..8352b066e6 100644
--- a/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
+++ b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
@@ -2,7 +2,7 @@
name: Symbol,
sort: Sort,
mode: InferMode,
-}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
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_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
index 3ba1eed611..fa04e67bc8 100644
--- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
+++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
@@ -11,7 +11,7 @@
self,
f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>)
) -> Result<(), ErrorGuaranteed>sourcefn check_func_params_uses(&mut self, expr: &Expr<'_>, is_top_level_conj: bool)
Checks that refinement parameters of function sort are used in allowed positions.
-sourcefn check_params_are_value_determined(&mut self, params: &[RefineParam<'_>])
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
Blanket Implementations§
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, '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_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
index 76e6dea020..ec167a3d6e 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
@@ -4,7 +4,7 @@
}Fields§
§infcx: &'a mut InferCtxt<'genv, 'tcx>
§errors: Errors<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> Result<(), ErrorGuaranteed>sourcefn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, '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_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
index 8ce074b905..a5811de32d 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
@@ -1,6 +1,6 @@
InferCtxt in flux_fhir_analysis::wf::sortck - Rust Struct flux_fhir_analysis::
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
§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_fhir_analysis/conv/errors/index.html b/doc/flux_fhir_analysis/conv/errors/index.html
index 3b608aa7ff..40c805915f 100644
--- a/doc/flux_fhir_analysis/conv/errors/index.html
+++ b/doc/flux_fhir_analysis/conv/errors/index.html
@@ -1 +1 @@
-flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
+flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
index 1a42b647fc..865cb8a773 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
@@ -1,8 +1,8 @@
-AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
+AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
span: Span,
name: Ident,
-}
Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
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_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
index c639ddebbc..0efdde4d5e 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
@@ -1,7 +1,7 @@
-AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
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_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
index bacb14b497..c19df9e3c8 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
@@ -1,7 +1,7 @@
-InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
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_fhir_analysis/conv/fn.bug_on_infer_sort.html b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
index 598ac05698..b52fede725 100644
--- a/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
@@ -1 +1 @@
-bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
+bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
index 6a867e86a2..e34d184e52 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
@@ -1,4 +1,4 @@
-conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
+conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
genv: GlobalEnv<'_, '_>,
func: &SpecFunc<'_>
) -> QueryResult<SpecFuncDecl>
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
index fe32db2a97..b557ca174d 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
@@ -1,4 +1,4 @@
-conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
+conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
genv: GlobalEnv<'_, '_>,
fsort: &FuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
index 710c51a3b7..b70c272bcc 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_lit.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
@@ -1 +1 @@
-conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
+conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
index bff8c4fd4b..d71f87000c 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
@@ -1,4 +1,4 @@
-conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
+conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
genv: GlobalEnv<'_, '_>,
sort: &PolyFuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
index d15979ee29..7ac1428109 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
@@ -1,4 +1,4 @@
-conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
+conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
index f1e2ef2f52..977b51cb9b 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
@@ -1,4 +1,4 @@
-conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
+conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
genv: GlobalEnv<'_, '_>,
sort: &Sort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
index 20cd1ac129..7030b959ab 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
@@ -1,4 +1,4 @@
-conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
+conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
genv: GlobalEnv<'_, '_>,
path: &SortPath<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
index 082cab288f..8c81f6cf98 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
@@ -1,4 +1,4 @@
-conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
+conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
genv: GlobalEnv<'_, '_>,
sorts: &[Sort<'_>],
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
index 27eeab02a3..82d056f8fd 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
@@ -1 +1 @@
-conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
+conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
index 002de1a000..ae912c0675 100644
--- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
@@ -1,4 +1,4 @@
-resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
+resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html
index df109044a8..fcaa02a9bb 100644
--- a/doc/flux_fhir_analysis/conv/index.html
+++ b/doc/flux_fhir_analysis/conv/index.html
@@ -1,4 +1,4 @@
-flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
+flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
well-formedness implies:
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
index 4bf3ced369..638f2a67dd 100644
--- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
+++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
@@ -1,7 +1,7 @@
ConvCtxt in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::ConvCtxt
source · pub struct ConvCtxt<'a, 'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>
) -> Self
sourcefn conv_generic_bounds(
@@ -63,74 +63,73 @@
&self,
env: &mut Env,
constr: &Constraint<'_>
-) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
+) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
&self,
env: &mut Env,
- alias: &AliasReft<'_>,
- func_args: &[Expr<'_>]
-) -> QueryResult<Expr>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
+ alias: &AliasReft<'_>
+) -> QueryResult<AliasReft>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
&self,
env: &mut Env,
qself: &Ty<'_>,
assoc_segment: &PathSegment<'_>
-) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
-sourcefn probe_type_param_bounds(
+) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
+sourcefn probe_type_param_bounds(
&self,
param_did: LocalDefId,
assoc_ident: Ident
-) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
+) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
&self,
all_candidates: impl Fn() -> I,
assoc_ident: Ident
) -> Result<TraitRef<'tcx>, ErrorGuaranteed>where
- I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
+ I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
&self,
item_generics: &Generics,
trait_ref: TraitRef<'tcx>
-) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
+) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
&self,
env: &mut Env,
arg: &RefineArg<'_>
-) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
+) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>]
-) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
+) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>],
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn fill_generic_args_defaults(
+) -> QueryResult
sourcefn fill_generic_args_defaults(
&self,
def_id: DefId,
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn conv_ty_to_generic_arg(
+) -> QueryResult
sourcefn conv_ty_to_generic_arg(
&self,
env: &mut Env,
kind: GenericParamDefKind,
ty: &Ty<'_>
-) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
+) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
&self,
kind: GenericParamDefKind,
ty_span: Span,
ty: &Ty
-) -> QueryResult<GenericArg>
sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
+) -> QueryResult<GenericArg>sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
if the type cannot be converted into a rty::SubsetTy
.
-sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
+
sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
&self,
env: &mut Env,
exprs: &[Expr<'_>]
-) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
+) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
&self,
env: &mut Env,
invariants: &[Expr<'_>]
-) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
+) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
&self,
env: &mut Env,
invariant: &Expr<'_>
-) -> QueryResult<Invariant>
sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<Invariant>sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, '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_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html
index 00b4c9449e..533f2f4f30 100644
--- a/doc/flux_fhir_analysis/conv/struct.Env.html
+++ b/doc/flux_fhir_analysis/conv/struct.Env.html
@@ -1,11 +1,11 @@
Env in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Env
source · pub(crate) struct Env {
layers: Vec<Layer>,
early_bound: FxIndexMap<ParamId, (Symbol, Sort)>,
-}
Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
+}Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
genv: GlobalEnv<'_, '_>,
early_bound: &[RefineParam<'_>],
wfckresults: &WfckResults<'_>
-) -> QueryResult<Self>
sourcefn depth(&self) -> usize
sourcefn push_layer(&mut self, layer: Layer)
sourcefn pop_layer(&mut self) -> Layer
sourcefn top_layer(&self) -> &Layer
sourcefn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>
sourcefn to_early_bound_vars(&self) -> List<Expr>
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
Blanket Implementations§
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
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_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html
index 11204b4cea..262d0e7c41 100644
--- a/doc/flux_fhir_analysis/conv/struct.Layer.html
+++ b/doc/flux_fhir_analysis/conv/struct.Layer.html
@@ -1,25 +1,25 @@
Layer in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Layer
source · struct Layer {
map: FxIndexMap<ParamId, ParamEntry>,
kind: LayerKind,
-}
Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
+}Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
cx: &ConvCtxt<'_, '_, '_>,
params: &[RefineParam<'_>],
kind: LayerKind
-) -> QueryResult<Self>
sourcefn list(
+) -> QueryResult<Self>
sourcefn list(
cx: &ConvCtxt<'_, '_, '_>,
bound_regions: u32,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn coalesce(
+) -> QueryResult<Self>
sourcefn coalesce(
cx: &ConvCtxt<'_, '_, '_>,
def_id: DefId,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
+) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
+) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
&self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<List<BoundVariableKind>>sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
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_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
index 4c69f4b5ac..783ca37a9c 100644
--- a/doc/flux_fhir_analysis/conv/struct.LookupResult.html
+++ b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
@@ -2,7 +2,7 @@
kind: LookupResultKind<'a>,
span: Span,
}Fields§
§kind: LookupResultKind<'a>
§span: Span
The span of the variable that originated the lookup. Used to report bugs.
-Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
Blanket Implementations§
source§impl<T> Any for Twhere
+Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
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_fhir_analysis/conv/struct.ParamEntry.html b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
index 51baaa0039..8352b066e6 100644
--- a/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
+++ b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
@@ -2,7 +2,7 @@
name: Symbol,
sort: Sort,
mode: InferMode,
-}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
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_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
index 3ba1eed611..fa04e67bc8 100644
--- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
+++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
@@ -11,7 +11,7 @@
self,
f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>)
) -> Result<(), ErrorGuaranteed>sourcefn check_func_params_uses(&mut self, expr: &Expr<'_>, is_top_level_conj: bool)
Checks that refinement parameters of function sort are used in allowed positions.
-sourcefn check_params_are_value_determined(&mut self, params: &[RefineParam<'_>])
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
Blanket Implementations§
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, '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_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
index 76e6dea020..ec167a3d6e 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
@@ -4,7 +4,7 @@
}Fields§
§infcx: &'a mut InferCtxt<'genv, 'tcx>
§errors: Errors<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> Result<(), ErrorGuaranteed>sourcefn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, '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_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
index 8ce074b905..a5811de32d 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
@@ -1,6 +1,6 @@
InferCtxt in flux_fhir_analysis::wf::sortck - Rust Struct flux_fhir_analysis::
fn collect_and_apply<I, F>(iter: I, f: F) -> Rwhere
diff --git a/doc/flux_fhir_analysis/conv/errors/index.html b/doc/flux_fhir_analysis/conv/errors/index.html
index 3b608aa7ff..40c805915f 100644
--- a/doc/flux_fhir_analysis/conv/errors/index.html
+++ b/doc/flux_fhir_analysis/conv/errors/index.html
@@ -1 +1 @@
-flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
+flux_fhir_analysis::conv::errors - Rust Module flux_fhir_analysis::conv::errors
source · Structs§
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
index 1a42b647fc..865cb8a773 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AmbiguousAssocType.html
@@ -1,8 +1,8 @@
-AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
+AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
span: Span,
name: Ident,
-}
Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
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_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
index c639ddebbc..0efdde4d5e 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
@@ -1,7 +1,7 @@
-AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
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_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
index bacb14b497..c19df9e3c8 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
@@ -1,7 +1,7 @@
-InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
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_fhir_analysis/conv/fn.bug_on_infer_sort.html b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
index 598ac05698..b52fede725 100644
--- a/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
@@ -1 +1 @@
-bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
+bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
index 6a867e86a2..e34d184e52 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
@@ -1,4 +1,4 @@
-conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
+conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
genv: GlobalEnv<'_, '_>,
func: &SpecFunc<'_>
) -> QueryResult<SpecFuncDecl>
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
index fe32db2a97..b557ca174d 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
@@ -1,4 +1,4 @@
-conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
+conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
genv: GlobalEnv<'_, '_>,
fsort: &FuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
index 710c51a3b7..b70c272bcc 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_lit.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
@@ -1 +1 @@
-conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
+conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
index bff8c4fd4b..d71f87000c 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
@@ -1,4 +1,4 @@
-conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
+conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
genv: GlobalEnv<'_, '_>,
sort: &PolyFuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
index d15979ee29..7ac1428109 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
@@ -1,4 +1,4 @@
-conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
+conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
index f1e2ef2f52..977b51cb9b 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
@@ -1,4 +1,4 @@
-conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
+conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
genv: GlobalEnv<'_, '_>,
sort: &Sort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
index 20cd1ac129..7030b959ab 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
@@ -1,4 +1,4 @@
-conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
+conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
genv: GlobalEnv<'_, '_>,
path: &SortPath<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
index 082cab288f..8c81f6cf98 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
@@ -1,4 +1,4 @@
-conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
+conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
genv: GlobalEnv<'_, '_>,
sorts: &[Sort<'_>],
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
index 27eeab02a3..82d056f8fd 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
@@ -1 +1 @@
-conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
+conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
index 002de1a000..ae912c0675 100644
--- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
@@ -1,4 +1,4 @@
-resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
+resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html
index df109044a8..fcaa02a9bb 100644
--- a/doc/flux_fhir_analysis/conv/index.html
+++ b/doc/flux_fhir_analysis/conv/index.html
@@ -1,4 +1,4 @@
-flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
+flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
well-formedness implies:
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
index 4bf3ced369..638f2a67dd 100644
--- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
+++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
@@ -1,7 +1,7 @@
ConvCtxt in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::ConvCtxt
source · pub struct ConvCtxt<'a, 'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>
) -> Self
sourcefn conv_generic_bounds(
@@ -63,74 +63,73 @@
&self,
env: &mut Env,
constr: &Constraint<'_>
-) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
+) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
&self,
env: &mut Env,
- alias: &AliasReft<'_>,
- func_args: &[Expr<'_>]
-) -> QueryResult<Expr>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
+ alias: &AliasReft<'_>
+) -> QueryResult<AliasReft>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
&self,
env: &mut Env,
qself: &Ty<'_>,
assoc_segment: &PathSegment<'_>
-) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
-sourcefn probe_type_param_bounds(
+) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
+sourcefn probe_type_param_bounds(
&self,
param_did: LocalDefId,
assoc_ident: Ident
-) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
+) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
&self,
all_candidates: impl Fn() -> I,
assoc_ident: Ident
) -> Result<TraitRef<'tcx>, ErrorGuaranteed>where
- I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
+ I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
&self,
item_generics: &Generics,
trait_ref: TraitRef<'tcx>
-) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
+) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
&self,
env: &mut Env,
arg: &RefineArg<'_>
-) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
+) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>]
-) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
+) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>],
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn fill_generic_args_defaults(
+) -> QueryResult
sourcefn fill_generic_args_defaults(
&self,
def_id: DefId,
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn conv_ty_to_generic_arg(
+) -> QueryResult
sourcefn conv_ty_to_generic_arg(
&self,
env: &mut Env,
kind: GenericParamDefKind,
ty: &Ty<'_>
-) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
+) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
&self,
kind: GenericParamDefKind,
ty_span: Span,
ty: &Ty
-) -> QueryResult<GenericArg>
sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
+) -> QueryResult<GenericArg>sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
if the type cannot be converted into a rty::SubsetTy
.
-sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
+
sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
&self,
env: &mut Env,
exprs: &[Expr<'_>]
-) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
+) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
&self,
env: &mut Env,
invariants: &[Expr<'_>]
-) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
+) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
&self,
env: &mut Env,
invariant: &Expr<'_>
-) -> QueryResult<Invariant>
sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<Invariant>sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, '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_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html
index 00b4c9449e..533f2f4f30 100644
--- a/doc/flux_fhir_analysis/conv/struct.Env.html
+++ b/doc/flux_fhir_analysis/conv/struct.Env.html
@@ -1,11 +1,11 @@
Env in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Env
source · pub(crate) struct Env {
layers: Vec<Layer>,
early_bound: FxIndexMap<ParamId, (Symbol, Sort)>,
-}
Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
+}Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
genv: GlobalEnv<'_, '_>,
early_bound: &[RefineParam<'_>],
wfckresults: &WfckResults<'_>
-) -> QueryResult<Self>
sourcefn depth(&self) -> usize
sourcefn push_layer(&mut self, layer: Layer)
sourcefn pop_layer(&mut self) -> Layer
sourcefn top_layer(&self) -> &Layer
sourcefn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>
sourcefn to_early_bound_vars(&self) -> List<Expr>
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
Blanket Implementations§
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
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_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html
index 11204b4cea..262d0e7c41 100644
--- a/doc/flux_fhir_analysis/conv/struct.Layer.html
+++ b/doc/flux_fhir_analysis/conv/struct.Layer.html
@@ -1,25 +1,25 @@
Layer in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Layer
source · struct Layer {
map: FxIndexMap<ParamId, ParamEntry>,
kind: LayerKind,
-}
Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
+}Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
cx: &ConvCtxt<'_, '_, '_>,
params: &[RefineParam<'_>],
kind: LayerKind
-) -> QueryResult<Self>
sourcefn list(
+) -> QueryResult<Self>
sourcefn list(
cx: &ConvCtxt<'_, '_, '_>,
bound_regions: u32,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn coalesce(
+) -> QueryResult<Self>
sourcefn coalesce(
cx: &ConvCtxt<'_, '_, '_>,
def_id: DefId,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
+) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
+) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
&self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<List<BoundVariableKind>>sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
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_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
index 4c69f4b5ac..783ca37a9c 100644
--- a/doc/flux_fhir_analysis/conv/struct.LookupResult.html
+++ b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
@@ -2,7 +2,7 @@
kind: LookupResultKind<'a>,
span: Span,
}Fields§
§kind: LookupResultKind<'a>
§span: Span
The span of the variable that originated the lookup. Used to report bugs.
-Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
Blanket Implementations§
source§impl<T> Any for Twhere
+Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
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_fhir_analysis/conv/struct.ParamEntry.html b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
index 51baaa0039..8352b066e6 100644
--- a/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
+++ b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
@@ -2,7 +2,7 @@
name: Symbol,
sort: Sort,
mode: InferMode,
-}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
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_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
index 3ba1eed611..fa04e67bc8 100644
--- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
+++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
@@ -11,7 +11,7 @@
self,
f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>)
) -> Result<(), ErrorGuaranteed>sourcefn check_func_params_uses(&mut self, expr: &Expr<'_>, is_top_level_conj: bool)
Checks that refinement parameters of function sort are used in allowed positions.
-sourcefn check_params_are_value_determined(&mut self, params: &[RefineParam<'_>])
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
Blanket Implementations§
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, '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_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
index 76e6dea020..ec167a3d6e 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
@@ -4,7 +4,7 @@
}Fields§
§infcx: &'a mut InferCtxt<'genv, 'tcx>
§errors: Errors<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> Result<(), ErrorGuaranteed>sourcefn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, '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_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
index 8ce074b905..a5811de32d 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
@@ -1,6 +1,6 @@
InferCtxt in flux_fhir_analysis::wf::sortck - Rust Struct flux_fhir_analysis::
Module flux_fhir_analysis::conv::errors
source · Structs§
Module flux_fhir_analysis::conv::errors
source · Structs§
Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
+AmbiguousAssocType in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AmbiguousAssocType
source · pub(super) struct AmbiguousAssocType {
span: Span,
name: Ident,
-}
Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
§name: Ident
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AmbiguousAssocTypewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AmbiguousAssocType
§impl DynSync for AmbiguousAssocType
§impl Freeze for AmbiguousAssocType
§impl RefUnwindSafe for AmbiguousAssocType
§impl Send for AmbiguousAssocType
§impl Sync for AmbiguousAssocType
§impl Unpin for AmbiguousAssocType
§impl UnwindSafe for AmbiguousAssocType
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_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
index c639ddebbc..0efdde4d5e 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html
@@ -1,7 +1,7 @@
-AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::AssocTypeNotFound
source · pub(super) struct AssocTypeNotFound {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for AssocTypeNotFoundwhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for AssocTypeNotFound
§impl DynSync for AssocTypeNotFound
§impl Freeze for AssocTypeNotFound
§impl RefUnwindSafe for AssocTypeNotFound
§impl Send for AssocTypeNotFound
§impl Sync for AssocTypeNotFound
§impl Unpin for AssocTypeNotFound
§impl UnwindSafe for AssocTypeNotFound
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_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
index bacb14b497..c19df9e3c8 100644
--- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
+++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html
@@ -1,7 +1,7 @@
-InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust Struct flux_fhir_analysis::conv::errors::InvalidBaseInstance
source · pub(super) struct InvalidBaseInstance {
span: Span,
-}
Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
- G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§span: Span
Implementations§
Trait Implementations§
source§impl<'_sess, G> Diagnostic<'_sess, G> for InvalidBaseInstancewhere
+ G: EmissionGuarantee,
Auto Trait Implementations§
§impl DynSend for InvalidBaseInstance
§impl DynSync for InvalidBaseInstance
§impl Freeze for InvalidBaseInstance
§impl RefUnwindSafe for InvalidBaseInstance
§impl Send for InvalidBaseInstance
§impl Sync for InvalidBaseInstance
§impl Unpin for InvalidBaseInstance
§impl UnwindSafe for InvalidBaseInstance
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_fhir_analysis/conv/fn.bug_on_infer_sort.html b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
index 598ac05698..b52fede725 100644
--- a/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.bug_on_infer_sort.html
@@ -1 +1 @@
-bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
+bug_on_infer_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::bug_on_infer_sort
source · pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
index 6a867e86a2..e34d184e52 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_decl.html
@@ -1,4 +1,4 @@
-conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
+conv_func_decl in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_decl
source · pub fn conv_func_decl(
genv: GlobalEnv<'_, '_>,
func: &SpecFunc<'_>
) -> QueryResult<SpecFuncDecl>
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
index fe32db2a97..b557ca174d 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html
@@ -1,4 +1,4 @@
-conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
+conv_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_func_sort
source · pub(crate) fn conv_func_sort(
genv: GlobalEnv<'_, '_>,
fsort: &FuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
index 710c51a3b7..b70c272bcc 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_lit.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_lit.html
@@ -1 +1 @@
-conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
+conv_lit in flux_fhir_analysis::conv - Rust
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
index bff8c4fd4b..d71f87000c 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_poly_func_sort.html
@@ -1,4 +1,4 @@
-conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
+conv_poly_func_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_poly_func_sort
source · fn conv_poly_func_sort(
genv: GlobalEnv<'_, '_>,
sort: &PolyFuncSort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
index d15979ee29..7ac1428109 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html
@@ -1,4 +1,4 @@
-conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
+conv_refine_param in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_refine_param
source · fn conv_refine_param(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
index f1e2ef2f52..977b51cb9b 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html
@@ -1,4 +1,4 @@
-conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
+conv_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort
source · pub(crate) fn conv_sort(
genv: GlobalEnv<'_, '_>,
sort: &Sort<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
index 20cd1ac129..7030b959ab 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html
@@ -1,4 +1,4 @@
-conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
+conv_sort_path in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sort_path
source · fn conv_sort_path(
genv: GlobalEnv<'_, '_>,
path: &SortPath<'_>,
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
index 082cab288f..8c81f6cf98 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html
@@ -1,4 +1,4 @@
-conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
+conv_sorts in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_sorts
source · fn conv_sorts(
genv: GlobalEnv<'_, '_>,
sorts: &[Sort<'_>],
next_infer_sort: &mut impl FnMut() -> Sort
diff --git a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
index 27eeab02a3..82d056f8fd 100644
--- a/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
+++ b/doc/flux_fhir_analysis/conv/fn.conv_un_op.html
@@ -1 +1 @@
-conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
+conv_un_op in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::conv_un_op
source · fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file
diff --git a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
index 002de1a000..ae912c0675 100644
--- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
+++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html
@@ -1,4 +1,4 @@
-resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
+resolve_param_sort in flux_fhir_analysis::conv - Rust Function flux_fhir_analysis::conv::resolve_param_sort
source · pub(crate) fn resolve_param_sort(
genv: GlobalEnv<'_, '_>,
param: &RefineParam<'_>,
wfckresults: Option<&WfckResults<'_>>
diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html
index df109044a8..fcaa02a9bb 100644
--- a/doc/flux_fhir_analysis/conv/index.html
+++ b/doc/flux_fhir_analysis/conv/index.html
@@ -1,4 +1,4 @@
-flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
+flux_fhir_analysis::conv - Rust Module flux_fhir_analysis::conv
source · Expand description
Conversion from types in fhir
to types in rty
Conversion assumes well-formedness and will panic if type are not well-formed. Among other things,
well-formedness implies:
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
index 4bf3ced369..638f2a67dd 100644
--- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
+++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html
@@ -1,7 +1,7 @@
ConvCtxt in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::ConvCtxt
source · pub struct ConvCtxt<'a, 'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>,
-}
Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>
§wfckresults: &'a WfckResults<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ConvCtxt<'a, 'genv, 'tcx>
sourcepub(crate) fn new(
genv: GlobalEnv<'genv, 'tcx>,
wfckresults: &'a WfckResults<'genv>
) -> Self
sourcefn conv_generic_bounds(
@@ -63,74 +63,73 @@
&self,
env: &mut Env,
constr: &Constraint<'_>
-) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
+) -> QueryResult<Constraint>
sourcefn conv_alias_reft(
&self,
env: &mut Env,
- alias: &AliasReft<'_>,
- func_args: &[Expr<'_>]
-) -> QueryResult<Expr>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
+ alias: &AliasReft<'_>
+) -> QueryResult<AliasReft>
sourcefn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>
sourcefn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>
sourcefn conv_assoc_path(
&self,
env: &mut Env,
qself: &Ty<'_>,
assoc_segment: &PathSegment<'_>
-) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
-sourcefn probe_type_param_bounds(
+) -> QueryResult<Ty>
sourcefn generics_of_owner(&self) -> QueryResult<Generics>
Return the generics of the containing owner item
+sourcefn probe_type_param_bounds(
&self,
param_did: LocalDefId,
assoc_ident: Ident
-) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
+) -> GenericPredicates<'tcx>
sourcefn probe_single_bound_for_assoc_item<I>(
&self,
all_candidates: impl Fn() -> I,
assoc_ident: Ident
) -> Result<TraitRef<'tcx>, ErrorGuaranteed>where
- I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
+ I: Iterator<Item = PolyTraitRef<'tcx>>,
sourcefn refine_trait_ref(
&self,
item_generics: &Generics,
trait_ref: TraitRef<'tcx>
-) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
+) -> QueryResult<TraitRef>
sourcefn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region
sourcefn conv_refine_arg(
&self,
env: &mut Env,
arg: &RefineArg<'_>
-) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
+) -> QueryResult<Expr>
sourcefn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>
sourcepub fn conv_generic_args(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>]
-) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
+) -> QueryResult<Vec<GenericArg>>
sourcefn conv_generic_args_into(
&self,
env: &mut Env,
def_id: DefId,
args: &[GenericArg<'_>],
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn fill_generic_args_defaults(
+) -> QueryResult
sourcefn fill_generic_args_defaults(
&self,
def_id: DefId,
into: &mut Vec<GenericArg>
-) -> QueryResult
sourcefn conv_ty_to_generic_arg(
+) -> QueryResult
sourcefn conv_ty_to_generic_arg(
&self,
env: &mut Env,
kind: GenericParamDefKind,
ty: &Ty<'_>
-) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
+) -> QueryResult<GenericArg>
sourcefn ty_to_generic_arg(
&self,
kind: GenericParamDefKind,
ty_span: Span,
ty: &Ty
-) -> QueryResult<GenericArg>
sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
+) -> QueryResult<GenericArg>sourcefn ty_to_base_generic(&self, ty_span: Span, ty: &Ty) -> QueryResult<GenericArg>
Convert an rty::Ty
into a rty::GenericArg::Base
if possible or raise an error
if the type cannot be converted into a rty::SubsetTy
.
-sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
+
sourcefn resolve_param_sort(&self, param: &RefineParam<'_>) -> QueryResult<Sort>
source§impl ConvCtxt<'_, '_, '_>
sourcefn owner(&self) -> FluxOwnerId
sourcefn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>
sourcefn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp
sourcefn bin_rel_sort(&self, fhir_id: FhirId) -> Sort
sourcefn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr
sourcefn conv_exprs(
&self,
env: &mut Env,
exprs: &[Expr<'_>]
-) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
+) -> QueryResult<List<Expr>>
sourcefn conv_invariants(
&self,
env: &mut Env,
invariants: &[Expr<'_>]
-) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
+) -> QueryResult<Vec<Invariant>>
sourcefn conv_invariant(
&self,
env: &mut Env,
invariant: &Expr<'_>
-) -> QueryResult<Invariant>
sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<Invariant>sourcefn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Freeze for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ConvCtxt<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ConvCtxt<'a, '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_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html
index 00b4c9449e..533f2f4f30 100644
--- a/doc/flux_fhir_analysis/conv/struct.Env.html
+++ b/doc/flux_fhir_analysis/conv/struct.Env.html
@@ -1,11 +1,11 @@
Env in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Env
source · pub(crate) struct Env {
layers: Vec<Layer>,
early_bound: FxIndexMap<ParamId, (Symbol, Sort)>,
-}
Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
+}Fields§
§layers: Vec<Layer>
§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>
Implementations§
source§impl Env
sourcepub(crate) fn new(
genv: GlobalEnv<'_, '_>,
early_bound: &[RefineParam<'_>],
wfckresults: &WfckResults<'_>
-) -> QueryResult<Self>
sourcefn depth(&self) -> usize
sourcefn push_layer(&mut self, layer: Layer)
sourcefn pop_layer(&mut self) -> Layer
sourcefn top_layer(&self) -> &Layer
sourcefn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>
sourcefn to_early_bound_vars(&self) -> List<Expr>
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
Blanket Implementations§
Auto Trait Implementations§
§impl DynSend for Env
§impl DynSync for Env
§impl Freeze for Env
§impl RefUnwindSafe for Env
§impl Send for Env
§impl Sync for Env
§impl Unpin for Env
§impl UnwindSafe for Env
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_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html
index 11204b4cea..262d0e7c41 100644
--- a/doc/flux_fhir_analysis/conv/struct.Layer.html
+++ b/doc/flux_fhir_analysis/conv/struct.Layer.html
@@ -1,25 +1,25 @@
Layer in flux_fhir_analysis::conv - Rust Struct flux_fhir_analysis::conv::Layer
source · struct Layer {
map: FxIndexMap<ParamId, ParamEntry>,
kind: LayerKind,
-}
Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
+}Fields§
§map: FxIndexMap<ParamId, ParamEntry>
§kind: LayerKind
Implementations§
source§impl Layer
sourcefn new(
cx: &ConvCtxt<'_, '_, '_>,
params: &[RefineParam<'_>],
kind: LayerKind
-) -> QueryResult<Self>
sourcefn list(
+) -> QueryResult<Self>
sourcefn list(
cx: &ConvCtxt<'_, '_, '_>,
bound_regions: u32,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn coalesce(
+) -> QueryResult<Self>
sourcefn coalesce(
cx: &ConvCtxt<'_, '_, '_>,
def_id: DefId,
params: &[RefineParam<'_>]
-) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
+) -> QueryResult<Self>
sourcefn get(&self, name: impl Borrow<ParamId>) -> Option<(usize, &ParamEntry)>
sourcefn into_bound_vars(
self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
+) -> QueryResult<List<BoundVariableKind>>
sourcefn to_bound_vars(
&self,
genv: GlobalEnv<'_, '_>
-) -> QueryResult<List<BoundVariableKind>>
sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> QueryResult<List<BoundVariableKind>>sourcefn into_iter(self) -> impl Iterator<Item = ParamEntry>
Trait Implementations§
Auto Trait Implementations§
§impl DynSend for Layer
§impl DynSync for Layer
§impl Freeze for Layer
§impl RefUnwindSafe for Layer
§impl Send for Layer
§impl Sync for Layer
§impl Unpin for Layer
§impl UnwindSafe for Layer
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_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
index 4c69f4b5ac..783ca37a9c 100644
--- a/doc/flux_fhir_analysis/conv/struct.LookupResult.html
+++ b/doc/flux_fhir_analysis/conv/struct.LookupResult.html
@@ -2,7 +2,7 @@
kind: LookupResultKind<'a>,
span: Span,
}Fields§
§kind: LookupResultKind<'a>
§span: Span
The span of the variable that originated the lookup. Used to report bugs.
-Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
Blanket Implementations§
source§impl<T> Any for Twhere
+Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl<'a> DynSend for LookupResult<'a>
§impl<'a> DynSync for LookupResult<'a>
§impl<'a> Freeze for LookupResult<'a>
§impl<'a> RefUnwindSafe for LookupResult<'a>
§impl<'a> Send for LookupResult<'a>
§impl<'a> Sync for LookupResult<'a>
§impl<'a> Unpin for LookupResult<'a>
§impl<'a> UnwindSafe for LookupResult<'a>
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_fhir_analysis/conv/struct.ParamEntry.html b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
index 51baaa0039..8352b066e6 100644
--- a/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
+++ b/doc/flux_fhir_analysis/conv/struct.ParamEntry.html
@@ -2,7 +2,7 @@
name: Symbol,
sort: Sort,
mode: InferMode,
-}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
Blanket Implementations§
source§impl<T> Any for Twhere
+}Fields§
§name: Symbol
§sort: Sort
§mode: InferMode
Implementations§
Trait Implementations§
source§impl Clone for ParamEntry
source§fn clone(&self) -> ParamEntry
Returns a copy of the value. Read more1.0.0 · source§fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read moreAuto Trait Implementations§
§impl DynSend for ParamEntry
§impl DynSync for ParamEntry
§impl Freeze for ParamEntry
§impl RefUnwindSafe for ParamEntry
§impl Send for ParamEntry
§impl Sync for ParamEntry
§impl Unpin for ParamEntry
§impl UnwindSafe for ParamEntry
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_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
index 3ba1eed611..fa04e67bc8 100644
--- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
+++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html
@@ -11,7 +11,7 @@
self,
f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>)
) -> Result<(), ErrorGuaranteed>sourcefn check_func_params_uses(&mut self, expr: &Expr<'_>, is_top_level_conj: bool)
Checks that refinement parameters of function sort are used in allowed positions.
-sourcefn check_params_are_value_determined(&mut self, params: &[RefineParam<'_>])
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
Blanket Implementations§
Trait Implementations§
source§impl Visitor for ParamUsesChecker<'_, '_, '_>
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ParamUsesChecker<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ParamUsesChecker<'a, '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_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
index 76e6dea020..ec167a3d6e 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html
@@ -4,7 +4,7 @@
}Fields§
§infcx: &'a mut InferCtxt<'genv, 'tcx>
§errors: Errors<'genv>
Implementations§
source§impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
Blanket Implementations§
source§impl<T> Any for Twhere
+) -> Result<(), ErrorGuaranteed>sourcefn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)
Trait Implementations§
source§impl Visitor for ImplicitParamInferer<'_, '_, '_>
source§fn visit_ty(&mut self, ty: &Ty<'_>)
source§fn visit_node(&mut self, node: &Node<'_>)
source§fn visit_item(&mut self, item: &Item<'_>)
source§fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)
source§fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)
source§fn visit_generics(&mut self, generics: &Generics<'_>)
source§fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)
source§fn visit_impl(&mut self, impl_: &Impl<'_>)
source§fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)
source§fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)
source§fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)
source§fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)
source§fn visit_variant(&mut self, variant: &VariantDef<'_>)
source§fn visit_field_def(&mut self, field: &FieldDef<'_>)
source§fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)
source§fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)
source§fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)
source§fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)
source§fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)
source§fn visit_fn_sig(&mut self, sig: &FnSig<'_>)
source§fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)
source§fn visit_refine_param(&mut self, param: &RefineParam<'_>)
source§fn visit_constraint(&mut self, constraint: &Constraint<'_>)
source§fn visit_fn_output(&mut self, output: &FnOutput<'_>)
source§fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)
source§fn visit_lifetime(&mut self, _lft: &Lifetime)
source§fn visit_bty(&mut self, bty: &BaseTy<'_>)
source§fn visit_qpath(&mut self, qpath: &QPath<'_>)
source§fn visit_path(&mut self, path: &Path<'_>)
source§fn visit_path_segment(&mut self, segment: &PathSegment<'_>)
source§fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)
source§fn visit_sort(&mut self, sort: &Sort<'_>)
source§fn visit_sort_path(&mut self, path: &SortPath<'_>)
source§fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)
source§fn visit_func_sort(&mut self, func: &FuncSort<'_>)
source§fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)
source§fn visit_expr(&mut self, expr: &Expr<'_>)
source§fn visit_alias_reft(&mut self, alias_reft: &AliasReft<'_>)
source§fn visit_literal(&mut self, _lit: &Lit)
source§fn visit_path_expr(&mut self, _path: &PathExpr<'_>)
Auto Trait Implementations§
§impl<'a, 'genv, 'tcx> !DynSend for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !DynSync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Freeze for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !RefUnwindSafe for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Send for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !Sync for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> Unpin for ImplicitParamInferer<'a, 'genv, 'tcx>
§impl<'a, 'genv, 'tcx> !UnwindSafe for ImplicitParamInferer<'a, '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_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
index 8ce074b905..a5811de32d 100644
--- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
+++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html
@@ -1,6 +1,6 @@
InferCtxt in flux_fhir_analysis::wf::sortck - Rust Struct flux_fhir_analysis::