Add functional updates

crates/flux-desugar/locales/en-US.ftl

@@ -13,6 +13,9 @@ desugar_unexpected_literal =
 desugar_invalid_dot_var =
     unsupported field access in refinement
 
+desugar_invalid_constructor_path =
+    invalid use of path in constructor
+
 desugar_invalid_func_as_var =
     invalid use of function
     .label = function not supported in this position
@@ -35,6 +38,10 @@ desugar_unresolved_generic_param =
 desugar_invalid_variant_ret =
     invalid variant return type
 
+desugar_multiple_spreads_in_constructor = 
+    multiple spreads found in constructor
+    .help = previous spread found here. consider removing it
+
 # Resolve errors
 
 desugar_duplicate_param =

crates/flux-desugar/src/desugar.rs

@@ -9,7 +9,7 @@ use flux_middle::{
     try_alloc_slice, MaybeExternId, ResolverOutput,
 };
 use flux_syntax::{
-    surface::{self, visit::Visitor as _, NodeId},
+    surface::{self, visit::Visitor as _, ConstructorArgs, FieldExpr, NodeId, Spread},
     walk_list,
 };
 use hir::{def::DefKind, ItemKind};
@@ -1329,11 +1329,74 @@ trait DesugarCtxt<'genv, 'tcx: 'genv> {
                     self.genv().alloc(e2?),
                 )
             }
+            surface::ExprKind::Constructor(path, constructor_args) => {
+                let path = self.desugar_constructor_path(path)?;
+                let field_exprs = constructor_args
+                    .iter()
+                    .filter_map(|arg| {
+                        match arg {
+                            ConstructorArgs::FieldExpr(e) => Some(e),
+                            ConstructorArgs::Spread(_) => None,
+                        }
+                    })
+                    .collect::<Vec<&FieldExpr>>();
+
+                let field_exprs = try_alloc_slice!(self.genv(), field_exprs, |field_expr| {
+                    let e = self.desugar_expr(&field_expr.expr)?;
+                    Ok(fhir::FieldExpr {
+                        ident: field_expr.ident,
+                        expr: e,
+                        fhir_id: self.next_fhir_id(),
+                        span: e.span,
+                    })
+                })?;
+
+                let spreads = constructor_args
+                    .iter()
+                    .filter_map(|arg| {
+                        match arg {
+                            ConstructorArgs::FieldExpr(_) => None,
+                            ConstructorArgs::Spread(s) => Some(s),
+                        }
+                    })
+                    .collect::<Vec<&Spread>>();
+
+                let spread = match &spreads[..] {
+                    [] => None,
+                    [s] => {
+                        let spread = fhir::Spread {
+                            expr: self.desugar_expr(&s.expr)?,
+                            span: s.span,
+                            fhir_id: self.next_fhir_id(),
+                        };
+                        Some(self.genv().alloc(spread))
+                    }
+                    [s1, s2, ..] => {
+                        // Multiple spreads found - emit an error
+                        return Err(self.emit_err(errors::MultipleSpreadsInConstructor::new(
+                            s1.span, s2.span,
+                        )));
+                    }
+                };
+                fhir::ExprKind::Constructor(path, field_exprs, spread)
+            }
         };
 
         Ok(fhir::Expr { kind, span: expr.span, fhir_id: self.next_fhir_id() })
     }
 
+    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 {
+            let segments = self
+                .genv()
+                .alloc_slice_fill_iter(path.segments.iter().map(|s| s.ident));
+            Ok(fhir::PathExpr { segments, res, fhir_id: self.next_fhir_id(), span: path.span })
+        } else {
+            Err(self.emit_err(errors::InvalidConstructorPath { span: path.span }))
+        }
+    }
+
     fn desugar_exprs(&mut self, exprs: &[surface::Expr]) -> Result<&'genv [fhir::Expr<'genv>]> {
         try_alloc_slice!(self.genv(), exprs, |e| self.desugar_expr(e))
     }

crates/flux-desugar/src/errors.rs

@@ -17,6 +17,13 @@ pub(super) struct UnexpectedLiteral {
     pub(super) span: Span,
 }
 
+#[derive(Diagnostic)]
+#[diag(desugar_invalid_constructor_path, code = E0999)]
+pub(super) struct InvalidConstructorPath {
+    #[primary_span]
+    pub(super) span: Span,
+}
+
 #[derive(Diagnostic)]
 #[diag(desugar_invalid_dot_var, code = E0999)]
 pub(super) struct InvalidDotVar {
@@ -88,3 +95,18 @@ impl InvalidVariantRet {
         Self { span: path.span }
     }
 }
