Skip to content

Commit

Permalink
Refactor gathering into its own module
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann committed Nov 5, 2023
1 parent dba7651 commit 6afcf3d
Showing 1 changed file with 2 additions and 304 deletions.
306 changes: 2 additions & 304 deletions crates/flux-desugar/src/desugar.rs
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
mod gather;

Check failure on line 1 in crates/flux-desugar/src/desugar.rs

View workflow job for this annotation

GitHub Actions / clippy

file not found for module `gather` 

error[E0583]: file not found for module `gather`
 --> crates/flux-desugar/src/desugar.rs:1:1
  |
1 | mod gather;
  | ^^^^^^^^^^^
  |
  = help: to create the module `gather`, create file "crates/flux-desugar/src/desugar/gather.rs" or "crates/flux-desugar/src/desugar/gather/mod.rs"

use std::{borrow::Borrow, iter};

use flux_common::{bug, index::IndexGen, iter::IterExt, span_bug};
Expand Down Expand Up @@ -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 } = &param.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<surface::Ident>,
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,
Expand Down Expand Up @@ -1602,14 +1335,6 @@ impl Binders {
}
}

impl<T: Borrow<surface::Ident>> std::ops::Index<T> 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,
Expand Down Expand Up @@ -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<fhir::Sort> {
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;
Expand All @@ -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,
Expand Down

0 comments on commit 6afcf3d

Please sign in to comment.