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.