+
+#[derive(Diagnostic)]
+#[diag(desugar_multiple_spreads_in_constructor, code = E0999)]
+pub(super) struct MultipleSpreadsInConstructor {
+    #[primary_span]
+    pub(super) span: Span,
+    #[help]
+    pub(super) prev_span: Span,
+}
+
+impl MultipleSpreadsInConstructor {
+    pub(super) fn new(span: Span, prev_span: Span) -> Self {
+        Self { span, prev_span }
+    }
+}

crates/flux-desugar/src/resolver/refinement_resolver.rs

@@ -296,6 +296,9 @@ impl<V: ScopedVisitor> surface::visit::Visitor for ScopedVisitorWrapper<V> {
                 self.on_func(*func, expr.node_id);
             }
             surface::ExprKind::Dot(path, _) => self.on_path(path),
+            surface::ExprKind::Constructor(path, _) => {
+                self.on_path(path);
+            }
             _ => {}
         }
         surface::visit::walk_expr(self, expr);
@@ -556,13 +559,19 @@ impl<'a, 'genv, 'tcx> RefinementResolver<'a, 'genv, 'tcx> {
         &mut self,
         segments: &[S],
     ) -> Option<ExprRes<NodeId>> {
-        let res = self
-            .resolver
-            .resolve_path_with_ribs(segments, ValueNS)?
-            .full_res()?;
+        let res = match self.resolver.resolve_path_with_ribs(segments, ValueNS) {
+            Some(r) => r.full_res()?,
+            _ => {
+                self.resolver
+                    .resolve_path_with_ribs(segments, TypeNS)?
+                    .full_res()?
+            }
+        };
         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)),
             _ => None,
         }
     }

crates/flux-fhir-analysis/locales/en-US.ftl

@@ -3,6 +3,11 @@
 fhir_analysis_sort_mismatch =
     mismatched sorts
     .label = expected `{$expected}`, found `{$found}`
+
+fhir_analysis_sort_mismatch_found_omitted =
+    mismatched sorts
+    .label = expected `{$expected}`
+
 fhir_analysis_arg_count_mismatch =
     this {$thing} takes {$expected ->
         [one] {$expected} refinement argument
@@ -56,6 +61,10 @@ fhir_analysis_unexpected_fun =
     mismatched sorts
     .label = expected `{$sort}`, found function
 
+fhir_analysis_unexpected_constructor = 
+    mismatched sorts
+    .label = expected `{$sort}`, found constructor
+
 fhir_analysis_param_count_mismatch =
     parameter count mismatch
     .label = this function has {$found ->
@@ -69,6 +78,13 @@ fhir_analysis_param_count_mismatch =
 fhir_analysis_field_not_found =
     no field `{$fld}` on sort `{$sort}`
 
+fhir_analysis_constructor_missing_fields = 
+    missing fields in constructor: {$missing_fields}
+
+fhir_analysis_duplicate_field_used = 
+    field `{$fld}` was previously used in constructor
+    .help = field `{$fld}` previously used here, consider removing it
+
 fhir_analysis_invalid_primitive_dot_access =
     `{$sort}` is a primitive sort and therefore doesn't have fields
 

crates/flux-fhir-analysis/src/conv/mod.rs

@@ -1590,6 +1590,8 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, 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"),
                 }
             }
             fhir::ExprKind::Literal(lit) => rty::Expr::constant(conv_lit(*lit)).at(espan),
@@ -1644,10 +1646,43 @@ impl<'genv, 'tcx, P: ConvPhase> ConvCtxt<'genv, 'tcx, P> {
                     .try_collect()?;
                 rty::Expr::adt(def_id, flds)
             }
+            fhir::ExprKind::Constructor(path, exprs, spread) => {
+                let def_id = match path.res {
+                    ExprRes::Struct(def_id) | ExprRes::Enum(def_id) => def_id,
+                    _ => span_bug!(path.span, "unexpected path in constructor"),
+                };
+                let assns = self.conv_constructor_exprs(def_id, env, exprs, spread)?;
+                rty::Expr::adt(def_id, assns)
+            }
         };
         Ok(self.add_coercions(expr, fhir_id))
     }
 
