Add Refine trait akin to ToRustc and Lower (#956)

flux-rs · Dec 18, 2024 · e7b94cc · e7b94cc
1 parent c48996e
commit e7b94cc
Show file tree

Hide file tree

Showing 7 changed files with 215 additions and 184 deletions.
diff --git 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<P> {
             ))?
         };
 
-        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
@@ -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<rty::TyCtor> {
     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<rty::PolyFnSig> {
     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
@@ -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
@@ -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
@@ -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)
     }