Float: Introduce floating point api normal

[Incarnation-p-lee]

• The normal and denormal api(s) are included.
• Add test cases for half, single and double floating point.
• Add normal to float interface.

[github-actions[bot]]

Test Results

    9 files  ±0     20 suites  ±0   0s :stopwatch: ±0s   641 tests ±0    641 :white_check_mark: ±0  0 :zzz: ±0  0 :x: ±0  2 053 runs  ±0  2 052 :white_check_mark: ±0  1 :zzz: ±0  0 :x: ±0 

Results for commit 504b043f. ± Comparison against base commit 34801ff9.

[Incarnation-p-lee]

BTW, there is another question about how to compare bitvec, assume we have code like below

type fp_bits = { 'n, 'n in {16, 32, 64}. bits('n) } /* Floating-point in bits. */
val      float_is_eq : (fp_bits, fp_bits) -> bool
function float_is_eq (op_0, op_1) = {
  let is_eq = op_0 == op_1;
  is_eq;
}

will have error similar to below

stderr:
Type error:
/home/pli/repos/sail/sail-fork/lib/float/eq.sail:43.14-26:
43 |  let is_eq = op_0 == op_1;
   |              ^----------^ checking function argument has type bitvector('ex290#)
   | Failed to prove constraint: 'ex292# == 'ex290#

The error message comes from Err_function_arg but I failed to get the point here.

[Alasdair]

It's because in this function the two fp_bits arguments could have different widths. The bitvector equality primitive is defined for bitvectors of the same length, i.e. forall 'n. (bits('n), bits('n)) -> bool.

type fp_bits = { 'n, 'n in {16, 32, 64}. bits('n) } /* Floating-point in bits. */
val      float_is_eq : (fp_bits, fp_bits) -> bool

You could do something like:

if length(op_0) == length(op_1) then op_0 == op_1 else false

But in this case it's probably better to do something like:

type valid_fp_bits('n : Int) -> Bool = 'n in {16, 32, 64}.

val float_is_eq : forall 'n, valid_fp_bits('n). (bits('n), bits('n)) -> bool

[Incarnation-p-lee]

It's because in this function the two fp_bits arguments could have different widths. The bitvector equality primitive is defined for bitvectors of the same length, i.e. forall 'n. (bits('n), bits('n)) -> bool.

type fp_bits = { 'n, 'n in {16, 32, 64}. bits('n) } /* Floating-point in bits. */
val      float_is_eq : (fp_bits, fp_bits) -> bool

You could do something like:

if length(op_0) == length(op_1) then op_0 == op_1 else false

But in this case it's probably better to do something like:

type valid_fp_bits('n : Int) -> Bool = 'n in {16, 32, 64}.

val float_is_eq : forall 'n, valid_fp_bits('n). (bits('n), bits('n)) -> bool

Thanks @Alasdair . Got the point here that the 'n in op_0 and op_1 are not the same 'n up to a point.