diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs
index a0fa4c9ab2..e9b1516c74 100644
--- a/crates/flux-fhir-analysis/src/conv/mod.rs
+++ b/crates/flux-fhir-analysis/src/conv/mod.rs
@@ -20,7 +20,7 @@ use flux_middle::{
rty::{
self,
fold::TypeFoldable,
- refining::{self, Refiner},
+ refining::{self, Refine, Refiner},
ESpan, List, RefineArgsExt, WfckResults, INNERMOST,
},
MaybeExternId,
@@ -1347,12 +1347,10 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt
{
))?
};
- let trait_ref = {
- let trait_ref = trait_ref
- .lower(tcx)
- .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?;
- self.refiner()?.refine_trait_ref(&trait_ref)?
- };
+ let trait_ref = trait_ref
+ .lower(tcx)
+ .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
+ .refine(&self.refiner()?)?;
let assoc_item = self
.trait_defines_associated_item_named(trait_ref.def_id, AssocKind::Type, assoc_ident)
diff --git a/crates/flux-fhir-analysis/src/conv/struct_compat.rs b/crates/flux-fhir-analysis/src/conv/struct_compat.rs
index 809c5b09df..ac2fc9b38e 100644
--- a/crates/flux-fhir-analysis/src/conv/struct_compat.rs
+++ b/crates/flux-fhir-analysis/src/conv/struct_compat.rs
@@ -14,7 +14,7 @@ use flux_middle::{
rty::{
self,
fold::{TypeFoldable, TypeFolder, TypeSuperFoldable},
- refining::Refiner,
+ refining::{Refine as _, Refiner},
},
MaybeExternId,
};
@@ -30,7 +30,7 @@ pub(crate) fn type_alias(
def_id: MaybeExternId,
) -> QueryResult {
let rust_ty = genv.lower_type_of(def_id.resolved_id())?.skip_binder();
- let expected = Refiner::default_for_item(genv, def_id.resolved_id())?.refine_ty(&rust_ty)?;
+ let expected = rust_ty.refine(&Refiner::default_for_item(genv, def_id.resolved_id())?)?;
let mut zipper = Zipper::new(genv, def_id);
if zipper
@@ -54,8 +54,8 @@ pub(crate) fn fn_sig(
def_id: MaybeExternId,
) -> QueryResult {
let rust_fn_sig = genv.lower_fn_sig(def_id.resolved_id())?.skip_binder();
- let expected =
- Refiner::default_for_item(genv, def_id.resolved_id())?.refine_poly_fn_sig(&rust_fn_sig)?;
+
+ let expected = Refiner::default_for_item(genv, def_id.resolved_id())?.refine(&rust_fn_sig)?;
let mut zipper = Zipper::new(genv, def_id);
if let Err(err) = zipper.zip_poly_fn_sig(fn_sig, &expected) {
diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs
index 32e9ee66ae..fe25c326cb 100644
--- a/crates/flux-middle/src/global_env.rs
+++ b/crates/flux-middle/src/global_env.rs
@@ -20,7 +20,11 @@ use crate::{
cstore::CrateStoreDyn,
fhir::{self, VariantIdx},
queries::{Providers, Queries, QueryErr, QueryResult},
- rty::{self, normalize::SpecFuncDefns, refining::Refiner},
+ rty::{
+ self,
+ normalize::SpecFuncDefns,
+ refining::{Refine as _, Refiner},
+ },
MaybeExternId, ResolvedDefId,
};
@@ -232,8 +236,8 @@ impl<'genv, 'tcx> GlobalEnv<'genv, 'tcx> {
let trait_ref = trait_ref.skip_binder();
let trait_ref = trait_ref
.lower(self.tcx())
- .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?;
- let trait_ref = Refiner::default_for_item(self, impl_id)?.refine_trait_ref(&trait_ref)?;
+ .map_err(|err| QueryErr::unsupported(trait_ref.def_id, err.into_err()))?
+ .refine(&Refiner::default_for_item(self, impl_id)?)?;
Ok(Some(rty::EarlyBinder(trait_ref)))
}
diff --git a/crates/flux-middle/src/queries.rs b/crates/flux-middle/src/queries.rs
index 27d9587407..bbe2593fc8 100644
--- a/crates/flux-middle/src/queries.rs
+++ b/crates/flux-middle/src/queries.rs
@@ -25,7 +25,7 @@ use crate::{
global_env::GlobalEnv,
rty::{
self,
- refining::{self, Refiner},
+ refining::{self, Refine, Refiner},
},
MaybeExternId, ResolvedDefId,
};
@@ -526,10 +526,8 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
.item_bounds(def_id)
.skip_binder()
.lower(genv.tcx())
- .map_err(|err| QueryErr::unsupported(def_id, err))?;
-
- let clauses =
- Refiner::default_for_item(genv, def_id)?.refine_clauses(&clauses)?;
+ .map_err(|err| QueryErr::unsupported(def_id, err))?
+ .refine(&Refiner::default_for_item(genv, def_id)?)?;
Ok(rty::EarlyBinder(clauses))
},
@@ -549,9 +547,9 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
|def_id| (self.providers.predicates_of)(genv, def_id.local_id()),
|def_id| genv.cstore().predicates_of(def_id),
|def_id| {
- let predicates = genv.lower_predicates_of(def_id)?;
- let predicates = Refiner::default_for_item(genv, def_id)?
- .refine_generic_predicates(&predicates)?;
+ let predicates = genv
+ .lower_predicates_of(def_id)?
+ .refine(&Refiner::default_for_item(genv, def_id)?)?;
Ok(rty::EarlyBinder(predicates))
},
)
@@ -713,9 +711,10 @@ impl<'genv, 'tcx> Queries<'genv, 'tcx> {
|def_id| (self.providers.fn_sig)(genv, def_id.local_id()),
|def_id| genv.cstore().fn_sig(def_id),
|def_id| {
- let fn_sig = genv.lower_fn_sig(def_id)?.skip_binder();
- let fn_sig =
- Refiner::default_for_item(genv, def_id)?.refine_poly_fn_sig(&fn_sig)?;
+ let fn_sig = genv
+ .lower_fn_sig(def_id)?
+ .skip_binder()
+ .refine(&Refiner::default_for_item(genv, def_id)?)?;
Ok(rty::EarlyBinder(fn_sig))
},
)
diff --git a/crates/flux-middle/src/rty/mod.rs b/crates/flux-middle/src/rty/mod.rs
index 4754f7b1f0..7e8f142377 100644
--- a/crates/flux-middle/src/rty/mod.rs
+++ b/crates/flux-middle/src/rty/mod.rs
@@ -41,7 +41,7 @@ use flux_rustc_bridge::{
};
use itertools::Itertools;
pub use normalize::SpecFuncDefns;
-use refining::Refiner;
+use refining::{Refine as _, Refiner};
use rustc_data_structures::{fx::FxIndexMap, unord::UnordMap};
use rustc_hir::{def_id::DefId, LangItem, Safety};
use rustc_index::{newtype_index, IndexSlice};
@@ -1223,11 +1223,10 @@ impl Ty {
let def_id = genv.tcx().require_lang_item(LangItem::OwnedBox, None);
let generics = genv.generics_of(def_id)?;
- let alloc_ty = Refiner::default_for_item(genv, def_id)?.refine_ty(
- &genv
- .lower_type_of(generics.own_params[1].def_id)?
- .skip_binder(),
- )?;
+ let alloc_ty = genv
+ .lower_type_of(generics.own_params[1].def_id)?
+ .skip_binder()
+ .refine(&Refiner::default_for_item(genv, def_id)?)?;
Ty::mk_box(genv, deref_ty, alloc_ty)
}
diff --git a/crates/flux-middle/src/rty/refining.rs b/crates/flux-middle/src/rty/refining.rs
index 9504169665..ca9fb2a152 100644
--- a/crates/flux-middle/src/rty/refining.rs
+++ b/crates/flux-middle/src/rty/refining.rs
@@ -3,7 +3,7 @@
//! Concretely, this module provides functions to go from types in [`flux_rustc_bridge::ty`] to
//! types in [`rty`].
-use flux_arc_interner::List;
+use flux_arc_interner::{List, SliceInternable};
use flux_common::bug;
use flux_rustc_bridge::{ty, ty::GenericArgsExt as _};
use itertools::Itertools;
@@ -101,100 +101,11 @@ impl<'genv, 'tcx> Refiner<'genv, 'tcx> {
})
}
- pub(crate) fn refine_generic_predicates(
- &self,
- generics: &ty::GenericPredicates,
- ) -> QueryResult {
- Ok(rty::GenericPredicates {
- parent: generics.parent,
- predicates: self.refine_clauses(&generics.predicates)?,
- })
+ pub fn refine(&self, t: &T) -> QueryResult {
+ t.refine(self)
}
- pub(crate) fn refine_clauses(&self, clauses: &[ty::Clause]) -> QueryResult> {
- let clauses = clauses
- .iter()
- .flat_map(|clause| self.refine_clause(clause).transpose())
- .try_collect()?;
-
- Ok(clauses)
- }
-
- fn refine_clause(&self, clause: &ty::Clause) -> QueryResult