From 2f7e6a81bf1706ad3ae788f4826e8ae7cd60f17e Mon Sep 17 00:00:00 2001 From: Karl Meakin Date: Sun, 11 Dec 2022 23:10:08 +0000 Subject: [PATCH] Check/synth record and tuple patterns --- fathom/src/surface/elaboration.rs | 298 ++++++-------------- fathom/src/surface/elaboration/order.rs | 16 +- fathom/src/surface/elaboration/patterns.rs | 281 ++++++++++++++++++ fathom/src/surface/elaboration/reporting.rs | 16 +- 4 files changed, 386 insertions(+), 225 deletions(-) create mode 100644 fathom/src/surface/elaboration/patterns.rs diff --git a/fathom/src/surface/elaboration.rs b/fathom/src/surface/elaboration.rs index 1294fb237..9f0e6a4f7 100644 --- a/fathom/src/surface/elaboration.rs +++ b/fathom/src/surface/elaboration.rs @@ -34,6 +34,7 @@ use crate::surface::elaboration::reporting::Message; use crate::surface::{distillation, pretty, BinOp, FormatField, Item, Module, Pattern, Term}; mod order; +mod patterns; mod reporting; mod unification; @@ -463,6 +464,70 @@ impl<'interner, 'arena> Context<'interner, 'arena> { (labels.into(), filtered_fields) } + fn check_tuple_fields( + &mut self, + range: ByteRange, + fields: &[F], + get_range: fn(&F) -> ByteRange, + expected_labels: &[StringId], + ) -> Result<(), ()> { + if fields.len() == expected_labels.len() { + return Ok(()); + } + + let mut found_labels = Vec::with_capacity(fields.len()); + let mut fields_iter = fields.iter().enumerate().peekable(); + let mut expected_labels_iter = expected_labels.iter(); + + // use the label names from the expected labels + while let Some(((_, field), label)) = + Option::zip(fields_iter.peek(), expected_labels_iter.next()) + { + found_labels.push((get_range(field), *label)); + fields_iter.next(); + } + + // use numeric labels for excess fields + for (index, field) in fields_iter { + found_labels.push(( + get_range(field), + self.interner.borrow_mut().get_tuple_label(index), + )); + } + + self.push_message(Message::MismatchedFieldLabels { + range, + found_labels, + expected_labels: expected_labels.to_vec(), + }); + Err(()) + } + + fn check_record_fields( + &mut self, + range: ByteRange, + fields: &[F], + get_label: impl Fn(&F) -> (ByteRange, StringId), + labels: &'arena [StringId], + ) -> Result<(), ()> { + if fields.len() == labels.len() + && fields + .iter() + .zip(labels.iter()) + .all(|(field, type_label)| get_label(field).1 == *type_label) + { + return Ok(()); + } + + // TODO: improve handling of duplicate labels + self.push_message(Message::MismatchedFieldLabels { + range, + found_labels: fields.iter().map(get_label).collect(), + expected_labels: labels.to_vec(), + }); + Err(()) + } + /// Parse a source string into number, assuming an ASCII encoding. fn parse_ascii( &mut self, @@ -696,177 +761,6 @@ impl<'interner, 'arena> Context<'interner, 'arena> { term } - /// Check that a pattern matches an expected type. - fn check_pattern( - &mut self, - pattern: &Pattern, - expected_type: &ArcValue<'arena>, - ) -> CheckedPattern { - match pattern { - Pattern::Name(range, name) => CheckedPattern::Binder(*range, *name), - Pattern::Placeholder(range) => CheckedPattern::Placeholder(*range), - Pattern::StringLiteral(range, lit) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::U8Type, [])) => self.parse_ascii(*range, *lit, Const::U8), - Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16), - Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32), - Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64), - // Some((Prim::Array8Type, [len, _])) => todo!(), - // Some((Prim::Array16Type, [len, _])) => todo!(), - // Some((Prim::Array32Type, [len, _])) => todo!(), - // Some((Prim::Array64Type, [len, _])) => todo!(), - Some((Prim::ReportedError, _)) => None, - _ => { - let expected_type = self.pretty_print_value(expected_type); - self.push_message(Message::StringLiteralNotSupported { - range: *range, - expected_type, - }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(*range, constant), - None => CheckedPattern::ReportedError(*range), - } - } - Pattern::NumberLiteral(range, lit) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::U8Type, [])) => self.parse_number_radix(*range, *lit, Const::U8), - Some((Prim::U16Type, [])) => self.parse_number_radix(*range, *lit, Const::U16), - Some((Prim::U32Type, [])) => self.parse_number_radix(*range, *lit, Const::U32), - Some((Prim::U64Type, [])) => self.parse_number_radix(*range, *lit, Const::U64), - Some((Prim::S8Type, [])) => self.parse_number(*range, *lit, Const::S8), - Some((Prim::S16Type, [])) => self.parse_number(*range, *lit, Const::S16), - Some((Prim::S32Type, [])) => self.parse_number(*range, *lit, Const::S32), - Some((Prim::S64Type, [])) => self.parse_number(*range, *lit, Const::S64), - Some((Prim::F32Type, [])) => self.parse_number(*range, *lit, Const::F32), - Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64), - Some((Prim::ReportedError, _)) => None, - _ => { - let expected_type = self.pretty_print_value(expected_type); - self.push_message(Message::NumericLiteralNotSupported { - range: *range, - expected_type, - }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(*range, constant), - None => CheckedPattern::ReportedError(*range), - } - } - Pattern::BooleanLiteral(range, boolean) => { - let constant = match expected_type.match_prim_spine() { - Some((Prim::BoolType, [])) => match *boolean { - true => Some(Const::Bool(true)), - false => Some(Const::Bool(false)), - }, - _ => { - self.push_message(Message::BooleanLiteralNotSupported { range: *range }); - None - } - }; - - match constant { - Some(constant) => CheckedPattern::ConstLit(*range, constant), - None => CheckedPattern::ReportedError(*range), - } - } - Pattern::RecordLiteral(_, _) => todo!(), - Pattern::Tuple(_, _) => todo!(), - } - } - - /// Synthesize the type of a pattern. - fn synth_pattern( - &mut self, - pattern: &Pattern, - ) -> (CheckedPattern, ArcValue<'arena>) { - match pattern { - Pattern::Name(range, name) => { - let source = MetaSource::NamedPatternType(*range, *name); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::Binder(*range, *name), r#type) - } - Pattern::Placeholder(range) => { - let source = MetaSource::PlaceholderPatternType(*range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::Placeholder(*range), r#type) - } - Pattern::StringLiteral(range, _) => { - self.push_message(Message::AmbiguousStringLiteral { range: *range }); - let source = MetaSource::ReportedErrorType(*range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::ReportedError(*range), r#type) - } - Pattern::NumberLiteral(range, _) => { - self.push_message(Message::AmbiguousNumericLiteral { range: *range }); - let source = MetaSource::ReportedErrorType(*range); - let r#type = self.push_unsolved_type(source); - (CheckedPattern::ReportedError(*range), r#type) - } - Pattern::BooleanLiteral(range, val) => { - let r#const = Const::Bool(*val); - let r#type = self.bool_type.clone(); - (CheckedPattern::ConstLit(*range, r#const), r#type) - } - Pattern::RecordLiteral(_, _) => todo!(), - Pattern::Tuple(_, _) => todo!(), - } - } - - /// Check that the type of an annotated pattern matches an expected type. - fn check_ann_pattern( - &mut self, - pattern: &Pattern, - r#type: Option<&Term<'_, ByteRange>>, - expected_type: &ArcValue<'arena>, - ) -> CheckedPattern { - match r#type { - None => self.check_pattern(pattern, expected_type), - Some(r#type) => { - let range = r#type.range(); - let r#type = self.check(r#type, &self.universe.clone()); - let r#type = self.eval_env().eval(&r#type); - - match self.unification_context().unify(&r#type, expected_type) { - Ok(()) => self.check_pattern(pattern, &r#type), - Err(error) => { - let lhs = self.pretty_print_value(&r#type); - let rhs = self.pretty_print_value(expected_type); - self.push_message(Message::FailedToUnify { - range, - lhs, - rhs, - error, - }); - CheckedPattern::ReportedError(range) - } - } - } - } - } - - /// Synthesize the type of an annotated pattern. - fn synth_ann_pattern( - &mut self, - pattern: &Pattern, - r#type: Option<&Term<'_, ByteRange>>, - ) -> (CheckedPattern, ArcValue<'arena>) { - match r#type { - None => self.synth_pattern(pattern), - Some(r#type) => { - let r#type = self.check(r#type, &self.universe.clone()); - let type_value = self.eval_env().eval(&r#type); - (self.check_pattern(pattern, &type_value), type_value) - } - } - } - /// Push a local definition onto the context. /// The supplied `pattern` is expected to be irrefutable. fn push_local_def( @@ -886,6 +780,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { None } CheckedPattern::ReportedError(_) => None, + CheckedPattern::RecordLit(_, _, _) => todo!(), }; self.local_env.push_def(name, expr, r#type); @@ -911,6 +806,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { None } CheckedPattern::ReportedError(_) => None, + CheckedPattern::RecordLit(_, _, _) => todo!(), }; let expr = self.local_env.push_param(name, r#type); @@ -970,18 +866,10 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.check_fun_lit(*range, patterns, body_expr, &expected_type) } (Term::RecordLiteral(range, expr_fields), Value::RecordType(labels, types)) => { - // TODO: improve handling of duplicate labels - if expr_fields.len() != labels.len() - || Iterator::zip(expr_fields.iter(), labels.iter()) - .any(|(expr_field, type_label)| expr_field.label.1 != *type_label) + if self + .check_record_fields(*range, expr_fields, |field| field.label, labels) + .is_err() { - self.push_message(Message::MismatchedFieldLabels { - range: *range, - expr_labels: (expr_fields.iter()) - .map(|expr_field| expr_field.label) - .collect(), - type_labels: labels.to_vec(), - }); return core::Term::Prim(range.into(), Prim::ReportedError); } @@ -1045,33 +933,11 @@ impl<'interner, 'arena> Context<'interner, 'arena> { core::Term::FormatRecord(range.into(), labels, formats) } (Term::Tuple(range, elem_exprs), Value::RecordType(labels, types)) => { - if elem_exprs.len() != labels.len() { - let mut expr_labels = Vec::with_capacity(elem_exprs.len()); - let mut elem_exprs = elem_exprs.iter().enumerate().peekable(); - let mut label_iter = labels.iter(); - - // use the label names from the expected type - while let Some(((_, elem_expr), label)) = - Option::zip(elem_exprs.peek(), label_iter.next()) - { - expr_labels.push((elem_expr.range(), *label)); - elem_exprs.next(); - } - - // use numeric labels for excess elems - for (index, elem_expr) in elem_exprs { - expr_labels.push(( - elem_expr.range(), - self.interner.borrow_mut().get_tuple_label(index), - )); - } - - self.push_message(Message::MismatchedFieldLabels { - range: *range, - expr_labels, - type_labels: labels.to_vec(), - }); - return core::Term::Prim(range.into(), Prim::ReportedError); + if self + .check_tuple_fields(*range, elem_exprs, |expr| expr.range(), labels) + .is_err() + { + return core::Term::error(range.into()); } let mut types = types.clone(); @@ -2027,6 +1893,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { self.elab_match_unreachable(match_info, equations); core::Term::Prim(range.into(), Prim::ReportedError) } + CheckedPattern::RecordLit(_, _, _) => todo!(), } } None => self.elab_match_absurd(is_reachable, match_info), @@ -2116,6 +1983,7 @@ impl<'interner, 'arena> Context<'interner, 'arena> { default_branch = (None, self.scope.to_scope(default_expr) as &_); self.local_env.pop(); } + CheckedPattern::RecordLit(_, _, _) => todo!(), }; // A default pattern was found, check any unreachable patterns. @@ -2196,15 +2064,17 @@ impl_from_str_radix!(u64); /// Simple patterns that have had some initial elaboration performed on them #[derive(Debug)] -enum CheckedPattern { - /// Pattern that binds local variable - Binder(ByteRange, StringId), +enum CheckedPattern<'arena> { + /// Error sentinel + ReportedError(ByteRange), /// Placeholder patterns that match everything Placeholder(ByteRange), + /// Pattern that binds local variable + Binder(ByteRange, StringId), /// Constant literals ConstLit(ByteRange, Const), - /// Error sentinel - ReportedError(ByteRange), + /// Record literals + RecordLit(ByteRange, &'arena [StringId], &'arena [Self]), } /// Scrutinee of a match expression diff --git a/fathom/src/surface/elaboration/order.rs b/fathom/src/surface/elaboration/order.rs index 2d2df8541..531556b40 100644 --- a/fathom/src/surface/elaboration/order.rs +++ b/fathom/src/surface/elaboration/order.rs @@ -332,8 +332,12 @@ fn push_pattern(pattern: &Pattern, local_names: &mut Vec) { Pattern::StringLiteral(_, _) => {} Pattern::NumberLiteral(_, _) => {} Pattern::BooleanLiteral(_, _) => {} - Pattern::RecordLiteral(_, _) => todo!(), - Pattern::Tuple(_, _) => todo!(), + Pattern::RecordLiteral(_, fields) => fields + .iter() + .for_each(|field| push_pattern(&field.pattern, local_names)), + Pattern::Tuple(_, patterns) => patterns + .iter() + .for_each(|pattern| push_pattern(pattern, local_names)), } } @@ -346,7 +350,11 @@ fn pop_pattern(pattern: &Pattern, local_names: &mut Vec) { Pattern::StringLiteral(_, _) => {} Pattern::NumberLiteral(_, _) => {} Pattern::BooleanLiteral(_, _) => {} - Pattern::RecordLiteral(_, _) => todo!(), - Pattern::Tuple(_, _) => todo!(), + Pattern::RecordLiteral(_, fields) => fields + .iter() + .for_each(|field| pop_pattern(&field.pattern, local_names)), + Pattern::Tuple(_, patterns) => patterns + .iter() + .for_each(|pattern| pop_pattern(pattern, local_names)), } } diff --git a/fathom/src/surface/elaboration/patterns.rs b/fathom/src/surface/elaboration/patterns.rs new file mode 100644 index 000000000..60cb99228 --- /dev/null +++ b/fathom/src/surface/elaboration/patterns.rs @@ -0,0 +1,281 @@ +use super::*; + +impl<'interner, 'arena> Context<'interner, 'arena> { + /// Check that a pattern matches an expected type. + pub(super) fn check_pattern( + &mut self, + pattern: &Pattern<'_, ByteRange>, + expected_type: &ArcValue<'arena>, + ) -> CheckedPattern<'arena> { + let expected_type = self.elim_env().force(expected_type); + + match (pattern, expected_type.as_ref()) { + (Pattern::Name(range, name), _) => CheckedPattern::Binder(*range, *name), + (Pattern::Placeholder(range), _) => CheckedPattern::Placeholder(*range), + (Pattern::StringLiteral(range, lit), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::U8Type, [])) => self.parse_ascii(*range, *lit, Const::U8), + Some((Prim::U16Type, [])) => self.parse_ascii(*range, *lit, Const::U16), + Some((Prim::U32Type, [])) => self.parse_ascii(*range, *lit, Const::U32), + Some((Prim::U64Type, [])) => self.parse_ascii(*range, *lit, Const::U64), + // Some((Prim::Array8Type, [len, _])) => todo!(), + // Some((Prim::Array16Type, [len, _])) => todo!(), + // Some((Prim::Array32Type, [len, _])) => todo!(), + // Some((Prim::Array64Type, [len, _])) => todo!(), + Some((Prim::ReportedError, _)) => None, + _ => { + let expected_type = self.pretty_print_value(&expected_type); + self.push_message(Message::StringLiteralNotSupported { + range: *range, + expected_type, + }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + (Pattern::NumberLiteral(range, lit), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::U8Type, [])) => self.parse_number_radix(*range, *lit, Const::U8), + Some((Prim::U16Type, [])) => self.parse_number_radix(*range, *lit, Const::U16), + Some((Prim::U32Type, [])) => self.parse_number_radix(*range, *lit, Const::U32), + Some((Prim::U64Type, [])) => self.parse_number_radix(*range, *lit, Const::U64), + Some((Prim::S8Type, [])) => self.parse_number(*range, *lit, Const::S8), + Some((Prim::S16Type, [])) => self.parse_number(*range, *lit, Const::S16), + Some((Prim::S32Type, [])) => self.parse_number(*range, *lit, Const::S32), + Some((Prim::S64Type, [])) => self.parse_number(*range, *lit, Const::S64), + Some((Prim::F32Type, [])) => self.parse_number(*range, *lit, Const::F32), + Some((Prim::F64Type, [])) => self.parse_number(*range, *lit, Const::F64), + Some((Prim::ReportedError, _)) => None, + _ => { + let expected_type = self.pretty_print_value(&expected_type); + self.push_message(Message::NumericLiteralNotSupported { + range: *range, + expected_type, + }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + (Pattern::BooleanLiteral(range, boolean), _) => { + let constant = match expected_type.match_prim_spine() { + Some((Prim::BoolType, [])) => match *boolean { + true => Some(Const::Bool(true)), + false => Some(Const::Bool(false)), + }, + _ => { + self.push_message(Message::BooleanLiteralNotSupported { range: *range }); + None + } + }; + + match constant { + Some(constant) => CheckedPattern::ConstLit(*range, constant), + None => CheckedPattern::ReportedError(*range), + } + } + ( + Pattern::RecordLiteral(range, pattern_fields), + Value::RecordType(labels, telescope), + ) => { + if self + .check_record_fields(*range, pattern_fields, |field| field.label, labels) + .is_err() + { + return CheckedPattern::ReportedError(*range); + } + + let mut telescope = telescope.clone(); + let mut pattern_fields = pattern_fields.iter(); + let mut patterns = SliceVec::new(self.scope, labels.len()); + + while let Some((field, (r#type, next_telescope))) = Option::zip( + pattern_fields.next(), + self.elim_env().split_telescope(telescope.clone()), + ) { + let pattern = self.check_pattern(&field.pattern, &r#type); + telescope = next_telescope(Spanned::empty(Arc::new(Value::local_var( + self.local_env.len().next_level(), + )))); + patterns.push(pattern); + } + CheckedPattern::RecordLit(*range, labels, patterns.into()) + } + (Pattern::Tuple(range, elem_patterns), Value::RecordType(labels, telescope)) => { + if self + .check_tuple_fields(*range, elem_patterns, |pattern| pattern.range(), labels) + .is_err() + { + return CheckedPattern::ReportedError(*range); + } + + let mut telescope = telescope.clone(); + let mut elem_patterns = elem_patterns.iter(); + let mut patterns = SliceVec::new(self.scope, elem_patterns.len()); + + while let Some((pattern, (r#type, next_telescope))) = Option::zip( + elem_patterns.next(), + self.elim_env().split_telescope(telescope.clone()), + ) { + let pattern = self.check_pattern(pattern, &r#type); + telescope = next_telescope(Spanned::empty(Arc::new(Value::local_var( + self.local_env.len().next_level(), + )))); + patterns.push(pattern); + } + + CheckedPattern::RecordLit(*range, labels, patterns.into()) + } + _ => { + let range = pattern.range(); + let (pattern, r#type) = self.synth_pattern(pattern); + match self.unification_context().unify(&r#type, &expected_type) { + Ok(()) => pattern, + Err(error) => { + let lhs = self.pretty_print_value(&r#type); + let rhs = self.pretty_print_value(&expected_type); + self.push_message(Message::FailedToUnify { + range, + lhs, + rhs, + error, + }); + CheckedPattern::ReportedError(range) + } + } + } + } + } + + /// Synthesize the type of a pattern. + pub(super) fn synth_pattern( + &mut self, + pattern: &Pattern, + ) -> (CheckedPattern<'arena>, ArcValue<'arena>) { + match pattern { + Pattern::Name(range, name) => { + let source = MetaSource::NamedPatternType(*range, *name); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::Binder(*range, *name), r#type) + } + Pattern::Placeholder(range) => { + let source = MetaSource::PlaceholderPatternType(*range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::Placeholder(*range), r#type) + } + Pattern::StringLiteral(range, _) => { + self.push_message(Message::AmbiguousStringLiteral { range: *range }); + let source = MetaSource::ReportedErrorType(*range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::ReportedError(*range), r#type) + } + Pattern::NumberLiteral(range, _) => { + self.push_message(Message::AmbiguousNumericLiteral { range: *range }); + let source = MetaSource::ReportedErrorType(*range); + let r#type = self.push_unsolved_type(source); + (CheckedPattern::ReportedError(*range), r#type) + } + Pattern::BooleanLiteral(range, val) => { + let r#const = Const::Bool(*val); + let r#type = self.bool_type.clone(); + (CheckedPattern::ConstLit(*range, r#const), r#type) + } + Pattern::RecordLiteral(range, pattern_fields) => { + let (labels, pattern_fields) = + self.report_duplicate_labels(*range, pattern_fields, |f| f.label); + + let mut patterns = SliceVec::new(self.scope, labels.len()); + let mut types = SliceVec::new(self.scope, labels.len()); + + for field in pattern_fields { + let (pattern, r#type) = self.synth_pattern(&field.pattern); + patterns.push(pattern); + types.push(self.quote_env().quote(self.scope, &r#type)); + } + + let telescope = Telescope::new(self.local_env.exprs.clone(), types.into()); + ( + CheckedPattern::RecordLit(*range, labels, patterns.into()), + Spanned::new(range.into(), Arc::new(Value::RecordType(labels, telescope))), + ) + } + Pattern::Tuple(range, elem_patterns) => { + let mut interner = self.interner.borrow_mut(); + let labels = interner.get_tuple_labels(0..elem_patterns.len()); + let labels = self.scope.to_scope_from_iter(labels.iter().copied()); + + let mut patterns = SliceVec::new(self.scope, labels.len()); + let mut types = SliceVec::new(self.scope, labels.len()); + + for pattern in elem_patterns.iter() { + let (pattern, r#type) = self.synth_pattern(pattern); + patterns.push(pattern); + types.push(self.quote_env().quote(self.scope, &r#type)); + } + + let telescope = Telescope::new(self.local_env.exprs.clone(), types.into()); + ( + CheckedPattern::RecordLit(*range, labels, patterns.into()), + Spanned::new(range.into(), Arc::new(Value::RecordType(labels, telescope))), + ) + } + } + } + + /// Check that the type of an annotated pattern matches an expected type. + pub(super) fn check_ann_pattern( + &mut self, + pattern: &Pattern, + r#type: Option<&Term<'_, ByteRange>>, + expected_type: &ArcValue<'arena>, + ) -> CheckedPattern<'arena> { + match r#type { + None => self.check_pattern(pattern, expected_type), + Some(r#type) => { + let range = r#type.range(); + let r#type = self.check(r#type, &self.universe.clone()); + let r#type = self.eval_env().eval(&r#type); + + match self.unification_context().unify(&r#type, expected_type) { + Ok(()) => self.check_pattern(pattern, &r#type), + Err(error) => { + let lhs = self.pretty_print_value(&r#type); + let rhs = self.pretty_print_value(expected_type); + self.push_message(Message::FailedToUnify { + range, + lhs, + rhs, + error, + }); + CheckedPattern::ReportedError(range) + } + } + } + } + } + + /// Synthesize the type of an annotated pattern. + pub(super) fn synth_ann_pattern( + &mut self, + pattern: &Pattern, + r#type: Option<&Term<'_, ByteRange>>, + ) -> (CheckedPattern<'arena>, ArcValue<'arena>) { + match r#type { + None => self.synth_pattern(pattern), + Some(r#type) => { + let r#type = self.check(r#type, &self.universe.clone()); + let type_value = self.eval_env().eval(&r#type); + (self.check_pattern(pattern, &type_value), type_value) + } + } + } +} diff --git a/fathom/src/surface/elaboration/reporting.rs b/fathom/src/surface/elaboration/reporting.rs index 2caaffc03..99e5c9a25 100644 --- a/fathom/src/surface/elaboration/reporting.rs +++ b/fathom/src/surface/elaboration/reporting.rs @@ -41,8 +41,8 @@ pub enum Message { }, MismatchedFieldLabels { range: ByteRange, - expr_labels: Vec<(ByteRange, StringId)>, - type_labels: Vec, + found_labels: Vec<(ByteRange, StringId)>, + expected_labels: Vec, // TODO: add expected type // expected_type: Doc<_>, }, @@ -199,8 +199,8 @@ impl Message { } Message::MismatchedFieldLabels { range, - expr_labels, - type_labels, + found_labels: expr_labels, + expected_labels: type_labels, } => { let interner = interner.borrow(); let mut diagnostic_labels = Vec::with_capacity(expr_labels.len()); @@ -212,9 +212,11 @@ impl Message { match type_labels.next() { None => { let expr_label = interner.resolve(*expr_label).unwrap(); - diagnostic_labels.push(primary_label(range).with_message( - format!("unexpected field `{expr_label}`",), - )); + diagnostic_labels.push( + primary_label(range).with_message(format!( + "unexpected field `{expr_label}`", + )), + ); continue 'expr_labels; } Some(type_label) if expr_label == type_label => {