remove sort_params from RefinedBy; find it from Sorts

flux-rs · Oct 20, 2023 · 90aec9f · 90aec9f
1 parent c1e2c89
commit 90aec9f
Show file tree

Hide file tree

Showing 9 changed files with 70 additions and 30 deletions.
diff --git 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<DefId> {
+    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(&param.name)
+        {
+            params.push(param.def_id);
+        }
+    }
+    params
+}
diff --git 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
@@ -789,7 +789,7 @@ impl Generics {
 impl RefinedBy {
     pub fn new(
         def_id: impl Into<DefId>,
-        generics: &Generics,
+        generics: &rustc_middle::ty::Generics,
         early_bound_params: impl IntoIterator<Item = Sort>,
         index_params: impl IntoIterator<Item = (Symbol, Sort)>,
         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<Sort>) -> Vec<DefId> {
-        // let sort_params: FxHashSet<_> = refined_by
-        // .sort_params
-        // .iter()
-        // .map(|ident| ident.name)
-        // .collect();
+    fn sort_params(generics: &rustc_middle::ty::Generics, sorts: &Vec<Sort>) -> Vec<DefId> {
         let mut sort_params: FxHashSet<DefId> = 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<DefId>) {
+        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
@@ -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
@@ -47,7 +47,6 @@ pub TyAlias: surface::TyAlias = {
     <ty:Ty>
     <hi:@R> => {
         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<Ident> = {
 }
 
 pub RefinedBy: surface::RefinedBy = {
-    <lo:@L> "<" <sort_params:Comma<Ident>> ">" "{" <index_params:RefineParams<"!">> "}" <hi:@R> => surface::RefinedBy {
-        sort_params,
-        index_params,
-        early_bound_params: vec![],
-        span: cx.map_span(lo, hi)
-    },
     <lo:@L> <index_params:RefineParams<"!">> <hi:@R> => 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
@@ -104,7 +104,6 @@ pub struct VariantRet {
 
 #[derive(Debug, Default)]
 pub struct RefinedBy {
-    pub sort_params: Vec<Ident>,
     pub early_bound_params: Vec<RefineParam>,
     pub index_params: Vec<RefineParam>,
     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
@@ -1,7 +1,12 @@
 use std::hash::Hash;
 #[flux::opaque]
-// #[flux::refined_by(<Tiger> { elems: Set<Tiger> })]
-#[flux::refined_by( elems: Set<Tiger> )] //~ ERROR unbound generic `Tiger`
-pub struct RSet<Tiger> {
-    pub inner: std::collections::HashSet<Tiger>,
+#[flux::refined_by(elems: Set<Tiger>)] //~ ERROR cannot find sort `Tiger`
+pub struct Foo<T> {
+    pub inner: std::collections::HashSet<T>,
+}
+
+#[flux::opaque]
+#[flux::refined_by(elems: Set)] //~ ERROR cannot find sort `Set`
+pub struct Bar<T> {
+    pub inner: std::collections::HashSet<T>,
 }
diff --git 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(<Tiger> { elems: Set<Tiger> })]
+#[flux::refined_by(elems: Set<Tiger>)]
 pub struct RSet<Tiger> {
     pub inner: std::collections::HashSet<Tiger>,
 }

diff --git 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(<Tiger> { elems: Set<Tiger> })]
+#[flux::refined_by(elems: Set<Tiger> )]
 pub struct RSet<Tiger> {
     pub inner: std::collections::HashSet<Tiger>,
 }