Support "or" patterns - multiple patterns for one match branch

[Timmmm]

Rust and OCaml, and I assume other languages that support Sail's style of pattern matching let you have multiple patterns for one match branch:

match some_int {
   0 | 1 => ...
   3 | 8 | 10 => ...

It would be nice if Sail supported this. Not a major issue at all but I and a few other people have been slightly caught up by it a few times.

Also I dunno if I like the | syntax because it has such strong ambiguity with bool/bitwise or. Like, this code is not obvious:

function foo(x : bits(5), a : bits(5), b : bits(5)) -> string =
   match x {
      a | b => "a or b",
      _ => "other",
  }

Does that mean it will match a or b, or a bitwise_or b? I would suggest using a comma if possible:

function foo(x : bits(5), a : bits(5), b : bits(5)) -> string =
   match x {
      a, b => "a or b",
      _ => "other",
  }

Maybe slightly unexpected to people familiar with Rust/OCaml/etc. and it does have potential confusion with tuples, but I reckon it's still better.

[Alasdair]

We actually have an or-pattern constructor internally. I think it's just a question of writing an elaboration pass that removes it, as not all our theorem prover targets support or-patterns.

Probably the simplest re-write is into guards:

match head {
  a | b => exp1,
  c => exp2
}

becomes

match head [
  d if match d { a => true, b => true, _ => false} => exp1,
  c => exp2,
}