Add float_compose to complement float_decompose

This can be useful for example to make a generic canonical_NaN() function.
rems-project · Oct 29, 2024 · b9d9e51 · b9d9e51
1 parent fe50754
commit b9d9e51
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/lib/float/common.sail b/lib/float/common.sail
@@ -66,6 +66,9 @@ function float_decompose(op) = {
   }
 }
 
+val      float_compose : forall 'n, 'n in { 16, 32, 64, 128 }. float_bits('n) -> bits('n)
+function float_compose(op) = op.sign @ op.exp @ op.mantissa
+
 val      not : forall ('p : Bool). bool('p) -> bool(not('p))
 function not(b) = not_bool(b)