diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 01d80a53f7..783668b5da 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -33,7 +33,11 @@ pub fn desugar_qualifier( genv: &GlobalEnv, qualifier: &surface::Qualifier, ) -> Result { - let mut binders = Binders::from_params(genv, &[], &qualifier.args)?; + let sort_params = &[]; + let sort_resolver = + SortResolver::with_sort_params(genv.sess, genv.map().sort_decls(), sort_params); + + let mut binders = Binders::from_params(genv, &sort_resolver, &qualifier.args)?; let index_gen = IndexGen::new(); let cx = ExprCtxt::new(genv, FluxOwnerId::Flux(qualifier.name.name), &index_gen); let expr = cx.desugar_expr(&binders, &qualifier.expr); @@ -49,14 +53,15 @@ pub fn desugar_qualifier( pub fn desugar_defn(genv: &GlobalEnv, defn: surface::FuncDef) -> Result> { if let Some(body) = defn.body { let sort_params = &defn.sort_vars[..]; - let mut binders = Binders::from_params(genv, sort_params, &defn.args)?; + let sort_resolver = + SortResolver::with_sort_params(genv.sess, genv.map().sort_decls(), sort_params); + let mut binders = Binders::from_params(genv, &sort_resolver, &defn.args)?; let local_id_gen = IndexGen::new(); let cx = ExprCtxt::new(genv, FluxOwnerId::Flux(defn.name.name), &local_id_gen); let expr = cx.desugar_expr(&binders, &body)?; let name = defn.name.name; let params = defn.sort_vars.len(); - let sort = SortResolver::with_sort_params(genv.sess, genv.map().sort_decls(), sort_params) - .resolve_sort(&defn.output)?; + let sort = sort_resolver.resolve_sort(&defn.output)?; let args = binders.pop_layer().into_params(&cx); Ok(Some(fhir::Defn { name, params, args, sort, expr })) } else { @@ -200,24 +205,9 @@ impl<'a, 'tcx> DesugarCtxt<'a, 'tcx> { pub(crate) fn desugar_generics(&self, generics: &surface::Generics) -> Result { let hir_generics = self.genv.hir().get_generics(self.owner.def_id).unwrap(); - let hir_generic_params = hir_generics.params.iter(); - // let parent_generic_params = self - // .genv - // .tcx - // .opt_local_parent(self.owner.def_id) - // .map(|parent_def_id| { - // self.genv - // .hir() - // .get_generics(parent_def_id) - // .unwrap() - // .params - // .iter() - // }) - // .into_iter() - // .flatten(); - - let generics_map: FxHashMap<_, _> = hir_generic_params - // .chain(parent_generic_params) + let generics_map: FxHashMap<_, _> = hir_generics + .params + .iter() .flat_map(|param| { if let hir::ParamName::Plain(name) = param.name { Some((name, param.def_id)) @@ -1475,12 +1465,12 @@ impl Binders { fn from_params<'a>( genv: &GlobalEnv, - sort_params: &[surface::Ident], + sort_resolver: &SortResolver, params: impl IntoIterator, ) -> Result { let mut binders = Self::new(); binders.push_layer(); - binders.insert_params_with_sort_params(genv, sort_params, params)?; + binders.insert_params(genv, sort_resolver, params)?; Ok(binders) } @@ -1502,18 +1492,18 @@ impl Binders { Ok(()) } - fn insert_params_with_sort_params<'a>( + fn insert_params<'a>( &mut self, genv: &GlobalEnv, - sort_params: &[surface::Ident], + sort_resolver: &SortResolver, params: impl IntoIterator, ) -> Result { - let sr = SortResolver::with_sort_params(genv.sess, genv.map().sort_decls(), sort_params); + // let sr = SortResolver::with_sort_params(genv.sess, genv.map().sort_decls(), sort_params); for param in params { self.insert_binder( genv.sess, param.name, - Binder::Refined(self.fresh(), sr.resolve_sort(¶m.sort)?, false), + Binder::Refined(self.fresh(), sort_resolver.resolve_sort(¶m.sort)?, false), )?; } Ok(()) diff --git a/crates/flux-desugar/src/lib.rs b/crates/flux-desugar/src/lib.rs index f701dcde19..97c77b8a66 100644 --- a/crates/flux-desugar/src/lib.rs +++ b/crates/flux-desugar/src/lib.rs @@ -1,6 +1,6 @@ //! Desugaring from types in [`flux_syntax::surface`] to types in [`flux_middle::fhir`] //! -//! # [NOTE:Generics-and-Desugaring] +//! # Generics-and-Desugaring //! //! Desugaring requires knowing the sort of each type so we can correctly resolve binders declared with //! @ syntax or arg syntax. In particular, to know the sort of a type parameter we need to know its @@ -56,7 +56,7 @@ pub fn desugar_struct_def( let (generics, predicates) = cx.as_lift_cx().lift_generics_with_predicates()?; genv.map().insert_generics(def_id, generics); - // Desugar of struct_def needs to happen AFTER inserting generics. See [NOTE:Generics-and-Desugaring] + // Desugar of struct_def needs to happen AFTER inserting generics. See #generics-and-desugaring let struct_def = cx.desugar_struct_def(struct_def, &mut Binders::new())?; if config::dump_fhir() { dbg::dump_item_info(genv.tcx, owner_id, "fhir", &struct_def).unwrap(); @@ -173,8 +173,9 @@ pub fn desugar_fn_sig( } /// HACK(nilehmann) this is a bit of a hack. We use it to properly register generics and predicates -/// for items that don't have surface syntax (impl blocks, traits, ...). In this cases we just [lift] -/// them from hir. +/// for items that don't have surface syntax (impl blocks, traits, ...), or for `impl` blocks with +/// explicit `generics` annotations. In the former case, we use `desugar`; in the latter cases we +/// just [lift] them from hir. pub fn desugar_generics_and_predicates( genv: &mut GlobalEnv, owner_id: OwnerId, diff --git a/crates/flux-middle/src/global_env.rs b/crates/flux-middle/src/global_env.rs index 9ffbf75219..f44c431f27 100644 --- a/crates/flux-middle/src/global_env.rs +++ b/crates/flux-middle/src/global_env.rs @@ -240,34 +240,6 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> { } } - // pub fn sort_of_res(&self, res: fhir::Res) -> Option { - // // CODESYNC(sort-of, 4) sorts should be given consistently - // match res { - // fhir::Res::PrimTy(PrimTy::Int(_) | PrimTy::Uint(_)) => Some(fhir::Sort::Int), - // fhir::Res::PrimTy(PrimTy::Bool) => Some(fhir::Sort::Bool), - // fhir::Res::PrimTy(PrimTy::Float(..) | PrimTy::Str | PrimTy::Char) => { - // Some(fhir::Sort::Unit) - // } - // fhir::Res::Def(DefKind::TyAlias { .. } | DefKind::Enum | DefKind::Struct, def_id) => { - // Some(fhir::Sort::Record(def_id)) - // } - // fhir::Res::SelfTyAlias { alias_to, .. } => { - // let self_ty = self.tcx.type_of(alias_to).skip_binder(); - // self.sort_of_self_ty(self_ty) - // } - // fhir::Res::Def(DefKind::TyParam, def_id) => { - // let param = self.get_generic_param(def_id.expect_local()); - // match ¶m.kind { - // fhir::GenericParamKind::BaseTy => Some(fhir::Sort::Param(def_id)), - // fhir::GenericParamKind::Type { .. } | fhir::GenericParamKind::Lifetime => None, - // } - // } - // fhir::Res::Def(DefKind::AssocTy | DefKind::OpaqueTy, _) - // | fhir::Res::SelfTyParam { .. } => None, - // fhir::Res::Def(..) => bug!("unexpected res {res:?}"), - // } - // } - fn sort_of_ty(&self, ty: &fhir::Ty) -> Option { match &ty.kind { fhir::TyKind::BaseTy(bty) | fhir::TyKind::Indexed(bty, _) => { diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 0a7dab0000..939afe9b36 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -11,7 +11,7 @@ use lalrpop_util::ParseError; grammar(cx: &mut ParseCtxt<'_>); pub Generics: surface::Generics = { - "<" > ">" => { + > => { surface::Generics { params, span: cx.map_span(lo, hi), @@ -61,10 +61,6 @@ pub TyAlias: surface::TyAlias = { } } -SortParams: Vec = { - "<" > ">" => params, -} - pub RefinedBy: surface::RefinedBy = { > => surface::RefinedBy { index_params, @@ -150,7 +146,7 @@ pub FnSig: surface::FnSig = { "fn" - + ")?> "(" ")" " )?> @@ -166,6 +162,7 @@ pub FnSig: surface::FnSig = { } else { surface::FnRetTy::Default(cx.map_span(ret_lo, ret_hi)) }; + let generics = generics.map(|z| z.1); surface::FnSig { asyncness, generics, diff --git a/crates/flux-tests/tests/lib/rmap.rs b/crates/flux-tests/tests/lib/rmap.rs index c5979998c1..7dc175b203 100644 --- a/crates/flux-tests/tests/lib/rmap.rs +++ b/crates/flux-tests/tests/lib/rmap.rs @@ -14,7 +14,7 @@ pub struct RMap { inner: std::collections::HashMap, } -#[flux::generics()] +#[flux::generics(K as base, V as base)] impl RMap { #[flux::trusted] pub fn new() -> Self { diff --git a/crates/flux-tests/tests/lib/rmapk.rs b/crates/flux-tests/tests/lib/rmapk.rs index 2cd9c0e72a..0e142fa457 100644 --- a/crates/flux-tests/tests/lib/rmapk.rs +++ b/crates/flux-tests/tests/lib/rmapk.rs @@ -17,7 +17,7 @@ pub struct RMap { inner: std::collections::HashMap, } -#[flux::generics()] +#[flux::generics(K as base, V as base)] impl RMap { #[flux::trusted] #[flux::sig(fn() -> RMap{m: m.keys == set_empty(0)})] diff --git a/crates/flux-tests/tests/lib/rset.rs b/crates/flux-tests/tests/lib/rset.rs index 3aa8eeed5f..70a244e03d 100644 --- a/crates/flux-tests/tests/lib/rset.rs +++ b/crates/flux-tests/tests/lib/rset.rs @@ -8,7 +8,7 @@ pub struct RSet { pub inner: std::collections::HashSet, } -#[flux::generics()] +#[flux::generics(T as base)] impl RSet { #[flux::trusted] #[flux::sig(fn() -> RSet[set_empty(0)])]