-
Notifications
You must be signed in to change notification settings - Fork 12
Record/tuple patterns and new pattern match compiler and coverage checker #430
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
base: main
Are you sure you want to change the base?
Conversation
1ef64a4 to
d24c4f9
Compare
wezm
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'll leave a full review of this to when Brendan returns from leave. Just noting one small issue with links in docs.
brendanzab
left a comment
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Still need to look deeper into this to try to understand the algorithm… there’s a bit to take in but it’s looking neat!
|
We could maybe pull out the rust upgrade into a separate PR if it helps clean things up. |
That was the intention, not sure why github included those commits in the PR. Fixed it now. |
792176f to
c31c1d1
Compare
c31c1d1 to
9dcfafa
Compare
7003365 to
86aa0c6
Compare
8dbe29a to
25f66bc
Compare
| #[allow(clippy::type_complexity)] | ||
| fn match_if_then_else<'arena>( | ||
| branches: &'arena [(Const, core::Term<'arena>)], | ||
| default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>, | ||
| ) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> { | ||
| ) -> Option<( | ||
| (Option<Option<StringId>>, &'arena core::Term<'arena>), | ||
| (Option<Option<StringId>>, &'arena core::Term<'arena>), | ||
| )> { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I’m… not really understanding what’s going on with the Option<Option<StringId>>s for the then and else branches?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In cases of the form
match x {
true => ...,
_ => ...,
}
or
match x {
false => ...,
_ => ...,
}
We have to push _ onto local_names, or else we get confusing bugs in distillation output. Alternatively, we could only distill matches to if-then-else syntax if they are of the form
match x {
true => ...,
false => ...,
}
|
Sorry for the slowness - taking a bit of time to get into this one |
e91303c to
cccdfb7
Compare
e3ff50e to
4cef50e
Compare
|
I’ve been looking at this more in depth locally. Doing a bit of messing around to understand it a bit more and tweaking the implementation a bit. While it’s big, I think it would be better to squash it into a single commit as it kind of only works all together. One nit-pick: could we use the actual the actual type names rather than |
4cef50e to
bc914d7
Compare
I think the preferred Rust style is to use
|
bc914d7 to
3917860
Compare
| let columns = | ||
| vec![(CheckedPattern::Placeholder(*range), scrut.clone()); ctor.arity()]; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why is it ok to duplicate these without updating scrut?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A wildcard pattern leaves the scrutinee unchanged: it does not project further into it. It is duplicated ctor.arity() times because the algorithm relies on the matrix always being rectangular.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh, was more wondering about the type of the scrutinee - does it need to be updated for each pattern (seeing as it seems like this is based on the arity of the constructor) or is that unecessary?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
No, updating the type is also unnecessary. The scrutinee is left completely unchanged by wildcard patterns because wildcard patterns match anything: they don't inspect or transform the scrutinee in any way
fdd2ba7 to
90af406
Compare
|
I’ve looked into merging this, trying to do some cleaning up (see: Kmeakin/fathom@pattern-matching...brendanzab:fathom:pattern-matching-cleanups), but I don’t think it is ready yet. Some of the pattern matching compilation is self-contained and can be iterated on for improved clarity, but my big fear is how it impacts the handling of local bindings in the elaborator. The |
90af406 to
8e82b43
Compare
8e82b43 to
696a03e
Compare
Future work
shiftis inefficient: we may want to add a newWeakenterm kind insteadwill become