Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add relevant matches to typed hole diagnostics #467

Merged
merged 1 commit into from
Jun 13, 2024
Merged

Add relevant matches to typed hole diagnostics #467

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 15 additions & 7 deletions numbat/src/diagnostic.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -473,15 +473,23 @@ impl ErrorDiagnostic for TypeCheckError {
TypeCheckError::ExponentiationNeedsTypeAnnotation(span) => d.with_labels(vec![span
.diagnostic_label(LabelStyle::Primary)
.with_message(inner_error)]),
TypeCheckError::TypedHoleInStatement(span, type_, statement) => d
.with_labels(vec![span
.diagnostic_label(LabelStyle::Primary)
.with_message(type_)])
.with_message("Found typed hole")
.with_notes(vec![
TypeCheckError::TypedHoleInStatement(span, type_, statement, matches) => {
let mut notes = vec![
format!("Found a hole of type '{type_}' in the statement:"),
format!(" {statement}"),
]),
];

if !matches.is_empty() {
notes.push("Relevant matches for this hole include:".into());
notes.push(format!(" {}", matches.join(", ")));
}

d.with_labels(vec![span
.diagnostic_label(LabelStyle::Primary)
.with_message(type_)])
.with_message("Found typed hole")
.with_notes(notes)
}
};
vec![d]
}
Expand Down
34 changes: 24 additions & 10 deletions numbat/src/typechecker/environment.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,8 +27,9 @@ pub struct FunctionMetadata {

#[derive(Clone, Debug)]
pub enum IdentifierKind {
/// A normal identifier (variable, unit) with the place where it has been defined
Normal(TypeScheme, Span),
/// A normal identifier (variable, unit) with the place where it has been defined.
/// The boolean flag signifies whether the identifier is a unit or not
Normal(TypeScheme, Span, bool),
/// A function
Function(FunctionSignature, FunctionMetadata),
/// Identifiers that are defined by the language: `_` and `ans` (see LAST_RESULT_IDENTIFIERS)
Expand All @@ -39,7 +40,7 @@ impl IdentifierKind {
fn get_type(&self) -> TypeScheme {
match self {
IdentifierKind::Predefined(t) => t.clone(),
IdentifierKind::Normal(t, _) => t.clone(),
IdentifierKind::Normal(t, _, _) => t.clone(),
IdentifierKind::Function(s, _) => s.fn_type.clone(),
}
}
Expand All @@ -51,14 +52,16 @@ pub struct Environment {
}

impl Environment {
pub fn add(&mut self, i: Identifier, type_: Type, span: Span) {
self.identifiers
.insert(i, IdentifierKind::Normal(TypeScheme::Concrete(type_), span));
pub fn add(&mut self, i: Identifier, type_: Type, span: Span, is_unit: bool) {
self.identifiers.insert(
i,
IdentifierKind::Normal(TypeScheme::Concrete(type_), span, is_unit),
);
}

pub fn add_scheme(&mut self, i: Identifier, scheme: TypeScheme, span: Span) {
pub fn add_scheme(&mut self, i: Identifier, scheme: TypeScheme, span: Span, is_unit: bool) {
self.identifiers
.insert(i, IdentifierKind::Normal(scheme, span));
.insert(i, IdentifierKind::Normal(scheme, span, is_unit));
}

pub(crate) fn add_function(
Expand All @@ -84,6 +87,17 @@ impl Environment {
self.identifiers.keys()
}

pub fn iter_relevant_matches(&self) -> impl Iterator<Item = (&Identifier, TypeScheme)> {
self.identifiers
.iter()
.filter(|(_, kind)| match kind {
IdentifierKind::Normal(_, _, true) => false,
IdentifierKind::Predefined(..) => false,
_ => true,
})
.map(|(id, kind)| (id, kind.get_type()))
}

pub(crate) fn get_function_info(
&self,
name: &str,
Expand All @@ -97,7 +111,7 @@ impl Environment {
pub(crate) fn generalize_types(&mut self, dtype_variables: &[TypeVariable]) {
for (_, kind) in self.identifiers.iter_mut() {
match kind {
IdentifierKind::Normal(t, _) => {
IdentifierKind::Normal(t, _, _) => {
t.generalize(dtype_variables);
}
IdentifierKind::Function(signature, _) => {
Expand All @@ -115,7 +129,7 @@ impl ApplySubstitution for Environment {
fn apply(&mut self, substitution: &Substitution) -> Result<(), SubstitutionError> {
for (_, kind) in self.identifiers.iter_mut() {
match kind {
IdentifierKind::Normal(t, _) => {
IdentifierKind::Normal(t, _, _) => {
t.apply(substitution)?;
}
IdentifierKind::Function(signature, _) => {
Expand Down
2 changes: 1 addition & 1 deletion numbat/src/typechecker/error.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -150,7 +150,7 @@ pub enum TypeCheckError {
DerivedUnitDefinitionMustNotBeGeneric(Span),

#[error("Typed hole")]
TypedHoleInStatement(Span, String, String),
TypedHoleInStatement(Span, String, String, Vec<String>),

#[error("Multiple typed holes in statement")]
MultipleTypedHoles(Span),
Expand Down
20 changes: 16 additions & 4 deletions numbat/src/typechecker/mod.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1139,7 +1139,7 @@ impl TypeChecker {

for (name, _) in decorator::name_and_aliases(identifier, decorators) {
self.env
.add(name.clone(), type_deduced.clone(), *identifier_span);
.add(name.clone(), type_deduced.clone(), *identifier_span, false);

self.value_namespace.add_identifier_allow_override(
name.clone(),
Expand Down Expand Up @@ -1183,8 +1183,12 @@ impl TypeChecker {
.into()
};
for (name, _) in decorator::name_and_aliases(unit_name, decorators) {
self.env
.add(name.clone(), Type::Dimension(type_specified.clone()), *span);
self.env.add(
name.clone(),
Type::Dimension(type_specified.clone()),
*span,
true,
);
}

typed_ast::Statement::DefineBaseUnit(
Expand Down Expand Up @@ -1261,7 +1265,7 @@ impl TypeChecker {

for (name, _) in decorator::name_and_aliases(identifier, decorators) {
self.env
.add(name.clone(), type_deduced.clone(), *identifier_span);
.add(name.clone(), type_deduced.clone(), *identifier_span, true);
}
typed_ast::Statement::DefineDerivedUnit(
identifier.clone(),
Expand Down Expand Up @@ -1350,6 +1354,7 @@ impl TypeChecker {
parameter.clone(),
TypeScheme::make_quantified(parameter_type.clone()),
*parameter_span,
false,
);
typed_parameters.push((*parameter_span, parameter.clone(), parameter_type));
}
Expand Down Expand Up @@ -1764,6 +1769,13 @@ impl TypeChecker {
span,
type_of_hole.to_readable_type(&self.registry).to_string(),
elaborated_statement.pretty_print().to_string(),
self.env
.iter_relevant_matches()
.filter(|(_, t)| t == &type_of_hole)
.take(10)
.map(|(n, _)| n)
.cloned()
.collect(),
));
}

Expand Down
10 changes: 5 additions & 5 deletions numbat/src/typechecker/tests/type_inference.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -403,26 +403,26 @@ fn recursive_functions() {
fn typed_holes() {
assert!(matches!(
get_typecheck_error("a + ?"),
TypeCheckError::TypedHoleInStatement(_, type_, _) if type_ == "A"
TypeCheckError::TypedHoleInStatement(_, type_, _, _) if type_ == "A"
));

assert!(matches!(
get_typecheck_error("c + a × ?"),
TypeCheckError::TypedHoleInStatement(_, type_, _) if type_ == "B"
TypeCheckError::TypedHoleInStatement(_, type_, _, _) if type_ == "B"
));

assert!(matches!(
get_typecheck_error("let x: B = c / ?"),
TypeCheckError::TypedHoleInStatement(_, type_, _) if type_ == "A"
TypeCheckError::TypedHoleInStatement(_, type_, _, _) if type_ == "A"
));

assert!(matches!(
get_typecheck_error("if true then a else ?"),
TypeCheckError::TypedHoleInStatement(_, type_, _) if type_ == "A"
TypeCheckError::TypedHoleInStatement(_, type_, _, _) if type_ == "A"
));

assert!(matches!(
get_typecheck_error("let x: C = ?(a, b)"),
TypeCheckError::TypedHoleInStatement(_, type_, _) if type_ == "Fn[(A, B) -> A × B]"
TypeCheckError::TypedHoleInStatement(_, type_, _, _) if type_ == "Fn[(A, B) -> A × B]"
));
}
1 change: 1 addition & 0 deletions numbat/src/typechecker/type_scheme.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -141,6 +141,7 @@ impl TypeScheme {
// Generate qualified type
let bounds = dtype_variables
.iter()
.filter(|v| type_.contains(v, true))
.map(|v| Bound::IsDim(Type::TVar(v.clone())))
.collect();
let qualified_type = QualifiedType::new(type_.clone(), bounds);
Expand Down
Loading