diff --git a/ml-proto/spec/f32.ml b/ml-proto/spec/f32.ml index 1befffac3b..17a016f834 100644 --- a/ml-proto/spec/f32.ml +++ b/ml-proto/spec/f32.ml @@ -1,126 +1,7 @@ -(* WebAssembly-compatible f32 implementation *) - -(* - * We represent f32 as its bits in an int32 so that we can be assured that all - * the bits of NaNs are preserved in all cases where we require them to be. - *) -type t = int32 -type bits = int32 - -(* TODO: Do something meaningful with nondeterminism *) -let bare_nan = 0x7f800000l -let nondeterministic_nan = 0x7fc0f0f0l - -let of_float = Int32.bits_of_float -let to_float = Int32.float_of_bits - -let of_bits x = x -let to_bits x = x - -(* Most arithmetic ops that return NaN return a nondeterministic NaN *) -let arith_of_bits = to_float -let bits_of_arith f = if f <> f then nondeterministic_nan else of_float f - -let zero = of_float 0.0 - -let add x y = bits_of_arith ((arith_of_bits x) +. (arith_of_bits y)) -let sub x y = bits_of_arith ((arith_of_bits x) -. (arith_of_bits y)) -let mul x y = bits_of_arith ((arith_of_bits x) *. (arith_of_bits y)) -let div x y = bits_of_arith ((arith_of_bits x) /. (arith_of_bits y)) - -let sqrt x = bits_of_arith (Pervasives.sqrt (arith_of_bits x)) - -let ceil x = bits_of_arith (Pervasives.ceil (arith_of_bits x)) -let floor x = bits_of_arith (Pervasives.floor (arith_of_bits x)) - -let trunc x = - let xf = arith_of_bits x in - (* preserve the sign of zero *) - if xf = 0.0 then x else - (* trunc is either ceil or floor depending on which one is toward zero *) - let f = if xf < 0.0 then Pervasives.ceil xf else Pervasives.floor xf in - bits_of_arith f - -let nearest x = - let xf = arith_of_bits x in - (* preserve the sign of zero *) - if xf = 0.0 then x else - (* nearest is either ceil or floor depending on which is nearest or even *) - let u = Pervasives.ceil xf in - let d = Pervasives.floor xf in - let um = abs_float (xf -. u) in - let dm = abs_float (xf -. d) in - let u_or_d = um < dm || - (um = dm && let h = u /. 2. in Pervasives.floor h = h) in - let f = if u_or_d then u else d in - bits_of_arith f - -let min x y = - let xf = arith_of_bits x in - let yf = arith_of_bits y in - (* min -0 0 is -0 *) - if xf = yf then Int32.logor x y else - if xf < yf then x else - if xf > yf then y else - nondeterministic_nan - -let max x y = - let xf = arith_of_bits x in - let yf = arith_of_bits y in - (* max -0 0 is 0 *) - if xf = yf then Int32.logand x y else - if xf > yf then x else - if xf < yf then y else - nondeterministic_nan - -(* abs, neg, and copysign are purely bitwise operations, even on NaN values *) -let abs x = - Int32.logand x Int32.max_int - -let neg x = - Int32.logxor x Int32.min_int - -let copysign x y = - Int32.logor (abs x) (Int32.logand y Int32.min_int) - -let eq x y = (arith_of_bits x) = (arith_of_bits y) -let ne x y = (arith_of_bits x) <> (arith_of_bits y) -let lt x y = (arith_of_bits x) < (arith_of_bits y) -let gt x y = (arith_of_bits x) > (arith_of_bits y) -let le x y = (arith_of_bits x) <= (arith_of_bits y) -let ge x y = (arith_of_bits x) >= (arith_of_bits y) - -let of_signless_string x len = - if x <> "nan" && - (len > 7) && - (String.sub x 0 6) = "nan(0x" && (String.get x (len - 1)) = ')' then - (let s = Int32.of_string (String.sub x 4 ((len - 5))) in - if s = Int32.zero then - raise (Failure "nan payload must not be zero") - else if Int32.logand s bare_nan <> Int32.zero then - raise (Failure "nan payload must not overlap with exponent bits") - else if s < Int32.zero then - raise (Failure "nan payload must not overlap with sign bit") - else - Int32.logor s bare_nan) - else - (* TODO: OCaml's float_of_string is insufficient *) - of_float (float_of_string x) - -let of_string x = - let len = String.length x in - if len > 0 && (String.get x 0) = '-' then - neg (of_signless_string (String.sub x 1 (len - 1)) (len - 1)) - else if len > 0 && (String.get x 0) = '+' then - of_signless_string (String.sub x 1 (len - 1)) (len - 1) - else - of_signless_string x len - -let to_string x = - (if x < Int32.zero then "-" else "") ^ let a = abs x in - let af = arith_of_bits a in - if af <> af then - ("nan(0x" ^ (Printf.sprintf "%lx" (abs (Int32.logxor bare_nan a))) ^ ")") - else - (* TODO: OCaml's string_of_float is insufficient *) - string_of_float (to_float a) +include Float.Make(struct + include Int32 + let nondeterministic_nan = 0x7fc0f0f0l + let bare_nan = 0x7f800000l + let print_nan_significand_digits a = + Printf.sprintf "%lx" (abs (Int32.logxor bare_nan a)) + end) diff --git a/ml-proto/spec/f32.mli b/ml-proto/spec/f32.mli deleted file mode 100644 index 1174efaa43..0000000000 --- a/ml-proto/spec/f32.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* WebAssembly-compatible f32 implementation *) - -type t -type bits = int32 - -val of_float : float -> t -val to_float : t -> float -val of_bits : bits -> t -val to_bits : t -> bits - -val zero : t - -val add : t -> t -> t -val sub : t -> t -> t -val mul : t -> t -> t -val div : t -> t -> t -val sqrt : t -> t -val min : t -> t -> t -val max : t -> t -> t -val ceil : t -> t -val floor : t -> t -val trunc : t -> t -val nearest : t -> t -val abs : t -> t -val neg : t -> t -val copysign : t -> t -> t -val eq : t -> t -> bool -val ne : t -> t -> bool -val lt : t -> t -> bool -val le : t -> t -> bool -val gt : t -> t -> bool -val ge : t -> t -> bool - -val of_string : string -> t -val to_string : t -> string diff --git a/ml-proto/spec/f64.ml b/ml-proto/spec/f64.ml index 460548055a..e55d99f137 100644 --- a/ml-proto/spec/f64.ml +++ b/ml-proto/spec/f64.ml @@ -1,126 +1,7 @@ -(* WebAssembly-compatible f64 implementation *) - -(* - * We represent f64 as its bits in an int64 so that we can be assured that all - * the bits of NaNs are preserved in all cases where we require them to be. - *) -type t = int64 -type bits = int64 - -(* TODO: Do something meaningful with nondeterminism *) -let bare_nan = 0x7ff0000000000000L -let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL - -let of_float = Int64.bits_of_float -let to_float = Int64.float_of_bits - -let of_bits x = x -let to_bits x = x - -(* Most arithmetic ops that return NaN return a nondeterministic NaN *) -let arith_of_bits = to_float -let bits_of_arith f = if f <> f then nondeterministic_nan else of_float f - -let zero = of_float 0.0 - -let add x y = bits_of_arith ((arith_of_bits x) +. (arith_of_bits y)) -let sub x y = bits_of_arith ((arith_of_bits x) -. (arith_of_bits y)) -let mul x y = bits_of_arith ((arith_of_bits x) *. (arith_of_bits y)) -let div x y = bits_of_arith ((arith_of_bits x) /. (arith_of_bits y)) - -let sqrt x = bits_of_arith (Pervasives.sqrt (arith_of_bits x)) - -let ceil x = bits_of_arith (Pervasives.ceil (arith_of_bits x)) -let floor x = bits_of_arith (Pervasives.floor (arith_of_bits x)) - -let trunc x = - let xf = arith_of_bits x in - (* preserve the sign of zero *) - if xf = 0.0 then x else - (* trunc is either ceil or floor depending on which one is toward zero *) - let f = if xf < 0.0 then Pervasives.ceil xf else Pervasives.floor xf in - bits_of_arith f - -let nearest x = - let xf = arith_of_bits x in - (* preserve the sign of zero *) - if xf = 0.0 then x else - (* nearest is either ceil or floor depending on which is nearest or even *) - let u = Pervasives.ceil xf in - let d = Pervasives.floor xf in - let um = abs_float (xf -. u) in - let dm = abs_float (xf -. d) in - let u_or_d = um < dm || - (um = dm && let h = u /. 2. in Pervasives.floor h = h) in - let f = if u_or_d then u else d in - bits_of_arith f - -let min x y = - let xf = arith_of_bits x in - let yf = arith_of_bits y in - (* min -0 0 is -0 *) - if xf = yf then Int64.logor x y else - if xf < yf then x else - if xf > yf then y else - nondeterministic_nan - -let max x y = - let xf = arith_of_bits x in - let yf = arith_of_bits y in - (* max -0 0 is 0 *) - if xf = yf then Int64.logand x y else - if xf > yf then x else - if xf < yf then y else - nondeterministic_nan - -(* abs, neg, and copysign are purely bitwise operations, even on NaN values *) -let abs x = - Int64.logand x Int64.max_int - -let neg x = - Int64.logxor x Int64.min_int - -let copysign x y = - Int64.logor (abs x) (Int64.logand y Int64.min_int) - -let eq x y = (arith_of_bits x) = (arith_of_bits y) -let ne x y = (arith_of_bits x) <> (arith_of_bits y) -let lt x y = (arith_of_bits x) < (arith_of_bits y) -let gt x y = (arith_of_bits x) > (arith_of_bits y) -let le x y = (arith_of_bits x) <= (arith_of_bits y) -let ge x y = (arith_of_bits x) >= (arith_of_bits y) - -let of_signless_string x len = - if x <> "nan" && - (len > 7) && - (String.sub x 0 6) = "nan(0x" && (String.get x (len - 1)) = ')' then - (let s = Int64.of_string (String.sub x 4 ((len - 5))) in - if s = Int64.zero then - raise (Failure "nan payload must not be zero") - else if Int64.logand s bare_nan <> Int64.zero then - raise (Failure "nan payload must not overlap with exponent bits") - else if s < Int64.zero then - raise (Failure "nan payload must not overlap with sign bit") - else - Int64.logor s bare_nan) - else - (* TODO: OCaml's float_of_string is insufficient *) - of_float (float_of_string x) - -let of_string x = - let len = String.length x in - if len > 0 && (String.get x 0) = '-' then - neg (of_signless_string (String.sub x 1 (len - 1)) (len - 1)) - else if len > 0 && (String.get x 0) = '+' then - of_signless_string (String.sub x 1 (len - 1)) (len - 1) - else - of_signless_string x len - -let to_string x = - (if x < Int64.zero then "-" else "") ^ let a = abs x in - let af = arith_of_bits a in - if af <> af then - ("nan(0x" ^ (Printf.sprintf "%Lx" (abs (Int64.logxor bare_nan a))) ^ ")") - else - (* TODO: OCaml's string_of_float is insufficient *) - string_of_float (to_float a) +include Float.Make(struct + include Int64 + let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL + let bare_nan = 0x7ff0000000000000L + let print_nan_significand_digits a = + Printf.sprintf "%Lx" (abs (Int64.logxor bare_nan a)) + end) diff --git a/ml-proto/spec/f64.mli b/ml-proto/spec/f64.mli deleted file mode 100644 index 45631cd7a8..0000000000 --- a/ml-proto/spec/f64.mli +++ /dev/null @@ -1,35 +0,0 @@ -(* WebAssembly-compatible f64 implementation *) - -type t -type bits = int64 - -val of_float : float -> t -val to_float : t -> float -val of_bits : bits -> t -val to_bits : t -> bits - -val zero : t - -val add : t -> t -> t -val sub : t -> t -> t -val mul : t -> t -> t -val div : t -> t -> t -val sqrt : t -> t -val min : t -> t -> t -val max : t -> t -> t -val ceil : t -> t -val floor : t -> t -val trunc : t -> t -val nearest : t -> t -val abs : t -> t -val neg : t -> t -val copysign : t -> t -> t -val eq : t -> t -> bool -val ne : t -> t -> bool -val lt : t -> t -> bool -val le : t -> t -> bool -val gt : t -> t -> bool -val ge : t -> t -> bool - -val of_string : string -> t -val to_string : t -> string diff --git a/ml-proto/spec/float.ml b/ml-proto/spec/float.ml new file mode 100644 index 0000000000..99f2af704b --- /dev/null +++ b/ml-proto/spec/float.ml @@ -0,0 +1,181 @@ +module type RepresentationType = +sig + type t + + val nondeterministic_nan : t + val bits_of_float : float -> t + val float_of_bits : t -> float + val of_string : string -> t + val to_string : t -> string + + val logand : t -> t -> t + val logor : t -> t -> t + val logxor : t -> t -> t + + val min_int : t + val max_int : t + + val zero : t + val bare_nan : t + val print_nan_significand_digits : t -> string +end + +module type S = +sig + type t + type bits + val of_float : float -> t + val to_float : t -> float + val of_string : string -> t + val to_string : t -> string + val of_bits : bits -> t + val to_bits : t -> bits + val add : t -> t -> t + val sub : t -> t -> t + val mul : t -> t -> t + val div : t -> t -> t + val sqrt : t -> t + val min : t -> t -> t + val max : t -> t -> t + val ceil : t -> t + val floor : t -> t + val trunc : t -> t + val nearest : t -> t + val abs : t -> t + val neg : t -> t + val copysign : t -> t -> t + val eq : t -> t -> bool + val ne : t -> t -> bool + val lt : t -> t -> bool + val le : t -> t -> bool + val gt : t -> t -> bool + val ge : t -> t -> bool + val zero: t +end + +module Make(Rep : RepresentationType) : S with type bits = Rep.t = +struct + type t = Rep.t + type bits = Rep.t + + (* TODO: Do something meaningful with nondeterminism *) + let nondeterministic_nan = Rep.nondeterministic_nan + let bare_nan = Rep.bare_nan + + let of_float = Rep.bits_of_float + let to_float = Rep.float_of_bits + + let of_bits x = x + let to_bits x = x + + (* Most arithmetic ops that return NaN return a nondeterministic NaN *) + let arith_of_bits = to_float + let bits_of_arith f = if f <> f then Rep.nondeterministic_nan else of_float f + + let zero = of_float 0.0 + + let add x y = bits_of_arith ((arith_of_bits x) +. (arith_of_bits y)) + let sub x y = bits_of_arith ((arith_of_bits x) -. (arith_of_bits y)) + let mul x y = bits_of_arith ((arith_of_bits x) *. (arith_of_bits y)) + let div x y = bits_of_arith ((arith_of_bits x) /. (arith_of_bits y)) + + let sqrt x = bits_of_arith (Pervasives.sqrt (arith_of_bits x)) + + let ceil x = bits_of_arith (Pervasives.ceil (arith_of_bits x)) + let floor x = bits_of_arith (Pervasives.floor (arith_of_bits x)) + + let trunc x = + let xf = arith_of_bits x in + (* preserve the sign of zero *) + if xf = 0.0 then x else + (* trunc is either ceil or floor depending on which one is toward zero *) + let f = if xf < 0.0 then Pervasives.ceil xf else Pervasives.floor xf in + bits_of_arith f + + let nearest x = + let xf = arith_of_bits x in + (* preserve the sign of zero *) + if xf = 0.0 then x else + (* nearest is either ceil or floor depending on which is nearest or even *) + let u = Pervasives.ceil xf in + let d = Pervasives.floor xf in + let um = abs_float (xf -. u) in + let dm = abs_float (xf -. d) in + let u_or_d = um < dm || + (um = dm && let h = u /. 2. in Pervasives.floor h = h) in + let f = if u_or_d then u else d in + bits_of_arith f + + let min x y = + let xf = arith_of_bits x in + let yf = arith_of_bits y in + (* min -0 0 is -0 *) + if xf = yf then Rep.logor x y else + if xf < yf then x else + if xf > yf then y else + nondeterministic_nan + + let max x y = + let xf = arith_of_bits x in + let yf = arith_of_bits y in + (* max -0 0 is 0 *) + if xf = yf then Rep.logand x y else + if xf > yf then x else + if xf < yf then y else + nondeterministic_nan + + (* abs, neg, and copysign are purely bitwise operations, even on NaN values *) + let abs x = + Rep.logand x Rep.max_int + + let neg x = + Rep.logxor x Rep.min_int + + let copysign x y = + Rep.logor (abs x) (Rep.logand y Rep.min_int) + + let eq x y = (arith_of_bits x) = (arith_of_bits y) + let ne x y = (arith_of_bits x) <> (arith_of_bits y) + let lt x y = (arith_of_bits x) < (arith_of_bits y) + let gt x y = (arith_of_bits x) > (arith_of_bits y) + let le x y = (arith_of_bits x) <= (arith_of_bits y) + let ge x y = (arith_of_bits x) >= (arith_of_bits y) + + let of_signless_string x len = + if x <> "nan" && + (len > 7) && + (String.sub x 0 6) = "nan(0x" && (String.get x (len - 1)) = ')' then + (let s = Rep.of_string (String.sub x 4 ((len - 5))) in + if s = Rep.zero then + raise (Failure "nan payload must not be zero") + else if Rep.logand s bare_nan <> Rep.zero then + raise (Failure "nan payload must not overlap with exponent bits") + else if s < Rep.zero then + raise (Failure "nan payload must not overlap with sign bit") + else + Rep.logor s bare_nan) + else + (* TODO: OCaml's float_of_string is insufficient *) + of_float (float_of_string x) + + let of_string x = + let len = String.length x in + if len > 0 && (String.get x 0) = '-' then + neg (of_signless_string (String.sub x 1 (len - 1)) (len - 1)) + else if len > 0 && (String.get x 0) = '+' then + of_signless_string (String.sub x 1 (len - 1)) (len - 1) + else + of_signless_string x len + + let to_string x = + (if x < Rep.zero then "-" else "") ^ + let a = abs x in + let af = arith_of_bits a in + if af <> af then + ("nan(0x" ^ Rep.print_nan_significand_digits a ^ ")") + else + (* TODO: OCaml's string_of_float is insufficient *) + string_of_float (to_float a) + +end + diff --git a/ml-proto/spec/values.ml b/ml-proto/spec/values.ml index b941db5ca6..1b90adc37d 100644 --- a/ml-proto/spec/values.ml +++ b/ml-proto/spec/values.ml @@ -12,7 +12,6 @@ type ('i32, 'i64, 'f32, 'f64) op = type value = (I32.t, I64.t, F32.t, F64.t) op - (* Typing *) let type_of = function