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 TotalityCheck and tests #103

Merged
merged 8 commits into from
Nov 6, 2018
Merged

Add TotalityCheck and tests #103

merged 8 commits into from
Nov 6, 2018

Conversation

johnynek
Copy link
Owner

@johnynek johnynek commented Nov 4, 2018

When we expanded the power of the patterns the naive exhaustivity checking was removed because it wouldn't work.

Since then, we have actually been rolling with no match exhaustivity checking.

This adds code to check all patterns are exhaustive. It seems that with the current pattern language, we actually don't need to typecheck to do totality checking, which is interesting. That might be a good property to maintain (and maybe is always, or almost always true...)

This turns out to be a bit tricky and I had to derive some formulas, which I just left in the comments. I have pretty good tests of the checker, but will see a better test when I wire it into the compiler.

@codecov-io
Copy link

codecov-io commented Nov 4, 2018

Codecov Report

Merging #103 into master will increase coverage by 1.82%.
The diff coverage is 91.66%.

Impacted file tree graph

@@            Coverage Diff             @@
##           master     #103      +/-   ##
==========================================
+ Coverage   71.25%   73.07%   +1.82%     
==========================================
  Files          37       38       +1     
  Lines        2007     2206     +199     
  Branches       47       59      +12     
==========================================
+ Hits         1430     1612     +182     
- Misses        577      594      +17
Impacted Files Coverage Δ
...e/src/main/scala/org/bykn/bosatsu/rankn/Type.scala 93.22% <100%> (+0.36%) ⬆️
...rc/main/scala/org/bykn/bosatsu/rankn/TypeEnv.scala 100% <100%> (ø) ⬆️
core/src/main/scala/org/bykn/bosatsu/Pattern.scala 93.1% <87.5%> (-2.14%) ⬇️
...rc/main/scala/org/bykn/bosatsu/TotalityCheck.scala 91.62% <91.62%> (ø)

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 056b243...6ad9ddc. Read the comment docs.

@johnynek
Copy link
Owner Author

johnynek commented Nov 6, 2018

This isn't perfect, but it is already big enough.

I'm going to merge then look for more tests to gain confidence.

I think it is important to note: we actually don't need perfect set operations on patterns: we just need to accurately detect if any branches are missing. Giving an exact minimal covering of the missing branches is not required.

@johnynek johnynek merged commit b6f96f9 into master Nov 6, 2018
* then make:
* Struct(d1, _, _), Struct(_, d2, _), ...
*/
def poke[M[_]: Applicative, A](items: List[A])(fn: A => M[List[A]]): M[List[List[A]]] =
Copy link
Owner Author

Choose a reason for hiding this comment

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

TODO: as a follow up, this can be handled recursively: we already have handling below. I'm also suspect of this method.

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.

None yet

2 participants