Skip to content

Commit

Permalink
simplify binders.insert_params
Browse files Browse the repository at this point in the history
  • Loading branch information
Ranjit Jhala committed Oct 24, 2023
1 parent 07b2e95 commit 672d1bb
Show file tree
Hide file tree
Showing 7 changed files with 29 additions and 69 deletions.
46 changes: 18 additions & 28 deletions crates/flux-desugar/src/desugar.rs
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,11 @@ pub fn desugar_qualifier(
genv: &GlobalEnv,
qualifier: &surface::Qualifier,
) -> Result<fhir::Qualifier> {
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);
Expand All @@ -49,14 +53,15 @@ pub fn desugar_qualifier(
pub fn desugar_defn(genv: &GlobalEnv, defn: surface::FuncDef) -> Result<Option<fhir::Defn>> {
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 {
Expand Down Expand Up @@ -200,24 +205,9 @@ impl<'a, 'tcx> DesugarCtxt<'a, 'tcx> {
pub(crate) fn desugar_generics(&self, generics: &surface::Generics) -> Result<fhir::Generics> {
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))
Expand Down Expand Up @@ -1475,12 +1465,12 @@ impl Binders {

fn from_params<'a>(
genv: &GlobalEnv,
sort_params: &[surface::Ident],
sort_resolver: &SortResolver,
params: impl IntoIterator<Item = &'a surface::RefineParam>,
) -> Result<Self> {
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)
}

Expand All @@ -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<Item = &'a surface::RefineParam>,
) -> 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(&param.sort)?, false),
Binder::Refined(self.fresh(), sort_resolver.resolve_sort(&param.sort)?, false),
)?;
}
Ok(())
Expand Down
9 changes: 5 additions & 4 deletions crates/flux-desugar/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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,
Expand Down
28 changes: 0 additions & 28 deletions crates/flux-middle/src/global_env.rs
Original file line number Diff line number Diff line change
Expand Up @@ -240,34 +240,6 @@ impl<'sess, 'tcx> GlobalEnv<'sess, 'tcx> {
}
}

// pub fn sort_of_res(&self, res: fhir::Res) -> Option<fhir::Sort> {
// // 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 &param.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<fhir::Sort> {
match &ty.kind {
fhir::TyKind::BaseTy(bty) | fhir::TyKind::Indexed(bty, _) => {
Expand Down
9 changes: 3 additions & 6 deletions crates/flux-syntax/src/grammar.lalrpop
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ use lalrpop_util::ParseError;
grammar(cx: &mut ParseCtxt<'_>);

pub Generics: surface::Generics = {
<lo:@L> "<" <params:Comma<GenericParam>> ">" <hi:@R> => {
<lo:@L> <params:Comma<GenericParam>> <hi:@R> => {
surface::Generics {
params,
span: cx.map_span(lo, hi),
Expand Down Expand Up @@ -61,10 +61,6 @@ pub TyAlias: surface::TyAlias = {
}
}

SortParams: Vec<Ident> = {
"<" <params:Comma<Ident>> ">" => params,
}

pub RefinedBy: surface::RefinedBy = {
<lo:@L> <index_params:RefineParams<"!">> <hi:@R> => surface::RefinedBy {
index_params,
Expand Down Expand Up @@ -150,7 +146,7 @@ pub FnSig: surface::FnSig = {
<lo:@L>
<asyncness:Async>
"fn"
<generics:Generics?>
<generics:("<" Generics ">")?>
"(" <args:Args> ")"
<ret_lo:@L> <ret_hi:@R>
<returns:("->" <Ty>)?>
Expand All @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-tests/tests/lib/rmap.rs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ pub struct RMap<K, V> {
inner: std::collections::HashMap<K, V>,
}

#[flux::generics(<K as base, V as base>)]
#[flux::generics(K as base, V as base)]
impl<K, V> RMap<K, V> {
#[flux::trusted]
pub fn new() -> Self {
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-tests/tests/lib/rmapk.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ pub struct RMap<K, V> {
inner: std::collections::HashMap<K, V>,
}

#[flux::generics(<K as base, V as base>)]
#[flux::generics(K as base, V as base)]
impl<K, V> RMap<K, V> {
#[flux::trusted]
#[flux::sig(fn() -> RMap<K, V>{m: m.keys == set_empty(0)})]
Expand Down
2 changes: 1 addition & 1 deletion crates/flux-tests/tests/lib/rset.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ pub struct RSet<T> {
pub inner: std::collections::HashSet<T>,
}

#[flux::generics(<T as base>)]
#[flux::generics(T as base)]
impl<T> RSet<T> {
#[flux::trusted]
#[flux::sig(fn() -> RSet<T>[set_empty(0)])]
Expand Down

0 comments on commit 672d1bb

Please sign in to comment.