Lean: Allow for match statments of heterogeneous bitvector length

[javra]

Fixes #1070.

[github-actions]

Test Results

   13 files  ±0     29 suites  ±0   0s ⏱️ ±0s
  841 tests ±0    841 ✅ ±0  0 💤 ±0  0 ❌ ±0 
3 516 runs  ±0  3 516 ✅ ±0  0 💤 ±0  0 ❌ ±0 

Results for commit f8be909. ± Comparison against base commit fbdcb92.

♻️ This comment has been updated with latest results.

[ineol]

def fp_sub (rm_3b : (BitVec 3)) (op1 : (BitVec k_m)) (op2 : (BitVec k_m)) : SailM (BitVec k_m) := do
  let (fflags, result_val) : (bits_fflags × (BitVec k_m)) ← do
    match (Sail.BitVec.length op2) with
    | 16 => (riscv_f16Sub rm_3b op1 op2)
    | 32 => (riscv_f32Sub rm_3b op1 op2)
    | _ => (riscv_f64Sub rm_3b op1 op2)
  (accrue_fflags fflags)
  (pure result_val)

I think there is an issue when the block of the let is monadic, because apparently we cannot put a type ascription in let x : typ <- ...

One solution is to do let x : typ := <- ... but it's not super pretty

[bacam]

This currently drops the optional arguments on recursive calls to doc_pat. Was that intentional?

[javra]

@bacam I don't think it matters, if there's no double typ ascriptions

@ineol Ah, thanks. Weirdly it accepts type ascriptions if it's an atomic binder, but not if there's a pattern 😢 Let's wait until someone weighs in on this topic then