diff --git a/examples/in_progress/my_cosine.mlw b/examples/in_progress/my_cosine.mlw
index 763ebba41265ec0656512d660d19c0c26013aa91..fb42ead0d17b48f2b407752b1f34397708848a20 100644
--- a/examples/in_progress/my_cosine.mlw
+++ b/examples/in_progress/my_cosine.mlw
@@ -84,6 +84,6 @@ module Combined
assert {
Abs.abs (1.0 -. (t'real x) *. (t'real x) *. 0.5 -. cos (t'real x)) <=. 0x1p-24
};
- sub (1.0:t) (mul (mul x x) (0.5:t))
+ safe_sub (1.0:t) (safe_mul (safe_mul x x) (0.5:t))
end
diff --git a/stdlib/ieee_float.mlw b/stdlib/ieee_float.mlw
index 27a4306f4db64cfe9de43b1a58b50119395b7d37..9147b0fbe51575eeadf51783b06dc2b5599555d0 100644
--- a/stdlib/ieee_float.mlw
+++ b/stdlib/ieee_float.mlw
@@ -60,7 +60,7 @@ module GenericFloat
(** {3 Constructors and Constants} *)
- constant zeroF : t (** +0.0 *)
+ val constant zeroF : t (** +0.0 *)
(* exp_bias = 2^(sb - 1) - 1 *)
(* max_finite_exp = 2^sb - 2 - exp_bias = exp_bias *)
(* max_significand = (2^eb + 2^eb - 1) * 2^(1-eb) *)
@@ -70,25 +70,25 @@ module GenericFloat
(** {3 Operators} *)
- function add mode t t : t
- function sub mode t t : t
- function mul mode t t : t
- function div mode t t : t
+ val function add mode t t : t
+ val function sub mode t t : t
+ val function mul mode t t : t
+ val function div mode t t : t
(** The four basic operations, rounded in the given mode *)
- function abs t : t (** Absolute value *)
- function neg t : t (** Opposite *)
- function fma mode t t t : t (** Fused multiply-add: x * y + z *)
- function sqrt mode t : t (** Square root *)
+ val function abs t : t (** Absolute value *)
+ val function neg t : t (** Opposite *)
+ val function fma mode t t t : t (** Fused multiply-add: x * y + z *)
+ val function sqrt mode t : t (** Square root *)
- function (.-_) (x:t) : t = neg x
- function (.+) (x y:t) : t = add RNE x y
- function (.-) (x y:t) : t = sub RNE x y
- function (.*) (x y:t) : t = mul RNE x y
- function (./) (x y:t) : t = div RNE x y
+ let function (.-_) (x:t) : t = neg x
+ let function (.+) (x y:t) : t = add RNE x y
+ let function (.-) (x y:t) : t = sub RNE x y
+ let function (.*) (x y:t) : t = mul RNE x y
+ let function (./) (x y:t) : t = div RNE x y
(** Notations for operations in the default mode RNE *)
- function roundToIntegral mode t : t
+ val function roundToIntegral mode t : t
(** Rounding to an integer *)
function min t t : t
@@ -100,22 +100,26 @@ module GenericFloat
2) if either argument is NaN then the other argument is returned
+ Due to the unclear status of min and max in IEEE norm, we
+ intentionally not provide these function as "val"s to be used in
+ programs
+
*)
(** {3 Comparisons} *)
- predicate le t t
- predicate lt t t
- predicate ge (x:t) (y:t) = le y x
- predicate gt (x:t) (y:t) = lt y x
- predicate eq t t
+ val predicate le t t
+ val predicate lt t t
+ let predicate ge (x:t) (y:t) = le y x
+ let predicate gt (x:t) (y:t) = lt y x
+ val predicate eq t t
(** equality on floats, different from = since not (eq NaN NaN) *)
- predicate (.<=) (x:t) (y:t) = le x y
- predicate (.<) (x:t) (y:t) = lt x y
- predicate (.>=) (x:t) (y:t) = ge x y
- predicate (.>) (x:t) (y:t) = gt x y
- predicate (.=) (x:t) (y:t) = eq x y
+ let predicate (.<=) (x:t) (y:t) = le x y
+ let predicate (.<) (x:t) (y:t) = lt x y
+ let predicate (.>=) (x:t) (y:t) = ge x y
+ let predicate (.>) (x:t) (y:t) = gt x y
+ let predicate (.=) (x:t) (y:t) = eq x y
(** Notations *)
@@ -798,15 +802,15 @@ module Float_BV_Converter
(* with unsigned int as bitvector *)
type t (* float *)
- function of_ubv8 mode BV8.t : t
- function of_ubv16 mode BV16.t : t
- function of_ubv32 mode BV32.t : t
- function of_ubv64 mode BV64.t : t
+ val function of_ubv8 mode BV8.t : t
+ val function of_ubv16 mode BV16.t : t
+ val function of_ubv32 mode BV32.t : t
+ val function of_ubv64 mode BV64.t : t
- function to_ubv8 mode t : BV8.t
- function to_ubv16 mode t : BV16.t
- function to_ubv32 mode t : BV32.t
- function to_ubv64 mode t : BV64.t
+ val function to_ubv8 mode t : BV8.t
+ val function to_ubv16 mode t : BV16.t
+ val function to_ubv32 mode t : BV32.t
+ val function to_ubv64 mode t : BV64.t
use real.RealInfix
use real.FromInt as FromInt
diff --git a/stdlib/mach/float.mlw b/stdlib/mach/float.mlw
index d3d496971d60a4f25d32c4f48aab528c577befe2..c5249f0a65a39acb774210c601752090ea527936 100644
--- a/stdlib/mach/float.mlw
+++ b/stdlib/mach/float.mlw
@@ -16,7 +16,7 @@ module Single
predicate add_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x +. t'real y)
- val add (x y: t) : t
+ val safe_add (x y: t) : t
requires { [@expl:floating-point overflow]
add_pre_ieee x y \/ add_pre_real x y }
ensures { add_post_ieee x y result /\ add_post_real x y result }
@@ -33,7 +33,7 @@ module Single
predicate sub_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x -. t'real y)
- val sub (x y: t) : t
+ val safe_sub (x y: t) : t
requires { [@expl:floating-point overflow]
sub_pre_ieee x y \/ sub_pre_real x y }
ensures { sub_post_ieee x y result /\ sub_post_real x y result }
@@ -50,7 +50,7 @@ module Single
predicate mul_post_real (x:t) (y:t) (r:t) =
t'real r = round RNE (t'real x *. t'real y)
- val mul (x y: t) : t
+ val safe_mul (x y: t) : t
requires { [@expl:floating-point overflow]
mul_pre_ieee x y \/ mul_pre_real x y }
ensures { mul_post_ieee x y result /\ mul_post_real x y result }