diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index ad9416734b..3e4b0e3eed 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -7,7 +7,6 @@ open Source open Ast open Script - (* Position handling *) let position_to_pos position = @@ -36,8 +35,8 @@ let literal at s t = match t with | Types.Int32Type -> Values.Int32 (I32.of_string s) @@ at | Types.Int64Type -> Values.Int64 (I64.of_string s) @@ at - | Types.Float32Type -> Values.Float32 (F32.of_string s) @@ at - | Types.Float64Type -> Values.Float64 (F64.of_string s) @@ at + | Types.Float32Type -> Values.Float32 (Values.F32.of_string s) @@ at + | Types.Float64Type -> Values.Float64 (Values.F64.of_string s) @@ at with _ -> Error.error at "constant out of range" diff --git a/ml-proto/spec/f32.ml b/ml-proto/spec/f32.ml deleted file mode 100644 index af602d794a..0000000000 --- a/ml-proto/spec/f32.ml +++ /dev/null @@ -1,94 +0,0 @@ -(* 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 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) - -(* TODO: OCaml's string_of_float and float_of_string are insufficient *) -let of_string x = of_float (float_of_string x) -let to_string x = string_of_float (to_float x) 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/f32_convert.ml b/ml-proto/spec/f32_convert.ml index 7dacfbcb1e..1843b4f139 100644 --- a/ml-proto/spec/f32_convert.ml +++ b/ml-proto/spec/f32_convert.ml @@ -1,3 +1,6 @@ +module F32 = Values.F32 +module F64 = Values.F64 + (* WebAssembly-compatible type conversions to f32 implementation *) let make_nan_nondeterministic x = F32.mul x (F32.of_float 1.) diff --git a/ml-proto/spec/f32_convert.mli b/ml-proto/spec/f32_convert.mli index bcff3589b6..8ad79af6c1 100644 --- a/ml-proto/spec/f32_convert.mli +++ b/ml-proto/spec/f32_convert.mli @@ -1,8 +1,8 @@ (* WebAssembly-compatible type conversions to f32 implementation *) -val demote_f64 : F64.t -> F32.t -val convert_s_i32 : I32.t -> F32.t -val convert_u_i32 : I32.t -> F32.t -val convert_s_i64 : I64.t -> F32.t -val convert_u_i64 : I64.t -> F32.t -val reinterpret_i32 : I32.t -> F32.t +val demote_f64 : Values.F64.t -> Values.F32.t +val convert_s_i32 : I32.t -> Values.F32.t +val convert_u_i32 : I32.t -> Values.F32.t +val convert_s_i64 : I64.t -> Values.F32.t +val convert_u_i64 : I64.t -> Values.F32.t +val reinterpret_i32 : I32.t -> Values.F32.t diff --git a/ml-proto/spec/f64.ml b/ml-proto/spec/f64.ml deleted file mode 100644 index 3c11879ef7..0000000000 --- a/ml-proto/spec/f64.ml +++ /dev/null @@ -1,94 +0,0 @@ -(* 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 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) - -(* TODO: OCaml's string_of_float and float_of_string are insufficient *) -let of_string x = of_float (float_of_string x) -let to_string x = string_of_float (to_float x) 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/f64_convert.ml b/ml-proto/spec/f64_convert.ml index 2f9d5bdad9..5d46b138fa 100644 --- a/ml-proto/spec/f64_convert.ml +++ b/ml-proto/spec/f64_convert.ml @@ -1,3 +1,6 @@ +module F32 = Values.F32 +module F64 = Values.F64 + (* WebAssembly-compatible type conversions to f64 implementation *) let make_nan_nondeterministic x = F64.mul x (F64.of_float 1.) diff --git a/ml-proto/spec/f64_convert.mli b/ml-proto/spec/f64_convert.mli index a1209a3e70..a6529fa785 100644 --- a/ml-proto/spec/f64_convert.mli +++ b/ml-proto/spec/f64_convert.mli @@ -1,8 +1,8 @@ (* WebAssembly-compatible type conversions to f64 implementation *) -val promote_f32 : F32.t -> F64.t -val convert_s_i32 : I32.t -> F64.t -val convert_u_i32 : I32.t -> F64.t -val convert_s_i64 : I64.t -> F64.t -val convert_u_i64 : I64.t -> F64.t -val reinterpret_i64 : I64.t -> F64.t +val promote_f32 : Values.F32.t -> Values.F64.t +val convert_s_i32 : I32.t -> Values.F64.t +val convert_u_i32 : I32.t -> Values.F64.t +val convert_s_i64 : I64.t -> Values.F64.t +val convert_u_i64 : I64.t -> Values.F64.t +val reinterpret_i64 : I64.t -> Values.F64.t diff --git a/ml-proto/spec/float.ml b/ml-proto/spec/float.ml new file mode 100644 index 0000000000..8db572b36e --- /dev/null +++ b/ml-proto/spec/float.ml @@ -0,0 +1,93 @@ +module FloatPrims(Rep : Floatsig.REP) : Floatsig.FLOAT with type bits = Rep.t = +struct + type t = Rep.t + type bits = Rep.t + + let nondeterministic_nan = Rep.nondeterministic_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 size = Rep.size + + (* TODO: OCaml's string_of_float and float_of_string are insufficient *) + let of_string x = of_float (float_of_string x) + let to_string x = string_of_float (to_float x) +end + diff --git a/ml-proto/spec/float.mli b/ml-proto/spec/float.mli new file mode 100644 index 0000000000..3f508d5447 --- /dev/null +++ b/ml-proto/spec/float.mli @@ -0,0 +1 @@ +module FloatPrims : functor (Rep : Floatsig.REP) -> Floatsig.FLOAT with type bits = Rep.t diff --git a/ml-proto/spec/floatsig.ml b/ml-proto/spec/floatsig.ml new file mode 100644 index 0000000000..25efb481ed --- /dev/null +++ b/ml-proto/spec/floatsig.ml @@ -0,0 +1,53 @@ +module type REP = +sig + type t + + val nondeterministic_nan : t + val bits_of_float : float -> t + val float_of_bits : t -> float + + val logand : t -> t -> t + val logor : t -> t -> t + val logxor : t -> t -> t + + val min_int : t + val max_int : t + + val size : int + +end + +module type FLOAT = +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 size : int + val zero: t +end + diff --git a/ml-proto/spec/i32_convert.ml b/ml-proto/spec/i32_convert.ml index 4ea0c0f772..304f6f6553 100644 --- a/ml-proto/spec/i32_convert.ml +++ b/ml-proto/spec/i32_convert.ml @@ -1,3 +1,6 @@ +module F32 = Values.F32 +module F64 = Values.F64 + (* WebAssembly-compatible type conversions to i32 implementation *) let wrap_i64 x = Int64.to_int32 x diff --git a/ml-proto/spec/i32_convert.mli b/ml-proto/spec/i32_convert.mli index 2737aadd22..4208ac8ef8 100644 --- a/ml-proto/spec/i32_convert.mli +++ b/ml-proto/spec/i32_convert.mli @@ -1,8 +1,8 @@ (* WebAssembly-compatible type conversions to i32 implementation *) val wrap_i64 : I64.t -> I32.t -val trunc_s_f32 : F32.t -> I32.t -val trunc_u_f32 : F32.t -> I32.t -val trunc_s_f64 : F64.t -> I32.t -val trunc_u_f64 : F64.t -> I32.t -val reinterpret_f32 : F32.t -> I32.t +val trunc_s_f32 : Values.F32.t -> I32.t +val trunc_u_f32 : Values.F32.t -> I32.t +val trunc_s_f64 : Values.F64.t -> I32.t +val trunc_u_f64 : Values.F64.t -> I32.t +val reinterpret_f32 : Values.F32.t -> I32.t diff --git a/ml-proto/spec/i64_convert.ml b/ml-proto/spec/i64_convert.ml index 0cf32f8c36..02b8f7c9eb 100644 --- a/ml-proto/spec/i64_convert.ml +++ b/ml-proto/spec/i64_convert.ml @@ -1,3 +1,6 @@ +module F32 = Values.F32 +module F64 = Values.F64 + (* WebAssembly-compatible type conversions to i64 implementation *) let extend_s_i32 x = Int64.of_int32 x diff --git a/ml-proto/spec/i64_convert.mli b/ml-proto/spec/i64_convert.mli index 50a3b3a3ea..f8f2906f1d 100644 --- a/ml-proto/spec/i64_convert.mli +++ b/ml-proto/spec/i64_convert.mli @@ -2,8 +2,8 @@ val extend_s_i32 : I32.t -> I64.t val extend_u_i32 : I32.t -> I64.t -val trunc_s_f32 : F32.t -> I64.t -val trunc_u_f32 : F32.t -> I64.t -val trunc_s_f64 : F64.t -> I64.t -val trunc_u_f64 : F64.t -> I64.t -val reinterpret_f64 : F64.t -> I64.t +val trunc_s_f32 : Values.F32.t -> I64.t +val trunc_u_f32 : Values.F32.t -> I64.t +val trunc_s_f64 : Values.F64.t -> I64.t +val trunc_u_f64 : Values.F64.t -> I64.t +val reinterpret_f64 : Values.F64.t -> I64.t diff --git a/ml-proto/spec/values.ml b/ml-proto/spec/values.ml index b941db5ca6..04fee1a4e5 100644 --- a/ml-proto/spec/values.ml +++ b/ml-proto/spec/values.ml @@ -10,8 +10,23 @@ open Types type ('i32, 'i64, 'f32, 'f64) op = Int32 of 'i32 | Int64 of 'i64 | Float32 of 'f32 | Float64 of 'f64 -type value = (I32.t, I64.t, F32.t, F64.t) op +module F32 = + Float.FloatPrims( + struct + include Int32 + let nondeterministic_nan = 0x7fc0f0f0l + let size = 32 + end) + +module F64 = + Float.FloatPrims( + struct + include Int64 + let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL + let size = 64 + end) +type value = (I32.t, I64.t, F32.t, F64.t) op (* Typing *)