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.

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

Add a simple exhaustiveness checker 🧐 #47

Merged
merged 3 commits into from
May 3, 2022
Merged

Conversation

jmackie
Copy link
Member

@jmackie jmackie commented May 2, 2022

More or less a verbatim Rust port of this blog post.

Raises an error for missing patterns, and raises warnings for redundant patterns.

Note that currently the Ditto pattern syntax consists only of constructors and variables:

/// A pattern to be matched.
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum Pattern {
/// A local constructor pattern.
LocalConstructor {
/// The source span for this pattern.
span: Span,
/// `Just`
constructor: ProperName,
/// Pattern arguments to the constructor.
arguments: Vec<Self>,
},
/// An imported constructor pattern.
ImportedConstructor {
/// The source span for this pattern.
span: Span,
/// `Maybe.Just`
constructor: FullyQualifiedProperName,
/// Pattern arguments to the constructor.
arguments: Vec<Self>,
},
/// A variable binding pattern.
Variable {
/// The source span for this pattern.
span: Span,
/// Name to bind.
name: Name,
},
/// An unused pattern.
Unused {
/// The source span for this pattern.
span: Span,
/// The unused name.
unused_name: UnusedName,
},
}

But this logic will get more elaborate once we add more pattern variants (e.g. #16).

@jmackie jmackie linked an issue May 2, 2022 that may be closed by this pull request
Comment on lines +469 to +490
for (ideal_argument, clause_argument) in ideal_arguments.iter().zip(clause_arguments) {
if let Some(arg_subst) = has_subst(supply, ideal_argument, clause_argument)? {
subst.extend(arg_subst)
} else {
return Ok(None);
}
}
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note (to self): got stuck on this bit for a while as the typeclass-y Haskell logic wasn't that obvious...

mconcat <$> (sequence (zipWith hasSubst pats1 pats2))

@codecov
Copy link

codecov bot commented May 2, 2022

Codecov Report

Merging #47 (0ece521) into main (2304f8b) will increase coverage by 0.82%.
The diff coverage is 97.20%.

@@            Coverage Diff             @@
##             main      #47      +/-   ##
==========================================
+ Coverage   76.88%   77.70%   +0.82%     
==========================================
  Files         109      111       +2     
  Lines        6948     7195     +247     
==========================================
+ Hits         5342     5591     +249     
+ Misses       1606     1604       -2     
Impacted Files Coverage Δ
crates/ditto-ast/src/kind.rs 100.00% <ø> (ø)
crates/ditto-ast/src/name.rs 77.77% <ø> (ø)
crates/ditto-ast/src/type.rs 82.55% <ø> (ø)
...ates/ditto-checker/src/typechecker/coverage/mod.rs 96.37% <96.37%> (ø)
...cker/src/module/type_declarations/tests/acyclic.rs 100.00% <100.00%> (ø)
crates/ditto-checker/src/result/type_error.rs 98.92% <100.00%> (+0.03%) ⬆️
crates/ditto-checker/src/result/warnings.rs 100.00% <100.00%> (ø)
...es/ditto-checker/src/typechecker/coverage/tests.rs 100.00% <100.00%> (ø)
crates/ditto-checker/src/typechecker/env.rs 97.87% <100.00%> (ø)
crates/ditto-checker/src/typechecker/mod.rs 96.40% <100.00%> (+0.14%) ⬆️
... and 4 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 2304f8b...0ece521. Read the comment docs.

Some(coverage::Error::NotCovered(ideal_patterns)) => {
let mut missing_patterns = ideal_patterns
.into_iter()
.map(|ideal_pattern| ideal_pattern.render())
Copy link
Member Author

@jmackie jmackie May 2, 2022

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm tempted to surround the rendered pattern in backticks to make it clearer that it's code (rather than prose) but that might be too visually noisy?

@jmackie jmackie merged commit 60be509 into main May 3, 2022
@jmackie jmackie deleted the exhaustiveness-checking branch May 3, 2022 08:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Exhaustiveness checking
1 participant