+    fn conv_constructor_exprs(
+        &mut self,
+        struct_def_id: DefId,
+        env: &mut Env,
+        exprs: &[fhir::FieldExpr],
+        spread: &Option<&fhir::Spread>,
+    ) -> QueryResult<List<rty::Expr>> {
+        let struct_adt = self.genv.adt_sort_def_of(struct_def_id)?;
+        let spread = spread
+            .map(|spread| self.conv_expr(env, &spread.expr))
+            .transpose()?;
+        let field_exprs_by_name: FxIndexMap<Symbol, &fhir::FieldExpr> =
+            exprs.iter().map(|e| (e.ident.name, e)).collect();
+        let mut assns = Vec::new();
+        for (idx, field_name) in struct_adt.field_names().iter().enumerate() {
+            if let Some(field_expr) = field_exprs_by_name.get(field_name) {
+                assns.push(self.conv_expr(env, &field_expr.expr)?);
+            } else if let Some(spread) = &spread {
+                let proj = rty::FieldProj::Adt { def_id: struct_def_id, field: idx as u32 };
+                assns.push(rty::Expr::field_proj(spread, proj));
+            }
+        }
+        Ok(List::from_vec(assns))
+    }
+
     fn conv_exprs(&mut self, env: &mut Env, exprs: &[fhir::Expr]) -> QueryResult<List<rty::Expr>> {
         exprs.iter().map(|e| self.conv_expr(env, e)).collect()
     }

crates/flux-fhir-analysis/src/wf/errors.rs

@@ -19,6 +19,21 @@ impl SortMismatch {
     }
 }
 
+#[derive(Diagnostic)]
+#[diag(fhir_analysis_sort_mismatch_found_omitted, code = E0999)]
+pub(super) struct SortMismatchFoundOmitted {
+    #[primary_span]
+    #[label]
+    span: Span,
+    expected: rty::Sort,
+}
+
+impl SortMismatchFoundOmitted {
+    pub(super) fn new(span: Span, expected: rty::Sort) -> Self {
+        Self { span, expected }
+    }
+}
+
 #[derive(Diagnostic)]
 #[diag(fhir_analysis_arg_count_mismatch, code = E0999)]
 pub(super) struct ArgCountMismatch {
@@ -137,6 +152,21 @@ impl<'a> UnexpectedFun<'a> {
     }
 }
 
+#[derive(Diagnostic)]
+#[diag(fhir_analysis_unexpected_constructor, code = E0999)]
+pub(super) struct UnexpectedConstructor<'a> {
+    #[primary_span]
+    #[label]
+    span: Span,
+    sort: &'a rty::Sort,
+}
+
+impl<'a> UnexpectedConstructor<'a> {
+    pub(super) fn new(span: Span, sort: &'a rty::Sort) -> Self {
+        Self { span, sort }
+    }
+}
+
 #[derive(Diagnostic)]
 #[diag(fhir_analysis_param_count_mismatch, code = E0999)]
 pub(super) struct ParamCountMismatch {
@@ -168,6 +198,41 @@ impl FieldNotFound {
     }
 }
 
+#[derive(Diagnostic)]
+#[diag(fhir_analysis_constructor_missing_fields, code = E0999)]
+pub(super) struct ConstructorMissingFields {
+    #[primary_span]
+    constructor_span: Span,
+    missing_fields: String,
+}
+
+impl ConstructorMissingFields {
+    pub(super) fn new(constructor_span: Span, missing_fields: Vec<Symbol>) -> Self {
+        let missing_fields = missing_fields
+            .into_iter()
+            .map(|x| format!("`{x}`"))
+            .collect::<Vec<String>>()
+            .join(", ");
+        Self { constructor_span, missing_fields }
+    }
+}
+
+#[derive(Diagnostic)]
+#[diag(fhir_analysis_duplicate_field_used, code = E0999)]
+pub(super) struct DuplicateFieldUsed {
+    #[primary_span]
+    span: Span,
+    fld: Ident,
+    #[help]
+    previous_span: Span,
+}
+
+impl DuplicateFieldUsed {
+    pub(super) fn new(fld: Ident, previous_fld: Ident) -> Self {
+        Self { span: fld.span, fld, previous_span: previous_fld.span }
+    }
+}
+
 #[derive(Diagnostic)]
 #[diag(fhir_analysis_invalid_primitive_dot_access, code = E0999)]
 pub(super) struct InvalidPrimitiveDotAccess<'a> {

crates/flux-fhir-analysis/src/wf/param_usage.rs

@@ -118,6 +118,11 @@ impl<'a, 'genv, 'tcx> ParamUsesChecker<'a, 'genv, 'tcx> {
                     self.check_func_params_uses(field, is_top_level_conj, is_top_level_var);
                 }
             }
+            fhir::ExprKind::Constructor(_path, exprs, _spread) => {
+                for expr in exprs {
+                    self.check_func_params_uses(&expr.expr, false, false);
+                }
+            }
         }
     }