Fix compilation of the Lean backend (#914)

Sail needs to give some of the implicit arguments to Lean because they
are not deducible from the type of the arguments.

Author: ineol

model/riscv_insts_vext_utils.sail

@@ -191,9 +191,11 @@ function write_velem_quad(vd, SEW, input, i) = {
     write_single_element(SEW, 4 * i + j, vd, slice(input, j * SEW, SEW));
 }
 
-/* Extracts 8 consecutive vector elements starting from index 8*i and returns a vector */
-val get_velem_oct_vec : forall 'n 'm 'p, 'n > 0 & 8 <= 'm <= 64 & 'p >= 0 & 8 * 'p + 7 < 'n. (vector('n, bits('m)), int('p)) -> vector(8, bits('m))
-function get_velem_oct_vec(v, i) = [ v[8 * i + 7], v[8 * i + 6], v[8 * i + 5], v[8 * i + 4], v[8 * i + 3], v[8 * i + 2], v[8 * i + 1], v[8 * i] ]
+/* Extracts 8 consecutive vector elements starting from index 8*i and returns a
+ * vector. The parameter n is implicit to help proof the proof assistant
+ * backends infer its value. */
+val get_velem_oct_vec : forall 'n 'm 'p, 'n > 0 & 8 <= 'm <= 64 & 'p >= 0 & 8 * 'p + 7 < 'n. (implicit('n), vector('n, bits('m)), int('p)) -> vector(8, bits('m))
+function get_velem_oct_vec(n, v, i) = [ v[8 * i + 7], v[8 * i + 6], v[8 * i + 5], v[8 * i + 4], v[8 * i + 3], v[8 * i + 2], v[8 * i + 1], v[8 * i] ]
 
 /* Writes each of the 8 elements from the input vector to the vector register vd, starting at position 8 * i */
 val write_velem_oct_vec : forall 'p 'n, 8 <= 'n <= 64 & 'p >= 0. (vregidx, int('n), vector(8, bits('n)), int('p)) -> unit
@@ -490,8 +492,9 @@ function count_leadingzeros (sig, len) = {
   len - idx - 1
 }
 
-val vrev8 : forall 'n 'm, 'n >= 0 & 'm >= 0. (vector('n, bits('m * 8))) -> vector('n, bits('m * 8))
-function vrev8(input) = {
+/* The parameter m is implicit to help proof the proof assistant backends infer its value. */
+val vrev8 : forall 'n 'm, 'n >= 0 & 'm >= 0. (implicit('m), vector('n, bits('m * 8))) -> vector('n, bits('m * 8))
+function vrev8(m, input) = {
   var output : vector('n, bits('m * 8)) = input;
   foreach (i from 0 to ('n - 1)) {
     output[i] = rev8(input[i]);