struct CrateChecker<'genv, 'tcx> {
genv: GlobalEnv<'genv, 'tcx>,
- cache: FixQueryCache,
+ cache: FixQueryCache,
checker_config: CheckerConfig,
-}Fields§
§genv: GlobalEnv<'genv, 'tcx>§cache: FixQueryCache§checker_config: CheckerConfigImplementations§
Source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
fn matches_check_def(&self, def_id: DefId) -> bool
fn matches_check_file(&self, def_id: LocalDefId) -> bool
fn check_def_catching_bugs(
+}Fields§
§genv: GlobalEnv<'genv, 'tcx>§cache: FixQueryCache§checker_config: CheckerConfigImplementations§
Source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
Sourcefn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
Sourcefn matches_check_def(&self, def_id: DefId) -> bool
Sourcefn matches_check_file(&self, def_id: LocalDefId) -> bool
Sourcefn check_def_catching_bugs(
&mut self,
def_id: LocalDefId,
) -> Result<(), ErrorGuaranteed>
Sourcefn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
Auto Trait Implementations§
§impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
§impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Blanket Implementations§
Source§impl<T> Any for Twhere
diff --git a/doc/flux_infer/infer/index.html b/doc/flux_infer/infer/index.html
index 92282888f0..7a9875f1d1 100644
--- a/doc/flux_infer/infer/index.html
+++ b/doc/flux_infer/infer/index.html
@@ -1,3 +1,3 @@
-flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
+flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
to recover the derivation when relating types via subtyping. The code that attaches the trace is
currently commented out because the output is too verbose.
Traits§
Functions§
Type Aliases§
Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Hash for Tag
1.3.0 · Source§fn hash_slice<H>(data: &[Self], state: &mut H)where
+}Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/index.html b/doc/flux_infer/refine_tree/index.html
index ea8f0141bf..c2467e505c 100644
--- a/doc/flux_infer/refine_tree/index.html
+++ b/doc/flux_infer/refine_tree/index.html
@@ -1,4 +1,4 @@
-flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
+
flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
available in a particular path during type-checking. For example, consider the following
program:
- A very explicit representation of
RefineCtxt for debugging/tracing/serialization ONLY. - A refinement tree tracks the “tree-like structure” of refinement variables and predicates
generated during refinement type-checking. This tree can be encoded as a fixpoint constraint
diff --git a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
index 0b60baae1e..371a0e2209 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
@@ -1,4 +1,4 @@
-
fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
+fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
children: &[NodePtr],
cx: &PrettyCx<'_, '_>,
f: &mut Formatter<'_>,
diff --git a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
index b65a5287f1..90cd418f59 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
@@ -1 +1 @@
-with_padding in flux_infer::refine_tree::pretty - Rust with_padding in flux_infer::refine_tree::pretty - Rust NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> Any for Twhere
+NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RcxBind.html b/doc/flux_infer/refine_tree/struct.RcxBind.html
index 66b8e246d3..842fcd1231 100644
--- a/doc/flux_infer/refine_tree/struct.RcxBind.html
+++ b/doc/flux_infer/refine_tree/struct.RcxBind.html
@@ -1,7 +1,7 @@
-RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
+RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
name: String,
sort: String,
-}
Fields§
§name: String§sort: StringTrait Implementations§
Source§impl Serialize for RcxBind
Source§fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where
+}Fields§
§name: String§sort: StringTrait Implementations§
Auto Trait Implementations§
§impl Freeze for RcxBind
§impl RefUnwindSafe for RcxBind
§impl Send for RcxBind
§impl Sync for RcxBind
§impl Unpin for RcxBind
§impl UnwindSafe for RcxBind
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxt.html b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
index 211e5c34a5..ef21899753 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxt.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
@@ -32,7 +32,7 @@
)Sourcepub fn unpack(&mut self, ty: &Ty) -> Ty
Sourcepub fn hoister(
&mut self,
assume_invariants: AssumeInvariants,
-) -> Hoister<Unpacker<'_, 'rcx>>
Sourcepub fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool)
Sourcepub fn replace_evars(&mut self, evars: &EVarSol)
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
index 58b24ea640..e17f80314c 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
@@ -1,8 +1,8 @@
-RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
+RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
bindings: Vec<RcxBind>,
exprs: Vec<String>,
}
Expand description
A very explicit representation of RefineCtxt for debugging/tracing/serialization ONLY.
-Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Source§impl Serialize for RefineCtxtTrace
Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Auto Trait Implementations§
§impl Freeze for RefineCtxtTrace
§impl RefUnwindSafe for RefineCtxtTrace
§impl Send for RefineCtxtTrace
§impl Sync for RefineCtxtTrace
§impl Unpin for RefineCtxtTrace
§impl UnwindSafe for RefineCtxtTrace
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineTree.html b/doc/flux_infer/refine_tree/struct.RefineTree.html
index 80683cd28f..8441c89569 100644
--- a/doc/flux_infer/refine_tree/struct.RefineTree.html
+++ b/doc/flux_infer/refine_tree/struct.RefineTree.html
@@ -19,7 +19,7 @@
) -> QueryResult<RefineTree>Sourcepub fn simplify(&mut self, defns: &SpecFuncDefns)
Sourcepub fn into_fixpoint(
self,
cx: &mut FixpointCtxt<'_, '_, Tag>,
-) -> QueryResult<Constraint>
Sourcepub fn refine_ctxt_at_root(&mut self) -> RefineCtxt<'_>
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.Scope.html b/doc/flux_infer/refine_tree/struct.Scope.html
index fe229512ce..99d93c021f 100644
--- a/doc/flux_infer/refine_tree/struct.Scope.html
+++ b/doc/flux_infer/refine_tree/struct.Scope.html
@@ -3,8 +3,8 @@
params: Vec<(Var, Sort)>,
}Expand description
A list of refinement variables and their sorts.
Fields§
§bindings: IndexVec<Name, Sort>§params: Vec<(Var, Sort)>Implementations§
Source§impl Scope
Sourcepub fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_
Sourcepub fn has_free_vars<T: TypeFoldable>(&self, t: &T) -> bool
Whether t has any free variables not in this scope
-Sourcefn contains_all(&self, iter: impl IntoIterator<Item = Name>) -> bool
Sourcefn contains(&self, name: Name) -> bool
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§impl<Q, K> Equivalent<K> for Qwhere
diff --git a/doc/flux_middle/all.html b/doc/flux_middle/all.html
index b30630d868..1c73baac8a 100644
--- a/doc/flux_middle/all.html
+++ b/doc/flux_middle/all.html
@@ -1 +1 @@
-List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _define_scoped
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::define_scoped
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
flux_middle - Rust Expand description
This crate contains common type definitions that are used by other crates.
Modules§
- Flux High-Level Intermediate Representation
- Defines how flux represents refinement types internally. Definitions in this module are used
during refinement type checking. A couple of important differences between definitions in this
-module and in
crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
+module and in crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
for an extern spec. - This enum serves as a type-level reminder that a local definition may be a wrapper for an
extern spec. This abstraction is not infallible, so one should be careful and decide in each
situation whether to use the local id or the resolved id.
- Normally, a
DefId is either local or external, and DefId::as_local can be used to
diff --git a/doc/flux_middle/macro._define_scoped!.html b/doc/flux_middle/macro._define_scoped!.html
deleted file mode 100644
index c63ebc6ad3..0000000000
--- a/doc/flux_middle/macro._define_scoped!.html
+++ /dev/null
@@ -1,11 +0,0 @@
-
-
-
-
- Redirection
-
-
- Redirecting to macro._define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/macro._define_scoped.html b/doc/flux_middle/macro._define_scoped.html
deleted file mode 100644
index ee55233dc3..0000000000
--- a/doc/flux_middle/macro._define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-_define_scoped in flux_middle - Rust macro_rules! _define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
_format_cx in flux_middle - Rust macro_rules! _format_cx {
+_format_cx in flux_middle - Rust macro_rules! _format_cx {
($($arg:tt)*) => { ... };
}
_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
+_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
_join in flux_middle - Rust macro_rules! _join {
+_join in flux_middle - Rust macro_rules! _join {
($sep:expr, $iter:expr) => { ... };
}
_parens in flux_middle - Rust macro_rules! _parens {
+_parens in flux_middle - Rust macro_rules! _parens {
($val:expr, $parenthesize:expr) => { ... };
}
_w in flux_middle - Rust macro_rules! _w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+_w in flux_middle - Rust macro_rules! _w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
_with_cx in flux_middle - Rust macro_rules! _with_cx {
- ($e:expr) => { ... };
+_with_cx in flux_middle - Rust macro_rules! _with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
+KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
All,
SelfOnly,
Hide,
-}
Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> Any for Twhere
+}Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_middle/pretty/fn.debug_nested.html b/doc/flux_middle/pretty/fn.debug_nested.html
index bcf604c0a7..fe85616140 100644
--- a/doc/flux_middle/pretty/fn.debug_nested.html
+++ b/doc/flux_middle/pretty/fn.debug_nested.html
@@ -1,4 +1,4 @@
-debug_nested in flux_middle::pretty - Rust pub fn debug_nested<T: Pretty>(
+debug_nested in flux_middle::pretty - Rust float_children in flux_middle::pretty - Rust pub fn float_children(
+float_children in flux_middle::pretty - Rust pub fn float_children(
children: Vec<Option<Vec<NestedString>>>,
) -> Option<Vec<NestedString>>
pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
+pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
f: &mut Formatter<'_>,
t: &T,
cfg_key: Option<&'static str>,
diff --git a/doc/flux_middle/pretty/index.html b/doc/flux_middle/pretty/index.html
index 09c8258f22..05b9339fec 100644
--- a/doc/flux_middle/pretty/index.html
+++ b/doc/flux_middle/pretty/index.html
@@ -1 +1 @@
-flux_middle::pretty - Rust flux_middle::pretty - Rust Redirection
-
-
- Redirecting to macro.define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/pretty/macro.define_scoped.html b/doc/flux_middle/pretty/macro.define_scoped.html
deleted file mode 100644
index 2b1e8cc432..0000000000
--- a/doc/flux_middle/pretty/macro.define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-define_scoped in flux_middle::pretty - Rust macro_rules! define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
+format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
($($arg:tt)*) => { ... };
}
impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
+impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
join in flux_middle::pretty - Rust macro_rules! join {
+join in flux_middle::pretty - Rust macro_rules! join {
($sep:expr, $iter:expr) => { ... };
}
parens in flux_middle::pretty - Rust macro_rules! parens {
+parens in flux_middle::pretty - Rust macro_rules! parens {
($val:expr, $parenthesize:expr) => { ... };
}
set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
+set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
($cx:expr, $opts:expr, [$($opt:ident),+ $(,)?]) => { ... };
}
w in flux_middle::pretty - Rust macro_rules! w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+w in flux_middle::pretty - Rust macro_rules! w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
- ($e:expr) => { ... };
+with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
+BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
name_gen: IndexGen<BoundVarName>,
- layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>,
-}
Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> Any for Twhere
+ layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>,
+}Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_middle/pretty/struct.BoundVarName.html b/doc/flux_middle/pretty/struct.BoundVarName.html
index 2d5ebc3f89..d9a442b370 100644
--- a/doc/flux_middle/pretty/struct.BoundVarName.html
+++ b/doc/flux_middle/pretty/struct.BoundVarName.html
@@ -1,30 +1,30 @@
-BoundVarName in flux_middle::pretty - Rust struct BoundVarName {
+BoundVarName in flux_middle::pretty - Rust
Source§impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> CrateChecker<'genv, 'tcx>
fn new(genv: GlobalEnv<'genv, 'tcx>) -> Self
fn matches_check_def(&self, def_id: DefId) -> bool
fn matches_check_file(&self, def_id: LocalDefId) -> bool
fn check_def_catching_bugs( &mut self, def_id: LocalDefId, ) -> Result<(), ErrorGuaranteed>
fn check_def(&mut self, def_id: LocalDefId) -> Result<(), ErrorGuaranteed>
impl<'genv, 'tcx> Freeze for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !RefUnwindSafe for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Send for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !Sync for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> Unpin for CrateChecker<'genv, 'tcx>
impl<'genv, 'tcx> !UnwindSafe for CrateChecker<'genv, 'tcx>
Source§impl<T> Any for Twhere
diff --git a/doc/flux_infer/infer/index.html b/doc/flux_infer/infer/index.html
index 92282888f0..7a9875f1d1 100644
--- a/doc/flux_infer/infer/index.html
+++ b/doc/flux_infer/infer/index.html
@@ -1,3 +1,3 @@
-flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
+flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
to recover the derivation when relating types via subtyping. The code that attaches the trace is
currently commented out because the output is too verbose.
Traits§
Functions§
Type Aliases§
Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Hash for Tag
1.3.0 · Source§fn hash_slice<H>(data: &[Self], state: &mut H)where
+}Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/index.html b/doc/flux_infer/refine_tree/index.html
index ea8f0141bf..c2467e505c 100644
--- a/doc/flux_infer/refine_tree/index.html
+++ b/doc/flux_infer/refine_tree/index.html
@@ -1,4 +1,4 @@
-flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
+
flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
available in a particular path during type-checking. For example, consider the following
program:
- A very explicit representation of
RefineCtxt for debugging/tracing/serialization ONLY. - A refinement tree tracks the “tree-like structure” of refinement variables and predicates
generated during refinement type-checking. This tree can be encoded as a fixpoint constraint
diff --git a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
index 0b60baae1e..371a0e2209 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
@@ -1,4 +1,4 @@
-
fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
+fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
children: &[NodePtr],
cx: &PrettyCx<'_, '_>,
f: &mut Formatter<'_>,
diff --git a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
index b65a5287f1..90cd418f59 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
@@ -1 +1 @@
-with_padding in flux_infer::refine_tree::pretty - Rust with_padding in flux_infer::refine_tree::pretty - Rust NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> Any for Twhere
+NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RcxBind.html b/doc/flux_infer/refine_tree/struct.RcxBind.html
index 66b8e246d3..842fcd1231 100644
--- a/doc/flux_infer/refine_tree/struct.RcxBind.html
+++ b/doc/flux_infer/refine_tree/struct.RcxBind.html
@@ -1,7 +1,7 @@
-RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
+RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
name: String,
sort: String,
-}
Fields§
§name: String§sort: StringTrait Implementations§
Source§impl Serialize for RcxBind
Source§fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where
+}Fields§
§name: String§sort: StringTrait Implementations§
Auto Trait Implementations§
§impl Freeze for RcxBind
§impl RefUnwindSafe for RcxBind
§impl Send for RcxBind
§impl Sync for RcxBind
§impl Unpin for RcxBind
§impl UnwindSafe for RcxBind
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxt.html b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
index 211e5c34a5..ef21899753 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxt.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
@@ -32,7 +32,7 @@
)Sourcepub fn unpack(&mut self, ty: &Ty) -> Ty
Sourcepub fn hoister(
&mut self,
assume_invariants: AssumeInvariants,
-) -> Hoister<Unpacker<'_, 'rcx>>
Sourcepub fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool)
Sourcepub fn replace_evars(&mut self, evars: &EVarSol)
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
index 58b24ea640..e17f80314c 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
@@ -1,8 +1,8 @@
-RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
+RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
bindings: Vec<RcxBind>,
exprs: Vec<String>,
}
Expand description
A very explicit representation of RefineCtxt for debugging/tracing/serialization ONLY.
-Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Source§impl Serialize for RefineCtxtTrace
Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Auto Trait Implementations§
§impl Freeze for RefineCtxtTrace
§impl RefUnwindSafe for RefineCtxtTrace
§impl Send for RefineCtxtTrace
§impl Sync for RefineCtxtTrace
§impl Unpin for RefineCtxtTrace
§impl UnwindSafe for RefineCtxtTrace
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineTree.html b/doc/flux_infer/refine_tree/struct.RefineTree.html
index 80683cd28f..8441c89569 100644
--- a/doc/flux_infer/refine_tree/struct.RefineTree.html
+++ b/doc/flux_infer/refine_tree/struct.RefineTree.html
@@ -19,7 +19,7 @@
) -> QueryResult<RefineTree>Sourcepub fn simplify(&mut self, defns: &SpecFuncDefns)
Sourcepub fn into_fixpoint(
self,
cx: &mut FixpointCtxt<'_, '_, Tag>,
-) -> QueryResult<Constraint>
Sourcepub fn refine_ctxt_at_root(&mut self) -> RefineCtxt<'_>
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.Scope.html b/doc/flux_infer/refine_tree/struct.Scope.html
index fe229512ce..99d93c021f 100644
--- a/doc/flux_infer/refine_tree/struct.Scope.html
+++ b/doc/flux_infer/refine_tree/struct.Scope.html
@@ -3,8 +3,8 @@
params: Vec<(Var, Sort)>,
}Expand description
A list of refinement variables and their sorts.
Fields§
§bindings: IndexVec<Name, Sort>§params: Vec<(Var, Sort)>Implementations§
Source§impl Scope
Sourcepub fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_
Sourcepub fn has_free_vars<T: TypeFoldable>(&self, t: &T) -> bool
Whether t has any free variables not in this scope
-Sourcefn contains_all(&self, iter: impl IntoIterator<Item = Name>) -> bool
Sourcefn contains(&self, name: Name) -> bool
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§impl<Q, K> Equivalent<K> for Qwhere
diff --git a/doc/flux_middle/all.html b/doc/flux_middle/all.html
index b30630d868..1c73baac8a 100644
--- a/doc/flux_middle/all.html
+++ b/doc/flux_middle/all.html
@@ -1 +1 @@
-List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _define_scoped
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::define_scoped
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
flux_middle - Rust Expand description
This crate contains common type definitions that are used by other crates.
Modules§
- Flux High-Level Intermediate Representation
- Defines how flux represents refinement types internally. Definitions in this module are used
during refinement type checking. A couple of important differences between definitions in this
-module and in
crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
+module and in crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
for an extern spec. - This enum serves as a type-level reminder that a local definition may be a wrapper for an
extern spec. This abstraction is not infallible, so one should be careful and decide in each
situation whether to use the local id or the resolved id.
- Normally, a
DefId is either local or external, and DefId::as_local can be used to
diff --git a/doc/flux_middle/macro._define_scoped!.html b/doc/flux_middle/macro._define_scoped!.html
deleted file mode 100644
index c63ebc6ad3..0000000000
--- a/doc/flux_middle/macro._define_scoped!.html
+++ /dev/null
@@ -1,11 +0,0 @@
-
-
-
-
- Redirection
-
-
- Redirecting to macro._define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/macro._define_scoped.html b/doc/flux_middle/macro._define_scoped.html
deleted file mode 100644
index ee55233dc3..0000000000
--- a/doc/flux_middle/macro._define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-_define_scoped in flux_middle - Rust macro_rules! _define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
_format_cx in flux_middle - Rust macro_rules! _format_cx {
+_format_cx in flux_middle - Rust macro_rules! _format_cx {
($($arg:tt)*) => { ... };
}
_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
+_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
_join in flux_middle - Rust macro_rules! _join {
+_join in flux_middle - Rust macro_rules! _join {
($sep:expr, $iter:expr) => { ... };
}
_parens in flux_middle - Rust macro_rules! _parens {
+_parens in flux_middle - Rust macro_rules! _parens {
($val:expr, $parenthesize:expr) => { ... };
}
_w in flux_middle - Rust macro_rules! _w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+_w in flux_middle - Rust macro_rules! _w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
_with_cx in flux_middle - Rust macro_rules! _with_cx {
- ($e:expr) => { ... };
+_with_cx in flux_middle - Rust macro_rules! _with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
+KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
All,
SelfOnly,
Hide,
-}
Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> Any for Twhere
+}Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_middle/pretty/fn.debug_nested.html b/doc/flux_middle/pretty/fn.debug_nested.html
index bcf604c0a7..fe85616140 100644
--- a/doc/flux_middle/pretty/fn.debug_nested.html
+++ b/doc/flux_middle/pretty/fn.debug_nested.html
@@ -1,4 +1,4 @@
-debug_nested in flux_middle::pretty - Rust pub fn debug_nested<T: Pretty>(
+debug_nested in flux_middle::pretty - Rust float_children in flux_middle::pretty - Rust pub fn float_children(
+float_children in flux_middle::pretty - Rust pub fn float_children(
children: Vec<Option<Vec<NestedString>>>,
) -> Option<Vec<NestedString>>
pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
+pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
f: &mut Formatter<'_>,
t: &T,
cfg_key: Option<&'static str>,
diff --git a/doc/flux_middle/pretty/index.html b/doc/flux_middle/pretty/index.html
index 09c8258f22..05b9339fec 100644
--- a/doc/flux_middle/pretty/index.html
+++ b/doc/flux_middle/pretty/index.html
@@ -1 +1 @@
-flux_middle::pretty - Rust flux_middle::pretty - Rust Redirection
-
-
- Redirecting to macro.define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/pretty/macro.define_scoped.html b/doc/flux_middle/pretty/macro.define_scoped.html
deleted file mode 100644
index 2b1e8cc432..0000000000
--- a/doc/flux_middle/pretty/macro.define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-define_scoped in flux_middle::pretty - Rust macro_rules! define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
+format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
($($arg:tt)*) => { ... };
}
impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
+impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
join in flux_middle::pretty - Rust macro_rules! join {
+join in flux_middle::pretty - Rust macro_rules! join {
($sep:expr, $iter:expr) => { ... };
}
parens in flux_middle::pretty - Rust macro_rules! parens {
+parens in flux_middle::pretty - Rust macro_rules! parens {
($val:expr, $parenthesize:expr) => { ... };
}
set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
+set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
($cx:expr, $opts:expr, [$($opt:ident),+ $(,)?]) => { ... };
}
w in flux_middle::pretty - Rust macro_rules! w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+w in flux_middle::pretty - Rust macro_rules! w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
- ($e:expr) => { ... };
+with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
+BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
name_gen: IndexGen<BoundVarName>,
- layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>,
-}
Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> Any for Twhere
+ layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>,
+}Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_middle/pretty/struct.BoundVarName.html b/doc/flux_middle/pretty/struct.BoundVarName.html
index 2d5ebc3f89..d9a442b370 100644
--- a/doc/flux_middle/pretty/struct.BoundVarName.html
+++ b/doc/flux_middle/pretty/struct.BoundVarName.html
@@ -1,30 +1,30 @@
-BoundVarName in flux_middle::pretty - Rust struct BoundVarName {
+BoundVarName in flux_middle::pretty - Rust
impl<T> Any for Twhere
diff --git a/doc/flux_infer/infer/index.html b/doc/flux_infer/infer/index.html
index 92282888f0..7a9875f1d1 100644
--- a/doc/flux_infer/infer/index.html
+++ b/doc/flux_infer/infer/index.html
@@ -1,3 +1,3 @@
-flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
+flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒 Context used to relate two types
a and b via subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTree that can be used to print information
to recover the derivation when relating types via subtyping. The code that attaches the trace is
currently commented out because the output is too verbose.
Traits§
Functions§
Type Aliases§
Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Hash for Tag
1.3.0 · Source§fn hash_slice<H>(data: &[Self], state: &mut H)where
+}Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl Copy for Tag
Source§impl Eq for Tag
Source§impl StructuralPartialEq for Tag
Auto Trait Implementations§
§impl Freeze for Tag
§impl RefUnwindSafe for Tag
§impl Send for Tag
§impl Sync for Tag
§impl Unpin for Tag
§impl UnwindSafe for Tag
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/index.html b/doc/flux_infer/refine_tree/index.html
index ea8f0141bf..c2467e505c 100644
--- a/doc/flux_infer/refine_tree/index.html
+++ b/doc/flux_infer/refine_tree/index.html
@@ -1,4 +1,4 @@
-flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
+
flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates
available in a particular path during type-checking. For example, consider the following
program:
- A very explicit representation of
RefineCtxt for debugging/tracing/serialization ONLY. - A refinement tree tracks the “tree-like structure” of refinement variables and predicates
generated during refinement type-checking. This tree can be encoded as a fixpoint constraint
diff --git a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
index 0b60baae1e..371a0e2209 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html
@@ -1,4 +1,4 @@
-
fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
+fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children(
children: &[NodePtr],
cx: &PrettyCx<'_, '_>,
f: &mut Formatter<'_>,
diff --git a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
index b65a5287f1..90cd418f59 100644
--- a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
+++ b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html
@@ -1 +1 @@
-with_padding in flux_infer::refine_tree::pretty - Rust with_padding in flux_infer::refine_tree::pretty - Rust NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> Any for Twhere
+NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);
Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for NodePtr
§impl !RefUnwindSafe for NodePtr
§impl !Send for NodePtr
§impl !Sync for NodePtr
§impl Unpin for NodePtr
§impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RcxBind.html b/doc/flux_infer/refine_tree/struct.RcxBind.html
index 66b8e246d3..842fcd1231 100644
--- a/doc/flux_infer/refine_tree/struct.RcxBind.html
+++ b/doc/flux_infer/refine_tree/struct.RcxBind.html
@@ -1,7 +1,7 @@
-RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
+RcxBind in flux_infer::refine_tree - Rust struct RcxBind {
name: String,
sort: String,
-}
Fields§
§name: String§sort: StringTrait Implementations§
Source§impl Serialize for RcxBind
Source§fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>where
+}Fields§
§name: String§sort: StringTrait Implementations§
Auto Trait Implementations§
§impl Freeze for RcxBind
§impl RefUnwindSafe for RcxBind
§impl Send for RcxBind
§impl Sync for RcxBind
§impl Unpin for RcxBind
§impl UnwindSafe for RcxBind
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxt.html b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
index 211e5c34a5..ef21899753 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxt.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxt.html
@@ -32,7 +32,7 @@
)Sourcepub fn unpack(&mut self, ty: &Ty) -> Ty
Sourcepub fn hoister(
&mut self,
assume_invariants: AssumeInvariants,
-) -> Hoister<Unpacker<'_, 'rcx>>
Sourcepub fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool)
Sourcepub fn replace_evars(&mut self, evars: &EVarSol)
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§impl<'a> Freeze for RefineCtxt<'a>
§impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§impl<'a> !Send for RefineCtxt<'a>
§impl<'a> !Sync for RefineCtxt<'a>
§impl<'a> Unpin for RefineCtxt<'a>
§impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
index 58b24ea640..e17f80314c 100644
--- a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
+++ b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html
@@ -1,8 +1,8 @@
-RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
+RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace {
bindings: Vec<RcxBind>,
exprs: Vec<String>,
}
Expand description
A very explicit representation of RefineCtxt for debugging/tracing/serialization ONLY.
-Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Source§impl Serialize for RefineCtxtTrace
Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§impl RefineCtxtTrace
Sourcepub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§impl Debug for RefineCtxtTrace
Auto Trait Implementations§
§impl Freeze for RefineCtxtTrace
§impl RefUnwindSafe for RefineCtxtTrace
§impl Send for RefineCtxtTrace
§impl Sync for RefineCtxtTrace
§impl Unpin for RefineCtxtTrace
§impl UnwindSafe for RefineCtxtTrace
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
diff --git a/doc/flux_infer/refine_tree/struct.RefineTree.html b/doc/flux_infer/refine_tree/struct.RefineTree.html
index 80683cd28f..8441c89569 100644
--- a/doc/flux_infer/refine_tree/struct.RefineTree.html
+++ b/doc/flux_infer/refine_tree/struct.RefineTree.html
@@ -19,7 +19,7 @@
) -> QueryResult<RefineTree>Sourcepub fn simplify(&mut self, defns: &SpecFuncDefns)
Sourcepub fn into_fixpoint(
self,
cx: &mut FixpointCtxt<'_, '_, Tag>,
-) -> QueryResult<Constraint>
Sourcepub fn refine_ctxt_at_root(&mut self) -> RefineCtxt<'_>
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Trait Implementations§
Source§impl Debug for RefineTree
Auto Trait Implementations§
§impl Freeze for RefineTree
§impl !RefUnwindSafe for RefineTree
§impl !Send for RefineTree
§impl !Sync for RefineTree
§impl Unpin for RefineTree
§impl !UnwindSafe for RefineTree
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.Scope.html b/doc/flux_infer/refine_tree/struct.Scope.html
index fe229512ce..99d93c021f 100644
--- a/doc/flux_infer/refine_tree/struct.Scope.html
+++ b/doc/flux_infer/refine_tree/struct.Scope.html
@@ -3,8 +3,8 @@
params: Vec<(Var, Sort)>,
}Expand description
A list of refinement variables and their sorts.
Fields§
§bindings: IndexVec<Name, Sort>§params: Vec<(Var, Sort)>Implementations§
Source§impl Scope
Sourcepub fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_
Sourcepub fn has_free_vars<T: TypeFoldable>(&self, t: &T) -> bool
Whether t has any free variables not in this scope
-Sourcefn contains_all(&self, iter: impl IntoIterator<Item = Name>) -> bool
Sourcefn contains(&self, name: Name) -> bool
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Trait Implementations§
Source§impl Eq for Scope
Source§impl StructuralPartialEq for Scope
Auto Trait Implementations§
§impl Freeze for Scope
§impl RefUnwindSafe for Scope
§impl Send for Scope
§impl Sync for Scope
§impl Unpin for Scope
§impl UnwindSafe for Scope
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§impl<Q, K> Equivalent<K> for Qwhere
diff --git a/doc/flux_middle/all.html b/doc/flux_middle/all.html
index b30630d868..1c73baac8a 100644
--- a/doc/flux_middle/all.html
+++ b/doc/flux_middle/all.html
@@ -1 +1 @@
-List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _define_scoped
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::define_scoped
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
flux_middle - Rust Expand description
This crate contains common type definitions that are used by other crates.
Modules§
- Flux High-Level Intermediate Representation
- Defines how flux represents refinement types internally. Definitions in this module are used
during refinement type checking. A couple of important differences between definitions in this
-module and in
crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
+module and in crate::fhir are: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefId and a DefId
for an extern spec. - This enum serves as a type-level reminder that a local definition may be a wrapper for an
extern spec. This abstraction is not infallible, so one should be careful and decide in each
situation whether to use the local id or the resolved id.
- Normally, a
DefId is either local or external, and DefId::as_local can be used to
diff --git a/doc/flux_middle/macro._define_scoped!.html b/doc/flux_middle/macro._define_scoped!.html
deleted file mode 100644
index c63ebc6ad3..0000000000
--- a/doc/flux_middle/macro._define_scoped!.html
+++ /dev/null
@@ -1,11 +0,0 @@
-
-
-
-
- Redirection
-
-
- Redirecting to macro._define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/macro._define_scoped.html b/doc/flux_middle/macro._define_scoped.html
deleted file mode 100644
index ee55233dc3..0000000000
--- a/doc/flux_middle/macro._define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-_define_scoped in flux_middle - Rust macro_rules! _define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
_format_cx in flux_middle - Rust macro_rules! _format_cx {
+_format_cx in flux_middle - Rust macro_rules! _format_cx {
($($arg:tt)*) => { ... };
}
_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
+_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
_join in flux_middle - Rust macro_rules! _join {
+_join in flux_middle - Rust macro_rules! _join {
($sep:expr, $iter:expr) => { ... };
}
_parens in flux_middle - Rust macro_rules! _parens {
+_parens in flux_middle - Rust macro_rules! _parens {
($val:expr, $parenthesize:expr) => { ... };
}
_w in flux_middle - Rust macro_rules! _w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+_w in flux_middle - Rust macro_rules! _w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
_with_cx in flux_middle - Rust macro_rules! _with_cx {
- ($e:expr) => { ... };
+_with_cx in flux_middle - Rust macro_rules! _with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
+KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs {
All,
SelfOnly,
Hide,
-}
Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> Any for Twhere
+}Variants§
Trait Implementations§
Auto Trait Implementations§
§impl Freeze for KVarArgs
§impl RefUnwindSafe for KVarArgs
§impl Send for KVarArgs
§impl Sync for KVarArgs
§impl Unpin for KVarArgs
§impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> CloneToUninit for Twhere
diff --git a/doc/flux_middle/pretty/fn.debug_nested.html b/doc/flux_middle/pretty/fn.debug_nested.html
index bcf604c0a7..fe85616140 100644
--- a/doc/flux_middle/pretty/fn.debug_nested.html
+++ b/doc/flux_middle/pretty/fn.debug_nested.html
@@ -1,4 +1,4 @@
-debug_nested in flux_middle::pretty - Rust pub fn debug_nested<T: Pretty>(
+debug_nested in flux_middle::pretty - Rust float_children in flux_middle::pretty - Rust pub fn float_children(
+float_children in flux_middle::pretty - Rust pub fn float_children(
children: Vec<Option<Vec<NestedString>>>,
) -> Option<Vec<NestedString>>
pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
+pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>(
f: &mut Formatter<'_>,
t: &T,
cfg_key: Option<&'static str>,
diff --git a/doc/flux_middle/pretty/index.html b/doc/flux_middle/pretty/index.html
index 09c8258f22..05b9339fec 100644
--- a/doc/flux_middle/pretty/index.html
+++ b/doc/flux_middle/pretty/index.html
@@ -1 +1 @@
-flux_middle::pretty - Rust flux_middle::pretty - Rust Redirection
-
-
- Redirecting to macro.define_scoped.html...
-
-
-
\ No newline at end of file
diff --git a/doc/flux_middle/pretty/macro.define_scoped.html b/doc/flux_middle/pretty/macro.define_scoped.html
deleted file mode 100644
index 2b1e8cc432..0000000000
--- a/doc/flux_middle/pretty/macro.define_scoped.html
+++ /dev/null
@@ -1,3 +0,0 @@
-define_scoped in flux_middle::pretty - Rust macro_rules! define_scoped {
- ($cx:ident, $fmt:expr) => { ... };
-}
format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($fmt:literal) => { ... };
- (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
- (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
+format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx {
+ ($cx:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $fmt:literal) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... };
+ (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... };
(@as_expr $e:expr) => { ... };
}
format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
+format_cx in flux_middle::pretty - Rust macro_rules! format_cx {
($($arg:tt)*) => { ... };
}
impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
+impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx {
($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... };
}
join in flux_middle::pretty - Rust macro_rules! join {
+join in flux_middle::pretty - Rust macro_rules! join {
($sep:expr, $iter:expr) => { ... };
}
parens in flux_middle::pretty - Rust macro_rules! parens {
+parens in flux_middle::pretty - Rust macro_rules! parens {
($val:expr, $parenthesize:expr) => { ... };
}
set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
+set_opts in flux_middle::pretty - Rust macro_rules! set_opts {
($cx:expr, $opts:expr, [$($opt:ident),+ $(,)?]) => { ... };
}
w in flux_middle::pretty - Rust macro_rules! w {
- ($fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal, $($args:tt)*) => { ... };
- ($f:expr, $fmt:literal) => { ... };
- ($fmt:literal) => { ... };
+w in flux_middle::pretty - Rust macro_rules! w {
+ ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... };
+ ($cx:expr, $f:expr, $fmt:literal) => { ... };
}
with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
- ($e:expr) => { ... };
+with_cx in flux_middle::pretty - Rust macro_rules! with_cx {
+ ($cx:expr, $e:expr) => { ... };
}
BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
+BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv {
name_gen: IndexGen<BoundVarName>,
- layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>,
-}
Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> Any for Twhere
+ layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>,
+}Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>Implementations§
Source§impl BoundVarEnv
Sourcefn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Sourcefn push_layer(&self, vars: &[BoundVariableKind])
Sourcefn pop_layer(&self)
Trait Implementations§
Source§impl Default for BoundVarEnv
Source§fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§impl !Freeze for BoundVarEnv
§impl !RefUnwindSafe for BoundVarEnv
§impl Send for BoundVarEnv
§impl !Sync for BoundVarEnv
§impl Unpin for BoundVarEnv
§impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§impl<T> From<T> for T
Source§fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_middle/pretty/struct.BoundVarName.html b/doc/flux_middle/pretty/struct.BoundVarName.html
index 2d5ebc3f89..d9a442b370 100644
--- a/doc/flux_middle/pretty/struct.BoundVarName.html
+++ b/doc/flux_middle/pretty/struct.BoundVarName.html
@@ -1,30 +1,30 @@
-BoundVarName in flux_middle::pretty - Rust struct BoundVarName {
+BoundVarName in flux_middle::pretty - Rust
Modules§
- pretty 🔒
Structs§
- Sub 🔒Context used to relate two types
aandbvia subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTreethat can be used to print information +flux_infer::infer - Rust Modules§
- pretty 🔒
Structs§
- Sub 🔒Context used to relate two types
aandbvia subtyping
Enums§
- Used for debugging to attach a “trace” to the
RefineTreethat can be used to print information to recover the derivation when relating types via subtyping. The code that attaches the trace is currently commented out because the output is too verbose.
Traits§
Functions§
Type Aliases§
Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§ impl Hash for Tag
1.3.0 · Source§ fn hash_slice<H>(data: &[Self], state: &mut H)
where +}Fields§
§reason: ConstrReason§src_span: Span§dst_span: Option<ESpan>Implementations§
Trait Implementations§
Source§ impl Copy for Tag
Source§ impl Eq for Tag
Source§ impl StructuralPartialEq for Tag
Auto Trait Implementations§
§ impl Freeze for Tag
§ impl RefUnwindSafe for Tag
§ impl Send for Tag
§ impl Sync for Tag
§ impl Unpin for Tag
§ impl UnwindSafe for Tag
Blanket Implementations§
Source§ impl Copy for Tag
Source§ impl Eq for Tag
Source§ impl StructuralPartialEq for Tag
Auto Trait Implementations§
§ impl Freeze for Tag
§ impl RefUnwindSafe for Tag
§ impl Send for Tag
§ impl Sync for Tag
§ impl Unpin for Tag
§ impl UnwindSafe for Tag
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> CloneToUninit for T
where diff --git a/doc/flux_infer/refine_tree/index.html b/doc/flux_infer/refine_tree/index.html index ea8f0141bf..c2467e505c 100644 --- a/doc/flux_infer/refine_tree/index.html +++ b/doc/flux_infer/refine_tree/index.html @@ -1,4 +1,4 @@ -flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates +
flux_infer::refine_tree - Rust Modules§
- pretty 🔒
Structs§
- Node 🔒
- NodePtr 🔒
- RcxBind 🔒
- A refinement context tracks all the refinement parameters and predicates available in a particular path during type-checking. For example, consider the following program:
- A very explicit representation of
RefineCtxtfor debugging/tracing/serialization ONLY. - A refinement tree tracks the “tree-like structure” of refinement variables and predicates generated during refinement type-checking. This tree can be encoded as a fixpoint constraint diff --git a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html index 0b60baae1e..371a0e2209 100644 --- a/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html +++ b/doc/flux_infer/refine_tree/pretty/fn.fmt_children.html @@ -1,4 +1,4 @@ -
fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children( +fmt_children in flux_infer::refine_tree::pretty - Rust fn fmt_children( children: &[NodePtr], cx: &PrettyCx<'_, '_>, f: &mut Formatter<'_>, diff --git a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html index b65a5287f1..90cd418f59 100644 --- a/doc/flux_infer/refine_tree/pretty/fn.with_padding.html +++ b/doc/flux_infer/refine_tree/pretty/fn.with_padding.html @@ -1 +1 @@ -with_padding in flux_infer::refine_tree::pretty - Rust \ No newline at end of file + with_padding in flux_infer::refine_tree::pretty - Rust \ No newline at end of file diff --git a/doc/flux_infer/refine_tree/struct.NodePtr.html b/doc/flux_infer/refine_tree/struct.NodePtr.html index 3d4dbdeba0..e73d99a97b 100644 --- a/doc/flux_infer/refine_tree/struct.NodePtr.html +++ b/doc/flux_infer/refine_tree/struct.NodePtr.html @@ -1,4 +1,4 @@ - NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§ impl Freeze for NodePtr
§ impl !RefUnwindSafe for NodePtr
§ impl !Send for NodePtr
§ impl !Sync for NodePtr
§ impl Unpin for NodePtr
§ impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§ impl<T> Any for T
where +NodePtr in flux_infer::refine_tree - Rust struct NodePtr(Rc<RefCell<Node>>);Tuple Fields§
§0: Rc<RefCell<Node>>Implementations§
Trait Implementations§
Auto Trait Implementations§
§ impl Freeze for NodePtr
§ impl !RefUnwindSafe for NodePtr
§ impl !Send for NodePtr
§ impl !Sync for NodePtr
§ impl Unpin for NodePtr
§ impl !UnwindSafe for NodePtr
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> CloneToUninit for T
where diff --git a/doc/flux_infer/refine_tree/struct.RcxBind.html b/doc/flux_infer/refine_tree/struct.RcxBind.html index 66b8e246d3..842fcd1231 100644 --- a/doc/flux_infer/refine_tree/struct.RcxBind.html +++ b/doc/flux_infer/refine_tree/struct.RcxBind.html @@ -1,7 +1,7 @@ -RcxBind in flux_infer::refine_tree - Rust struct RcxBind { +RcxBind in flux_infer::refine_tree - Rust struct RcxBind { name: String, sort: String, -}Fields§
§name: String§sort: StringTrait Implementations§
Source§ impl Serialize for RcxBind
Source§ fn serialize<__S>(&self, __serializer: __S) -> Result<__S::Ok, __S::Error>
where +}Fields§
§name: String§sort: StringTrait Implementations§
Auto Trait Implementations§
§ impl Freeze for RcxBind
§ impl RefUnwindSafe for RcxBind
§ impl Send for RcxBind
§ impl Sync for RcxBind
§ impl Unpin for RcxBind
§ impl UnwindSafe for RcxBind
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxt.html b/doc/flux_infer/refine_tree/struct.RefineCtxt.html index 211e5c34a5..ef21899753 100644 --- a/doc/flux_infer/refine_tree/struct.RefineCtxt.html +++ b/doc/flux_infer/refine_tree/struct.RefineCtxt.html @@ -32,7 +32,7 @@ )Source pub fn unpack(&mut self, ty: &Ty) -> Ty
Source pub fn hoister( &mut self, assume_invariants: AssumeInvariants, -) -> Hoister<Unpacker<'_, 'rcx>>
Source pub fn assume_invariants(&mut self, ty: &Ty, overflow_checking: bool)
Source pub fn replace_evars(&mut self, evars: &EVarSol)
Trait Implementations§
Source§ impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§ impl<'a> Freeze for RefineCtxt<'a>
§ impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§ impl<'a> !Send for RefineCtxt<'a>
§ impl<'a> !Sync for RefineCtxt<'a>
§ impl<'a> Unpin for RefineCtxt<'a>
§ impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Trait Implementations§
Source§ impl Debug for RefineCtxt<'_>
Auto Trait Implementations§
§ impl<'a> Freeze for RefineCtxt<'a>
§ impl<'a> !RefUnwindSafe for RefineCtxt<'a>
§ impl<'a> !Send for RefineCtxt<'a>
§ impl<'a> !Sync for RefineCtxt<'a>
§ impl<'a> Unpin for RefineCtxt<'a>
§ impl<'a> !UnwindSafe for RefineCtxt<'a>
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> From<T> for T
Source§ fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html index 58b24ea640..e17f80314c 100644 --- a/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html +++ b/doc/flux_infer/refine_tree/struct.RefineCtxtTrace.html @@ -1,8 +1,8 @@ -RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace { +RefineCtxtTrace in flux_infer::refine_tree - Rust pub struct RefineCtxtTrace { bindings: Vec<RcxBind>, exprs: Vec<String>, }Expand description
A very explicit representation of
-RefineCtxtfor debugging/tracing/serialization ONLY.Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§ impl RefineCtxtTrace
Source pub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§ impl Debug for RefineCtxtTrace
Source§ impl Serialize for RefineCtxtTrace
Fields§
§bindings: Vec<RcxBind>§exprs: Vec<String>Implementations§
Source§ impl RefineCtxtTrace
Source pub fn new(genv: GlobalEnv<'_, '_>, rcx: &RefineCtxt<'_>) -> Self
Trait Implementations§
Source§ impl Debug for RefineCtxtTrace
Auto Trait Implementations§
§ impl Freeze for RefineCtxtTrace
§ impl RefUnwindSafe for RefineCtxtTrace
§ impl Send for RefineCtxtTrace
§ impl Sync for RefineCtxtTrace
§ impl Unpin for RefineCtxtTrace
§ impl UnwindSafe for RefineCtxtTrace
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where diff --git a/doc/flux_infer/refine_tree/struct.RefineTree.html b/doc/flux_infer/refine_tree/struct.RefineTree.html index 80683cd28f..8441c89569 100644 --- a/doc/flux_infer/refine_tree/struct.RefineTree.html +++ b/doc/flux_infer/refine_tree/struct.RefineTree.html @@ -19,7 +19,7 @@ ) -> QueryResult<RefineTree>Source pub fn simplify(&mut self, defns: &SpecFuncDefns)
Source pub fn into_fixpoint( self, cx: &mut FixpointCtxt<'_, '_, Tag>, -) -> QueryResult<Constraint>
Source pub fn refine_ctxt_at_root(&mut self) -> RefineCtxt<'_>
Trait Implementations§
Source§ impl Debug for RefineTree
Auto Trait Implementations§
§ impl Freeze for RefineTree
§ impl !RefUnwindSafe for RefineTree
§ impl !Send for RefineTree
§ impl !Sync for RefineTree
§ impl Unpin for RefineTree
§ impl !UnwindSafe for RefineTree
Blanket Implementations§
Trait Implementations§
Source§ impl Debug for RefineTree
Auto Trait Implementations§
§ impl Freeze for RefineTree
§ impl !RefUnwindSafe for RefineTree
§ impl !Send for RefineTree
§ impl !Sync for RefineTree
§ impl Unpin for RefineTree
§ impl !UnwindSafe for RefineTree
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> From<T> for T
Source§ fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_infer/refine_tree/struct.Scope.html b/doc/flux_infer/refine_tree/struct.Scope.html index fe229512ce..99d93c021f 100644 --- a/doc/flux_infer/refine_tree/struct.Scope.html +++ b/doc/flux_infer/refine_tree/struct.Scope.html @@ -3,8 +3,8 @@ params: Vec<(Var, Sort)>, }Expand description
A list of refinement variables and their sorts.
Fields§
§bindings: IndexVec<Name, Sort>§params: Vec<(Var, Sort)>Implementations§
Source§ impl Scope
Source pub fn iter(&self) -> impl Iterator<Item = (Var, Sort)> + '_
Source pub fn has_free_vars<T: TypeFoldable>(&self, t: &T) -> bool
Whether
-thas any free variables not in this scopeSource fn contains_all(&self, iter: impl IntoIterator<Item = Name>) -> bool
Source fn contains(&self, name: Name) -> bool
Trait Implementations§
Source§ impl Eq for Scope
Source§ impl StructuralPartialEq for Scope
Auto Trait Implementations§
§ impl Freeze for Scope
§ impl RefUnwindSafe for Scope
§ impl Send for Scope
§ impl Sync for Scope
§ impl Unpin for Scope
§ impl UnwindSafe for Scope
Blanket Implementations§
Trait Implementations§
Source§ impl Eq for Scope
Source§ impl StructuralPartialEq for Scope
Auto Trait Implementations§
§ impl Freeze for Scope
§ impl RefUnwindSafe for Scope
§ impl Send for Scope
§ impl Sync for Scope
§ impl Unpin for Scope
§ impl UnwindSafe for Scope
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more§ impl<Q, K> Equivalent<K> for Q
where diff --git a/doc/flux_middle/all.html b/doc/flux_middle/all.html index b30630d868..1c73baac8a 100644 --- a/doc/flux_middle/all.html +++ b/doc/flux_middle/all.html @@ -1 +1 @@ -List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _define_scoped
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::define_scoped
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
List of all items in this crate List of all items
Structs
- PlaceTy
- ResolverOutput
- Specs
- TheoryFunc
- big_int::BigInt
- fhir::AliasReft
- fhir::AssocItemConstraint
- fhir::BareFnTy
- fhir::BaseTy
- fhir::ConstArg
- fhir::EnumDef
- fhir::Expr
- fhir::FhirId
- fhir::FieldDef
- fhir::FieldExpr
- fhir::FluxItems
- fhir::FnDecl
- fhir::FnOutput
- fhir::FnSig
- fhir::FuncSort
- fhir::GenericParam
- fhir::Generics
- fhir::Impl
- fhir::ImplAssocReft
- fhir::ImplItem
- fhir::Item
- fhir::ItemLocalId
- fhir::MutTy
- fhir::OpaqueTy
- fhir::ParamId
- fhir::PartialRes
- fhir::Path
- fhir::PathExpr
- fhir::PathSegment
- fhir::PolyFuncSort
- fhir::PolyTraitRef
- fhir::Qualifier
- fhir::RefineParam
- fhir::RefinedBy
- fhir::Requires
- fhir::SortDecl
- fhir::SortPath
- fhir::SpecFunc
- fhir::Spread
- fhir::StructDef
- fhir::Trait
- fhir::TraitAssocReft
- fhir::TraitItem
- fhir::Ty
- fhir::TyAlias
- fhir::VariantDef
- fhir::VariantIdx
- fhir::VariantRet
- fhir::WhereBoundPredicate
- fhir::lift::LiftCtxt
- fhir::lift::errors::UnsupportedHir
- global_env::GlobalEnv
- global_env::GlobalEnvInner
- global_env::Ident
- global_env::Map
- global_env::Symbol
- pretty::BoundVarEnv
- pretty::BoundVarName
- pretty::Join
- pretty::NestedString
- pretty::Parens
- pretty::PrettyCx
- pretty::WithCx
- queries::Providers
- queries::Queries
- queries::QueryErrAt
- rty::AdtDef
- rty::AdtDefData
- rty::AdtFlags
- rty::AdtSortDef
- rty::AdtSortDefData
- rty::AliasReft
- rty::AliasTy
- rty::AssocRefinement
- rty::AssocRefinements
- rty::Binder
- rty::BoundReft
- rty::BoundRegion
- rty::BoundVar
- rty::BvSizeVid
- rty::Clause
- rty::Const
- rty::ConstVid
- rty::CoroutineObligPredicate
- rty::DebruijnIndex
- rty::ESpan
- rty::EarlyBinder
- rty::EarlyParamRegion
- rty::EarlyReftParam
- rty::ExistentialProjection
- rty::ExistentialTraitRef
- rty::Expr
- rty::FnOutput
- rty::FnSig
- rty::FnTraitPredicate
- rty::FuncSort
- rty::GenericParamDef
- rty::GenericPredicates
- rty::Generics
- rty::Invariant
- rty::KVar
- rty::KVid
- rty::Lambda
- rty::LateParamRegion
- rty::LocalTableInContext
- rty::LocalTableInContextMut
- rty::Name
- rty::NumVid
- rty::OutlivesPredicate
- rty::ParamConst
- rty::ParamSort
- rty::ParamTy
- rty::Path
- rty::PolyFuncSort
- rty::ProjectionPredicate
- rty::Qualifier
- rty::Real
- rty::RefineParam
- rty::RefinementGenerics
- rty::RegionVid
- rty::ScalarInt
- rty::SortVid
- rty::SpecFunc
- rty::SpecFuncDecl
- rty::SpecFuncDefns
- rty::SubsetTy
- rty::TraitPredicate
- rty::TraitRef
- rty::Ty
- rty::TyVid
- rty::VariantIdx
- rty::VariantSig
- rty::WfckResults
- rty::binder::Binder
- rty::binder::EarlyBinder
- rty::canonicalize::CanonicalConstrTy
- rty::canonicalize::Hoister
- rty::canonicalize::LocalHoister
- rty::evars::EVar
- rty::evars::EVarCtxt
- rty::evars::EVarCxId
- rty::evars::EVarGen
- rty::evars::EVarSol
- rty::evars::EVid
- rty::evars::UnsolvedEvar
- rty::expr::AliasReft
- rty::expr::BoundReft
- rty::expr::ESpan
- rty::expr::EarlyReftParam
- rty::expr::Expr
- rty::expr::FieldBind
- rty::expr::KVar
- rty::expr::KVid
- rty::expr::Lambda
- rty::expr::Name
- rty::expr::Path
- rty::expr::Real
- rty::normalize::BaseSpanner
- rty::normalize::Normalizer
- rty::normalize::SpecFuncDefns
- rty::pretty::IdxFmt
- rty::projections::Normalizer
- rty::projections::TVarSubst
- rty::refining::Refiner
- rty::region_matching::RegionSubst
- rty::subst::BoundVarReplacer
- rty::subst::EVarSubstFolder
- rty::subst::FnMutDelegate
- rty::subst::GenericArgsDelegate
- rty::subst::GenericsSubstFolder
- rty::subst::GenericsSubstForSort
- rty::subst::SortSubst
Enums
- ExternSpecMappingErr
- MaybeExternId
- ResolvedDefId
- big_int::Sign
- fhir::AssocItemConstraintKind
- fhir::BaseTyKind
- fhir::BinOp
- fhir::CheckOverflow
- fhir::ConstArgKind
- fhir::Ensures
- fhir::ExprKind
- fhir::ExprRes
- fhir::FluxItem
- fhir::FluxLocalDefId
- fhir::FluxOwnerId
- fhir::GenericArg
- fhir::GenericBound
- fhir::GenericParamKind
- fhir::Ignored
- fhir::ImplItemKind
- fhir::InferMode
- fhir::ItemKind
- fhir::Lifetime
- fhir::Lit
- fhir::Mutability
- fhir::Node
- fhir::OwnerNode
- fhir::ParamKind
- fhir::PrimSort
- fhir::PrimTy
- fhir::QPath
- fhir::Res
- fhir::Sort
- fhir::SortRes
- fhir::SpecFuncKind
- fhir::StructKind
- fhir::TraitBoundModifier
- fhir::TraitItemKind
- fhir::Trusted
- fhir::TyKind
- fhir::UnOp
- pretty::KVarArgs
- queries::QueryErr
- rty::AggregateKind
- rty::AliasKind
- rty::BaseTy
- rty::BinOp
- rty::BoundReftKind
- rty::BoundRegionKind
- rty::BoundVariableKind
- rty::BvSize
- rty::ClauseKind
- rty::ClosureKind
- rty::Coercion
- rty::ConstKind
- rty::Constant
- rty::ConstantInfo
- rty::Ensures
- rty::ExistentialPredicate
- rty::ExprKind
- rty::FieldProj
- rty::FloatTy
- rty::GenericArg
- rty::GenericParamDefKind
- rty::HoleKind
- rty::IntTy
- rty::Loc
- rty::Mutability
- rty::NumVarValue
- rty::Opaqueness
- rty::PtrKind
- rty::Region
- rty::Sort
- rty::SortArg
- rty::SortCtor
- rty::SortInfer
- rty::SortParamKind
- rty::TyKind
- rty::TyOrBase
- rty::TyOrCtor
- rty::UintTy
- rty::UnOp
- rty::Var
- rty::binder::BoundReftKind
- rty::binder::BoundVariableKind
- rty::canonicalize::CanonicalTy
- rty::evars::EVarState
- rty::expr::AggregateKind
- rty::expr::BinOp
- rty::expr::Constant
- rty::expr::ExprKind
- rty::expr::FieldProj
- rty::expr::HoleKind
- rty::expr::Loc
- rty::expr::UnOp
- rty::expr::Var
- rty::expr::pretty::Precedence
- rty::projections::Candidate
Traits
- PlaceExt
- cstore::CrateStore
- fhir::visit::Visitor
- pretty::FromOpt
- pretty::Pretty
- pretty::PrettyNested
- rty::GenericArgsExt
- rty::RefineArgsExt
- rty::canonicalize::HoisterDelegate
- rty::fold::FallibleTypeFolder
- rty::fold::TypeFoldable
- rty::fold::TypeFolder
- rty::fold::TypeSuperFoldable
- rty::fold::TypeSuperVisitable
- rty::fold::TypeVisitable
- rty::fold::TypeVisitor
- rty::subst::BoundVarReplacerDelegate
- rty::subst::GenericsSubstDelegate
- rty::subst::SortSubstDelegate
Macros
- _Bool
- _Int
- _Ref
- _Uint
- _format_args_cx
- _format_cx
- _impl_debug_with_default_cx
- _join
- _parens
- _w
- _with_cx
- pretty::format_args_cx
- pretty::format_cx
- pretty::impl_debug_with_default_cx
- pretty::join
- pretty::parens
- pretty::set_opts
- pretty::w
- pretty::with_cx
- queries::empty_query
- query_bug
- rty::Bool
- rty::Int
- rty::Ref
- rty::Uint
- rty::expr::impl_ops
- rty::fold::TrivialTypeTraversalImpls
- try_alloc_slice
- walk_list
Functions
- def_id_to_string
- fhir::visit::walk_alias_reft
- fhir::visit::walk_assoc_item_constraint
- fhir::visit::walk_bty
- fhir::visit::walk_ensures
- fhir::visit::walk_enum_def
- fhir::visit::walk_expr
- fhir::visit::walk_field_def
- fhir::visit::walk_field_expr
- fhir::visit::walk_fn_decl
- fhir::visit::walk_fn_output
- fhir::visit::walk_fn_sig
- fhir::visit::walk_func_sort
- fhir::visit::walk_generic_arg
- fhir::visit::walk_generic_bound
- fhir::visit::walk_generics
- fhir::visit::walk_impl
- fhir::visit::walk_impl_assoc_reft
- fhir::visit::walk_impl_item
- fhir::visit::walk_item
- fhir::visit::walk_node
- fhir::visit::walk_opaque_ty
- fhir::visit::walk_path
- fhir::visit::walk_path_segment
- fhir::visit::walk_poly_func_sort
- fhir::visit::walk_poly_trait_ref
- fhir::visit::walk_qpath
- fhir::visit::walk_refine_param
- fhir::visit::walk_requires
- fhir::visit::walk_sort
- fhir::visit::walk_sort_path
- fhir::visit::walk_struct_def
- fhir::visit::walk_trait_assoc_reft
- fhir::visit::walk_trait_item
- fhir::visit::walk_ty
- fhir::visit::walk_ty_alias
- fhir::visit::walk_variant
- fhir::visit::walk_variant_ret
- fhir::visit::walk_where_predicate
- pretty::debug_nested
- pretty::float_children
- pretty::pprint_with_default_cx
- queries::dispatch_query
- queries::run_with_cache
- rty::expr::pretty::aggregate_nested
- rty::expr::pretty::should_parenthesize
- rty::int_invariants
- rty::pretty::fmt_alias_ty
- rty::pretty::nested_with_bound_vars
- rty::projections::assemble_candidates_from_predicates
- rty::refining::refine_bound_variables
- rty::refining::refine_default
- rty::refining::refine_generic_param_def_kind
- rty::refining::refine_generics
- rty::region_matching::replace_regions_with_unique_vars
- rty::region_matching::rty_match_regions
- rty::region_matching::ty_match_regions
- rty::slice_invariants
- rty::uint_invariants
Type Aliases
- cstore::CrateStoreDyn
- cstore::OptResult
- fhir::Arena
- fhir::GenericBounds
- fhir::SortDecls
- fhir::lift::Result
- queries::Cache
- queries::QueryResult
- rty::BoundVariableKinds
- rty::Clauses
- rty::GenericArgs
- rty::ItemLocalMap
- rty::List
- rty::PolyExistentialPredicate
- rty::PolyExistentialTraitRef
- rty::PolyFnSig
- rty::PolyProjectionPredicate
- rty::PolyTraitPredicate
- rty::PolyTraitRef
- rty::PolyVariant
- rty::PolyVariants
- rty::RefineArgs
- rty::SubsetTyCtor
- rty::TyCtor
- rty::TypeOutlivesPredicate
- rty::binder::BoundVariableKinds
- rty::binder::List
Statics
Constants
flux_middle - Rust Expand description
This crate contains common type definitions that are used by other crates.
Modules§
- Flux High-Level Intermediate Representation
- Defines how flux represents refinement types internally. Definitions in this module are used during refinement type checking. A couple of important differences between definitions in this -module and in
crate::fhirare: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefIdand aDefId+module and incrate::fhirare: - sort_of 🔒
Macros§
Structs§
Enums§
- Represents errors that can occur when inserting a mapping between a
LocalDefIdand aDefIdfor an extern spec. - This enum serves as a type-level reminder that a local definition may be a wrapper for an extern spec. This abstraction is not infallible, so one should be careful and decide in each situation whether to use the local id or the resolved id.
- Normally, a
DefIdis either local or external, andDefId::as_localcan be used to diff --git a/doc/flux_middle/macro._define_scoped!.html b/doc/flux_middle/macro._define_scoped!.html deleted file mode 100644 index c63ebc6ad3..0000000000 --- a/doc/flux_middle/macro._define_scoped!.html +++ /dev/null @@ -1,11 +0,0 @@ - - - - -Redirection - - -Redirecting to macro._define_scoped.html...
- - - \ No newline at end of file diff --git a/doc/flux_middle/macro._define_scoped.html b/doc/flux_middle/macro._define_scoped.html deleted file mode 100644 index ee55233dc3..0000000000 --- a/doc/flux_middle/macro._define_scoped.html +++ /dev/null @@ -1,3 +0,0 @@ -_define_scoped in flux_middle - Rust macro_rules! _define_scoped { - ($cx:ident, $fmt:expr) => { ... }; -}
_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx { - ($fmt:literal, $($args:tt)*) => { ... }; - ($fmt:literal) => { ... }; - (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... }; +
_format_args_cx in flux_middle - Rust macro_rules! _format_args_cx { + ($cx:expr, $fmt:literal, $($args:tt)*) => { ... }; + ($cx:expr, $fmt:literal) => { ... }; + (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... }; (@as_expr $e:expr) => { ... }; }
_format_cx in flux_middle - Rust macro_rules! _format_cx { +
_format_cx in flux_middle - Rust macro_rules! _format_cx { ($($arg:tt)*) => { ... }; }
_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx { +
_impl_debug_with_default_cx in flux_middle - Rust macro_rules! _impl_debug_with_default_cx { ($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... }; }
_join in flux_middle - Rust macro_rules! _join { +
_join in flux_middle - Rust macro_rules! _join { ($sep:expr, $iter:expr) => { ... }; }
_parens in flux_middle - Rust macro_rules! _parens { +
_parens in flux_middle - Rust macro_rules! _parens { ($val:expr, $parenthesize:expr) => { ... }; }
_w in flux_middle - Rust macro_rules! _w { - ($fmt:literal, $($args:tt)*) => { ... }; - ($f:expr, $fmt:literal, $($args:tt)*) => { ... }; - ($f:expr, $fmt:literal) => { ... }; - ($fmt:literal) => { ... }; +
_w in flux_middle - Rust macro_rules! _w { + ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... }; + ($cx:expr, $f:expr, $fmt:literal) => { ... }; }
_with_cx in flux_middle - Rust macro_rules! _with_cx { - ($e:expr) => { ... }; +
_with_cx in flux_middle - Rust macro_rules! _with_cx { + ($cx:expr, $e:expr) => { ... }; }
KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs { +KVarArgs in flux_middle::pretty - Rust pub enum KVarArgs { All, SelfOnly, Hide, -}Variants§
Trait Implementations§
Auto Trait Implementations§
§ impl Freeze for KVarArgs
§ impl RefUnwindSafe for KVarArgs
§ impl Send for KVarArgs
§ impl Sync for KVarArgs
§ impl Unpin for KVarArgs
§ impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§ impl<T> Any for T
where +}Variants§
Trait Implementations§
Auto Trait Implementations§
§ impl Freeze for KVarArgs
§ impl RefUnwindSafe for KVarArgs
§ impl Send for KVarArgs
§ impl Sync for KVarArgs
§ impl Unpin for KVarArgs
§ impl UnwindSafe for KVarArgs
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> CloneToUninit for T
where diff --git a/doc/flux_middle/pretty/fn.debug_nested.html b/doc/flux_middle/pretty/fn.debug_nested.html index bcf604c0a7..fe85616140 100644 --- a/doc/flux_middle/pretty/fn.debug_nested.html +++ b/doc/flux_middle/pretty/fn.debug_nested.html @@ -1,4 +1,4 @@ -debug_nested in flux_middle::pretty - Rust pub fn debug_nested<T: Pretty>( +debug_nested in flux_middle::pretty - Rust \ No newline at end of file diff --git a/doc/flux_middle/pretty/fn.float_children.html b/doc/flux_middle/pretty/fn.float_children.html index 1e96513b8d..2afd362823 100644 --- a/doc/flux_middle/pretty/fn.float_children.html +++ b/doc/flux_middle/pretty/fn.float_children.html @@ -1,3 +1,3 @@ - float_children in flux_middle::pretty - Rust pub fn float_children( +float_children in flux_middle::pretty - Rust pub fn float_children( children: Vec<Option<Vec<NestedString>>>, ) -> Option<Vec<NestedString>>pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>( +pprint_with_default_cx in flux_middle::pretty - Rust pub fn pprint_with_default_cx<T: Pretty>( f: &mut Formatter<'_>, t: &T, cfg_key: Option<&'static str>, diff --git a/doc/flux_middle/pretty/index.html b/doc/flux_middle/pretty/index.html index 09c8258f22..05b9339fec 100644 --- a/doc/flux_middle/pretty/index.html +++ b/doc/flux_middle/pretty/index.html @@ -1 +1 @@ -flux_middle::pretty - Rust \ No newline at end of file + flux_middle::pretty - Rust \ No newline at end of file diff --git a/doc/flux_middle/pretty/macro.define_scoped!.html b/doc/flux_middle/pretty/macro.define_scoped!.html deleted file mode 100644 index 3a341d3519..0000000000 --- a/doc/flux_middle/pretty/macro.define_scoped!.html +++ /dev/null @@ -1,11 +0,0 @@ - - - - - Redirection - - -Redirecting to macro.define_scoped.html...
- - - \ No newline at end of file diff --git a/doc/flux_middle/pretty/macro.define_scoped.html b/doc/flux_middle/pretty/macro.define_scoped.html deleted file mode 100644 index 2b1e8cc432..0000000000 --- a/doc/flux_middle/pretty/macro.define_scoped.html +++ /dev/null @@ -1,3 +0,0 @@ -define_scoped in flux_middle::pretty - Rust macro_rules! define_scoped { - ($cx:ident, $fmt:expr) => { ... }; -}
format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx { - ($fmt:literal, $($args:tt)*) => { ... }; - ($fmt:literal) => { ... }; - (@go ($fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... }; - (@go ($fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... }; +
format_args_cx in flux_middle::pretty - Rust macro_rules! format_args_cx { + ($cx:expr, $fmt:literal, $($args:tt)*) => { ... }; + ($cx:expr, $fmt:literal) => { ... }; + (@go ($cx:ident, $fmt:literal; ^$head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; $head:expr, $($tail:tt)*) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; ^$head:expr) -> ($($accum:tt)*)) => { ... }; + (@go ($cx:ident, $fmt:literal; $head:expr) -> ($($accum:tt)*)) => { ... }; (@as_expr $e:expr) => { ... }; }
format_cx in flux_middle::pretty - Rust macro_rules! format_cx { +
format_cx in flux_middle::pretty - Rust macro_rules! format_cx { ($($arg:tt)*) => { ... }; }
impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx { +
impl_debug_with_default_cx in flux_middle::pretty - Rust macro_rules! impl_debug_with_default_cx { ($($ty:ty $(=> $key:literal)?),* $(,)?) => { ... }; }
join in flux_middle::pretty - Rust macro_rules! join { +
join in flux_middle::pretty - Rust macro_rules! join { ($sep:expr, $iter:expr) => { ... }; }
parens in flux_middle::pretty - Rust macro_rules! parens { +
parens in flux_middle::pretty - Rust macro_rules! parens { ($val:expr, $parenthesize:expr) => { ... }; }
set_opts in flux_middle::pretty - Rust macro_rules! set_opts { +
set_opts in flux_middle::pretty - Rust macro_rules! set_opts { ($cx:expr, $opts:expr, [$($opt:ident),+ $(,)?]) => { ... }; }
w in flux_middle::pretty - Rust macro_rules! w { - ($fmt:literal, $($args:tt)*) => { ... }; - ($f:expr, $fmt:literal, $($args:tt)*) => { ... }; - ($f:expr, $fmt:literal) => { ... }; - ($fmt:literal) => { ... }; +
w in flux_middle::pretty - Rust macro_rules! w { + ($cx:expr, $f:expr, $fmt:literal, $($args:tt)*) => { ... }; + ($cx:expr, $f:expr, $fmt:literal) => { ... }; }
with_cx in flux_middle::pretty - Rust macro_rules! with_cx { - ($e:expr) => { ... }; +
with_cx in flux_middle::pretty - Rust macro_rules! with_cx { + ($cx:expr, $e:expr) => { ... }; }
BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv { +BoundVarEnv in flux_middle::pretty - Rust struct BoundVarEnv { name_gen: IndexGen<BoundVarName>, - layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>, -}Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<FxHashMap<BoundVar, BoundVarName>>>Implementations§
Source§ impl BoundVarEnv
Source fn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Source fn push_layer(&self, vars: &[BoundVariableKind])
Source fn pop_layer(&self)
Trait Implementations§
Source§ impl Default for BoundVarEnv
Source§ fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§ impl !Freeze for BoundVarEnv
§ impl !RefUnwindSafe for BoundVarEnv
§ impl Send for BoundVarEnv
§ impl !Sync for BoundVarEnv
§ impl Unpin for BoundVarEnv
§ impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§ impl<T> Any for T
where + layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>, +}Fields§
§name_gen: IndexGen<BoundVarName>§layers: RefCell<Vec<UnordMap<BoundVar, BoundVarName>>>Implementations§
Source§ impl BoundVarEnv
Source fn lookup(&self, debruijn: DebruijnIndex, var: BoundVar) -> Option<BoundVarName>
Source fn push_layer(&self, vars: &[BoundVariableKind])
Source fn pop_layer(&self)
Trait Implementations§
Source§ impl Default for BoundVarEnv
Source§ fn default() -> BoundVarEnv
Returns the “default value” for a type. Read moreAuto Trait Implementations§
§ impl !Freeze for BoundVarEnv
§ impl !RefUnwindSafe for BoundVarEnv
§ impl Send for BoundVarEnv
§ impl !Sync for BoundVarEnv
§ impl Unpin for BoundVarEnv
§ impl UnwindSafe for BoundVarEnv
Blanket Implementations§
Source§ impl<T> BorrowMut<T> for T
where T: ?Sized,Source§ fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read moreSource§ impl<T> From<T> for T
Source§ fn from(t: T) -> T
Returns the argument unchanged.
diff --git a/doc/flux_middle/pretty/struct.BoundVarName.html b/doc/flux_middle/pretty/struct.BoundVarName.html index 2d5ebc3f89..d9a442b370 100644 --- a/doc/flux_middle/pretty/struct.BoundVarName.html +++ b/doc/flux_middle/pretty/struct.BoundVarName.html @@ -1,30 +1,30 @@ -BoundVarName in flux_middle::pretty - Rust struct BoundVarName { +BoundVarName in flux_middle::pretty - Rust