diff --git a/doc/flux_fhir_analysis/annot_check/errors/struct.ArrayLenMismatch.html b/doc/flux_fhir_analysis/annot_check/errors/struct.ArrayLenMismatch.html index b79f28223b..46eac67c1c 100644 --- a/doc/flux_fhir_analysis/annot_check/errors/struct.ArrayLenMismatch.html +++ b/doc/flux_fhir_analysis/annot_check/errors/struct.ArrayLenMismatch.html @@ -3,7 +3,7 @@ len: usize, expected_span: Span, expected_len: usize, -}

Fields§

§span: Span§len: usize§expected_span: Span§expected_len: usize

Implementations§

source§

impl ArrayLenMismatch

source

pub(super) fn new(len: &ArrayLen, expected_len: &ArrayLen) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for ArrayLenMismatchwhere +}

Fields§

§span: Span§len: usize§expected_span: Span§expected_len: usize

Implementations§

source§

impl ArrayLenMismatch

source

pub(super) fn new(len: &ArrayLen, expected_len: &ArrayLen) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for ArrayLenMismatchwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/annot_check/errors/struct.FieldCountMismatch.html b/doc/flux_fhir_analysis/annot_check/errors/struct.FieldCountMismatch.html index 10254da552..6af9ac357c 100644 --- a/doc/flux_fhir_analysis/annot_check/errors/struct.FieldCountMismatch.html +++ b/doc/flux_fhir_analysis/annot_check/errors/struct.FieldCountMismatch.html @@ -4,8 +4,8 @@ expected_span: Span, expected_fields: usize, }

Fields§

§span: Span§fields: usize§expected_span: Span§expected_fields: usize

Implementations§

source§

impl FieldCountMismatch

source

pub(super) fn from_variants( - variant: &VariantDef<'_>, - expected_variant: &VariantDef<'_> + variant: &VariantDef<'_>, + expected_variant: &VariantDef<'_> ) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for FieldCountMismatchwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, diff --git a/doc/flux_fhir_analysis/annot_check/errors/struct.FunArgCountMismatch.html b/doc/flux_fhir_analysis/annot_check/errors/struct.FunArgCountMismatch.html index 6629b9d485..c89f35e988 100644 --- a/doc/flux_fhir_analysis/annot_check/errors/struct.FunArgCountMismatch.html +++ b/doc/flux_fhir_analysis/annot_check/errors/struct.FunArgCountMismatch.html @@ -3,7 +3,7 @@ args: usize, expected_span: Span, expected_args: usize, -}

Fields§

§span: Span§args: usize§expected_span: Span§expected_args: usize

Implementations§

source§

impl FunArgCountMismatch

source

pub(super) fn new(decl: &FnDecl<'_>, expected_decl: &FnDecl<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for FunArgCountMismatchwhere +}

Fields§

§span: Span§args: usize§expected_span: Span§expected_args: usize

Implementations§

source§

impl FunArgCountMismatch

source

pub(super) fn new(decl: &FnDecl<'_>, expected_decl: &FnDecl<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for FunArgCountMismatchwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/annot_check/errors/struct.GenericArgCountMismatch.html b/doc/flux_fhir_analysis/annot_check/errors/struct.GenericArgCountMismatch.html index 05a2496f8f..c87e0b9f04 100644 --- a/doc/flux_fhir_analysis/annot_check/errors/struct.GenericArgCountMismatch.html +++ b/doc/flux_fhir_analysis/annot_check/errors/struct.GenericArgCountMismatch.html @@ -4,7 +4,7 @@ expected: usize, def_descr: &'static str, expected_span: Span, -}

Fields§

§span: Span§found: usize§expected: usize§def_descr: &'static str§expected_span: Span

Implementations§

source§

impl GenericArgCountMismatch

source

pub(super) fn new(path: &Path<'_>, expected_path: &Path<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for GenericArgCountMismatchwhere +}

Fields§

§span: Span§found: usize§expected: usize§def_descr: &'static str§expected_span: Span

Implementations§

source§

impl GenericArgCountMismatch

source

pub(super) fn new(path: &Path<'_>, expected_path: &Path<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for GenericArgCountMismatchwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/annot_check/errors/struct.InvalidRefinement.html b/doc/flux_fhir_analysis/annot_check/errors/struct.InvalidRefinement.html index baec8be484..8c330b649b 100644 --- a/doc/flux_fhir_analysis/annot_check/errors/struct.InvalidRefinement.html +++ b/doc/flux_fhir_analysis/annot_check/errors/struct.InvalidRefinement.html @@ -4,7 +4,7 @@ expected_ty: String, has_note: Option<()>, note: String, -}

Fields§

§span: Span§expected_span: Span§expected_ty: String§has_note: Option<()>§note: String

Implementations§

source§

impl InvalidRefinement

source

pub(super) fn from_tys(ty: &Ty<'_>, expected_ty: &Ty<'_>) -> Self

source

pub(super) fn from_paths(path: &Path<'_>, expected_path: &Path<'_>) -> Self

source

pub(super) fn from_btys(bty: &BaseTy<'_>, expected_bty: &BaseTy<'_>) -> Self

source

pub(super) fn from_qpaths(qpath: &QPath<'_>, expected_qpath: &QPath<'_>) -> Self

source

pub(super) fn with_note(self, note: impl ToString) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidRefinementwhere +}

Fields§

§span: Span§expected_span: Span§expected_ty: String§has_note: Option<()>§note: String

Implementations§

source§

impl InvalidRefinement

source

pub(super) fn from_tys(ty: &Ty<'_>, expected_ty: &Ty<'_>) -> Self

source

pub(super) fn from_paths(path: &Path<'_>, expected_path: &Path<'_>) -> Self

source

pub(super) fn from_btys(bty: &BaseTy<'_>, expected_bty: &BaseTy<'_>) -> Self

source

pub(super) fn from_qpaths(qpath: &QPath<'_>, expected_qpath: &QPath<'_>) -> Self

source

pub(super) fn with_note(self, note: impl ToString) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidRefinementwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_enum_def.html b/doc/flux_fhir_analysis/annot_check/fn.check_enum_def.html index afe54ce577..b37d8a6268 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_enum_def.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_enum_def.html @@ -1,6 +1,6 @@ check_enum_def in flux_fhir_analysis::annot_check - Rust
pub(crate) fn check_enum_def<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
     owner_id: OwnerId,
-    enum_def: &EnumDef<'_>
+    enum_def: &EnumDef<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_fn_sig.html b/doc/flux_fhir_analysis/annot_check/fn.check_fn_sig.html index 8c61fee6a9..a991f0a5a0 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_fn_sig.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_fn_sig.html @@ -1,6 +1,6 @@ check_fn_sig in flux_fhir_analysis::annot_check - Rust
pub(crate) fn check_fn_sig<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
     owner_id: OwnerId,
-    fn_sig: &FnSig<'_>
+    fn_sig: &FnSig<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_impl_item.html b/doc/flux_fhir_analysis/annot_check/fn.check_impl_item.html index 2c564a1817..b2eb0af9c2 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_impl_item.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_impl_item.html @@ -1,5 +1,5 @@ check_impl_item in flux_fhir_analysis::annot_check - Rust
fn check_impl_item<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
-    impl_item: &ImplItem<'_>
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
+    impl_item: &ImplItem<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_item.html b/doc/flux_fhir_analysis/annot_check/fn.check_item.html index 6f02b9285a..ab1b63e1f2 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_item.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_item.html @@ -1,5 +1,5 @@ check_item in flux_fhir_analysis::annot_check - Rust
fn check_item<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
-    item: &Item<'_>
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
+    item: &Item<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_node.html b/doc/flux_fhir_analysis/annot_check/fn.check_node.html index c3f373b9f5..63c036cee7 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_node.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_node.html @@ -1,5 +1,5 @@ check_node in flux_fhir_analysis::annot_check - Rust
pub(crate) fn check_node<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
-    node: &Node<'_>
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
+    node: &Node<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_struct_def.html b/doc/flux_fhir_analysis/annot_check/fn.check_struct_def.html index 3b9e620737..d0c4e844f1 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_struct_def.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_struct_def.html @@ -1,6 +1,6 @@ check_struct_def in flux_fhir_analysis::annot_check - Rust
pub(crate) fn check_struct_def<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
     owner_id: OwnerId,
-    struct_def: &StructDef<'_>
+    struct_def: &StructDef<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_trait_item.html b/doc/flux_fhir_analysis/annot_check/fn.check_trait_item.html index a74281ecb8..fce6f48969 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_trait_item.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_trait_item.html @@ -1,5 +1,5 @@ check_trait_item in flux_fhir_analysis::annot_check - Rust
fn check_trait_item<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
-    trait_item: &TraitItem<'_>
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
+    trait_item: &TraitItem<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/fn.check_ty_alias.html b/doc/flux_fhir_analysis/annot_check/fn.check_ty_alias.html index ad877f64b6..c08d6e2c3e 100644 --- a/doc/flux_fhir_analysis/annot_check/fn.check_ty_alias.html +++ b/doc/flux_fhir_analysis/annot_check/fn.check_ty_alias.html @@ -1,6 +1,6 @@ check_ty_alias in flux_fhir_analysis::annot_check - Rust
pub(crate) fn check_ty_alias<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    wfckresults: &mut WfckResults<'genv>,
+    genv: GlobalEnv<'genv, '_>,
+    wfckresults: &mut WfckResults<'genv>,
     owner_id: OwnerId,
-    ty_alias: &TyAlias<'_>
+    ty_alias: &TyAlias<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/index.html b/doc/flux_fhir_analysis/annot_check/index.html index 4361c691e5..945e6833fe 100644 --- a/doc/flux_fhir_analysis/annot_check/index.html +++ b/doc/flux_fhir_analysis/annot_check/index.html @@ -1,4 +1,4 @@ -flux_fhir_analysis::annot_check - Rust
Expand description

Check if an fhir annotation is a valid refinement of the corresponding rust declaration.

-

To check if an fhir is valid, we first lift the hir declaration into fhir and then +flux_fhir_analysis::annot_check - Rust

Expand description

Check if an fhir annotation is a valid refinement of the corresponding rust declaration.

+

To check if an fhir is valid, we first lift the hir declaration into fhir and then “zip” them together.

Modules

Structs

Functions

Type Aliases

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/annot_check/struct.Zipper.html b/doc/flux_fhir_analysis/annot_check/struct.Zipper.html index 6b74b9bb9d..b5e297e524 100644 --- a/doc/flux_fhir_analysis/annot_check/struct.Zipper.html +++ b/doc/flux_fhir_analysis/annot_check/struct.Zipper.html @@ -1,47 +1,47 @@ Zipper in flux_fhir_analysis::annot_check - Rust
struct Zipper<'zip, 'genv, 'tcx> {
-    genv: GlobalEnv<'genv, 'tcx>,
-    wfckresults: &'zip mut WfckResults<'genv>,
-    locs: UnordMap<ParamId, Ty<'genv>>,
-    self_ty: Option<Ty<'genv>>,
-}

Fields§

§genv: GlobalEnv<'genv, 'tcx>§wfckresults: &'zip mut WfckResults<'genv>§locs: UnordMap<ParamId, Ty<'genv>>§self_ty: Option<Ty<'genv>>

Implementations§

source§

impl<'zip, 'genv, 'tcx> Zipper<'zip, 'genv, 'tcx>

source

fn new( - genv: GlobalEnv<'genv, 'tcx>, - wfckresults: &'zip mut WfckResults<'genv>, - self_ty: Option<Ty<'genv>> + genv: GlobalEnv<'genv, 'tcx>, + wfckresults: &'zip mut WfckResults<'genv>, + locs: UnordMap<ParamId, Ty<'genv>>, + self_ty: Option<Ty<'genv>>, +}

Fields§

§genv: GlobalEnv<'genv, 'tcx>§wfckresults: &'zip mut WfckResults<'genv>§locs: UnordMap<ParamId, Ty<'genv>>§self_ty: Option<Ty<'genv>>

Implementations§

source§

impl<'zip, 'genv, 'tcx> Zipper<'zip, 'genv, 'tcx>

source

fn new( + genv: GlobalEnv<'genv, 'tcx>, + wfckresults: &'zip mut WfckResults<'genv>, + self_ty: Option<Ty<'genv>> ) -> Self

source

fn zip_enum_variant( &mut self, - variant: &VariantDef<'_>, - expected_variant: &VariantDef<'genv> + variant: &VariantDef<'_>, + expected_variant: &VariantDef<'genv> ) -> Result<(), ErrorGuaranteed>

source

fn zip_fn_decl( &mut self, - fn_decl: &FnDecl<'_>, - expected_fn_sig: &FnDecl<'genv> + fn_decl: &FnDecl<'_>, + expected_fn_sig: &FnDecl<'genv> ) -> Result<(), ErrorGuaranteed>

source

fn zip_constraints( &mut self, - constrs: &[Constraint<'_>] + constrs: &[Constraint<'_>] ) -> Result<(), ErrorGuaranteed>

source

fn zip_tys( &mut self, - tys: &[Ty<'_>], - expected_tys: &[Ty<'genv>] + tys: &[Ty<'_>], + expected_tys: &[Ty<'genv>] ) -> Result<(), ErrorGuaranteed>

source

fn zip_ty( &mut self, - ty: &Ty<'_>, - expected_ty: &Ty<'genv> + ty: &Ty<'_>, + expected_ty: &Ty<'genv> ) -> Result<(), ErrorGuaranteed>

source

fn zip_generic_arg( &mut self, - arg1: &GenericArg<'_>, - arg2: &GenericArg<'genv> -) -> Result<(), ErrorGuaranteed>

source

fn zip_lifetime(&mut self, lft: Lifetime, expected_lft: Lifetime)

source

fn zip_bty( + arg1: &GenericArg<'_>, + arg2: &GenericArg<'genv> +) -> Result<(), ErrorGuaranteed>

source

fn zip_lifetime(&mut self, lft: Lifetime, expected_lft: Lifetime)

source

fn zip_bty( &mut self, - bty: &BaseTy<'_>, - expected_bty: &BaseTy<'genv> + bty: &BaseTy<'_>, + expected_bty: &BaseTy<'genv> ) -> Result<(), ErrorGuaranteed>

source

fn zip_qpath( &mut self, - qpath: &QPath<'_>, - expected_qpath: &QPath<'genv> -) -> Result<(), ErrorGuaranteed>

source

fn is_same_res(&self, res: Res, expected: Res) -> bool

source

fn zip_path( + qpath: &QPath<'_>, + expected_qpath: &QPath<'genv> +) -> Result<(), ErrorGuaranteed>

source

fn is_same_res(&self, res: Res, expected: Res) -> bool

source

fn zip_path( &mut self, - path: &Path<'_>, - expected_path: &Path<'genv> + path: &Path<'_>, + expected_path: &Path<'genv> ) -> Result<(), ErrorGuaranteed>

source

fn emit_err<'a>(&'a self, err: impl IntoDiagnostic<'a>) -> ErrorGuaranteed

Auto Trait Implementations§

§

impl<'zip, 'genv, 'tcx> !RefUnwindSafe for Zipper<'zip, 'genv, 'tcx>

§

impl<'zip, 'genv, 'tcx> !Send for Zipper<'zip, 'genv, 'tcx>

§

impl<'zip, 'genv, 'tcx> !Sync for Zipper<'zip, 'genv, 'tcx>

§

impl<'zip, 'genv, 'tcx> Unpin for Zipper<'zip, 'genv, 'tcx>

§

impl<'zip, 'genv, 'tcx> !UnwindSafe for Zipper<'zip, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere diff --git a/doc/flux_fhir_analysis/annot_check/type.LocsMap.html b/doc/flux_fhir_analysis/annot_check/type.LocsMap.html index 84d05c649d..1f3e356c67 100644 --- a/doc/flux_fhir_analysis/annot_check/type.LocsMap.html +++ b/doc/flux_fhir_analysis/annot_check/type.LocsMap.html @@ -1,3 +1,3 @@ -LocsMap in flux_fhir_analysis::annot_check - Rust
type LocsMap<'genv> = UnordMap<ParamId, Ty<'genv>>;

Aliased Type§

struct LocsMap<'genv> {
-    inner: HashMap<ParamId, Ty<'genv>, BuildHasherDefault<FxHasher>>,
-}

Fields§

§inner: HashMap<ParamId, Ty<'genv>, BuildHasherDefault<FxHasher>>
\ No newline at end of file +LocsMap in flux_fhir_analysis::annot_check - Rust
type LocsMap<'genv> = UnordMap<ParamId, Ty<'genv>>;

Aliased Type§

struct LocsMap<'genv> {
+    inner: HashMap<ParamId, Ty<'genv>, BuildHasherDefault<FxHasher>>,
+}

Fields§

§inner: HashMap<ParamId, Ty<'genv>, BuildHasherDefault<FxHasher>>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/compare_impl_item/errors/struct.IncompatibleSort.html b/doc/flux_fhir_analysis/compare_impl_item/errors/struct.IncompatibleSort.html index 2d67d800fa..b24958cf80 100644 --- a/doc/flux_fhir_analysis/compare_impl_item/errors/struct.IncompatibleSort.html +++ b/doc/flux_fhir_analysis/compare_impl_item/errors/struct.IncompatibleSort.html @@ -1,13 +1,13 @@ IncompatibleSort in flux_fhir_analysis::compare_impl_item::errors - Rust
pub(super) struct IncompatibleSort {
     span: Span,
     name: Symbol,
-    expected: FuncSort,
-    found: FuncSort,
-}

Fields§

§span: Span§name: Symbol§expected: FuncSort§found: FuncSort

Implementations§

source§

impl IncompatibleSort

source

pub(super) fn new( + expected: FuncSort, + found: FuncSort, +}

Fields§

§span: Span§name: Symbol§expected: FuncSort§found: FuncSort

Implementations§

source§

impl IncompatibleSort

source

pub(super) fn new( span: Span, name: Symbol, - expected: FuncSort, - found: FuncSort + expected: FuncSort, + found: FuncSort ) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for IncompatibleSortwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, diff --git a/doc/flux_fhir_analysis/compare_impl_item/fn.check_assoc_reft.html b/doc/flux_fhir_analysis/compare_impl_item/fn.check_assoc_reft.html index 21f5b36992..66a48ceb0b 100644 --- a/doc/flux_fhir_analysis/compare_impl_item/fn.check_assoc_reft.html +++ b/doc/flux_fhir_analysis/compare_impl_item/fn.check_assoc_reft.html @@ -1,5 +1,5 @@ check_assoc_reft in flux_fhir_analysis::compare_impl_item - Rust
fn check_assoc_reft(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     impl_id: LocalDefId,
     trait_id: DefId,
     name: Symbol
diff --git a/doc/flux_fhir_analysis/compare_impl_item/fn.check_impl_against_trait.html b/doc/flux_fhir_analysis/compare_impl_item/fn.check_impl_against_trait.html
index 132ba731f4..4de49b5619 100644
--- a/doc/flux_fhir_analysis/compare_impl_item/fn.check_impl_against_trait.html
+++ b/doc/flux_fhir_analysis/compare_impl_item/fn.check_impl_against_trait.html
@@ -1,4 +1,4 @@
 check_impl_against_trait in flux_fhir_analysis::compare_impl_item - Rust
pub fn check_impl_against_trait(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     impl_id: LocalDefId
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/enum.Entry.html b/doc/flux_fhir_analysis/conv/enum.Entry.html index 1364e479a2..b80388c5a7 100644 --- a/doc/flux_fhir_analysis/conv/enum.Entry.html +++ b/doc/flux_fhir_analysis/conv/enum.Entry.html @@ -1,16 +1,16 @@ Entry in flux_fhir_analysis::conv - Rust
enum Entry {
     Sort {
-        infer_mode: InferMode,
+        infer_mode: InferMode,
         name: Symbol,
-        sort: Sort,
+        sort: Sort,
         idx: u32,
     },
     Unit(Symbol),
-}

Variants§

§

Sort

Fields

§infer_mode: InferMode
§name: Symbol
§sort: Sort
§idx: u32

The index of the entry in the layer skipping all Entry::Unit if Layer::filter_unit +}

Variants§

§

Sort

Fields

§infer_mode: InferMode
§name: Symbol
§sort: Sort
§idx: u32

The index of the entry in the layer skipping all Entry::Unit if Layer::filter_unit is true

§

Unit(Symbol)

We track parameters of unit sort separately because we avoid creating bound variables for them in function signatures.

-

Implementations§

source§

impl Entry

source

fn new(idx: u32, sort: Sort, infer_mode: InferMode, name: Symbol) -> Self

Trait Implementations§

source§

impl Clone for Entry

source§

fn clone(&self) -> Entry

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl Debug for Entry

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl RefUnwindSafe for Entry

§

impl Send for Entry

§

impl Sync for Entry

§

impl Unpin for Entry

§

impl UnwindSafe for Entry

Blanket Implementations§

source§

impl<T> Any for Twhere +

Implementations§

source§

impl Entry

source

fn new(idx: u32, sort: Sort, infer_mode: InferMode, name: Symbol) -> Self

Trait Implementations§

source§

impl Clone for Entry

source§

fn clone(&self) -> Entry

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl Debug for Entry

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl RefUnwindSafe for Entry

§

impl Send for Entry

§

impl Sync for Entry

§

impl Unpin for Entry

§

impl UnwindSafe for Entry

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/conv/enum.LookupResultKind.html b/doc/flux_fhir_analysis/conv/enum.LookupResultKind.html index 313e07ec34..ee087ae057 100644 --- a/doc/flux_fhir_analysis/conv/enum.LookupResultKind.html +++ b/doc/flux_fhir_analysis/conv/enum.LookupResultKind.html @@ -7,9 +7,9 @@ EarlyParam { idx: u32, name: Symbol, - sort: Sort, + sort: Sort, }, -}

Variants§

§

LateBound

Fields

§level: u32
§entry: &'a Entry
§

EarlyParam

Fields

§idx: u32
§name: Symbol
§sort: Sort

Trait Implementations§

source§

impl<'a> Debug for LookupResultKind<'a>

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl<'a> RefUnwindSafe for LookupResultKind<'a>

§

impl<'a> Send for LookupResultKind<'a>

§

impl<'a> Sync for LookupResultKind<'a>

§

impl<'a> Unpin for LookupResultKind<'a>

§

impl<'a> UnwindSafe for LookupResultKind<'a>

Blanket Implementations§

source§

impl<T> Any for Twhere +}

