-
Notifications
You must be signed in to change notification settings - Fork 14
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
Record/tuple patterns and new pattern match compiler and coverage checker #430
base: main
Are you sure you want to change the base?
Conversation
1ef64a4
to
d24c4f9
Compare
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.
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
fathom/src/surface/distillation.rs
Outdated
#[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
shift
is inefficient: we may want to add a newWeaken
term kind insteadwill become