aboutsummaryrefslogtreecommitdiff
path: root/kernel/float64.mli
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-05-22 11:59:43 +0200
committerPierre-Marie Pédrot2020-05-22 11:59:43 +0200
commit7e09ee64b721baf0803c5fdb91c4687fded112cb (patch)
tree9f3f691be9b0500e846fee282183d5e0975bec8c /kernel/float64.mli
parent90389df4d03a6a6232e0372ff3efee720f85d284 (diff)
parent04e22abe4378e29671def7b4d9c7e509c58ef6b6 (diff)
Merge PR #11986: [primitive floats] Add low level printing
Ack-by: SkySkimmer Reviewed-by: ppedrot
Diffstat (limited to 'kernel/float64.mli')
-rw-r--r--kernel/float64.mli12
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/float64.mli b/kernel/float64.mli
index d43ff4553f..0afbfa89da 100644
--- a/kernel/float64.mli
+++ b/kernel/float64.mli
@@ -19,9 +19,19 @@ val is_nan : t -> bool
val is_infinity : t -> bool
val is_neg_infinity : t -> bool
-val to_string : t -> string
val of_string : string -> t
+(** Print a float exactly as an hexadecimal value (exact decimal
+ * printing would be possible but sometimes requires more than 700
+ * digits). *)
+val to_hex_string : t -> string
+
+(** Print a float as a decimal value. The printing is not exact (the
+ * real value printed is not always the given floating-point value),
+ * however printing is precise enough that forall float [f],
+ * [of_string (to_decimal_string f) = f]. *)
+val to_string : t -> string
+
val compile : t -> string
val of_float : float -> t