Support patterns on arrays and opaque types.

[maximebuyse]

Closes #464 , #804

We add a phase to rewrite array patterns and usize/isize/i128/u128 patterns.

The phase rewrites them with if let guards.

For integer types the idea is to rewrite:

match x {
  1 => ...
}

as

match x {
  x if let true = (x == 1) => ...
}

For array/slice patterns, the idea is to rewrite:

match x {
  [a, b] => ...
}

as

match x {
 t if let (a, b) = (t[0], t[1]) => ...
}

In the case of slice patterns we also test the length of the slice in the condition:

match x {
  [a,.., b] => ...
}

becomes

match x {
 t if let Some(a, b) = if t.len() >= 2 then Some(t[0], t[t.len()-1]) else None => ...
}

In case the subpatterns of an array also need a guard to be rewritten, we rewrite using a pattern matching.

In case there is a disjunctive pattern with guards in the subpatterns, we try to take a boolean disjunction of the guards. When it is not possible we call the phase hoist_disjunctive_patterns and separate the arm into one arm for each case of the disjunction.

[maximebuyse]

@W95Psp Not sure that you got notified but this now ready for review!

[W95Psp]

I started to look at this a bit, there are issues with fresh vars I think https://hax-playground.cryspen.com/#fstar/7ec551634b/gist=898efdab8cc9c41469c5f28e72216b6e

[maximebuyse]

I started to look at this a bit, there are issues with fresh vars I think https://hax-playground.cryspen.com/#fstar/7ec551634b/gist=898efdab8cc9c41469c5f28e72216b6e

Good catch, I pushed a fix.

[franziskuskiefer]

Looks like there are conflicts that need to get resolved.

[franziskuskiefer]

@W95Psp @maximebuyse what's the state of this? Please update or close.

[github-actions[bot]]

This PR has been marked as stale due to a lack of activity for 60 days. If you believe this pull request is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[karthikbhargavan]

I have a branch I am working on to use refined integers for machine integers, which solves matching on size and u128. I would also like to redo the library so that arrays are lists, this would solve the issue here in a different way.

[franziskuskiefer]

We'll resolve this in other ways.