Variants§

§

LateBound

Fields

§level: u32
§entry: &'a Entry
§

EarlyParam

Fields

§idx: u32
§name: Symbol
§sort: Sort

Trait Implementations§

source§

impl<'a> Debug for LookupResultKind<'a>

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

impl<'a> RefUnwindSafe for LookupResultKind<'a>

§

impl<'a> Send for LookupResultKind<'a>

§

impl<'a> Sync for LookupResultKind<'a>

§

impl<'a> Unpin for LookupResultKind<'a>

§

impl<'a> UnwindSafe for LookupResultKind<'a>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound.html index 8edaab0df3..8ad10ea1e7 100644 --- a/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound.html +++ b/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound.html @@ -1 +1 @@ -_DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust
const _DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound: ();
\ No newline at end of file +_DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust
const _DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_AssocTypeNotFound: ();
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance.html index c47d96326a..3eb81c8fdd 100644 --- a/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance.html +++ b/doc/flux_fhir_analysis/conv/errors/constant._DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance.html @@ -1 +1 @@ -_DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust
const _DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance: ();
\ No newline at end of file +_DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust
const _DERIVE_rustc_errors_IntoDiagnostic_diagnostic_handler_sess_G_FOR_InvalidBaseInstance: ();
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/errors/index.html b/doc/flux_fhir_analysis/conv/errors/index.html index 71f68e03ec..9925f64a54 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
\ No newline at end of file +flux_fhir_analysis::conv::errors - Rust
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html b/doc/flux_fhir_analysis/conv/errors/struct.AssocTypeNotFound.html index 133b1a5e77..0a6646dc28 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
pub(super) struct AssocTypeNotFound {
+AssocTypeNotFound in flux_fhir_analysis::conv::errors - Rust
pub(super) struct AssocTypeNotFound {
     span: Span,
-}

Fields§

§span: Span

Implementations§

source§

impl AssocTypeNotFound

source

pub(super) fn new(ident: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for AssocTypeNotFoundwhere - G: EmissionGuarantee,

Fields§

§span: Span

Implementations§

source§

impl AssocTypeNotFound

source

pub(super) fn new(ident: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for AssocTypeNotFoundwhere + G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler ) -> DiagnosticBuilder<'__diagnostic_handler_sess, G>

Write out as a diagnostic out of Handler.

Auto Trait Implementations§

Blanket Implementations§

source§

impl<T> Any for Twhere diff --git a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html index 30d1ec8c80..16dcc89005 100644 --- a/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html +++ b/doc/flux_fhir_analysis/conv/errors/struct.InvalidBaseInstance.html @@ -1,8 +1,8 @@ -InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust
pub(super) struct InvalidBaseInstance<'fhir> {
+InvalidBaseInstance in flux_fhir_analysis::conv::errors - Rust
pub(super) struct InvalidBaseInstance<'fhir> {
     span: Span,
-    ty: &'fhir Ty<'fhir>,
-}

Fields§

§span: Span§ty: &'fhir Ty<'fhir>

Implementations§

source§

impl<'fhir> InvalidBaseInstance<'fhir>

source

pub(super) fn new(ty: &'fhir Ty<'fhir>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'fhir, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidBaseInstance<'fhir>where - G: EmissionGuarantee,

source§

fn into_diagnostic( + ty: &'fhir Ty<'fhir>, +}

Fields§

§span: Span§ty: &'fhir Ty<'fhir>

Implementations§

source§

impl<'fhir> InvalidBaseInstance<'fhir>

source

pub(super) fn new(ty: &'fhir Ty<'fhir>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'fhir, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidBaseInstance<'fhir>where + G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler ) -> DiagnosticBuilder<'__diagnostic_handler_sess, G>

Write out as a diagnostic out of Handler.

Auto Trait Implementations§

§

impl<'fhir> RefUnwindSafe for InvalidBaseInstance<'fhir>

§

impl<'fhir> Send for InvalidBaseInstance<'fhir>

§

impl<'fhir> Sync for InvalidBaseInstance<'fhir>

§

impl<'fhir> Unpin for InvalidBaseInstance<'fhir>

§

impl<'fhir> UnwindSafe for InvalidBaseInstance<'fhir>

Blanket Implementations§

source§

impl<T> Any for Twhere 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 0ea6af9bd2..aa7a1a3abf 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
pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file +bug_on_infer_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn bug_on_infer_sort() -> Sort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_adt_sort_def.html b/doc/flux_fhir_analysis/conv/fn.conv_adt_sort_def.html index d6f5253f3c..fe306b0d76 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_adt_sort_def.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_adt_sort_def.html @@ -1,5 +1,5 @@ conv_adt_sort_def in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_adt_sort_def(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId,
-    refined_by: &RefinedBy<'_>
-) -> AdtSortDef
\ No newline at end of file + refined_by: &RefinedBy<'_> +) -> AdtSortDef

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_assoc_reft_def.html b/doc/flux_fhir_analysis/conv/fn.conv_assoc_reft_def.html index e7f4de12e5..8095dcc732 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_assoc_reft_def.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_assoc_reft_def.html @@ -1,5 +1,5 @@ conv_assoc_reft_def in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_assoc_reft_def<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    assoc_reft: &ImplAssocReft<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Lambda>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + assoc_reft: &ImplAssocReft<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Lambda>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_defn.html b/doc/flux_fhir_analysis/conv/fn.conv_defn.html index f854ce6832..63e948734a 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_defn.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_defn.html @@ -1,5 +1,5 @@ conv_defn in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_defn<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    func: &SpecFunc<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Option<SpecFunc>>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + func: &SpecFunc<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Option<SpecFunc>>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_fn_decl.html b/doc/flux_fhir_analysis/conv/fn.conv_fn_decl.html index d023fa6c6d..5a14d182e7 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_fn_decl.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_fn_decl.html @@ -1,6 +1,6 @@ conv_fn_decl in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_fn_decl<'genv>(
-    genv: GlobalEnv<'genv, '_>,
+    genv: GlobalEnv<'genv, '_>,
     def_id: LocalDefId,
-    decl: &FnDecl<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<EarlyBinder<PolyFnSig>>
\ No newline at end of file + decl: &FnDecl<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<EarlyBinder<PolyFnSig>>

\ 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 0c9b080486..906c64d3c0 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
pub fn conv_func_decl(
-    genv: GlobalEnv<'_, '_>,
-    func: &SpecFunc<'_>
-) -> SpecFuncDecl
\ No newline at end of file +conv_func_decl in flux_fhir_analysis::conv - Rust
pub fn conv_func_decl(
+    genv: GlobalEnv<'_, '_>,
+    func: &SpecFunc<'_>
+) -> 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 6ca0d016b7..8771ee91b1 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_func_sort.html @@ -1,5 +1,5 @@ -conv_func_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_func_sort(
-    genv: GlobalEnv<'_, '_>,
-    fsort: &FuncSort<'_>,
-    next_infer_sort: &mut impl FnMut() -> Sort
-) -> FuncSort
\ No newline at end of file +conv_func_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_func_sort(
+    genv: GlobalEnv<'_, '_>,
+    fsort: &FuncSort<'_>,
+    next_infer_sort: &mut impl FnMut() -> Sort
+) -> FuncSort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_generic_param_kind.html b/doc/flux_fhir_analysis/conv/fn.conv_generic_param_kind.html index 32e6e3d57e..8e4c607fe8 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_generic_param_kind.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_generic_param_kind.html @@ -1 +1 @@ -conv_generic_param_kind in flux_fhir_analysis::conv - Rust
fn conv_generic_param_kind(kind: &GenericParamKind<'_>) -> GenericParamDefKind
\ No newline at end of file +conv_generic_param_kind in flux_fhir_analysis::conv - Rust
fn conv_generic_param_kind(kind: &GenericParamKind<'_>) -> GenericParamDefKind
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_generic_predicates.html b/doc/flux_fhir_analysis/conv/fn.conv_generic_predicates.html index 356a490bdd..97f5bdaac8 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_generic_predicates.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_generic_predicates.html @@ -1,6 +1,6 @@ conv_generic_predicates in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_generic_predicates<'genv>(
-    genv: GlobalEnv<'genv, '_>,
+    genv: GlobalEnv<'genv, '_>,
     def_id: LocalDefId,
-    predicates: &[WhereBoundPredicate<'_>],
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<EarlyBinder<GenericPredicates>>
\ No newline at end of file + predicates: &[WhereBoundPredicate<'_>], + wfckresults: &WfckResults<'genv> +) -> QueryResult<EarlyBinder<GenericPredicates>>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_generics.html b/doc/flux_fhir_analysis/conv/fn.conv_generics.html index 0f27bdfef1..d5a06275b8 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_generics.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_generics.html @@ -1,5 +1,5 @@ conv_generics in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_generics(
-    rust_generics: &Generics<'_>,
-    generics: &Generics<'_>,
+    rust_generics: &Generics<'_>,
+    generics: &Generics<'_>,
     is_trait: Option<LocalDefId>
-) -> QueryResult<Generics>
\ No newline at end of file +) -> QueryResult<Generics>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_invariants.html b/doc/flux_fhir_analysis/conv/fn.conv_invariants.html index beaa729a40..6611797c83 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_invariants.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_invariants.html @@ -1,7 +1,7 @@ conv_invariants in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_invariants<'genv>(
-    genv: GlobalEnv<'genv, '_>,
+    genv: GlobalEnv<'genv, '_>,
     def_id: LocalDefId,
-    params: &[RefineParam<'_>],
-    invariants: &[Expr<'_>],
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Vec<Invariant>>
\ No newline at end of file + params: &[RefineParam<'_>], + invariants: &[Expr<'_>], + wfckresults: &WfckResults<'genv> +) -> QueryResult<Vec<Invariant>>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_lit.html b/doc/flux_fhir_analysis/conv/fn.conv_lit.html index 55f20147f6..dbca82adc9 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
fn conv_lit(lit: Lit) -> Constant
\ No newline at end of file +conv_lit in flux_fhir_analysis::conv - Rust
fn conv_lit(lit: Lit) -> Constant
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_opaque_ty.html b/doc/flux_fhir_analysis/conv/fn.conv_opaque_ty.html index 40e4d480d5..6430596ada 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_opaque_ty.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_opaque_ty.html @@ -1,6 +1,6 @@ conv_opaque_ty in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_opaque_ty<'genv>(
-    genv: GlobalEnv<'genv, '_>,
+    genv: GlobalEnv<'genv, '_>,
     def_id: LocalDefId,
-    opaque_ty: &OpaqueTy<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<List<Clause>>
\ No newline at end of file + opaque_ty: &OpaqueTy<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<List<Clause>>

\ 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 d403dbe81a..d055b2f598 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,5 +1,5 @@ -conv_poly_func_sort in flux_fhir_analysis::conv - Rust
fn conv_poly_func_sort(
-    genv: GlobalEnv<'_, '_>,
-    sort: &PolyFuncSort<'_>,
-    next_infer_sort: &mut impl FnMut() -> Sort
-) -> PolyFuncSort
\ No newline at end of file +conv_poly_func_sort in flux_fhir_analysis::conv - Rust
fn conv_poly_func_sort(
+    genv: GlobalEnv<'_, '_>,
+    sort: &PolyFuncSort<'_>,
+    next_infer_sort: &mut impl FnMut() -> Sort
+) -> PolyFuncSort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_qualifier.html b/doc/flux_fhir_analysis/conv/fn.conv_qualifier.html index 14ebad029f..0db13fa526 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_qualifier.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_qualifier.html @@ -1,5 +1,5 @@ conv_qualifier in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_qualifier<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    qualifier: &Qualifier<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Qualifier>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + qualifier: &Qualifier<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Qualifier>
\ No newline at end of file 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 0bc46c8a68..54d11a29c8 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_refine_param.html @@ -1,5 +1,5 @@ -conv_refine_param in flux_fhir_analysis::conv - Rust
fn conv_refine_param(
-    genv: GlobalEnv<'_, '_>,
-    param: &RefineParam<'_>,
-    wfckresults: Option<&WfckResults<'_>>
-) -> RefineParam
\ No newline at end of file +conv_refine_param in flux_fhir_analysis::conv - Rust
fn conv_refine_param(
+    genv: GlobalEnv<'_, '_>,
+    param: &RefineParam<'_>,
+    wfckresults: Option<&WfckResults<'_>>
+) -> RefineParam
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_refinement_generics.html b/doc/flux_fhir_analysis/conv/fn.conv_refinement_generics.html index b03a7ab5fb..1ce42e4ba0 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_refinement_generics.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_refinement_generics.html @@ -1,5 +1,5 @@ conv_refinement_generics in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_refinement_generics<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    params: &[RefineParam<'_>],
-    wfckresults: Option<&WfckResults<'genv>>
-) -> List<RefineParam>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + params: &[RefineParam<'_>], + wfckresults: Option<&WfckResults<'genv>> +) -> List<RefineParam>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sort.html b/doc/flux_fhir_analysis/conv/fn.conv_sort.html index d3cec5077f..2c99716dd9 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_sort.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_sort.html @@ -1,5 +1,5 @@ -conv_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_sort(
-    genv: GlobalEnv<'_, '_>,
-    sort: &Sort<'_>,
-    next_infer_sort: &mut impl FnMut() -> Sort
-) -> Sort
\ No newline at end of file +conv_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_sort(
+    genv: GlobalEnv<'_, '_>,
+    sort: &Sort<'_>,
+    next_infer_sort: &mut impl FnMut() -> Sort
+) -> Sort
\ No newline at end of file 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 d7c4a6b0fc..84f1a350c7 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_sort_path.html @@ -1,5 +1,5 @@ -conv_sort_path in flux_fhir_analysis::conv - Rust
fn conv_sort_path(
-    genv: GlobalEnv<'_, '_>,
-    path: &SortPath<'_>,
-    next_infer_sort: &mut impl FnMut() -> Sort
-) -> Sort
\ No newline at end of file +conv_sort_path in flux_fhir_analysis::conv - Rust
fn conv_sort_path(
+    genv: GlobalEnv<'_, '_>,
+    path: &SortPath<'_>,
+    next_infer_sort: &mut impl FnMut() -> Sort
+) -> Sort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html index cd33e969c8..dfc20daf2d 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_sorts.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_sorts.html @@ -1,5 +1,5 @@ -conv_sorts in flux_fhir_analysis::conv - Rust
fn conv_sorts(
-    genv: GlobalEnv<'_, '_>,
-    sorts: &[Sort<'_>],
-    next_infer_sort: &mut impl FnMut() -> Sort
-) -> Vec<Sort>
\ No newline at end of file +conv_sorts in flux_fhir_analysis::conv - Rust
fn conv_sorts(
+    genv: GlobalEnv<'_, '_>,
+    sorts: &[Sort<'_>],
+    next_infer_sort: &mut impl FnMut() -> Sort
+) -> Vec<Sort>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.conv_ty.html b/doc/flux_fhir_analysis/conv/fn.conv_ty.html index 97f9a86adf..7856a3e0b9 100644 --- a/doc/flux_fhir_analysis/conv/fn.conv_ty.html +++ b/doc/flux_fhir_analysis/conv/fn.conv_ty.html @@ -1,5 +1,5 @@ conv_ty in flux_fhir_analysis::conv - Rust
pub(crate) fn conv_ty<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    ty: &Ty<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Binder<Ty>>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + ty: &Ty<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Binder<Ty>>
\ No newline at end of file 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 27de298968..e7fe5c1df9 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
fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file +conv_un_op in flux_fhir_analysis::conv - Rust
fn conv_un_op(op: UnOp) -> UnOp
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/fn.expand_type_alias.html b/doc/flux_fhir_analysis/conv/fn.expand_type_alias.html index 7d18c3b700..92f00a9cbc 100644 --- a/doc/flux_fhir_analysis/conv/fn.expand_type_alias.html +++ b/doc/flux_fhir_analysis/conv/fn.expand_type_alias.html @@ -1,6 +1,6 @@ expand_type_alias in flux_fhir_analysis::conv - Rust
pub(crate) fn expand_type_alias<'genv>(
-    genv: GlobalEnv<'genv, '_>,
+    genv: GlobalEnv<'genv, '_>,
     def_id: DefId,
-    alias: &TyAlias<'_>,
-    wfckresults: &WfckResults<'genv>
-) -> QueryResult<Binder<Ty>>
\ No newline at end of file + alias: &TyAlias<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Binder<Ty>>

\ 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 7f7a30e79e..c8fdf248b0 100644 --- a/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html +++ b/doc/flux_fhir_analysis/conv/fn.resolve_param_sort.html @@ -1,5 +1,5 @@ -resolve_param_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn resolve_param_sort(
-    genv: GlobalEnv<'_, '_>,
-    param: &RefineParam<'_>,
-    wfckresults: Option<&WfckResults<'_>>
-) -> Sort
\ No newline at end of file +resolve_param_sort in flux_fhir_analysis::conv - Rust
pub(crate) fn resolve_param_sort(
+    genv: GlobalEnv<'_, '_>,
+    param: &RefineParam<'_>,
+    wfckresults: Option<&WfckResults<'_>>
+) -> Sort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/conv/index.html b/doc/flux_fhir_analysis/conv/index.html index 49158f400d..aac9b982ec 100644 --- a/doc/flux_fhir_analysis/conv/index.html +++ b/doc/flux_fhir_analysis/conv/index.html @@ -1,10 +1,10 @@ -flux_fhir_analysis::conv - Rust
Expand description

Conversion from types in [fhir] to types in [rty]

+flux_fhir_analysis::conv - Rust
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:

  1. Names are bound correctly.
  2. Refinement parameters appear in allowed positions. This is particularly important for -refinement predicates, aka abstract refinements, since the syntax in [rty] has +refinement predicates, aka abstract refinements, since the syntax in rty has syntactic restrictions on predicates.
  3. Refinements are well-sorted.
diff --git a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html index 7d7c18c74e..f5abd554f6 100644 --- a/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html +++ b/doc/flux_fhir_analysis/conv/struct.ConvCtxt.html @@ -1,114 +1,114 @@ ConvCtxt in flux_fhir_analysis::conv - Rust
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>

source

pub(crate) fn new( - genv: GlobalEnv<'genv, 'tcx>, - wfckresults: &'a WfckResults<'genv> + 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>

source

pub(crate) fn new( + genv: GlobalEnv<'genv, 'tcx>, + wfckresults: &'a WfckResults<'genv> ) -> Self

source

fn conv_generic_bounds( &self, env: &mut Env, - bounded_ty: Ty, - bounds: GenericBounds<'_> -) -> QueryResult<Vec<Clause>>

source

fn conv_generic_bound( + bounded_ty: Ty, + bounds: GenericBounds<'_> +) -> QueryResult<Vec<Clause>>

source

fn conv_generic_bound( &self, env: &mut Env, - bounded_ty: &Ty, - bound: &GenericBound<'_>, - clauses: &mut Vec<Clause> -) -> QueryResult

source

fn conv_trait_bound( + bounded_ty: &Ty, + bound: &GenericBound<'_>, + clauses: &mut Vec<Clause> +) -> QueryResult

source

fn conv_trait_bound( &self, env: &mut Env, - bounded_ty: &Ty, + bounded_ty: &Ty, trait_id: DefId, - args: &[GenericArg<'_>], - params: &[GenericParam<'_>], - clauses: &mut Vec<Clause> -) -> QueryResult

source

fn conv_trait_bound_generic_param( + args: &[GenericArg<'_>], + params: &[GenericParam<'_>], + clauses: &mut Vec<Clause> +) -> QueryResult

source

fn conv_trait_bound_generic_param( &self, - param: &GenericParam<'_> -) -> QueryResult<BoundVariableKind>

source

fn conv_fn_bound( + param: &GenericParam<'_> +) -> QueryResult<BoundVariableKind>

source

fn conv_fn_bound( &self, env: &mut Env, - self_ty: &Ty, - trait_ref: &PolyTraitRef<'_>, + self_ty: &Ty, + trait_ref: &PolyTraitRef<'_>, kind: ClosureKind, - clauses: &mut Vec<Clause> -) -> QueryResult<()>

source

fn conv_type_bindings( + clauses: &mut Vec<Clause> +) -> QueryResult<()>

source

fn conv_type_bindings( &self, env: &mut Env, - bounded_ty: &Ty, + bounded_ty: &Ty, trait_def_id: DefId, - bindings: &[TypeBinding<'_>], - clauses: &mut Vec<Clause> -) -> QueryResult<()>

source

fn trait_defines_associated_item_named( + bindings: &[TypeBinding<'_>], + clauses: &mut Vec<Clause> +) -> QueryResult<()>

source

fn trait_defines_associated_item_named( &self, trait_def_id: DefId, assoc_kind: AssocKind, - assoc_name: SurfaceIdent + assoc_name: SurfaceIdent ) -> Option<&AssocItem>

source

fn conv_fn_output( &self, env: &mut Env, - output: &FnOutput<'_> -) -> QueryResult<Binder<FnOutput>>

source

pub(crate) fn conv_enum_def_variants( - genv: GlobalEnv<'genv, '_>, + output: &FnOutput<'_> +) -> QueryResult<Binder<FnOutput>>

source

pub(crate) fn conv_enum_def_variants( + genv: GlobalEnv<'genv, '_>, adt_def_id: DefId, - enum_def: &EnumDef<'_>, - wfckresults: &WfckResults<'genv> -) -> QueryResult<Vec<PolyVariant>>

source

fn conv_enum_variant( - genv: GlobalEnv<'genv, '_>, + enum_def: &EnumDef<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Vec<PolyVariant>>

source

fn conv_enum_variant( + genv: GlobalEnv<'genv, '_>, adt_def_id: DefId, - variant: &VariantDef<'_>, - wfckresults: &WfckResults<'genv> -) -> QueryResult<PolyVariant>

source

pub(crate) fn conv_struct_def_variant( - genv: GlobalEnv<'genv, '_>, + variant: &VariantDef<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<PolyVariant>

source

pub(crate) fn conv_struct_def_variant( + genv: GlobalEnv<'genv, '_>, adt_def_id: DefId, - struct_def: &StructDef<'_>, - wfckresults: &WfckResults<'genv> -) -> QueryResult<Opaqueness<PolyVariant>>

source

fn conv_constr( + struct_def: &StructDef<'_>, + wfckresults: &WfckResults<'genv> +) -> QueryResult<Opaqueness<PolyVariant>>

source

fn conv_constr( &self, env: &mut Env, - constr: &Constraint<'_> -) -> QueryResult<Constraint>

source

fn conv_alias_reft( + constr: &Constraint<'_> +) -> QueryResult<Constraint>

source

fn conv_alias_reft( &self, env: &mut Env, - alias: &AliasReft<'_>, - func_args: &[Expr<'_>] -) -> QueryResult<Expr>

source

fn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>

source

fn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>

source

fn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region

source

fn conv_refine_arg( + alias: &AliasReft<'_>, + func_args: &[Expr<'_>] +) -> QueryResult<Expr>

source

fn conv_ty(&self, env: &mut Env, ty: &Ty<'_>) -> QueryResult<Ty>

source

fn conv_base_ty(&self, env: &mut Env, bty: &BaseTy<'_>) -> QueryResult<Ty>

source

fn conv_lifetime(&self, env: &Env, lft: Lifetime) -> Region

source

fn conv_refine_arg( &self, env: &mut Env, - arg: &RefineArg<'_> -) -> QueryResult<Expr>

source

fn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>

source

pub fn conv_generic_args( + arg: &RefineArg<'_> +) -> QueryResult<Expr>

source

fn conv_ty_ctor(&self, env: &mut Env, path: &Path<'_>) -> QueryResult<TyCtor>

source

pub fn conv_generic_args( &self, env: &mut Env, def_id: DefId, - args: &[GenericArg<'_>] -) -> QueryResult<Vec<GenericArg>>

source

fn conv_generic_args_into( + args: &[GenericArg<'_>] +) -> QueryResult<Vec<GenericArg>>

source

fn conv_generic_args_into( &self, env: &mut Env, def_id: DefId, - args: &[GenericArg<'_>], - into: &mut Vec<GenericArg> -) -> QueryResult

source

fn fill_generic_args_defaults( + args: &[GenericArg<'_>], + into: &mut Vec<GenericArg> +) -> QueryResult

source

fn fill_generic_args_defaults( &self, def_id: DefId, - into: &mut Vec<GenericArg> -) -> QueryResult

source

fn conv_generic_base( + into: &mut Vec<GenericArg> +) -> QueryResult

source

fn conv_generic_base( &self, env: &mut Env, - ty: &Ty<'_> -) -> QueryResult<SubsetTyCtor>

source

fn resolve_param_sort(&self, param: &RefineParam<'_>) -> Sort

source§

impl ConvCtxt<'_, '_, '_>

source

fn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>

source

fn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp

source

fn bin_rel_sort(&self, fhir_id: FhirId) -> Sort

source

fn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr

source

fn conv_exprs( + ty: &Ty<'_> +) -> QueryResult<SubsetTyCtor>

source

fn resolve_param_sort(&self, param: &RefineParam<'_>) -> Sort

source§

impl ConvCtxt<'_, '_, '_>

source

fn conv_expr(&self, env: &mut Env, expr: &Expr<'_>) -> QueryResult<Expr>

source

fn conv_bin_op(&self, op: BinOp, fhir_id: FhirId) -> BinOp

source

fn bin_rel_sort(&self, fhir_id: FhirId) -> Sort

source

fn conv_func(&self, env: &Env, func: &PathExpr<'_>) -> Expr

source

fn conv_exprs( &self, env: &mut Env, - exprs: &[Expr<'_>] -) -> QueryResult<List<Expr>>

source

fn conv_invariants( + exprs: &[Expr<'_>] +) -> QueryResult<List<Expr>>

source

fn conv_invariants( &self, env: &mut Env, - invariants: &[Expr<'_>] -) -> QueryResult<Vec<Invariant>>

source

fn conv_invariant( + invariants: &[Expr<'_>] +) -> QueryResult<Vec<Invariant>>

source

fn conv_invariant( &self, env: &mut Env, - invariant: &Expr<'_> -) -> QueryResult<Invariant>

source

fn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr

Auto Trait Implementations§

§

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 + invariant: &Expr<'_> +) -> QueryResult<Invariant>

source

fn add_coercions(&self, expr: Expr, fhir_id: FhirId) -> Expr

Auto Trait Implementations§

§

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 T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/conv/struct.Env.html b/doc/flux_fhir_analysis/conv/struct.Env.html index d048d5a67a..6e5bb2f7a8 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
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

source

pub(crate) fn new( - genv: GlobalEnv<'_, '_>, - early_bound: &[RefineParam<'_>], - wfckresults: &WfckResults<'_> -) -> Self

source

fn depth(&self) -> usize

source

fn push_layer(&mut self, layer: Layer)

source

fn pop_layer(&mut self) -> Layer

source

fn top_layer(&self) -> &Layer

source

fn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>

source

fn to_early_bound_vars(&self) -> List<Expr>

Auto Trait Implementations§

§

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> Any for Twhere + early_bound: FxIndexMap<ParamId, (Symbol, Sort)>, +}

Fields§

§layers: Vec<Layer>§early_bound: FxIndexMap<ParamId, (Symbol, Sort)>

Implementations§

source§

impl Env

source

pub(crate) fn new( + genv: GlobalEnv<'_, '_>, + early_bound: &[RefineParam<'_>], + wfckresults: &WfckResults<'_> +) -> Self

source

fn depth(&self) -> usize

source

fn push_layer(&mut self, layer: Layer)

source

fn pop_layer(&mut self) -> Layer

source

fn top_layer(&self) -> &Layer

source

fn lookup(&self, var: &PathExpr<'_>) -> LookupResult<'_>

source

fn to_early_bound_vars(&self) -> List<Expr>

Auto Trait Implementations§

§

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> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/conv/struct.Layer.html b/doc/flux_fhir_analysis/conv/struct.Layer.html index 7fd20e77c8..24908dd2f5 100644 --- a/doc/flux_fhir_analysis/conv/struct.Layer.html +++ b/doc/flux_fhir_analysis/conv/struct.Layer.html @@ -1,28 +1,28 @@ Layer in flux_fhir_analysis::conv - Rust
struct Layer {
-    map: FxIndexMap<ParamId, Entry>,
+    map: FxIndexMap<ParamId, Entry>,
     filter_unit: bool,
     kind: LayerKind,
-}

Fields§

§map: FxIndexMap<ParamId, Entry>§filter_unit: bool

Whether to skip variables bound to Unit in this layer.

-
§kind: LayerKind

Implementations§

source§

impl Layer

source

fn new( +}

Fields§

§map: FxIndexMap<ParamId, Entry>§filter_unit: bool

Whether to skip variables bound to Unit in this layer.

+
§kind: LayerKind

Implementations§

source§

impl Layer

source

fn new( cx: &ConvCtxt<'_, '_, '_>, late_bound_regions: u32, - params: &[RefineParam<'_>], + params: &[RefineParam<'_>], filter_unit: bool, kind: LayerKind -) -> Self

source

fn list( +) -> Self

source

fn list( cx: &ConvCtxt<'_, '_, '_>, late_bound_regions: u32, - params: &[RefineParam<'_>], + params: &[RefineParam<'_>], filter_unit: bool -) -> Self

source

fn record( +) -> Self

source

fn record( cx: &ConvCtxt<'_, '_, '_>, def_id: DefId, - params: &[RefineParam<'_>] -) -> Self

source

fn get( + params: &[RefineParam<'_>] +) -> Self

source

fn get( &self, - name: impl Borrow<ParamId>, + name: impl Borrow<ParamId>, level: u32 -) -> Option<LookupResultKind<'_>>

source

fn into_bound_vars(self, genv: GlobalEnv<'_, '_>) -> List<BoundVariableKind>

source

fn to_bound_vars(&self, genv: GlobalEnv<'_, '_>) -> List<BoundVariableKind>

source

fn into_iter(self) -> impl Iterator<Item = (Sort, InferMode, Symbol)>

Trait Implementations§

source§

impl Clone for Layer

source§

fn clone(&self) -> Layer

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl Debug for Layer

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

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 +) -> Option<LookupResultKind<'_>>

source

fn into_bound_vars(self, genv: GlobalEnv<'_, '_>) -> List<BoundVariableKind>

source

fn to_bound_vars(&self, genv: GlobalEnv<'_, '_>) -> List<BoundVariableKind>

source

fn into_iter(self) -> impl Iterator<Item = (Sort, InferMode, Symbol)>

Trait Implementations§

source§

impl Clone for Layer

source§

fn clone(&self) -> Layer

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl Debug for Layer

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

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 T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/conv/struct.LookupResult.html b/doc/flux_fhir_analysis/conv/struct.LookupResult.html index 119c893ed9..d8ff765be0 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§

source§

impl LookupResult<'_>

source

fn to_expr(&self) -> Expr

source

fn is_adt(&self) -> Option<&AdtSortDef>

source

fn to_path(&self) -> Path

source

fn get_field(&self, fld: SurfaceIdent) -> Expr

Trait Implementations§

source§

impl<'a> Debug for LookupResult<'a>

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

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§

source§

impl<'a> Debug for LookupResult<'a>

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more

Auto Trait Implementations§

§

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 T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/fn.adt_def.html b/doc/flux_fhir_analysis/fn.adt_def.html index 5f44c802c5..cdf39e169c 100644 --- a/doc/flux_fhir_analysis/fn.adt_def.html +++ b/doc/flux_fhir_analysis/fn.adt_def.html @@ -1,4 +1,4 @@ adt_def in flux_fhir_analysis - Rust
pub(crate) fn adt_def(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> QueryResult<AdtDef>
\ No newline at end of file +) -> QueryResult<AdtDef>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.adt_sort_def_of.html b/doc/flux_fhir_analysis/fn.adt_sort_def_of.html index a89fb07a83..73623ee02f 100644 --- a/doc/flux_fhir_analysis/fn.adt_sort_def_of.html +++ b/doc/flux_fhir_analysis/fn.adt_sort_def_of.html @@ -1,4 +1,4 @@ adt_sort_def_of in flux_fhir_analysis - Rust
pub(crate) fn adt_sort_def_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> AdtSortDef
\ No newline at end of file +) -> AdtSortDef

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.assoc_refinement_def.html b/doc/flux_fhir_analysis/fn.assoc_refinement_def.html index 4875a9fc21..db68040173 100644 --- a/doc/flux_fhir_analysis/fn.assoc_refinement_def.html +++ b/doc/flux_fhir_analysis/fn.assoc_refinement_def.html @@ -1,5 +1,5 @@ assoc_refinement_def in flux_fhir_analysis - Rust
pub(crate) fn assoc_refinement_def(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     impl_id: LocalDefId,
     name: Symbol
-) -> QueryResult<EarlyBinder<Lambda>>
\ No newline at end of file +) -> QueryResult<EarlyBinder<Lambda>>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.assoc_refinements_of.html b/doc/flux_fhir_analysis/fn.assoc_refinements_of.html index 9bfec51b44..dc58a72b94 100644 --- a/doc/flux_fhir_analysis/fn.assoc_refinements_of.html +++ b/doc/flux_fhir_analysis/fn.assoc_refinements_of.html @@ -1,4 +1,4 @@ assoc_refinements_of in flux_fhir_analysis - Rust
pub(crate) fn assoc_refinements_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     local_id: LocalDefId
-) -> AssocRefinements
\ No newline at end of file +) -> AssocRefinements
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.check_crate_wf.html b/doc/flux_fhir_analysis/fn.check_crate_wf.html index a476888a62..0ba6ee68d9 100644 --- a/doc/flux_fhir_analysis/fn.check_crate_wf.html +++ b/doc/flux_fhir_analysis/fn.check_crate_wf.html @@ -1 +1 @@ -check_crate_wf in flux_fhir_analysis - Rust
pub fn check_crate_wf(genv: GlobalEnv<'_, '_>) -> Result<(), ErrorGuaranteed>
\ No newline at end of file +check_crate_wf in flux_fhir_analysis - Rust
pub fn check_crate_wf(genv: GlobalEnv<'_, '_>) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.check_wf.html b/doc/flux_fhir_analysis/fn.check_wf.html index d80ddb754f..2a6061855f 100644 --- a/doc/flux_fhir_analysis/fn.check_wf.html +++ b/doc/flux_fhir_analysis/fn.check_wf.html @@ -1,4 +1,4 @@ check_wf in flux_fhir_analysis - Rust
pub(crate) fn check_wf<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    flux_id: FluxLocalDefId
-) -> QueryResult<Rc<WfckResults<'genv>>>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + flux_id: FluxLocalDefId +) -> QueryResult<Rc<WfckResults<'genv>>>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.fn_sig.html b/doc/flux_fhir_analysis/fn.fn_sig.html index 8fd8f8063a..938b79e72b 100644 --- a/doc/flux_fhir_analysis/fn.fn_sig.html +++ b/doc/flux_fhir_analysis/fn.fn_sig.html @@ -1,4 +1,4 @@ fn_sig in flux_fhir_analysis - Rust

Function flux_fhir_analysis::fn_sig

source ·
pub(crate) fn fn_sig(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> QueryResult<EarlyBinder<PolyFnSig>>
\ No newline at end of file +) -> QueryResult<EarlyBinder<PolyFnSig>>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.generics_of.html b/doc/flux_fhir_analysis/fn.generics_of.html index a5bba6e3a9..6381055013 100644 --- a/doc/flux_fhir_analysis/fn.generics_of.html +++ b/doc/flux_fhir_analysis/fn.generics_of.html @@ -1,4 +1,4 @@ generics_of in flux_fhir_analysis - Rust
pub(crate) fn generics_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     local_id: LocalDefId
-) -> QueryResult<Generics>
\ No newline at end of file +) -> QueryResult<Generics>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.invariants_of.html b/doc/flux_fhir_analysis/fn.invariants_of.html index 92987ca888..de1e4ff410 100644 --- a/doc/flux_fhir_analysis/fn.invariants_of.html +++ b/doc/flux_fhir_analysis/fn.invariants_of.html @@ -1,4 +1,4 @@ invariants_of in flux_fhir_analysis - Rust
pub(crate) fn invariants_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> QueryResult<Vec<Invariant>>
\ No newline at end of file +) -> QueryResult<Vec<Invariant>>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.item_bounds.html b/doc/flux_fhir_analysis/fn.item_bounds.html index 150d48d192..eb59eb5081 100644 --- a/doc/flux_fhir_analysis/fn.item_bounds.html +++ b/doc/flux_fhir_analysis/fn.item_bounds.html @@ -1,4 +1,4 @@ item_bounds in flux_fhir_analysis - Rust
pub(crate) fn item_bounds(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     local_id: LocalDefId
-) -> QueryResult<EarlyBinder<List<Clause>>>
\ No newline at end of file +) -> QueryResult<EarlyBinder<List<Clause>>> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.normalize.html b/doc/flux_fhir_analysis/fn.normalize.html index 09ac866125..62da2d63f8 100644 --- a/doc/flux_fhir_analysis/fn.normalize.html +++ b/doc/flux_fhir_analysis/fn.normalize.html @@ -1,4 +1,4 @@ -normalize in flux_fhir_analysis - Rust
pub(crate) fn normalize<T: TypeFoldable>(
-    genv: GlobalEnv<'_, '_>,
+normalize in flux_fhir_analysis - Rust
pub(crate) fn normalize<T: TypeFoldable>(
+    genv: GlobalEnv<'_, '_>,
     t: T
-) -> QueryResult<T>
\ No newline at end of file +) -> QueryResult<T>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.predicates_of.html b/doc/flux_fhir_analysis/fn.predicates_of.html index 6c46d9484e..82b9f6ade0 100644 --- a/doc/flux_fhir_analysis/fn.predicates_of.html +++ b/doc/flux_fhir_analysis/fn.predicates_of.html @@ -1,4 +1,4 @@ predicates_of in flux_fhir_analysis - Rust
pub(crate) fn predicates_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     local_id: LocalDefId
-) -> QueryResult<EarlyBinder<GenericPredicates>>
\ No newline at end of file +) -> QueryResult<EarlyBinder<GenericPredicates>> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.provide.html b/doc/flux_fhir_analysis/fn.provide.html index 79e529e078..023835b276 100644 --- a/doc/flux_fhir_analysis/fn.provide.html +++ b/doc/flux_fhir_analysis/fn.provide.html @@ -1 +1 @@ -provide in flux_fhir_analysis - Rust
pub fn provide(providers: &mut Providers)
\ No newline at end of file +provide in flux_fhir_analysis - Rust
pub fn provide(providers: &mut Providers)
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.qualifiers.html b/doc/flux_fhir_analysis/fn.qualifiers.html index 4503d23791..efb4535451 100644 --- a/doc/flux_fhir_analysis/fn.qualifiers.html +++ b/doc/flux_fhir_analysis/fn.qualifiers.html @@ -1 +1 @@ -qualifiers in flux_fhir_analysis - Rust
pub(crate) fn qualifiers(genv: GlobalEnv<'_, '_>) -> QueryResult<Vec<Qualifier>>
\ No newline at end of file +qualifiers in flux_fhir_analysis - Rust
pub(crate) fn qualifiers(genv: GlobalEnv<'_, '_>) -> QueryResult<Vec<Qualifier>>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.refinement_generics_of.html b/doc/flux_fhir_analysis/fn.refinement_generics_of.html index c2fe4a13e0..677bb9fdb5 100644 --- a/doc/flux_fhir_analysis/fn.refinement_generics_of.html +++ b/doc/flux_fhir_analysis/fn.refinement_generics_of.html @@ -1,4 +1,4 @@ refinement_generics_of in flux_fhir_analysis - Rust
pub(crate) fn refinement_generics_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     local_id: LocalDefId
-) -> QueryResult<RefinementGenerics>
\ No newline at end of file +) -> QueryResult<RefinementGenerics> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.sort_of_assoc_reft.html b/doc/flux_fhir_analysis/fn.sort_of_assoc_reft.html index e6d815e661..43b3c0fcd8 100644 --- a/doc/flux_fhir_analysis/fn.sort_of_assoc_reft.html +++ b/doc/flux_fhir_analysis/fn.sort_of_assoc_reft.html @@ -1,5 +1,5 @@ sort_of_assoc_reft in flux_fhir_analysis - Rust
pub(crate) fn sort_of_assoc_reft(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId,
     name: Symbol
-) -> Option<EarlyBinder<FuncSort>>
\ No newline at end of file +) -> Option<EarlyBinder<FuncSort>> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.spec_func_decls.html b/doc/flux_fhir_analysis/fn.spec_func_decls.html index 2ecccbd052..eefdb11f94 100644 --- a/doc/flux_fhir_analysis/fn.spec_func_decls.html +++ b/doc/flux_fhir_analysis/fn.spec_func_decls.html @@ -1,3 +1,3 @@ spec_func_decls in flux_fhir_analysis - Rust
pub(crate) fn spec_func_decls(
-    genv: GlobalEnv<'_, '_>
-) -> FxHashMap<Symbol, SpecFuncDecl>
\ No newline at end of file + genv: GlobalEnv<'_, '_> +) -> FxHashMap<Symbol, SpecFuncDecl> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.spec_func_defns.html b/doc/flux_fhir_analysis/fn.spec_func_defns.html index 4eb691bb65..3713ace1a2 100644 --- a/doc/flux_fhir_analysis/fn.spec_func_defns.html +++ b/doc/flux_fhir_analysis/fn.spec_func_defns.html @@ -1,3 +1,3 @@ spec_func_defns in flux_fhir_analysis - Rust
pub(crate) fn spec_func_defns(
-    genv: GlobalEnv<'_, '_>
-) -> QueryResult<SpecFuncDefns>
\ No newline at end of file + genv: GlobalEnv<'_, '_> +) -> QueryResult<SpecFuncDefns> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.type_of.html b/doc/flux_fhir_analysis/fn.type_of.html index c4d7d9582e..6c7122ae1f 100644 --- a/doc/flux_fhir_analysis/fn.type_of.html +++ b/doc/flux_fhir_analysis/fn.type_of.html @@ -1,4 +1,4 @@ type_of in flux_fhir_analysis - Rust
pub(crate) fn type_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> QueryResult<EarlyBinder<TyCtor>>
\ No newline at end of file +) -> QueryResult<EarlyBinder<TyCtor>> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/fn.variants_of.html b/doc/flux_fhir_analysis/fn.variants_of.html index 3737da00ce..7421ebc521 100644 --- a/doc/flux_fhir_analysis/fn.variants_of.html +++ b/doc/flux_fhir_analysis/fn.variants_of.html @@ -1,4 +1,4 @@ variants_of in flux_fhir_analysis - Rust
pub(crate) fn variants_of(
-    genv: GlobalEnv<'_, '_>,
+    genv: GlobalEnv<'_, '_>,
     def_id: LocalDefId
-) -> QueryResult<Opaqueness<EarlyBinder<PolyVariants>>>
\ No newline at end of file +) -> QueryResult<Opaqueness<EarlyBinder<PolyVariants>>> \ No newline at end of file diff --git a/doc/flux_fhir_analysis/index.html b/doc/flux_fhir_analysis/index.html index 8833c1ee1e..83e99f813e 100644 --- a/doc/flux_fhir_analysis/index.html +++ b/doc/flux_fhir_analysis/index.html @@ -1,3 +1,3 @@ flux_fhir_analysis - Rust

Modules

  • Check if an fhir annotation is a valid refinement of the corresponding rust declaration.
  • conv 🔒
    Conversion from types in [fhir] to types in [rty]
  • errors 🔒
  • wf 🔒
    Checks type well-formedness

Statics

Modules

Statics

  • Raw content of Fluent resource for this crate, generated by fluent_messages macro, imported by rustc_driver to include all crates’ resources in one bundle.

Functions

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/errors/struct.DuplicatedEnsures.html b/doc/flux_fhir_analysis/wf/errors/struct.DuplicatedEnsures.html index 3749fc86e8..3fdc4ca356 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.DuplicatedEnsures.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.DuplicatedEnsures.html @@ -1,7 +1,7 @@ DuplicatedEnsures in flux_fhir_analysis::wf::errors - Rust
pub(super) struct DuplicatedEnsures {
     span: Span,
     loc: String,
-}

Fields§

§span: Span§loc: String

Implementations§

source§

impl DuplicatedEnsures

source

pub(super) fn new(loc: &PathExpr<'_>) -> DuplicatedEnsures

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for DuplicatedEnsureswhere +}

Fields§

§span: Span§loc: String

Implementations§

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for DuplicatedEnsureswhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.ExpectedFun.html b/doc/flux_fhir_analysis/wf/errors/struct.ExpectedFun.html index 9d40537716..6e1d7af72d 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.ExpectedFun.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.ExpectedFun.html @@ -1,7 +1,7 @@ ExpectedFun in flux_fhir_analysis::wf::errors - Rust
pub(super) struct ExpectedFun<'a> {
     span: Span,
-    found: &'a Sort,
-}

Fields§

§span: Span§found: &'a Sort

Implementations§

source§

impl<'a> ExpectedFun<'a>

source

pub(super) fn new(span: Span, found: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for ExpectedFun<'a>where + found: &'a Sort, +}

Fields§

§span: Span§found: &'a Sort

Implementations§

source§

impl<'a> ExpectedFun<'a>

source

pub(super) fn new(span: Span, found: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for ExpectedFun<'a>where G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.FieldNotFound.html b/doc/flux_fhir_analysis/wf/errors/struct.FieldNotFound.html index a130b5b9c0..4fe8bb9666 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.FieldNotFound.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.FieldNotFound.html @@ -1,8 +1,8 @@ FieldNotFound in flux_fhir_analysis::wf::errors - Rust
pub(super) struct FieldNotFound {
     span: Span,
-    sort: Sort,
-    fld: SurfaceIdent,
-}

Fields§

§span: Span§sort: Sort§fld: SurfaceIdent

Implementations§

source§

impl FieldNotFound

source

pub(super) fn new(sort: Sort, fld: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for FieldNotFoundwhere + sort: Sort, + fld: SurfaceIdent, +}

Fields§

§span: Span§sort: Sort§fld: SurfaceIdent

Implementations§

source§

impl FieldNotFound

source

pub(super) fn new(sort: Sort, fld: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for FieldNotFoundwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.InvalidParamPos.html b/doc/flux_fhir_analysis/wf/errors/struct.InvalidParamPos.html index 6990609ab8..685461d8f9 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.InvalidParamPos.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.InvalidParamPos.html @@ -1,8 +1,8 @@ InvalidParamPos in flux_fhir_analysis::wf::errors - Rust
pub(super) struct InvalidParamPos<'a> {
     span: Span,
-    sort: &'a Sort,
+    sort: &'a Sort,
     is_pred: bool,
-}

Fields§

§span: Span§sort: &'a Sort§is_pred: bool

Implementations§

source§

impl<'a> InvalidParamPos<'a>

source

pub(super) fn new(span: Span, sort: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidParamPos<'a>where +}

Fields§

§span: Span§sort: &'a Sort§is_pred: bool

Implementations§

source§

impl<'a> InvalidParamPos<'a>

source

pub(super) fn new(span: Span, sort: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidParamPos<'a>where G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.InvalidPrimitiveDotAccess.html b/doc/flux_fhir_analysis/wf/errors/struct.InvalidPrimitiveDotAccess.html index 0c1e3c759f..32fdf57c00 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.InvalidPrimitiveDotAccess.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.InvalidPrimitiveDotAccess.html @@ -1,7 +1,7 @@ InvalidPrimitiveDotAccess in flux_fhir_analysis::wf::errors - Rust
pub(super) struct InvalidPrimitiveDotAccess<'a> {
     span: Span,
-    sort: &'a Sort,
-}

Fields§

§span: Span§sort: &'a Sort

Implementations§

source§

impl<'a> InvalidPrimitiveDotAccess<'a>

source

pub(super) fn new(sort: &'a Sort, fld: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidPrimitiveDotAccess<'a>where + sort: &'a Sort, +}

Fields§

§span: Span§sort: &'a Sort

Implementations§

source§

impl<'a> InvalidPrimitiveDotAccess<'a>

source

pub(super) fn new(sort: &'a Sort, fld: SurfaceIdent) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for InvalidPrimitiveDotAccess<'a>where G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.MissingEnsures.html b/doc/flux_fhir_analysis/wf/errors/struct.MissingEnsures.html index 19ea07cea1..9c0c6f7dee 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.MissingEnsures.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.MissingEnsures.html @@ -1,6 +1,6 @@ MissingEnsures in flux_fhir_analysis::wf::errors - Rust
pub(super) struct MissingEnsures {
     span: Span,
-}

Fields§

§span: Span

Implementations§

source§

impl MissingEnsures

source

pub(super) fn new(loc: &PathExpr<'_>) -> MissingEnsures

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for MissingEnsureswhere +}

Fields§

§span: Span

Implementations§

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for MissingEnsureswhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.SortAnnotationNeeded.html b/doc/flux_fhir_analysis/wf/errors/struct.SortAnnotationNeeded.html index 9929b38c67..cd3b6e67f4 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.SortAnnotationNeeded.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.SortAnnotationNeeded.html @@ -1,6 +1,6 @@ SortAnnotationNeeded in flux_fhir_analysis::wf::errors - Rust
pub(super) struct SortAnnotationNeeded {
     span: Span,
-}

Fields§

§span: Span

Implementations§

source§

impl SortAnnotationNeeded

source

pub(super) fn new(param: &RefineParam<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for SortAnnotationNeededwhere +}

Fields§

§span: Span

Implementations§

source§

impl SortAnnotationNeeded

source

pub(super) fn new(param: &RefineParam<'_>) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for SortAnnotationNeededwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.SortMismatch.html b/doc/flux_fhir_analysis/wf/errors/struct.SortMismatch.html index 75f707a56f..7a1b7a8c53 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.SortMismatch.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.SortMismatch.html @@ -1,8 +1,8 @@ SortMismatch in flux_fhir_analysis::wf::errors - Rust
pub(super) struct SortMismatch {
     span: Span,
-    expected: Sort,
-    found: Sort,
-}

Fields§

§span: Span§expected: Sort§found: Sort

Implementations§

source§

impl SortMismatch

source

pub(super) fn new(span: Span, expected: Sort, found: Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for SortMismatchwhere + expected: Sort, + found: Sort, +}

Fields§

§span: Span§expected: Sort§found: Sort

Implementations§

source§

impl SortMismatch

source

pub(super) fn new(span: Span, expected: Sort, found: Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for SortMismatchwhere G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/errors/struct.UnexpectedFun.html b/doc/flux_fhir_analysis/wf/errors/struct.UnexpectedFun.html index 60310de94c..e455faf5ed 100644 --- a/doc/flux_fhir_analysis/wf/errors/struct.UnexpectedFun.html +++ b/doc/flux_fhir_analysis/wf/errors/struct.UnexpectedFun.html @@ -1,7 +1,7 @@ UnexpectedFun in flux_fhir_analysis::wf::errors - Rust
pub(super) struct UnexpectedFun<'a> {
     span: Span,
-    sort: &'a Sort,
-}

Fields§

§span: Span§sort: &'a Sort

Implementations§

source§

impl<'a> UnexpectedFun<'a>

source

pub(super) fn new(span: Span, sort: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for UnexpectedFun<'a>where + sort: &'a Sort, +}

Fields§

§span: Span§sort: &'a Sort

Implementations§

source§

impl<'a> UnexpectedFun<'a>

source

pub(super) fn new(span: Span, sort: &'a Sort) -> Self

Trait Implementations§

source§

impl<'__diagnostic_handler_sess, 'a, G> IntoDiagnostic<'__diagnostic_handler_sess, G> for UnexpectedFun<'a>where G: EmissionGuarantee,

source§

fn into_diagnostic( self, sess: &'__diagnostic_handler_sess Handler diff --git a/doc/flux_fhir_analysis/wf/fn.check_flux_item.html b/doc/flux_fhir_analysis/wf/fn.check_flux_item.html index 9fffc54519..72b0460a2a 100644 --- a/doc/flux_fhir_analysis/wf/fn.check_flux_item.html +++ b/doc/flux_fhir_analysis/wf/fn.check_flux_item.html @@ -1,4 +1,4 @@ check_flux_item in flux_fhir_analysis::wf - Rust
pub(crate) fn check_flux_item<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    item: &FluxItem<'_>
-) -> Result<WfckResults<'genv>, ErrorGuaranteed>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + item: &FluxItem<'_> +) -> Result<WfckResults<'genv>, ErrorGuaranteed>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/fn.check_fn_quals.html b/doc/flux_fhir_analysis/wf/fn.check_fn_quals.html index 0b32c2e38f..8144784e65 100644 --- a/doc/flux_fhir_analysis/wf/fn.check_fn_quals.html +++ b/doc/flux_fhir_analysis/wf/fn.check_fn_quals.html @@ -1,5 +1,5 @@ check_fn_quals in flux_fhir_analysis::wf - Rust
pub(crate) fn check_fn_quals(
     sess: &FluxSession,
     qualifiers: &UnordSet<Symbol>,
-    fn_quals: &[SurfaceIdent]
+    fn_quals: &[SurfaceIdent]
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/fn.check_node.html b/doc/flux_fhir_analysis/wf/fn.check_node.html index 9b99944a39..04ce62c429 100644 --- a/doc/flux_fhir_analysis/wf/fn.check_node.html +++ b/doc/flux_fhir_analysis/wf/fn.check_node.html @@ -1,4 +1,4 @@ check_node in flux_fhir_analysis::wf - Rust
pub(crate) fn check_node<'genv>(
-    genv: GlobalEnv<'genv, '_>,
-    node: &Node<'_>
-) -> Result<WfckResults<'genv>, ErrorGuaranteed>
\ No newline at end of file + genv: GlobalEnv<'genv, '_>, + node: &Node<'_> +) -> Result<WfckResults<'genv>, ErrorGuaranteed>

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/fn.insert_params.html b/doc/flux_fhir_analysis/wf/fn.insert_params.html index 9e48e15bcf..568e008c7f 100644 --- a/doc/flux_fhir_analysis/wf/fn.insert_params.html +++ b/doc/flux_fhir_analysis/wf/fn.insert_params.html @@ -1,5 +1,5 @@ insert_params in flux_fhir_analysis::wf - Rust
fn insert_params(
     infcx: &mut InferCtxt<'_, '_>,
-    node: &Node<'_>
+    node: &Node<'_>
 ) -> Result<(), ErrorGuaranteed>
Expand description

Initializes the inference context with all parameters required to check node

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/fn.resolve_params.html b/doc/flux_fhir_analysis/wf/fn.resolve_params.html index 504cda2eb5..ab90796c1b 100644 --- a/doc/flux_fhir_analysis/wf/fn.resolve_params.html +++ b/doc/flux_fhir_analysis/wf/fn.resolve_params.html @@ -1,5 +1,5 @@ resolve_params in flux_fhir_analysis::wf - Rust
fn resolve_params(
     infcx: &mut InferCtxt<'_, '_>,
-    node: &Node<'_>
-) -> Result<(), ErrorGuaranteed>
Expand description

Check that all params with [fhir::Sort::Infer] have a sort inferred and save it in the [WfckResults]

+ node: &Node<'_> +) -> Result<(), ErrorGuaranteed>
Expand description

Check that all params with fhir::Sort::Infer have a sort inferred and save it in the WfckResults

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/fn.visit_refine_params.html b/doc/flux_fhir_analysis/wf/fn.visit_refine_params.html index b78e85e683..b5d55cda95 100644 --- a/doc/flux_fhir_analysis/wf/fn.visit_refine_params.html +++ b/doc/flux_fhir_analysis/wf/fn.visit_refine_params.html @@ -1 +1 @@ -visit_refine_params in flux_fhir_analysis::wf - Rust
fn visit_refine_params(node: &Node<'_>, f: impl FnMut(&RefineParam<'_>))
\ No newline at end of file +visit_refine_params in flux_fhir_analysis::wf - Rust
fn visit_refine_params(node: &Node<'_>, f: impl FnMut(&RefineParam<'_>))
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/index.html b/doc/flux_fhir_analysis/wf/index.html index 05f06b0c11..b593753d0f 100644 --- a/doc/flux_fhir_analysis/wf/index.html +++ b/doc/flux_fhir_analysis/wf/index.html @@ -1,3 +1,3 @@ flux_fhir_analysis::wf - Rust

Module flux_fhir_analysis::wf

source ·
Expand description

Checks type well-formedness

Well-formedness checking assumes names are correctly bound which is guaranteed after desugaring.

-

Modules

  • errors 🔒
  • Code to check whether refinement parameters are used in allowed positions.
  • sortck 🔒

Structs

Functions

Type Aliases

\ No newline at end of file +

Modules

  • errors 🔒
  • Code to check whether refinement parameters are used in allowed positions.
  • sortck 🔒

Structs

Functions

Type Aliases

\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/param_usage/fn.check.html b/doc/flux_fhir_analysis/wf/param_usage/fn.check.html index 0486166e09..9dd58b226a 100644 --- a/doc/flux_fhir_analysis/wf/param_usage/fn.check.html +++ b/doc/flux_fhir_analysis/wf/param_usage/fn.check.html @@ -1,4 +1,4 @@ check in flux_fhir_analysis::wf::param_usage - Rust
pub(crate) fn check(
     infcx: &InferCtxt<'_, '_>,
-    node: &Node<'_>
+    node: &Node<'_>
 ) -> Result<(), ErrorGuaranteed>
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/param_usage/index.html b/doc/flux_fhir_analysis/wf/param_usage/index.html index bc28a053c8..11a28a0948 100644 --- a/doc/flux_fhir_analysis/wf/param_usage/index.html +++ b/doc/flux_fhir_analysis/wf/param_usage/index.html @@ -1,5 +1,5 @@ flux_fhir_analysis::wf::param_usage - Rust
Expand description

Code to check whether refinement parameters are used in allowed positions.

-

The correct usage of a parameter depends on whether its infer mode is evar or kvar. +

The correct usage of a parameter depends on whether its infer mode is evar or kvar. For evar mode, parameters must be used at least once as an index in a position that fully determines their value (see https://arxiv.org/pdf/2209.13000.pdf for details). Parameters with kvar mode (i.e., abstract refinement predicates) must only be used in function position 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 12a53dc7aa..dce23ebb46 100644 --- a/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html +++ b/doc/flux_fhir_analysis/wf/param_usage/struct.ParamUsesChecker.html @@ -1,17 +1,17 @@ ParamUsesChecker in flux_fhir_analysis::wf::param_usage - Rust

struct ParamUsesChecker<'a, 'genv, 'tcx> {
     infcx: &'a InferCtxt<'genv, 'tcx>,
-    xi: SnapshotMap<ParamId, ()>,
+    xi: SnapshotMap<ParamId, ()>,
     errors: Errors<'genv>,
-}

Fields§

§infcx: &'a InferCtxt<'genv, 'tcx>§xi: SnapshotMap<ParamId, ()>

Keeps track of all refinement parameters that are used as an index such that their value is fully +}

Fields§

§infcx: &'a InferCtxt<'genv, 'tcx>§xi: SnapshotMap<ParamId, ()>

Keeps track of all refinement parameters that are used as an index such that their value is fully determined. The name xi is taken from 1, where the well-formedness judgment uses an uppercase Xi (Ξ) for a context that is similar in purpose.

-

This is basically a set of [fhir::ParamId] implemented with a snapshot map such that elements +

This is basically a set of fhir::ParamId implemented with a snapshot map such that elements can be removed in batch when there’s a change in polarity.

§errors: Errors<'genv>

Implementations§

source§

impl<'a, 'genv, 'tcx> ParamUsesChecker<'a, 'genv, 'tcx>

source

fn new(infcx: &'a InferCtxt<'genv, 'tcx>) -> Self

source

fn run( self, f: impl FnOnce(&mut ParamUsesChecker<'_, '_, '_>) -) -> Result<(), ErrorGuaranteed>

source

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

-
source

fn 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<'_>)

§

fn visit_node(&mut self, node: &Node<'_>)

§

fn visit_item(&mut self, item: &Item<'_>)

§

fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)

§

fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)

§

fn visit_generics(&mut self, generics: &Generics<'_>)

§

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)

§

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)

§

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)

§

fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)

§

fn visit_field_def(&mut self, field: &FieldDef<'_>)

§

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)

§

fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)

§

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)

§

fn visit_fn_sig(&mut self, sig: &FnSig<'_>)

§

fn visit_refine_param(&mut self, param: &RefineParam<'_>)

§

fn visit_constraint(&mut self, constraint: &Constraint<'_>)

§

fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)

§

fn visit_lifetime(&mut self, _lft: &Lifetime)

§

fn visit_bty(&mut self, bty: &BaseTy<'_>)

§

fn visit_qpath(&mut self, qpath: &QPath<'_>)

§

fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)

§

fn visit_sort(&mut self, sort: &Sort<'_>)

§

fn visit_sort_path(&mut self, path: &SortPath<'_>)

§

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)

§

fn visit_func_sort(&mut self, func: &FuncSort<'_>)

§

fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)

§

fn visit_literal(&mut self, _lit: &Lit)

§

fn visit_path_expr(&mut self, _path: &PathExpr<'_>)

Auto Trait Implementations§

§

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> Any for Twhere +) -> Result<(), ErrorGuaranteed>

source

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

+
source

fn 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_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> !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> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/wf/sortck/fn.synth_lit.html b/doc/flux_fhir_analysis/wf/sortck/fn.synth_lit.html index 475e5a7c18..0bf57d7057 100644 --- a/doc/flux_fhir_analysis/wf/sortck/fn.synth_lit.html +++ b/doc/flux_fhir_analysis/wf/sortck/fn.synth_lit.html @@ -1 +1 @@ -synth_lit in flux_fhir_analysis::wf::sortck - Rust
fn synth_lit(lit: Lit) -> Sort
\ No newline at end of file +synth_lit in flux_fhir_analysis::wf::sortck - Rust
fn synth_lit(lit: Lit) -> Sort
\ No newline at end of file diff --git a/doc/flux_fhir_analysis/wf/sortck/struct.FullResolver.html b/doc/flux_fhir_analysis/wf/sortck/struct.FullResolver.html index 56e10ed590..3a29fb03ac 100644 --- a/doc/flux_fhir_analysis/wf/sortck/struct.FullResolver.html +++ b/doc/flux_fhir_analysis/wf/sortck/struct.FullResolver.html @@ -1,19 +1,19 @@ FullResolver in flux_fhir_analysis::wf::sortck - Rust
struct FullResolver<'a, 'genv, 'tcx> {
     infcx: &'a mut InferCtxt<'genv, 'tcx>,
-}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl FallibleTypeFolder for FullResolver<'_, '_, '_>

§

type Error = ()

source§

fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error>

§

fn try_fold_binder<T>( +}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl FallibleTypeFolder for FullResolver<'_, '_, '_>

§

type Error = ()

source§

fn try_fold_sort(&mut self, sort: &Sort) -> Result<Sort, Self::Error>

source§

fn try_fold_binder<T>( &mut self, - t: &Binder<T> -) -> Result<Binder<T>, Self::Error>where - T: TypeFoldable,

§

fn try_fold_ty( + t: &Binder<T> +) -> Result<Binder<T>, Self::Error>where + T: TypeFoldable,

source§

fn try_fold_ty( &mut self, - ty: &Interned<TyS> -) -> Result<Interned<TyS>, Self::Error>

§

fn try_fold_bty(&mut self, bty: &BaseTy) -> Result<BaseTy, Self::Error>

§

fn try_fold_subset_ty( + ty: &Interned<TyS> +) -> Result<Interned<TyS>, Self::Error>

source§

fn try_fold_bty(&mut self, bty: &BaseTy) -> Result<BaseTy, Self::Error>

source§

fn try_fold_subset_ty( &mut self, - constr: &SubsetTy -) -> Result<SubsetTy, Self::Error>

§

fn try_fold_region(&mut self, re: &Region) -> Result<Region, Self::Error>

§

fn try_fold_expr( + constr: &SubsetTy +) -> Result<SubsetTy, Self::Error>

source§

fn try_fold_region(&mut self, re: &Region) -> Result<Region, Self::Error>

source§

fn try_fold_expr( &mut self, - expr: &Interned<ExprS> -) -> Result<Interned<ExprS>, Self::Error>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for FullResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere + expr: &Interned<ExprS> +) -> Result<Interned<ExprS>, Self::Error>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for FullResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for FullResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html index fbf62196ca..499ae7ee10 100644 --- a/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html +++ b/doc/flux_fhir_analysis/wf/sortck/struct.ImplicitParamInferer.html @@ -3,8 +3,8 @@ errors: Errors<'genv>, }

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>§errors: Errors<'genv>

Implementations§

source§

impl<'a, 'genv, 'tcx> ImplicitParamInferer<'a, 'genv, 'tcx>

source

pub(crate) fn infer( infcx: &'a mut InferCtxt<'genv, 'tcx>, - node: &Node<'_> -) -> Result<(), ErrorGuaranteed>

source

fn infer_implicit_params(&mut self, idx: &RefineArg<'_>, expected: &Sort)

Trait Implementations§

source§

impl Visitor for ImplicitParamInferer<'_, '_, '_>

source§

fn visit_ty(&mut self, ty: &Ty<'_>)

§

fn visit_node(&mut self, node: &Node<'_>)

§

fn visit_item(&mut self, item: &Item<'_>)

§

fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)

§

fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)

§

fn visit_generics(&mut self, generics: &Generics<'_>)

§

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)

§

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)

§

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)

§

fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)

§

fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)

§

fn visit_variant(&mut self, variant: &VariantDef<'_>)

§

fn visit_field_def(&mut self, field: &FieldDef<'_>)

§

fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)

§

fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)

§

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)

§

fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)

§

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)

§

fn visit_fn_sig(&mut self, sig: &FnSig<'_>)

§

fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)

§

fn visit_refine_param(&mut self, param: &RefineParam<'_>)

§

fn visit_constraint(&mut self, constraint: &Constraint<'_>)

§

fn visit_fn_output(&mut self, output: &FnOutput<'_>)

§

fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)

§

fn visit_lifetime(&mut self, _lft: &Lifetime)

§

fn visit_bty(&mut self, bty: &BaseTy<'_>)

§

fn visit_qpath(&mut self, qpath: &QPath<'_>)

§

fn visit_path(&mut self, path: &Path<'_>)

§

fn visit_path_segment(&mut self, segment: &PathSegment<'_>)

§

fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)

§

fn visit_sort(&mut self, sort: &Sort<'_>)

§

fn visit_sort_path(&mut self, path: &SortPath<'_>)

§

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)

§

fn visit_func_sort(&mut self, func: &FuncSort<'_>)

§

fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)

§

fn visit_expr(&mut self, expr: &Expr<'_>)

§

fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)

§

fn visit_literal(&mut self, _lit: &Lit)

§

fn visit_path_expr(&mut self, _path: &PathExpr<'_>)

Auto Trait Implementations§

§

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 + node: &Node<'_> +) -> Result<(), ErrorGuaranteed>

source

fn 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_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> !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 T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html index 07b883652d..8acb2f9e35 100644 --- a/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html +++ b/doc/flux_fhir_analysis/wf/sortck/struct.InferCtxt.html @@ -1,82 +1,82 @@ InferCtxt in flux_fhir_analysis::wf::sortck - Rust
pub(super) struct InferCtxt<'genv, 'tcx> {
-    pub genv: GlobalEnv<'genv, 'tcx>,
-    params: UnordMap<ParamId, (Sort, ParamKind)>,
-    pub(super) sort_unification_table: InPlaceUnificationTable<SortVid>,
-    num_unification_table: InPlaceUnificationTable<NumVid>,
-    pub wfckresults: WfckResults<'genv>,
-}

Fields§

§genv: GlobalEnv<'genv, 'tcx>§params: UnordMap<ParamId, (Sort, ParamKind)>§sort_unification_table: InPlaceUnificationTable<SortVid>§num_unification_table: InPlaceUnificationTable<NumVid>§wfckresults: WfckResults<'genv>

Implementations§

source§

impl<'genv, 'tcx> InferCtxt<'genv, 'tcx>

source

pub(super) fn new(genv: GlobalEnv<'genv, 'tcx>, owner: FluxOwnerId) -> Self

source

pub(super) fn check_refine_arg( - &mut self, - arg: &RefineArg<'_>, - expected: &Sort + pub genv: GlobalEnv<'genv, 'tcx>, + params: UnordMap<ParamId, (Sort, ParamKind)>, + pub(super) sort_unification_table: InPlaceUnificationTable<SortVid>, + num_unification_table: InPlaceUnificationTable<NumVid>, + pub wfckresults: WfckResults<'genv>, +}

Fields§

§genv: GlobalEnv<'genv, 'tcx>§params: UnordMap<ParamId, (Sort, ParamKind)>§sort_unification_table: InPlaceUnificationTable<SortVid>§num_unification_table: InPlaceUnificationTable<NumVid>§wfckresults: WfckResults<'genv>

Implementations§

source§

impl<'genv, 'tcx> InferCtxt<'genv, 'tcx>

source

pub(super) fn new(genv: GlobalEnv<'genv, 'tcx>, owner: FluxOwnerId) -> Self

source

pub(super) fn check_refine_arg( + &mut self, + arg: &RefineArg<'_>, + expected: &Sort ) -> Result<(), ErrorGuaranteed>

source

fn check_abs( &mut self, - arg: &RefineArg<'_>, - params: &[RefineParam<'_>], - body: &Expr<'_>, - expected: &Sort + arg: &RefineArg<'_>, + params: &[RefineParam<'_>], + body: &Expr<'_>, + expected: &Sort ) -> Result<(), ErrorGuaranteed>

source

fn check_record( &mut self, - arg: &RefineArg<'_>, - flds: &[RefineArg<'_>], - expected: &Sort + arg: &RefineArg<'_>, + flds: &[RefineArg<'_>], + expected: &Sort ) -> Result<(), ErrorGuaranteed>

source

pub(super) fn check_expr( &mut self, - expr: &Expr<'_>, - expected: &Sort + expr: &Expr<'_>, + expected: &Sort ) -> Result<(), ErrorGuaranteed>

source

pub(super) fn check_loc( &mut self, - loc: &PathExpr<'_> -) -> Result<(), ErrorGuaranteed>

source

fn synth_expr(&mut self, expr: &Expr<'_>) -> Result<Sort, ErrorGuaranteed>

source

fn synth_var(&mut self, path: &PathExpr<'_>) -> Sort

source

fn synth_binary_op( + loc: &PathExpr<'_> +) -> Result<(), ErrorGuaranteed>

source

fn synth_expr(&mut self, expr: &Expr<'_>) -> Result<Sort, ErrorGuaranteed>

source

fn synth_var(&mut self, path: &PathExpr<'_>) -> Sort

source

fn synth_binary_op( &mut self, - expr: &Expr<'_>, + expr: &Expr<'_>, op: BinOp, - e1: &Expr<'_>, - e2: &Expr<'_> -) -> Result<Sort, ErrorGuaranteed>

source

fn synth_unary_op( + e1: &Expr<'_>, + e2: &Expr<'_> +) -> Result<Sort, ErrorGuaranteed>

source

fn synth_unary_op( &mut self, op: UnOp, - e: &Expr<'_> -) -> Result<Sort, ErrorGuaranteed>

source

fn synth_app( + e: &Expr<'_> +) -> Result<Sort, ErrorGuaranteed>

source

fn synth_app( &mut self, - func: &PathExpr<'_>, - args: &[Expr<'_>], + func: &PathExpr<'_>, + args: &[Expr<'_>], span: Span -) -> Result<Sort, ErrorGuaranteed>

source

fn synth_alias_reft_app( +) -> Result<Sort, ErrorGuaranteed>

source

fn synth_alias_reft_app( &mut self, - alias: &AliasReft<'_>, - args: &[Expr<'_>], + alias: &AliasReft<'_>, + args: &[Expr<'_>], span: Span -) -> Result<Sort, ErrorGuaranteed>

source

fn synth_func( +) -> Result<Sort, ErrorGuaranteed>

source

fn synth_func( &mut self, - func: &PathExpr<'_> -) -> Result<FuncSort, ErrorGuaranteed>

source

fn instantiate_func_sort(&mut self, fsort: PolyFuncSort) -> FuncSort

source§

impl<'genv> InferCtxt<'genv, '_>

source

pub(super) fn insert_params(&mut self, params: &[RefineParam<'_>])

Push a layer of binders. We assume all names are fresh so we don’t care about shadowing

-
source

pub(super) fn insert_param(&mut self, id: ParamId, sort: Sort, kind: ParamKind)

source

fn is_coercible(&mut self, sort1: &Sort, sort2: &Sort, fhir_id: FhirId) -> bool

Whether a value of sort1 can be automatically coerced to a value of sort2. A value of an -[rty::SortCtor::Adt] sort with a single field of sort s can be coerced to a value of sort + func: &PathExpr<'_> +) -> Result<FuncSort, ErrorGuaranteed>

source

fn instantiate_func_sort(&mut self, fsort: PolyFuncSort) -> FuncSort

source§

impl<'genv> InferCtxt<'genv, '_>

source

pub(super) fn insert_params(&mut self, params: &[RefineParam<'_>])

Push a layer of binders. We assume all names are fresh so we don’t care about shadowing

+
source

pub(super) fn insert_param(&mut self, id: ParamId, sort: Sort, kind: ParamKind)

source

fn is_coercible(&mut self, sort1: &Sort, sort2: &Sort, fhir_id: FhirId) -> bool

Whether a value of sort1 can be automatically coerced to a value of sort2. A value of an +rty::SortCtor::Adt sort with a single field of sort s can be coerced to a value of sort s and vice versa, i.e., we can automatically project the field out of the record or inject a value into a record.

source

fn is_coercible_from_func( &mut self, - sort: &Sort, - fhir_id: FhirId -) -> Option<PolyFuncSort>

source

fn is_coercible_to_func( + sort: &Sort, + fhir_id: FhirId +) -> Option<PolyFuncSort>

source

fn is_coercible_to_func( &mut self, - sort: &Sort, - fhir_id: FhirId -) -> Option<PolyFuncSort>

source

fn try_equate(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

source

fn try_equate_inner(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

source

fn equate(&mut self, sort1: &Sort, sort2: &Sort) -> Sort

source

pub(crate) fn next_sort_var(&mut self) -> Sort

source

fn next_num_var(&mut self) -> Sort

source

fn next_sort_vid(&mut self) -> SortVid

source

fn next_num_vid(&mut self) -> NumVid

source

pub(crate) fn resolve_param_sort( + sort: &Sort, + fhir_id: FhirId +) -> Option<PolyFuncSort>

source

fn try_equate(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

source

fn try_equate_inner(&mut self, sort1: &Sort, sort2: &Sort) -> Option<Sort>

source

fn equate(&mut self, sort1: &Sort, sort2: &Sort) -> Sort

source

pub(crate) fn next_sort_var(&mut self) -> Sort

source

fn next_num_var(&mut self) -> Sort

source

fn next_sort_vid(&mut self) -> SortVid

source

fn next_num_vid(&mut self) -> NumVid

source

pub(crate) fn resolve_param_sort( &mut self, - param: &RefineParam<'_> + param: &RefineParam<'_> ) -> Result<(), ErrorGuaranteed>

source

fn ensure_resolved_var( &mut self, - path: &PathExpr<'_> -) -> Result<Sort, ErrorGuaranteed>

source

fn is_single_field_record(&mut self, sort: &Sort) -> Option<(DefId, Sort)>

source

pub(crate) fn into_results(self) -> WfckResults<'genv>

source

pub(crate) fn infer_mode(&self, id: ParamId) -> InferMode

source

pub(crate) fn param_sort(&self, id: ParamId) -> Sort

source

fn shallow_resolve(&mut self, sort: &Sort) -> Sort

source

fn resolve_vars_if_possible(&mut self, sort: &Sort) -> Sort

source

pub(crate) fn fully_resolve(&mut self, sort: &Sort) -> Result<Sort, ()>

source§

impl InferCtxt<'_, '_>

source

fn emit_sort_mismatch( + path: &PathExpr<'_> +) -> Result<Sort, ErrorGuaranteed>

source

fn is_single_field_record(&mut self, sort: &Sort) -> Option<(DefId, Sort)>

source

pub(crate) fn into_results(self) -> WfckResults<'genv>

source

pub(crate) fn infer_mode(&self, id: ParamId) -> InferMode

source

pub(crate) fn param_sort(&self, id: ParamId) -> Sort

source

fn shallow_resolve(&mut self, sort: &Sort) -> Sort

source

fn resolve_vars_if_possible(&mut self, sort: &Sort) -> Sort

source

pub(crate) fn fully_resolve(&mut self, sort: &Sort) -> Result<Sort, ()>

source§

impl InferCtxt<'_, '_>

source

fn emit_sort_mismatch( &mut self, span: Span, - expected: &Sort, - found: &Sort + expected: &Sort, + found: &Sort ) -> ErrorGuaranteed

source

fn emit_field_not_found( &mut self, - sort: &Sort, - field: SurfaceIdent + sort: &Sort, + field: SurfaceIdent ) -> ErrorGuaranteed

source

fn emit_err<'b>(&'b self, err: impl IntoDiagnostic<'b>) -> ErrorGuaranteed

Auto Trait Implementations§

§

impl<'genv, 'tcx> !RefUnwindSafe for InferCtxt<'genv, 'tcx>

§

impl<'genv, 'tcx> !Send for InferCtxt<'genv, 'tcx>

§

impl<'genv, 'tcx> !Sync for InferCtxt<'genv, 'tcx>

§

impl<'genv, 'tcx> Unpin for InferCtxt<'genv, 'tcx>

§

impl<'genv, 'tcx> !UnwindSafe for InferCtxt<'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere diff --git a/doc/flux_fhir_analysis/wf/sortck/struct.OpportunisticResolver.html b/doc/flux_fhir_analysis/wf/sortck/struct.OpportunisticResolver.html index 12d0550202..b5c60506fe 100644 --- a/doc/flux_fhir_analysis/wf/sortck/struct.OpportunisticResolver.html +++ b/doc/flux_fhir_analysis/wf/sortck/struct.OpportunisticResolver.html @@ -1,33 +1,33 @@ OpportunisticResolver in flux_fhir_analysis::wf::sortck - Rust
struct OpportunisticResolver<'a, 'genv, 'tcx> {
     infcx: &'a mut InferCtxt<'genv, 'tcx>,
-}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl TypeFolder for OpportunisticResolver<'_, '_, '_>

source§

fn fold_sort(&mut self, sort: &Sort) -> Sort

§

fn fold_binder<T>(&mut self, t: &Binder<T>) -> Binder<T>where - T: TypeFoldable,

§

fn fold_ty(&mut self, ty: &Interned<TyS>) -> Interned<TyS>

§

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

§

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

§

fn fold_region(&mut self, re: &Region) -> Region

§

fn fold_expr(&mut self, expr: &Interned<ExprS>) -> Interned<ExprS>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for OpportunisticResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere +}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl TypeFolder for OpportunisticResolver<'_, '_, '_>

source§

fn fold_sort(&mut self, sort: &Sort) -> Sort

source§

fn fold_binder<T>(&mut self, t: &Binder<T>) -> Binder<T>where + T: TypeFoldable,

source§

fn fold_ty(&mut self, ty: &Interned<TyS>) -> Interned<TyS>

source§

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

source§

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

source§

fn fold_region(&mut self, re: &Region) -> Region

source§

fn fold_expr(&mut self, expr: &Interned<ExprS>) -> Interned<ExprS>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for OpportunisticResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for OpportunisticResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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<F> FallibleTypeFolder for Fwhere - F: TypeFolder,

§

type Error = !

§

fn try_fold_binder<T>( + T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<F> FallibleTypeFolder for Fwhere + F: TypeFolder,

§

type Error = !

source§

fn try_fold_binder<T>( &mut self, - t: &Binder<T> -) -> Result<Binder<T>, <F as FallibleTypeFolder>::Error>where - T: TypeFoldable,

§

fn try_fold_sort( + t: &Binder<T> +) -> Result<Binder<T>, <F as FallibleTypeFolder>::Error>where + T: TypeFoldable,

source§

fn try_fold_sort( &mut self, - sort: &Sort -) -> Result<Sort, <F as FallibleTypeFolder>::Error>

§

fn try_fold_ty( + sort: &Sort +) -> Result<Sort, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_ty( &mut self, - ty: &Interned<TyS> -) -> Result<Interned<TyS>, <F as FallibleTypeFolder>::Error>

§

fn try_fold_bty( + ty: &Interned<TyS> +) -> Result<Interned<TyS>, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_bty( &mut self, - bty: &BaseTy -) -> Result<BaseTy, <F as FallibleTypeFolder>::Error>

§

fn try_fold_subset_ty( + bty: &BaseTy +) -> Result<BaseTy, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_subset_ty( &mut self, - ty: &SubsetTy -) -> Result<SubsetTy, <F as FallibleTypeFolder>::Error>

§

fn try_fold_region( + ty: &SubsetTy +) -> Result<SubsetTy, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_region( &mut self, - re: &Region -) -> Result<Region, <F as FallibleTypeFolder>::Error>

§

fn try_fold_expr( + re: &Region +) -> Result<Region, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_expr( &mut self, - expr: &Interned<ExprS> -) -> Result<Interned<ExprS>, <F as FallibleTypeFolder>::Error>

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

+ expr: &Interned<ExprS> +) -> Result<Interned<ExprS>, <F as FallibleTypeFolder>::Error>

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of diff --git a/doc/flux_fhir_analysis/wf/sortck/struct.ShallowResolver.html b/doc/flux_fhir_analysis/wf/sortck/struct.ShallowResolver.html index acde288a3c..9f39eb5de8 100644 --- a/doc/flux_fhir_analysis/wf/sortck/struct.ShallowResolver.html +++ b/doc/flux_fhir_analysis/wf/sortck/struct.ShallowResolver.html @@ -1,33 +1,33 @@ ShallowResolver in flux_fhir_analysis::wf::sortck - Rust

struct ShallowResolver<'a, 'genv, 'tcx> {
     infcx: &'a mut InferCtxt<'genv, 'tcx>,
-}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl TypeFolder for ShallowResolver<'_, '_, '_>

source§

fn fold_sort(&mut self, sort: &Sort) -> Sort

§

fn fold_binder<T>(&mut self, t: &Binder<T>) -> Binder<T>where - T: TypeFoldable,

§

fn fold_ty(&mut self, ty: &Interned<TyS>) -> Interned<TyS>

§

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

§

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

§

fn fold_region(&mut self, re: &Region) -> Region

§

fn fold_expr(&mut self, expr: &Interned<ExprS>) -> Interned<ExprS>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for ShallowResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere +}

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>

Trait Implementations§

source§

impl TypeFolder for ShallowResolver<'_, '_, '_>

source§

fn fold_sort(&mut self, sort: &Sort) -> Sort

source§

fn fold_binder<T>(&mut self, t: &Binder<T>) -> Binder<T>where + T: TypeFoldable,

source§

fn fold_ty(&mut self, ty: &Interned<TyS>) -> Interned<TyS>

source§

fn fold_bty(&mut self, bty: &BaseTy) -> BaseTy

source§

fn fold_subset_ty(&mut self, constr: &SubsetTy) -> SubsetTy

source§

fn fold_region(&mut self, re: &Region) -> Region

source§

fn fold_expr(&mut self, expr: &Interned<ExprS>) -> Interned<ExprS>

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for ShallowResolver<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for ShallowResolver<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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<F> FallibleTypeFolder for Fwhere - F: TypeFolder,

§

type Error = !

§

fn try_fold_binder<T>( + T: ?Sized,

source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<F> FallibleTypeFolder for Fwhere + F: TypeFolder,

§

type Error = !

source§

fn try_fold_binder<T>( &mut self, - t: &Binder<T> -) -> Result<Binder<T>, <F as FallibleTypeFolder>::Error>where - T: TypeFoldable,

§

fn try_fold_sort( + t: &Binder<T> +) -> Result<Binder<T>, <F as FallibleTypeFolder>::Error>where + T: TypeFoldable,

source§

fn try_fold_sort( &mut self, - sort: &Sort -) -> Result<Sort, <F as FallibleTypeFolder>::Error>

§

fn try_fold_ty( + sort: &Sort +) -> Result<Sort, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_ty( &mut self, - ty: &Interned<TyS> -) -> Result<Interned<TyS>, <F as FallibleTypeFolder>::Error>

§

fn try_fold_bty( + ty: &Interned<TyS> +) -> Result<Interned<TyS>, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_bty( &mut self, - bty: &BaseTy -) -> Result<BaseTy, <F as FallibleTypeFolder>::Error>

§

fn try_fold_subset_ty( + bty: &BaseTy +) -> Result<BaseTy, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_subset_ty( &mut self, - ty: &SubsetTy -) -> Result<SubsetTy, <F as FallibleTypeFolder>::Error>

§

fn try_fold_region( + ty: &SubsetTy +) -> Result<SubsetTy, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_region( &mut self, - re: &Region -) -> Result<Region, <F as FallibleTypeFolder>::Error>

§

fn try_fold_expr( + re: &Region +) -> Result<Region, <F as FallibleTypeFolder>::Error>

source§

fn try_fold_expr( &mut self, - expr: &Interned<ExprS> -) -> Result<Interned<ExprS>, <F as FallibleTypeFolder>::Error>

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

+ expr: &Interned<ExprS> +) -> Result<Interned<ExprS>, <F as FallibleTypeFolder>::Error>

source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of diff --git a/doc/flux_fhir_analysis/wf/struct.Wf.html b/doc/flux_fhir_analysis/wf/struct.Wf.html index 8dfc9d0760..5be8b21cb7 100644 --- a/doc/flux_fhir_analysis/wf/struct.Wf.html +++ b/doc/flux_fhir_analysis/wf/struct.Wf.html @@ -3,8 +3,8 @@ errors: Errors<'genv>, }

Fields§

§infcx: &'a mut InferCtxt<'genv, 'tcx>§errors: Errors<'genv>

Implementations§

source§

impl<'a, 'genv, 'tcx> Wf<'a, 'genv, 'tcx>

source

fn check( infcx: &'a mut InferCtxt<'genv, 'tcx>, - node: &Node<'_> -) -> Result<(), ErrorGuaranteed>

source

fn check_output_locs(&mut self, fn_decl: &FnDecl<'_>)

Trait Implementations§

source§

impl Visitor for Wf<'_, '_, '_>

source§

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)

source§

fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)

source§

fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)

source§

fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)

source§

fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)

source§

fn visit_constraint(&mut self, constraint: &Constraint<'_>)

source§

fn visit_ty(&mut self, ty: &Ty<'_>)

source§

fn visit_path(&mut self, path: &Path<'_>)

§

fn visit_node(&mut self, node: &Node<'_>)

§

fn visit_item(&mut self, item: &Item<'_>)

§

fn visit_trait_item(&mut self, trait_item: &TraitItem<'_>)

§

fn visit_impl_item(&mut self, impl_item: &ImplItem<'_>)

§

fn visit_generics(&mut self, generics: &Generics<'_>)

§

fn visit_where_predicate(&mut self, predicate: &WhereBoundPredicate<'_>)

§

fn visit_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)

§

fn visit_variant(&mut self, variant: &VariantDef<'_>)

§

fn visit_field_def(&mut self, field: &FieldDef<'_>)

§

fn visit_ty_alias(&mut self, ty_alias: &TyAlias<'_>)

§

fn visit_opaque_ty(&mut self, opaque_ty: &OpaqueTy<'_>)

§

fn visit_generic_bound(&mut self, bound: &GenericBound<'_>)

§

fn visit_poly_trait_ref(&mut self, trait_ref: &PolyTraitRef<'_>)

§

fn visit_fn_sig(&mut self, sig: &FnSig<'_>)

§

fn visit_refine_param(&mut self, param: &RefineParam<'_>)

§

fn visit_fn_output(&mut self, output: &FnOutput<'_>)

§

fn visit_generic_arg(&mut self, arg: &GenericArg<'_>)

§

fn visit_lifetime(&mut self, _lft: &Lifetime)

§

fn visit_bty(&mut self, bty: &BaseTy<'_>)

§

fn visit_qpath(&mut self, qpath: &QPath<'_>)

§

fn visit_path_segment(&mut self, segment: &PathSegment<'_>)

§

fn visit_type_binding(&mut self, binding: &TypeBinding<'_>)

§

fn visit_sort(&mut self, sort: &Sort<'_>)

§

fn visit_sort_path(&mut self, path: &SortPath<'_>)

§

fn visit_poly_func_sort(&mut self, func: &PolyFuncSort<'_>)

§

fn visit_func_sort(&mut self, func: &FuncSort<'_>)

§

fn visit_refine_arg(&mut self, arg: &RefineArg<'_>)

§

fn visit_expr(&mut self, expr: &Expr<'_>)

§

fn visit_alias_pred(&mut self, alias_pred: &AliasReft<'_>)

§

fn visit_literal(&mut self, _lit: &Lit)

§

fn visit_path_expr(&mut self, _path: &PathExpr<'_>)

Auto Trait Implementations§

§

impl<'a, 'genv, 'tcx> !RefUnwindSafe for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for Wf<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere + node: &Node<'_> +) -> Result<(), ErrorGuaranteed>

source

fn check_output_locs(&mut self, fn_decl: &FnDecl<'_>)

Trait Implementations§

source§

impl Visitor for Wf<'_, '_, '_>

source§

fn visit_impl_assoc_reft(&mut self, assoc_reft: &ImplAssocReft<'_>)

source§

fn visit_struct_def(&mut self, struct_def: &StructDef<'_>)

source§

fn visit_enum_def(&mut self, enum_def: &EnumDef<'_>)

source§

fn visit_variant_ret(&mut self, ret: &VariantRet<'_>)

source§

fn visit_fn_decl(&mut self, decl: &FnDecl<'_>)

source§

fn visit_constraint(&mut self, constraint: &Constraint<'_>)

source§

fn visit_ty(&mut self, ty: &Ty<'_>)

source§

fn visit_path(&mut self, path: &Path<'_>)

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_trait_assoc_reft(&mut self, assoc_reft: &TraitAssocReft<'_>)

source§

fn visit_variant(&mut self, variant: &VariantDef<'_>)

source§

fn visit_field_def(&mut self, field: &FieldDef<'_>)

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_refine_param(&mut self, param: &RefineParam<'_>)

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_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> !RefUnwindSafe for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Send for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !Sync for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> Unpin for Wf<'a, 'genv, 'tcx>

§

impl<'a, 'genv, 'tcx> !UnwindSafe for Wf<'a, 'genv, 'tcx>

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
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
source§

impl<T> From<T> for T

source§

fn from(t: T) -> T

Returns the argument unchanged.

diff --git a/doc/src/flux_fhir_analysis/conv.rs.html b/doc/src/flux_fhir_analysis/conv.rs.html index 0b5504a322..793fff14f5 100644 --- a/doc/src/flux_fhir_analysis/conv.rs.html +++ b/doc/src/flux_fhir_analysis/conv.rs.html @@ -1495,6 +1495,14 @@ 1495 1496 1497 +1498 +1499 +1500 +1501 +1502 +1503 +1504 +1505
//! 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,
@@ -2229,11 +2237,19 @@
                 match path.res {
                     fhir::Res::Def(DefKind::AssocTy, assoc_id) => {
                         let trait_id = self.genv.tcx().trait_of_item(assoc_id).unwrap();
-                        let self_ty = self.conv_ty(env, self_ty.as_deref().unwrap())?;
                         let [.., trait_segment, assoc_segment] = path.segments else {
                             span_bug!(bty.span, "expected at least two segments");
                         };
-                        let mut args = vec![rty::GenericArg::Ty(self_ty)];
+
+                        let trait_generics = self.genv.generics_of(trait_id)?;
+                        let self_ty = self_ty.as_deref().unwrap();
+                        let self_ty =
+                            if let rty::GenericParamDefKind::Base = trait_generics.params[0].kind {
+                                rty::GenericArg::Base(self.conv_generic_base(env, self_ty)?)
+                            } else {
+                                rty::GenericArg::Ty(self.conv_ty(env, self_ty)?)
+                            };
+                        let mut args = vec![self_ty];
                         self.conv_generic_args_into(env, trait_id, trait_segment.args, &mut args)?;
                         self.conv_generic_args_into(env, assoc_id, assoc_segment.args, &mut args)?;
                         let args = List::from_vec(args);
diff --git a/doc/trait.impl/flux_middle/fhir/visit/trait.Visitor.js b/doc/trait.impl/flux_middle/fhir/visit/trait.Visitor.js
index a1bcb1df36..a8a9eb4af8 100644
--- a/doc/trait.impl/flux_middle/fhir/visit/trait.Visitor.js
+++ b/doc/trait.impl/flux_middle/fhir/visit/trait.Visitor.js
@@ -1,3 +1,3 @@
 (function() {var implementors = {
-"flux_fhir_analysis":[["impl Visitor for Wf<'_, '_, '_>"],["impl Visitor for ParamUsesChecker<'_, '_, '_>"],["impl Visitor for ImplicitParamInferer<'_, '_, '_>"]]
+"flux_fhir_analysis":[["impl Visitor for Wf<'_, '_, '_>"],["impl Visitor for ParamUsesChecker<'_, '_, '_>"],["impl Visitor for ImplicitParamInferer<'_, '_, '_>"]]
 };if (window.register_implementors) {window.register_implementors(implementors);} else {window.pending_implementors = implementors;}})()
\ No newline at end of file
diff --git a/doc/trait.impl/flux_middle/rty/fold/trait.FallibleTypeFolder.js b/doc/trait.impl/flux_middle/rty/fold/trait.FallibleTypeFolder.js
index adaa0cb7dd..cf1b11e909 100644
--- a/doc/trait.impl/flux_middle/rty/fold/trait.FallibleTypeFolder.js
+++ b/doc/trait.impl/flux_middle/rty/fold/trait.FallibleTypeFolder.js
@@ -1,5 +1,5 @@
 (function() {var implementors = {
-"flux_fhir_analysis":[["impl FallibleTypeFolder for FullResolver<'_, '_, '_>"]],
+"flux_fhir_analysis":[["impl FallibleTypeFolder for FullResolver<'_, '_, '_>"]],
 "flux_middle":[],
 "flux_refineck":[["impl FallibleTypeFolder for Unfolder<'_, '_, '_, '_>"]]
 };if (window.register_implementors) {window.register_implementors(implementors);} else {window.pending_implementors = implementors;}})()
\ No newline at end of file
diff --git a/doc/trait.impl/flux_middle/rty/fold/trait.TypeFolder.js b/doc/trait.impl/flux_middle/rty/fold/trait.TypeFolder.js
index 86084d7433..2499db5c98 100644
--- a/doc/trait.impl/flux_middle/rty/fold/trait.TypeFolder.js
+++ b/doc/trait.impl/flux_middle/rty/fold/trait.TypeFolder.js
@@ -1,5 +1,5 @@
 (function() {var implementors = {
-"flux_fhir_analysis":[["impl TypeFolder for OpportunisticResolver<'_, '_, '_>"],["impl TypeFolder for ShallowResolver<'_, '_, '_>"]],
+"flux_fhir_analysis":[["impl TypeFolder for OpportunisticResolver<'_, '_, '_>"],["impl TypeFolder for ShallowResolver<'_, '_, '_>"]],
 "flux_middle":[],
 "flux_refineck":[["impl TypeFolder for Unpacker<'_, '_>"],["impl TypeFolder for Updater<'_>"]]
 };if (window.register_implementors) {window.register_implementors(implementors);} else {window.pending_implementors = implementors;}})()
\ No newline at end of file