Remove explicit type annotations and redundant type variables in Vector code

[Timmmm]

This removes a load of the redundant type variables let 'n = num_elem in favour of using 'num_elem directly (and similarly for SEW).

I also removed a load of the explicit type annotations which are not needed.

[github-actions]

Test Results

398 tests  ±0   398 ✅ ±0   1m 48s ⏱️ +3s
  1 suites ±0     0 💤 ±0 
  1 files   ±0     0 ❌ ±0 

Results for commit 958c251. ± Comparison against base commit e145e11.

[pmundkur]

Have you checked against the vector test suite as well?

[pmundkur]

This overall seems like a nice cleanup.

I'm reluctant to remove type annotations like the above. They certainly helped me in understanding the code and the type errors I was seeing when refactoring the instruction retires. With all the conversions from bitvectors to vectors of bitvectors and back, I'd imagine they'll also be useful to new readers of the spec,

[nadime15]

Something I would like to add (though I am not 100% sure whether the following example works or not) is that sometimes it might not be possible to completely eliminate type annotations and type variables. For example, in this code:

function clause execute (VSHA2ms(vs2, vs1, vd)) = {
  let SEW      = get_sew();
  let LMUL_pow = get_lmul_pow();
  let num_elem = get_num_elem(LMUL_pow, SEW);

  assert(SEW == 32 | SEW == 64);

  let 'n = num_elem;
  let 'm = SEW;

  let vs2_val = read_vreg(num_elem, SEW, LMUL_pow, vs2);
  let vs1_val = read_vreg(num_elem, SEW, LMUL_pow, vs1);
  let vd_val  = read_vreg(num_elem, SEW, LMUL_pow, vd);
  
  var w : vector(20, bits('m)) = undefined; 
 ...
}

I need to define let 'm to initialize w, and suddenly, the vector type appears. I could use let 'SEW = get_sew(), but then I would have to deal with 'SEW and SEW.

And I agree with @pmundkur these type annotations have been really helpful in understanding the code. The reader has a much clearer picture of what’s actually happening. Yes, it's verbose, but in these cases, it's not too much and actually helps.

[arichardson]

I'm not convinced the vector('n, bits('m)) annotation really helps much.

Once you've looked at one function you know that reading a vreg gives you a num_elem vector of fixed-width bits(). IMO the type annotation is mostly noise?

[jordancarlin]

I think I agree with @arichardson on this one. Especially when we think about including this in the spec.

When reading this code in the spec, these extra type annotations add lots of noise and don't add much clarity (since most of these readers will not be as familiar with the Sail type system). For people who are actually developing the model, it is pretty clear once you take a look at what each of the functions does (which you'll need to do anyways).

[Timmmm]

Yeah I think it does help with readability a little, but not enough to justify the extra noise. Hopefully eventually we have proper IDE support so you can just hover variables to see their types, or use inlay hints.

We could even add type tooltips to asciidoctor-sail - that would be neat.

[pmundkur]

Getting an idea of the types involved in the lines I highlighted above requires looking up:

val read_vmask : forall 'n, 'n > 0. (int('n), bits(1), vregidx) -> bits('n)
val read_vreg : forall 'n 'm 'p, 'n >= 0 & 'm >= 0. (int('n), int('m), int('p), vregidx) -> vector('n, bits('m))

from vext_regs.sail. Other instructions require looking up init_masked_* from insts_vext_utils.sail and so on. That is harder to read than the simpler

let vm_val  : bits('n)  = ...
let vs1_val : vector('n, bits('m)) = ...

Looking up these functions in multiple other files and parsing these type signatures slows down the reader. Arguably, the above signatures are more complex than the

val carryless_mul : forall 'n, 'n > 0. (bits('n), bits('n)) -> bits(2 * 'n)
operator *_c = {carryless_mul}

of the initial version of #822, for which the review (which I heartily agreed with) said:

I'd avoid the overloaded operator to make it more clear even if it's longer.

Since the goal is to integrate the code from model into specs, it should be easy to read for someone with limited experience and not use too much clever stuff.

IMHO, the cleverness involved in reverse-engineering the types involved in the vector code is much higher.

I'd be okay with removing them once hover tooltips are available for readers of the rendered HTML and PDF, not just in IDEs, but not before.

I agree with the concern about the noise when included in the spec; perhaps we could render these with more conventional notation there? e.g.

let vm_val  : bits('n)  = ...
let vs1_val : bits('m)['n] = ...

or similar?

[Timmmm]

I think if we must keep the types then I might just abandon this change... not sure I can face changing them all to vector('num_elem, bits('SEW)) etc - just deleting them was tedious enough!

[pmundkur]

I totally understand; I can take a crack at that tedium next week if you'd like. The rest of the cleanup is quite nice and worth keeping.