diff --git a/README.md b/README.md index 63073569ab..81ad189c5b 100644 --- a/README.md +++ b/README.md @@ -16,3 +16,24 @@ For an overview, take a look at the [`flux` website](https://flux-rs.github.io). Documentation, including installation and usage guides can be found on the [website](https://flux-rs.github.io/flux). + +----- +fn sort_params( + generics: &rustc_middle::ty::Generics, + refined_by: &surface::RefinedBy, +) -> Vec { + let sort_params: FxHashSet<_> = refined_by + .sort_params + .iter() + .map(|ident| ident.name) + .collect(); + let mut params = vec![]; + for param in &generics.params { + if let rustc_middle::ty::GenericParamDefKind::Type { .. } = param.kind && + sort_params.contains(¶m.name) + { + params.push(param.def_id); + } + } + params +} \ No newline at end of file diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index c0a2c5920c..39a7f7c618 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -19,7 +19,7 @@ use rustc_hir as hir; use rustc_hir::OwnerId; use rustc_middle::ty::Generics; use rustc_span::{ - def_id::{DefId, LocalDefId}, + def_id::LocalDefId, sym::{self}, symbol::kw, Span, Symbol, @@ -108,10 +108,9 @@ pub fn desugar_refined_by( )) }) .try_collect_exhaust()?; - let sort_params: Vec<_> = sort_params(generics, refined_by); Ok(fhir::RefinedBy::new( owner_id.def_id, - sort_params, + &generics, early_bound_params, index_params, refined_by.span, diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 68d5a6e04e..2c1a7ce0b9 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -789,7 +789,7 @@ impl Generics { impl RefinedBy { pub fn new( def_id: impl Into, - generics: &Generics, + generics: &rustc_middle::ty::Generics, early_bound_params: impl IntoIterator, index_params: impl IntoIterator, span: Span, @@ -800,25 +800,21 @@ impl RefinedBy { .into_iter() .inspect(|(_, sort)| sorts.push(sort.clone())) .collect(); - // let sort_params = sort_params.into_iter().collect(); let sort_params = Self::sort_params(generics, &sorts); RefinedBy { def_id: def_id.into(), sort_params, span, index_params, early_bound, sorts } } - fn sort_params(generics: &Generics, sorts: &Vec) -> Vec { - // let sort_params: FxHashSet<_> = refined_by - // .sort_params - // .iter() - // .map(|ident| ident.name) - // .collect(); + fn sort_params(generics: &rustc_middle::ty::Generics, sorts: &Vec) -> Vec { let mut sort_params: FxHashSet = Default::default(); - TODO_walk_over_sorts_to_gather_all_Param_defids(); + for sort in sorts { + sort.gather_sort_params(&mut sort_params); + } let mut params = vec![]; for param in &generics.params { - let def_id = param.def_id.to_def_id(); - if let GenericParamKind::Type { .. } = param.kind && + let def_id = param.def_id; + if let rustc_middle::ty::GenericParamDefKind::Type { .. } = param.kind && sort_params.contains(&def_id) { params.push(def_id); @@ -954,6 +950,34 @@ impl Sort { Sort::Func(fsort) => Sort::Func(fsort.param_subst(subst)), // bug!("unexpected subst in (nested) func-sort {self:?}"), } } + + pub fn gather_sort_params(&self, params: &mut FxHashSet) { + match self { + Sort::Int + | Sort::Bool + | Sort::Real + | Sort::Loc + | Sort::Unit + | Sort::BitVec(_) + | Sort::Var(_) + | Sort::Infer(_) + | Sort::Wildcard => {} + Sort::Param(def_id) => { + params.insert(*def_id); + } + Sort::App(_, args) => { + for arg in args { + arg.gather_sort_params(params); + } + } + Sort::Func(fsort) => { + for arg in &fsort.fsort.inputs_and_output { + arg.gather_sort_params(params); + } + } + Sort::Record(_, _) => bug!("unexpected record sort"), + } + } } impl ena::unify::UnifyKey for SortVid { diff --git a/crates/flux-middle/src/fhir/lift.rs b/crates/flux-middle/src/fhir/lift.rs index ee4d98fa22..9d08d37e0f 100644 --- a/crates/flux-middle/src/fhir/lift.rs +++ b/crates/flux-middle/src/fhir/lift.rs @@ -20,7 +20,7 @@ pub struct LiftCtxt<'a, 'tcx> { owner: OwnerId, } -pub fn lift_refined_by(tcx: TyCtxt, sess: &FluxSession, owner_id: OwnerId) -> fhir::RefinedBy { +pub fn lift_refined_by(tcx: TyCtxt, owner_id: OwnerId) -> fhir::RefinedBy { let def_id = owner_id.def_id; let item = tcx.hir().expect_item(def_id); match item.kind { diff --git a/crates/flux-syntax/src/grammar.lalrpop b/crates/flux-syntax/src/grammar.lalrpop index 411b2bf6db..6ab9bcf802 100644 --- a/crates/flux-syntax/src/grammar.lalrpop +++ b/crates/flux-syntax/src/grammar.lalrpop @@ -47,7 +47,6 @@ pub TyAlias: surface::TyAlias = { => { let refined_by = surface::RefinedBy { - sort_params: vec![], early_bound_params: early_bound_params.unwrap_or_default(), index_params: index_params.unwrap_or_default(), span: cx.map_span(refined_by_lo, refined_by_hi) @@ -67,14 +66,7 @@ SortParams: Vec = { } pub RefinedBy: surface::RefinedBy = { - "<" > ">" "{" > "}" => surface::RefinedBy { - sort_params, - index_params, - early_bound_params: vec![], - span: cx.map_span(lo, hi) - }, > => surface::RefinedBy { - sort_params: vec![], index_params, early_bound_params: vec![], span: cx.map_span(lo, hi) diff --git a/crates/flux-syntax/src/surface.rs b/crates/flux-syntax/src/surface.rs index 6f36c5b0b9..fa5e621da0 100644 --- a/crates/flux-syntax/src/surface.rs +++ b/crates/flux-syntax/src/surface.rs @@ -104,7 +104,6 @@ pub struct VariantRet { #[derive(Debug, Default)] pub struct RefinedBy { - pub sort_params: Vec, pub early_bound_params: Vec, pub index_params: Vec, pub span: Span, diff --git a/crates/flux-tests/tests/neg/error_messages/wf/poly_sort.rs b/crates/flux-tests/tests/neg/error_messages/wf/poly_sort.rs index 860193eb30..d9705df59c 100644 --- a/crates/flux-tests/tests/neg/error_messages/wf/poly_sort.rs +++ b/crates/flux-tests/tests/neg/error_messages/wf/poly_sort.rs @@ -1,7 +1,12 @@ use std::hash::Hash; #[flux::opaque] -// #[flux::refined_by( { elems: Set })] -#[flux::refined_by( elems: Set )] //~ ERROR unbound generic `Tiger` -pub struct RSet { - pub inner: std::collections::HashSet, +#[flux::refined_by(elems: Set)] //~ ERROR cannot find sort `Tiger` +pub struct Foo { + pub inner: std::collections::HashSet, +} + +#[flux::opaque] +#[flux::refined_by(elems: Set)] //~ ERROR cannot find sort `Set` +pub struct Bar { + pub inner: std::collections::HashSet, } diff --git a/crates/flux-tests/tests/neg/surface/rset00.rs b/crates/flux-tests/tests/neg/surface/rset00.rs index 7c761f8db1..1bcfa6afdd 100644 --- a/crates/flux-tests/tests/neg/surface/rset00.rs +++ b/crates/flux-tests/tests/neg/surface/rset00.rs @@ -1,6 +1,6 @@ use std::hash::Hash; #[flux::opaque] -#[flux::refined_by( { elems: Set })] +#[flux::refined_by(elems: Set)] pub struct RSet { pub inner: std::collections::HashSet, } diff --git a/crates/flux-tests/tests/pos/surface/rset00.rs b/crates/flux-tests/tests/pos/surface/rset00.rs index e3058470e9..438b43c542 100644 --- a/crates/flux-tests/tests/pos/surface/rset00.rs +++ b/crates/flux-tests/tests/pos/surface/rset00.rs @@ -1,6 +1,6 @@ use std::hash::Hash; #[flux::opaque] -#[flux::refined_by( { elems: Set })] +#[flux::refined_by(elems: Set )] pub struct RSet { pub inner: std::collections::HashSet, }