Skip to content

Commit

Permalink
Some cleanup (#912)
Browse files Browse the repository at this point in the history
  • Loading branch information
@nilehmann
nilehmann authored Nov 27, 2024
1 parent c9145d7 commit c4841c3
Show file tree
Hide file tree
Showing 7 changed files with 106 additions and 100 deletions.
2 changes: 1 addition & 1 deletion crates/flux-desugar/src/desugar.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1394,7 +1394,7 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> {

fn desugar_constructor_path(&self, path: &surface::ExprPath) -> Result<fhir::PathExpr<'genv>> {
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));
Expand Down
21 changes: 7 additions & 14 deletions crates/flux-desugar/src/resolver/refinement_resolver.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -288,22 +288,16 @@ impl<V: ScopedVisitor> surface::visit::Visitor for ScopedVisitorWrapper<V> {
}

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);
Expand Down Expand Up @@ -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,
}
}
Expand Down
34 changes: 17 additions & 17 deletions crates/flux-fhir-analysis/locales/en-US.ftl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
61 changes: 30 additions & 31 deletions crates/flux-fhir-analysis/src/conv/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -706,21 +706,15 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
fn conv_sort_path(&mut self, path: &fhir::SortPath) -> QueryResult<rty::Sort> {
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))),
Expand Down Expand Up @@ -767,17 +761,11 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
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 } => {
Expand All @@ -793,7 +781,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
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,
Expand All @@ -809,6 +797,17 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {

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
Expand Down Expand Up @@ -1758,8 +1757,9 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
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),
Expand Down Expand Up @@ -1817,7 +1817,7 @@ impl<'genv, 'tcx: 'genv, P: ConvPhase<'genv, 'tcx>> ConvCtxt<P> {
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 {
Expand Down Expand Up @@ -2159,14 +2159,13 @@ pub fn conv_func_decl(genv: GlobalEnv, func: &fhir::SpecFunc) -> QueryResult<rty
fn emit_prim_sort_generics_error(
genv: GlobalEnv,
path: &fhir::SortPath,
name: &'static str,
expected: usize,
prim_sort: fhir::PrimSort,
) -> 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)
}
Expand Down Expand Up @@ -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) }
}
}

Expand Down
42 changes: 16 additions & 26 deletions crates/flux-fhir-analysis/src/wf/sortck.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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<rustc_span::Symbol> =
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(())
}
Expand Down Expand Up @@ -262,19 +256,18 @@ 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
.genv
.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,
Expand Down Expand Up @@ -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")
}
}
}
Expand Down
Loading

0 comments on commit c4841c3

Please sign in to comment.