Lean: Manage when clauses in match_bv

[arthur-adjedj]

This PR re-enables match_bv, and makes an attempt at managing when clauses correctly. This PR currently compiles RISC-V, but fails on a few C tests because of different limitations from the implementation:

• encdec and encdec_subrange: The elaboration of bitvector pattern-matching inside another (non-bitvector) pattern such as here currently fails, and leads to ill-formed syntax.
• option_nest and special_annot: some exhaustive patterns appear as let <pat> := <term>, but Lean does not manage to prove the exhaustiveness. A MWE of this issue is the following:

example : Bool :=
  /-missing cases:
    false-/
  match true with
    | true => true

This probably warrants a RFC on the Lean repo.

• vector_init: The output differs from the expected output:
  Expected:

ok
ok
v[i] = 1
v[i] = 2
v[i] = 3
v[i] = 9223372036854775807000

Actual output (it's missing the first ok):

ok
v[i] = 1
v[i] = 2
v[i] = 3
v[i] = 9223372036854775807000

• vector_subrange_pattern: some TODO_ARG_PATTERNs appear in a few places. My initial guess is that subrange patterns in function clauses are not deleted correctly by the remove_vector_subrange_pats rewrite pass, though I have not investigated this any further.

Furthermore, the make_cases_exhaustive rewrite pass does not work in the presence of patterns with when clauses, and failwiths when it encounters one, so I had to turn it off for now, leading to some matches getting an additional superfluous wildcard pattern-match here and there. It could probably be tweaked to simply give-up on the exhaustiveness checks whenever it encounters a when pattern.

I do not have more time to dedicate to this PR, so I will leave this here as is. Anyone feel free to try and fix these errors, or consider them to not matter too much and skip them in the test suite altogether.

[github-actions]

Test Results

   13 files     27 suites   0s ⏱️
  854 tests   848 ✅ 0 💤 0 ❌ 6 🔥
3 716 runs  3 710 ✅ 0 💤 0 ❌ 6 🔥

For more details on these errors, see this check.

Results for commit 13bdc46.

♻️ This comment has been updated with latest results.

[tobiasgrosser]

I just tested this. While the code looks great, I am getting 10 syntax and type errors on the full sail model and lean hangs at write_CSR when trying to build the full model. Here the code I am getting: https://github.com/opencompl/sail-riscv/pull/1/files

I currently get the error unexpected identifier; expected '_' with a line under reg:

def csr_name_map_forwards (arg_ : (BitVec 12)) : SailM String := do
  match_bv arg_ with
  | 001100000001 => do (pure "misa")
[...]
  | reg => do (hex_bits_12_forwards reg)

On the positive side, the bv_match model has 82000 lines vs the current model's 105000 lines.

[arthur-adjedj]

I guess I did mess something up before putting up the PR then. Thanks for taking the time to run this on your end, I'll have it hopefully fixed soon.

[javra]

  match true with
    | true => true

Would we assume this to be exhaustive because the expression syntactically matches a constructor? I'm not sure I'd count on this being changed. OCaml also gives me a non-exhaustiveness warning on the same match block.

[javra]

vector_init: The output differs from the expected output:

That's to do with literals 🤔 In the second match block it matches an Option (BitVec 16) and states the value in binary, but prints it as 1111111111111111 instead of 0b1111111111111111. I'll try to fix it.

[Alasdair]

Sail also considers such a match statement as incomplete:

Warning: Incomplete pattern match statement at test.sail:8.2-7:
8 |  match true {
  |  ^---^
  | 
The following expression is unmatched: false

But it's just a warning in Sail not an error, so you might have to add _ => <raise error> case in the translated code.

[javra]

@arthur-adjedj: Pushed a fix for vector_init to javra:match_bv (can't push to your repo).

[javra]

One idea to sidestep the issues generally for now: We could add a pragma to Sail to mark functions in which match_bv should be used. We automatically mark those functions created by forward and backward matches of bidirectional mappings.