From 6afcf3daee995fbf2f0e6ef50f10d37859ea3c40 Mon Sep 17 00:00:00 2001 From: Nico Lehmann Date: Sun, 5 Nov 2023 14:01:28 -0800 Subject: [PATCH] Refactor gathering into its own module --- crates/flux-desugar/src/desugar.rs | 306 +---------------------------- 1 file changed, 2 insertions(+), 304 deletions(-) diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 3f158e1847..c4c09dabb9 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -1,3 +1,5 @@ +mod gather; + use std::{borrow::Borrow, iter}; use flux_common::{bug, index::IndexGen, iter::IterExt, span_bug}; @@ -1134,275 +1136,6 @@ impl<'a, 'tcx> ExprCtxt<'a, 'tcx> { } } -impl DesugarCtxt<'_, '_> { - fn gather_params_variant( - &self, - variant_def: &surface::VariantDef, - binders: &mut Binders, - ) -> Result { - for ty in &variant_def.fields { - self.gather_params_ty(None, ty, TypePos::Input, binders)?; - } - // Traverse `VariantRet` to find illegal binders and report invalid refinement errors. - self.gather_params_variant_ret(&variant_def.ret, binders)?; - - // Check binders in `VariantRet` - variant_def - .ret - .indices - .indices - .iter() - .try_for_each_exhaust(|idx| { - if let surface::RefineArg::Bind(_, kind, span) = idx { - Err(self.emit_err(errors::IllegalBinder::new(*span, *kind))) - } else { - Ok(()) - } - }) - } - - fn gather_params_variant_ret( - &self, - ret: &surface::VariantRet, - binders: &mut Binders, - ) -> Result { - self.gather_params_path(&ret.path, TypePos::Other, binders)?; - let Some(sort) = sort_of_surface_path(self.genv, self.resolver_output, &ret.path) else { - return Err(self.emit_err(errors::RefinedUnrefinableType::new(ret.path.span))); - }; - self.gather_params_indices(sort, &ret.indices, TypePos::Other, binders) - } - - fn gather_params_predicates( - &self, - predicates: &[surface::WhereBoundPredicate], - binders: &mut Binders, - ) -> Result { - for predicate in predicates { - self.gather_params_ty(None, &predicate.bounded_ty, TypePos::Other, binders)?; - for bound in &predicate.bounds { - self.gather_params_path(&bound.path, TypePos::Other, binders)?; - } - } - Ok(()) - } - - fn gather_input_params_fn_sig(&self, fn_sig: &surface::FnSig, binders: &mut Binders) -> Result { - let generics = self.genv.tcx.generics_of(self.owner.def_id); - let sr = - SortResolver::with_generics(self.genv.sess, self.genv.map().sort_decls(), generics); - for param in fn_sig.generics.iter().flat_map(|g| &g.params) { - let surface::GenericParamKind::Refine { sort } = ¶m.kind else { continue }; - binders.insert_binder( - self.genv.sess, - param.name, - Binder::Refined(binders.fresh(), sr.resolve_sort(sort)?, false), - )?; - } - for arg in &fn_sig.args { - self.gather_params_fun_arg(arg, binders)?; - } - - Ok(()) - } - - fn gather_output_params_fn_sig( - &self, - fn_sig: &surface::FnSig, - binders: &mut Binders, - ) -> Result { - if let surface::FnRetTy::Ty(ty) = &fn_sig.returns { - self.gather_params_ty(None, ty, TypePos::Output, binders)?; - } - for cstr in &fn_sig.ensures { - if let surface::Constraint::Type(_, ty) = cstr { - self.gather_params_ty(None, ty, TypePos::Output, binders)?; - }; - } - Ok(()) - } - - fn gather_params_fun_arg(&self, arg: &surface::Arg, binders: &mut Binders) -> Result { - match arg { - surface::Arg::Constr(bind, path, _) => { - let zz = sort_of_surface_path(self.genv, self.resolver_output, path); - let Some(sort) = zz else { - return Err(self.emit_err(errors::RefinedUnrefinableType::new(path.span))); - }; - - binders.insert_binder(self.genv.sess, *bind, binders.binder_from_sort(sort))?; - } - surface::Arg::StrgRef(loc, ty) => { - binders.insert_binder( - self.genv.sess, - *loc, - Binder::Refined(binders.fresh(), fhir::Sort::Loc, false), - )?; - self.gather_params_ty(None, ty, TypePos::Input, binders)?; - } - surface::Arg::Ty(bind, ty) => { - self.gather_params_ty(*bind, ty, TypePos::Input, binders)?; - } - } - Ok(()) - } - - fn gather_params_ty( - &self, - bind: Option, - ty: &surface::Ty, - pos: TypePos, - binders: &mut Binders, - ) -> Result { - match &ty.kind { - surface::TyKind::Indexed { bty, indices } => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - let Some(sort) = index_sort(self.genv, self.resolver_output, bty) else { - return Err(self.emit_err(errors::RefinedUnrefinableType::new(ty.span))); - }; - self.gather_params_indices(sort, indices, pos, binders)?; - self.gather_params_bty(bty, pos, binders) - } - surface::TyKind::Base(bty) => { - if let Some(bind) = bind { - binders.insert_binder( - self.genv.sess, - bind, - binders.binder_from_bty(self.genv, self.resolver_output, bty), - )?; - } - self.gather_params_bty(bty, pos, binders) - } - - surface::TyKind::Ref(_, ty) | surface::TyKind::Constr(_, ty) => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - self.gather_params_ty(None, ty, pos, binders) - } - surface::TyKind::Tuple(tys) => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - for ty in tys { - self.gather_params_ty(None, ty, pos, binders)?; - } - Ok(()) - } - surface::TyKind::Array(ty, _) => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - self.gather_params_ty(None, ty, TypePos::Other, binders) - } - surface::TyKind::Exists { bty, .. } => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - self.gather_params_bty(bty, pos, binders) - } - surface::TyKind::GeneralExists { ty, .. } => { - if let Some(bind) = bind { - binders.insert_binder(self.genv.sess, bind, Binder::Unrefined)?; - } - // Declaring parameters with @ inside and existential has weird behavior if names - // are being shadowed. Thus, we don't allow it to keep things simple. We could eventually - // allow it if we resolve the weird behavior by detecting shadowing. - self.gather_params_ty(None, ty, TypePos::Other, binders) - } - surface::TyKind::ImplTrait(_, bounds) => { - for bound in bounds { - self.gather_params_path(&bound.path, TypePos::Other, binders)?; - } - Ok(()) - } - } - } - - fn gather_params_indices( - &self, - sort: fhir::Sort, - indices: &surface::Indices, - pos: TypePos, - binders: &mut Binders, - ) -> Result { - if let [surface::RefineArg::Bind(ident, kind, span)] = indices.indices[..] { - if !pos.is_binder_allowed(kind) { - return Err(self.emit_err(errors::IllegalBinder::new(span, kind))); - } - binders.insert_binder(self.genv.sess, ident, binders.binder_from_sort(sort))?; - } else { - let sorts = as_tuple(self.genv, &sort); - if sorts.len() != indices.indices.len() { - return Err(self.emit_err(errors::RefineArgCountMismatch::new( - indices.span, - sorts.len(), - indices.indices.len(), - ))); - } - - for (idx, sort) in iter::zip(&indices.indices, sorts) { - if let surface::RefineArg::Bind(ident, kind, span) = idx { - if !pos.is_binder_allowed(*kind) { - return Err(self.emit_err(errors::IllegalBinder::new(*span, *kind))); - } - binders.insert_binder( - self.genv.sess, - *ident, - binders.binder_from_sort(sort.clone()), - )?; - } - } - } - Ok(()) - } - - fn gather_params_path( - &self, - path: &surface::Path, - pos: TypePos, - binders: &mut Binders, - ) -> Result { - // CODESYNC(type-holes, 3) - if path.is_hole() { - return Ok(()); - } - let res = self.resolver_output.path_res_map[&path.node_id]; - let pos = if self.genv.is_box(res) { pos } else { TypePos::Other }; - path.generics - .iter() - .try_for_each_exhaust(|arg| self.gather_params_generic_arg(arg, pos, binders)) - } - - fn gather_params_generic_arg( - &self, - arg: &surface::GenericArg, - pos: TypePos, - binders: &mut Binders, - ) -> Result { - match arg { - surface::GenericArg::Type(ty) => self.gather_params_ty(None, ty, pos, binders), - surface::GenericArg::Constraint(_, ty) => self.gather_params_ty(None, ty, pos, binders), - } - } - - fn gather_params_bty( - &self, - bty: &surface::BaseTy, - pos: TypePos, - binders: &mut Binders, - ) -> Result { - match &bty.kind { - surface::BaseTyKind::Path(path) => self.gather_params_path(path, pos, binders), - surface::BaseTyKind::Slice(ty) => { - self.gather_params_ty(None, ty, TypePos::Other, binders) - } - } - } -} - struct SortResolver<'a> { sess: &'a FluxSession, sort_decls: &'a fhir::SortDecls, @@ -1602,14 +1335,6 @@ impl Binders { } } -impl> std::ops::Index for Binders { - type Output = Binder; - - fn index(&self, index: T) -> &Self::Output { - self.get(index).unwrap() - } -} - fn desugar_bin_op(op: surface::BinOp) -> fhir::BinOp { match op { surface::BinOp::Iff => fhir::BinOp::Iff, @@ -1750,13 +1475,6 @@ fn sort_of_surface_path( fhir::Res::Def(..) => bug!("unexpected res {res:?}"), } } -fn as_tuple<'a>(genv: &'a GlobalEnv, sort: &'a fhir::Sort) -> Vec { - if let fhir::Sort::Record(def_id, sort_args) = sort { - genv.index_sorts_of(*def_id, sort_args) - } else { - vec![sort.clone()] - } -} trait DesugarContext<'a, 'tcx> { fn next_fhir_id(&self) -> FhirId; @@ -1774,26 +1492,6 @@ impl<'a, 'tcx> DesugarContext<'a, 'tcx> for ExprCtxt<'a, 'tcx> { } } -#[derive(Clone, Copy)] -enum TypePos { - /// Type in input position allowing `@n` binders - Input, - /// Type in output position allowing `#n` binders - Output, - /// Any other position which doesn't allow binders, e.g., inside generic arguments (except for boxes) - Other, -} - -impl TypePos { - fn is_binder_allowed(self, kind: surface::BindKind) -> bool { - match self { - TypePos::Input => matches!(kind, surface::BindKind::At), - TypePos::Output => matches!(kind, surface::BindKind::Pound), - TypePos::Other => false, - } - } -} - struct Sorts { int: Symbol, real: Symbol,