matchs simplification phases

[W95Psp]

Rust patterns are very expressive.
The different languages we target have variable expressiveness in patterns, and often are less expressive than Rust ones.

Issues related to the lack of expressivity of matches:

• Array/Slice Patterns are not supported #804
• F*: pattern matching is disallowed on usizes, isizes (+u128/i128/f32/f64) #464
• Phase to desugar as patterns (x @ subpattern) #833
• Unsupported Rust: range patterns #925
• Matches: guards are dropped! #807
• (deep) disjunctive patterns in backend that don't support them (e.g. F*) #463

[maximebuyse]

A first solution that we designed to deal with these issues would be to add if let guards for patterns in the Hax AST. When a guard is present in the initial rust code, we would import it in the AST as an if let guard (if let true = guard). Then we would add the following phases:

• Destruct opaque type patterns: This one would be parameterized by the list of opaque types to deal with (for example usize, isize, arrays for the f* backend) and how to rewrite the patterns for these types. For example match x { [a,..] => a, _ => 0} would rewrite as match x { v if let Some(a) = if v.len() >= 1 {Some(v[0])} else {None}=> a, _ => 0}
• A phase eliminating these if let patterns:

match x {
  None => 0, 
  Some(v) if let A(y) = v => y, 
  Some(B(y)) => y,
  _ => 1}

would rewrite as

match x {
  None => 0, 
  _ => 
    let r = match x {
      Some(v) => match v {A(y)=> Some(y), _ => None},
      _ => None};
    match r {
       Some(y) => y,
       None => match x {
         Some(B(y)) => y,
         _ => 1}
    }
}

• A phase eliminating nested disjunctive patterns: Rewrite them as shallow patterns. match x { Some(1|2) => 1, _ => 0} would rewrite as match x { Some(1)|Some(2) => 1, _ => 0}
• A phase eliminating shallow disjunctive patterns (for backends that don't support them): Duplicate the arms. match x { Some(1)|Some(2) => 1, _ => 0} would rewrite as match x { Some(1) => 1, Some(2) => 1, _ => 0}

[maximebuyse]

Sub-issue for if let guards: #814

[maximebuyse]

A first solution that we designed to deal with these issues would be to add if let guards for patterns in the Hax AST. When a guard is present in the initial rust code, we would import it in the AST as an if let guard (if let true = guard). Then we would add the following phases:

* Destruct opaque type patterns: This one would be parameterized by the list of opaque types to deal with (for example usize, isize, arrays for the f* backend) and how to rewrite the patterns for these types. For example `match x { [a,..] => a, _ => 0}` would rewrite as `match x { v if let Some(a) = if v.len() >= 1 {Some(v[0])} else {None}=> a, _ => 0}`

* A phase eliminating these `if let` patterns:

match x {
  None => 0, 
  Some(v) if let A(y) = v => y, 
  Some(B(y)) => y,
  _ => 1}

would rewrite as

match x {
  None => 0, 
  _ => 
    let r = match x {
      Some(v) => match v {A(y)=> Some(y), _ => None},
      _ => None};
    match r {
       Some(y) => y,
       None => match x {
         Some(B(y)) => y,
         _ => 1}
    }
}

* A phase eliminating nested disjunctive patterns: Rewrite them as shallow patterns. `match x { Some(1|2) => 1, _ => 0}` would rewrite as  `match x { Some(1)|Some(2) => 1, _ => 0}`

* A phase eliminating shallow disjunctive patterns (for backends that don't support them): Duplicate the arms. `match x { Some(1)|Some(2) => 1, _ => 0}`  would rewrite as `match x { Some(1) => 1, Some(2) => 1, _ => 0}`

To simplify we will allow guards only on whole patterns and not sub patterns. Deep disjunction elimination will need to take place before the phase introducing guards.

[maximebuyse]

For the phase taking care of opaque types and array patterns, we should implement a visitor working bottom-up and rewriting these patterns with IfLet guards (for example [a,b] rewrites to _ if let (a, b) = (t[0], t[1])) . We should somehow accumulate the guards and combine them (using tuples if there is no sequentiality, something more complicated if there is). Accumulation should be stored outside the visitor using a side effect.
If there is a disjunctive pattern somewhere with the need to introduce different captured variables (they may differ by the name or type) on different cases, we should raise an exception and hoist the disjunctions (reusing the phase already implemented for that), we don't apply the hoisting phase first because we still want to keep deep disjunctions in backends that support them.

Note on array/slice patterns in Rust:

• they are very similar so we should implement them as only one case in the AST (PArray), the type of the pattern should allow to distinguish (which is important because size checks can be needed for slices but not arrays).
• they contain 3 information: prefix, slice, suffix. prefix can be kept as args in PArray, but we should add slice and suffix. It seems like slice is most of the time a wildcard but it can also be a binding ([start @ .., "z"] for example), there should be no other case so maybe we can represent it with an option of an identifier?

We don't want to try making a fully parameterized phase as it would be hard too complicated with how phases are done. But we should parameterize it by some flags allowing to activate or not the features it implements (arrays, usizes, isizes, etc.).

[franziskuskiefer]

@maximebuyse are you actually working on this right now or shall it have a different status?

[maximebuyse]

@maximebuyse are you actually working on this right now or shall it have a different status?

I am working on it (more specifically on #464 and #804)

[maximebuyse]

I currently have an almost finished version for opaque types and array patterns. Three things are still missing:

• Parameterization of the phase (to choose which patterns to rewrite or not). This would require the signature of the phase to be different from other phases which I tried but it didn't work well with preprocessing of phases.
• Disjunctions when they are not rewritten with the same pattern and a combined guard. This will be handled by throwing an exception that will be caught to hoist the disjunction and separate the arm in multiple arms (to allow multiple guards). This requires to reuse the code in the phase that hoists disjunctive patterns but that also doesn't work well with the signature of the phase.
• Array patterns. Especially because of the case where subpatterns also have guards. Those guards can use variables captured by the pattern which means combining the guards (and capturing in the guard instead of the pattern) must be done with care.

[github-actions]

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