diff --git a/crates/flux-desugar/src/desugar.rs b/crates/flux-desugar/src/desugar.rs index 64f166ab80..3ea3a758bd 100644 --- a/crates/flux-desugar/src/desugar.rs +++ b/crates/flux-desugar/src/desugar.rs @@ -1394,7 +1394,7 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> { fn desugar_constructor_path(&self, path: &surface::ExprPath) -> Result> { let res = self.resolver_output().expr_path_res_map[&path.node_id]; - if let ExprRes::Struct(..) | ExprRes::Enum(..) = res { + if let ExprRes::Ctor(..) = res { let segments = self .genv() .alloc_slice_fill_iter(path.segments.iter().map(|s| s.ident)); diff --git a/crates/flux-desugar/src/resolver/refinement_resolver.rs b/crates/flux-desugar/src/resolver/refinement_resolver.rs index 53a4a9c4fb..f487b350aa 100644 --- a/crates/flux-desugar/src/resolver/refinement_resolver.rs +++ b/crates/flux-desugar/src/resolver/refinement_resolver.rs @@ -288,22 +288,16 @@ impl surface::visit::Visitor for ScopedVisitorWrapper { } fn visit_expr(&mut self, expr: &surface::Expr) { - match &expr.kind { - surface::ExprKind::Path(path) => { - self.on_path(path); - } - surface::ExprKind::App(func, _) => { - self.on_func(*func, expr.node_id); - } - surface::ExprKind::Dot(path, _) => self.on_path(path), - surface::ExprKind::Constructor(Some(path), _) => { - self.on_path(path); - } - _ => {} + if let surface::ExprKind::App(func, _) = &expr.kind { + self.on_func(*func, expr.node_id); } surface::visit::walk_expr(self, expr); } + fn visit_path_expr(&mut self, path: &surface::ExprPath) { + self.on_path(path); + } + fn visit_base_sort(&mut self, bsort: &surface::BaseSort) { self.on_base_sort(bsort); surface::visit::walk_base_sort(self, bsort); @@ -570,8 +564,7 @@ impl<'a, 'genv, 'tcx> RefinementResolver<'a, 'genv, 'tcx> { match res { fhir::Res::Def(DefKind::ConstParam, def_id) => Some(ExprRes::ConstGeneric(def_id)), fhir::Res::Def(DefKind::Const, def_id) => Some(ExprRes::Const(def_id)), - fhir::Res::Def(DefKind::Struct, def_id) => Some(ExprRes::Struct(def_id)), - fhir::Res::Def(DefKind::Enum, def_id) => Some(ExprRes::Enum(def_id)), + fhir::Res::Def(DefKind::Struct | DefKind::Enum, def_id) => Some(ExprRes::Ctor(def_id)), _ => None, } } diff --git a/crates/flux-fhir-analysis/locales/en-US.ftl b/crates/flux-fhir-analysis/locales/en-US.ftl index 1d5279c8a0..792af8dbb4 100644 --- a/crates/flux-fhir-analysis/locales/en-US.ftl +++ b/crates/flux-fhir-analysis/locales/en-US.ftl @@ -57,7 +57,7 @@ fhir_analysis_unexpected_fun = mismatched sorts .label = expected `{$sort}`, found function -fhir_analysis_unexpected_constructor = +fhir_analysis_unexpected_constructor = mismatched sorts .label = expected `{$sort}`, found constructor @@ -74,10 +74,10 @@ fhir_analysis_param_count_mismatch = fhir_analysis_field_not_found = no field `{$fld}` on sort `{$sort}` -fhir_analysis_constructor_missing_fields = +fhir_analysis_constructor_missing_fields = missing fields in constructor: {$missing_fields} -fhir_analysis_duplicate_field_used = +fhir_analysis_duplicate_field_used = field `{$fld}` was previously used in constructor .help = field `{$fld}` previously used here, consider removing it @@ -212,38 +212,38 @@ fhir_analysis_too_many_generic_args = *[other] arguments } -fhir_analysis_generics_on_primitive_sort = - primitive sort {$name} expects {$expected -> +fhir_analysis_generics_on_primitive_sort = + primitive sort {$name} expects {$expected -> [0] no generics [one] exactly one generic argument *[other] exactly {$expected} generic arguments } but found {$found} .label = incorrect generics on primitive sort -fhir_analysis_too_many_generics_on_sort = - sorts associated with this {$def_descr} should have {$max -> +fhir_analysis_incorrect_generics_on_sort = + sorts associated with this {$def_descr} should have {$expected -> [0] no generic arguments - [one] at most one generic argument - *[other] at most {$max} generic arguments + [one] one generic argument + *[other] {$expected} generic arguments } but {$found} generic {$found -> - [one] argument - *[other] arguments + [one] argument was + *[other] arguments were } supplied - .label = expected {$max -> + .label = expected {$expected -> [0] no generic arguments - [one] at most one generic argument - *[other] at most {$max} generic arguments + [one] one generic argument + *[other] {$expected} generic arguments } on sort -fhir_analysis_generics_on_type_parameter = +fhir_analysis_generics_on_type_parameter = type parameter expects no generics but found {$found} .label = found generics on sort type parameter -fhir_analysis_generics_on_self_alias = +fhir_analysis_generics_on_self_alias = type alias Self expects no generics but found {$found} .label = found generics on type `Self` -fhir_analysis_generics_on_opaque_sort = +fhir_analysis_generics_on_opaque_sort = user defined opaque sorts have no generics but found {$found} .label = found generics on user defined opaque sort diff --git a/crates/flux-fhir-analysis/src/conv/mod.rs b/crates/flux-fhir-analysis/src/conv/mod.rs index 7bd265ae99..c679f173c0 100644 --- a/crates/flux-fhir-analysis/src/conv/mod.rs +++ b/crates/flux-fhir-analysis/src/conv/mod.rs @@ -706,21 +706,15 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ fn conv_sort_path(&mut self, path: &fhir::SortPath) -> QueryResult { let ctor = match path.res { fhir::SortRes::PrimSort(fhir::PrimSort::Int) => { - if !path.args.is_empty() { - Err(emit_prim_sort_generics_error(self.genv(), path, "int", 0))?; - } + self.check_prim_sort_generics(path, fhir::PrimSort::Int)?; return Ok(rty::Sort::Int); } fhir::SortRes::PrimSort(fhir::PrimSort::Bool) => { - if !path.args.is_empty() { - Err(emit_prim_sort_generics_error(self.genv(), path, "bool", 0))?; - } + self.check_prim_sort_generics(path, fhir::PrimSort::Bool)?; return Ok(rty::Sort::Bool); } fhir::SortRes::PrimSort(fhir::PrimSort::Real) => { - if !path.args.is_empty() { - Err(emit_prim_sort_generics_error(self.genv(), path, "real", 0))?; - } + self.check_prim_sort_generics(path, fhir::PrimSort::Real)?; return Ok(rty::Sort::Real); } fhir::SortRes::SortParam(n) => return Ok(rty::Sort::Var(rty::ParamSort::from(n))), @@ -767,17 +761,11 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ return Ok(rty::Sort::Alias(rty::AliasKind::Projection, alias_ty)); } fhir::SortRes::PrimSort(fhir::PrimSort::Set) => { - if path.args.len() != 1 { - // Has to have one argument - Err(emit_prim_sort_generics_error(self.genv(), path, "Set", 1))?; - } + self.check_prim_sort_generics(path, fhir::PrimSort::Set)?; rty::SortCtor::Set } fhir::SortRes::PrimSort(fhir::PrimSort::Map) => { - if path.args.len() != 2 { - // Has to have two arguments - Err(emit_prim_sort_generics_error(self.genv(), path, "Map", 2))?; - } + self.check_prim_sort_generics(path, fhir::PrimSort::Map)?; rty::SortCtor::Map } fhir::SortRes::User { name } => { @@ -793,7 +781,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ fhir::SortRes::Adt(def_id) => { let sort_def = self.genv().adt_sort_def_of(def_id)?; if path.args.len() > sort_def.param_count() { - let err = errors::TooManyGenericsOnSort::new( + let err = errors::IncorrectGenericsOnSort::new( self.genv(), def_id, path.segments.last().unwrap().span, @@ -809,6 +797,17 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ Ok(rty::Sort::app(ctor, args)) } + + fn check_prim_sort_generics( + &mut self, + path: &fhir::SortPath<'_>, + prim_sort: fhir::PrimSort, + ) -> QueryResult { + if path.args.len() != prim_sort.generics() { + Err(emit_prim_sort_generics_error(self.genv(), path, prim_sort))?; + } + Ok(()) + } } /// Conversion of types @@ -1758,8 +1757,9 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ ExprRes::GlobalFunc(..) => { span_bug!(var.span, "unexpected func in var position") } - ExprRes::Struct(..) => span_bug!(var.span, "unexpected struct in var position"), - ExprRes::Enum(..) => span_bug!(var.span, "unexpected enum in var position"), + ExprRes::Ctor(..) => { + span_bug!(var.span, "unexpected constructor in var position") + } } } fhir::ExprKind::Literal(lit) => rty::Expr::constant(conv_lit(*lit)).at(espan), @@ -1817,7 +1817,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt

{ fhir::ExprKind::Constructor(path, exprs, spread) => { let def_id = if let Some(path) = path { match path.res { - ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id, + ExprRes::Ctor(def_id) => def_id, _ => span_bug!(path.span, "unexpected path in constructor"), } } else { @@ -2159,14 +2159,13 @@ pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult ErrorGuaranteed { let err = errors::GenericsOnPrimitiveSort::new( path.segments.last().unwrap().span, - name, + prim_sort.name_str(), path.args.len(), - expected, + prim_sort.generics(), ); genv.sess().emit_err(err) } @@ -2378,25 +2377,25 @@ mod errors { } #[derive(Diagnostic)] - #[diag(fhir_analysis_too_many_generics_on_sort, code = E0999)] - pub(super) struct TooManyGenericsOnSort { + #[diag(fhir_analysis_incorrect_generics_on_sort, code = E0999)] + pub(super) struct IncorrectGenericsOnSort { #[primary_span] #[label] span: Span, found: usize, - max: usize, + expected: usize, def_descr: &'static str, } - impl TooManyGenericsOnSort { + impl IncorrectGenericsOnSort { pub(super) fn new( genv: GlobalEnv, def_id: DefId, span: Span, found: usize, - max: usize, + expected: usize, ) -> Self { - Self { span, found, max, def_descr: genv.tcx().def_descr(def_id) } + Self { span, found, expected, def_descr: genv.tcx().def_descr(def_id) } } } diff --git a/crates/flux-fhir-analysis/src/wf/sortck.rs b/crates/flux-fhir-analysis/src/wf/sortck.rs index bfb8335b5e..c2dbf5ba30 100644 --- a/crates/flux-fhir-analysis/src/wf/sortck.rs +++ b/crates/flux-fhir-analysis/src/wf/sortck.rs @@ -16,7 +16,7 @@ use flux_middle::{ use itertools::{izip, Itertools}; use rustc_data_structures::unord::UnordMap; use rustc_errors::Diagnostic; -use rustc_hash::{FxHashMap, FxHashSet}; +use rustc_hash::FxHashMap; use rustc_span::{def_id::DefId, symbol::Ident, Span}; use super::errors; @@ -95,33 +95,27 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { expected: &rty::Sort, ) -> Result { let sort_by_field_name = sort_def.sort_by_field_name(sort_args); - let mut used_fields = FxHashSet::default(); + let mut used_fields = FxHashMap::default(); for expr in field_exprs { // make sure that the field is actually a field - if let Some(sort) = sort_by_field_name.get(&expr.ident.name) { - self.check_expr(&expr.expr, sort)?; - } else { + let Some(sort) = sort_by_field_name.get(&expr.ident.name) else { return Err(self.emit_err(errors::FieldNotFound::new(expected.clone(), expr.ident))); - } - if let Some(old_field) = used_fields.replace(expr.ident) { + }; + if let Some(old_field) = used_fields.insert(expr.ident.name, expr.ident) { return Err(self.emit_err(errors::DuplicateFieldUsed::new(expr.ident, old_field))); } + self.check_expr(&expr.expr, sort)?; } if let Some(spread) = spread { // must check that the spread is of the same sort as the constructor - self.check_expr(&spread.expr, expected)?; - Ok(()) + self.check_expr(&spread.expr, expected) } else if sort_by_field_name.len() != used_fields.len() { // emit an error because all fields are not used - let used_field_names: Vec = - used_fields.into_iter().map(|k| k.name).collect(); - let fields_remaining = sort_by_field_name + let missing_fields = sort_by_field_name .into_keys() - .filter(|x| !used_field_names.contains(x)) + .filter(|x| !used_fields.contains_key(x)) .collect(); - return Err( - self.emit_err(errors::ConstructorMissingFields::new(expr_span, fields_remaining)) - ); + Err(self.emit_err(errors::ConstructorMissingFields::new(expr_span, missing_fields))) } else { Ok(()) } @@ -262,7 +256,7 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { // first get the sort based on the path - for example S { ... } => S // and we should expect sort to be a struct or enum app let path_def_id = match path.res { - ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id, + ExprRes::Ctor(def_id) => def_id, _ => span_bug!(expr.span, "unexpected path in constructor"), }; let sort_def = self @@ -270,11 +264,10 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { .adt_sort_def_of(path_def_id) .map_err(|e| self.emit_err(e))?; // generate fresh inferred sorts for each param - let fresh_args = (0..sort_def.param_count()) + let fresh_args: rty::List<_> = (0..sort_def.param_count()) .map(|_| self.next_sort_var()) - .collect_vec(); - let sort = - rty::Sort::App(rty::SortCtor::Adt(sort_def.clone()), fresh_args.clone().into()); + .collect(); + let sort = rty::Sort::App(rty::SortCtor::Adt(sort_def.clone()), fresh_args.clone()); // check fields & spread against fresh args self.check_field_exprs( expr.span, @@ -304,11 +297,8 @@ impl<'genv, 'tcx> InferCtxt<'genv, 'tcx> { ExprRes::GlobalFunc(_, _) => { span_bug!(path.span, "unexpected func in var position") } - ExprRes::Struct(_) => { - span_bug!(path.span, "unexpected struct in var position") - } - ExprRes::Enum(_) => { - span_bug!(path.span, "unexpected enum in var position") + ExprRes::Ctor(_) => { + span_bug!(path.span, "unexpected constructor in var position") } } } diff --git a/crates/flux-middle/src/fhir.rs b/crates/flux-middle/src/fhir.rs index 697a2a9d30..6d2dd2a017 100644 --- a/crates/flux-middle/src/fhir.rs +++ b/crates/flux-middle/src/fhir.rs @@ -826,6 +826,29 @@ pub enum PrimSort { Map, } +impl PrimSort { + pub fn name_str(self) -> &'static str { + match self { + PrimSort::Int => "int", + PrimSort::Bool => "bool", + PrimSort::Real => "real", + PrimSort::Set => "Set", + PrimSort::Map => "Map", + } + } + + /// Number of generics expected by this primitive sort + pub fn generics(self) -> usize { + match self { + PrimSort::Int => 0, + PrimSort::Bool => 0, + PrimSort::Real => 0, + PrimSort::Set => 1, + PrimSort::Map => 2, + } + } +} + #[derive(Clone, Copy)] pub enum SortRes { /// A primitive sort. @@ -855,7 +878,7 @@ pub enum SortRes { /// } /// ``` SelfParamAssoc { trait_id: DefId, ident: Ident }, - /// The sort of an adt (enum/struct). + /// The sort automatically generated for an adt (enum/struct) with a `flux::refined_by` annotation Adt(DefId), } @@ -962,16 +985,18 @@ pub enum Lit { Int(i128), Real(i128), Bool(bool), - Str(Symbol), // `rustc_span::Symbol` interns a value with the type - Char(char), // all Rust chars are u32s + Str(Symbol), + Char(char), } #[derive(Clone, Copy, Debug)] pub enum ExprRes { Param(ParamKind, Id), Const(DefId), - Struct(DefId), - Enum(DefId), + /// The constructor of an [adt sort] + /// + /// [adt sort]: SortRes::Adt + Ctor(DefId), ConstGeneric(DefId), NumConst(i128), GlobalFunc(SpecFuncKind, Symbol), @@ -985,8 +1010,7 @@ impl ExprRes { ExprRes::NumConst(val) => ExprRes::NumConst(val), ExprRes::GlobalFunc(kind, name) => ExprRes::GlobalFunc(kind, name), ExprRes::ConstGeneric(def_id) => ExprRes::ConstGeneric(def_id), - ExprRes::Struct(def_id) => ExprRes::Struct(def_id), - ExprRes::Enum(def_id) => ExprRes::Enum(def_id), + ExprRes::Ctor(def_id) => ExprRes::Ctor(def_id), } } diff --git a/tests/tests/neg/error_messages/conv/mismatched_generics.rs b/tests/tests/neg/error_messages/conv/mismatched_generics.rs index 907d8a524f..b24638f165 100644 --- a/tests/tests/neg/error_messages/conv/mismatched_generics.rs +++ b/tests/tests/neg/error_messages/conv/mismatched_generics.rs @@ -7,7 +7,7 @@ struct S { } defs! { - fn foo(s: S) -> int { //~ Error sorts associated with this struct should have no generic arguments but 1 generic argument supplied + fn foo(s: S) -> int { //~ Error sorts associated with this struct should have no generic arguments but 1 generic argument was supplied s.n } @@ -17,7 +17,7 @@ defs! { fn foo3(x: Map) -> int { //~ Error primitive sort Map expects exactly 2 generic arguments but found 1 1 - } + } fn foo4(x: Map) -> int { //~ Error primitive sort Map expects exactly 2 generic arguments but found 0 1 @@ -37,9 +37,9 @@ defs! { } #[flux::refined_by(f: T)] //~ Error type parameter expects no generics but found 1 -struct X { +struct X { #[flux::field(T[f])] - f: T + f: T, } #[flux::assoc(fn foo(x: Self) -> int)] //~ Error type alias Self expects no generics but found 1