From efd271815ea27ddd926851a8f2d6446e53a3f4ce Mon Sep 17 00:00:00 2001
From: Dan Gohman <sunfish@mozilla.com>
Date: Mon, 14 Sep 2015 08:43:37 -0700
Subject: [PATCH 1/2] wasm-compatible float32 and float64 arithmetic

---
 ml-proto/src/Makefile           |  2 +-
 ml-proto/src/given/float32.ml   | 95 +++++++++++++++++++++++++++++++++
 ml-proto/src/given/float32.mli  | 34 ++++++++++++
 ml-proto/src/given/float64.ml   | 95 +++++++++++++++++++++++++++++++++
 ml-proto/src/given/float64.mli  | 34 ++++++++++++
 ml-proto/src/host/parser.mly    |  5 +-
 ml-proto/src/spec/arithmetic.ml | 94 +++++++++++++++++++++-----------
 ml-proto/src/spec/memory.ml     | 12 ++---
 ml-proto/src/spec/types.ml      |  8 ---
 ml-proto/src/spec/values.ml     | 14 ++---
 10 files changed, 334 insertions(+), 59 deletions(-)
 create mode 100644 ml-proto/src/given/float32.ml
 create mode 100644 ml-proto/src/given/float32.mli
 create mode 100644 ml-proto/src/given/float64.ml
 create mode 100644 ml-proto/src/given/float64.mli

diff --git a/ml-proto/src/Makefile b/ml-proto/src/Makefile
index a1837d6b6d..864e47b5c7 100644
--- a/ml-proto/src/Makefile
+++ b/ml-proto/src/Makefile
@@ -5,7 +5,7 @@
 NAME = wasm
 INCLUDES = -I host -I given -I spec
 MODULES = \
-  host/flags given/lib given/source spec/error \
+  host/flags given/lib given/source given/float32 given/float64 spec/error \
   spec/types spec/values spec/memory spec/ast \
   spec/check spec/arithmetic spec/eval \
   host/print host/builtins host/script \
diff --git a/ml-proto/src/given/float32.ml b/ml-proto/src/given/float32.ml
new file mode 100644
index 0000000000..3991d56de3
--- /dev/null
+++ b/ml-proto/src/given/float32.ml
@@ -0,0 +1,95 @@
+(* WebAssembly-compatible float32 implementation *)
+
+(*
+ * We represent float32 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
+
+(* 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)
+
+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) && (mod_float u 2.0 = 0.0)) 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 = 0.0 && yf = 0.0 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 = 0.0 && yf = 0.0 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: type conversion functions *)
diff --git a/ml-proto/src/given/float32.mli b/ml-proto/src/given/float32.mli
new file mode 100644
index 0000000000..126caf4453
--- /dev/null
+++ b/ml-proto/src/given/float32.mli
@@ -0,0 +1,34 @@
+(* WebAssembly-compatible float32 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 of_string : string -> t
+val to_string : t -> string
+
+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
diff --git a/ml-proto/src/given/float64.ml b/ml-proto/src/given/float64.ml
new file mode 100644
index 0000000000..da49d36dc8
--- /dev/null
+++ b/ml-proto/src/given/float64.ml
@@ -0,0 +1,95 @@
+(* WebAssembly-compatible float64 implementation *)
+
+(*
+ * We represent float64 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
+
+(* 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)
+
+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) && (mod_float u 2.0 = 0.0)) 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 = 0.0 && yf = 0.0 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 = 0.0 && yf = 0.0 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: type conversion functions *)
diff --git a/ml-proto/src/given/float64.mli b/ml-proto/src/given/float64.mli
new file mode 100644
index 0000000000..fef07a86a1
--- /dev/null
+++ b/ml-proto/src/given/float64.mli
@@ -0,0 +1,34 @@
+(* WebAssembly-compatible float64 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 of_string : string -> t
+val to_string : t -> string
+
+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
diff --git a/ml-proto/src/host/parser.mly b/ml-proto/src/host/parser.mly
index 5b0e85da98..abaaa50f41 100644
--- a/ml-proto/src/host/parser.mly
+++ b/ml-proto/src/host/parser.mly
@@ -36,9 +36,8 @@ let literal at s t =
     match t with
     | Types.Int32Type -> Values.Int32 (Int32.of_string s) @@ at
     | Types.Int64Type -> Values.Int64 (Int64.of_string s) @@ at
-    | Types.Float32Type ->
-      Values.Float32 (Values.float32 (float_of_string s)) @@ at
-    | Types.Float64Type -> Values.Float64 (float_of_string s) @@ at
+    | Types.Float32Type -> Values.Float32 (Float32.of_string s) @@ at
+    | Types.Float64Type -> Values.Float64 (Float64.of_string s) @@ at
   with _ -> Error.error at "constant out of range"
 
 
diff --git a/ml-proto/src/spec/arithmetic.ml b/ml-proto/src/spec/arithmetic.ml
index 234a07cebc..7c9daf104d 100644
--- a/ml-proto/src/spec/arithmetic.ml
+++ b/ml-proto/src/spec/arithmetic.ml
@@ -86,21 +86,51 @@ 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 of_value : int -> value -> float
-  val to_value : float -> value
+  val of_value : int -> value -> t
+  val to_value : t -> value
 end
 
 module Float32X =
 struct
+  include Float32
   let size = 32
-  let to_value z = Float32 (float32 z)
+  let to_value z = Float32 z
   let of_value n =
     function Float32 z -> z | v -> raise (TypeError (n, v, Float32Type))
 end
 
 module Float64X =
 struct
+  include Float64
   let size = 64
   let to_value z = Float64 z
   let of_value n =
@@ -167,14 +197,14 @@ struct
       | ExtendUInt32 -> fun v ->
         Int.of_big_int_u (Int32X.to_big_int_u (Int32X.of_value 1 v))
       | WrapInt64 -> fun v -> Int.of_int64 (Int64X.of_value 1 v)
-      | TruncSFloat32 -> fun v -> Int.of_float (Float32X.of_value 1 v)
-      | TruncUFloat32 -> fun v -> of_float_u (Float32X.of_value 1 v)
-      | TruncSFloat64 -> fun v -> Int.of_float (Float64X.of_value 1 v)
-      | TruncUFloat64 -> fun v -> of_float_u (Float64X.of_value 1 v)
+      | TruncSFloat32 -> fun v -> Int.of_float (Float32.to_float (Float32X.of_value 1 v))
+      | TruncUFloat32 -> fun v -> of_float_u (Float32.to_float (Float32X.of_value 1 v))
+      | TruncSFloat64 -> fun v -> Int.of_float (Float64.to_float (Float64X.of_value 1 v))
+      | TruncUFloat64 -> fun v -> of_float_u (Float64.to_float (Float64X.of_value 1 v))
       | ReinterpretFloat -> fun v ->
         if Int.size = 32
-        then Int.bits_of_float (Float32X.of_value 1 v)
-        else Int.bits_of_float (Float64X.of_value 1 v)
+        then Int.bits_of_float (Float32.to_float (Float32X.of_value 1 v))
+        else Int.bits_of_float (Float64.to_float (Float64X.of_value 1 v))
     in fun v -> Int.to_value (f v)
 end
 
@@ -190,35 +220,35 @@ struct
 
   let unop op =
     let f = match op with
-      | Neg -> (~-.)
-      | Abs -> abs_float
-      | Sqrt  -> sqrt
-      | Ceil -> ceil
-      | Floor -> floor
-      | Trunc -> fun _ -> 0.0  (* TODO *)
-      | Nearest -> fun _ -> 0.0  (* TODO *)
+      | Neg -> Float.neg
+      | Abs -> Float.abs
+      | Sqrt  -> Float.sqrt
+      | Ceil -> Float.ceil
+      | Floor -> Float.floor
+      | Trunc -> Float.trunc
+      | Nearest -> Float.nearest
     in fun v -> Float.to_value (f (Float.of_value 1 v))
 
   let binop op =
     let f = match op with
-      | Add -> (+.)
-      | Sub -> (-.)
-      | Mul -> ( *.)
-      | Div -> (/.)
-      | Min -> min
-      | Max -> max
-      | CopySign -> copysign
+      | Add -> Float.add
+      | Sub -> Float.sub
+      | Mul -> Float.mul
+      | Div -> Float.div
+      | Min -> Float.min
+      | Max -> Float.max
+      | CopySign -> Float.copysign
     in
     fun v1 v2 -> Float.to_value (f (Float.of_value 1 v1) (Float.of_value 2 v2))
 
   let relop op =
     let f = match op with
-      | Eq -> (=)
-      | Neq -> (<>)
-      | Lt -> (<)
-      | Le -> (<=)
-      | Gt -> (>)
-      | Ge -> (>=)
+      | Eq -> Float.eq
+      | Neq -> Float.ne
+      | Lt -> Float.lt
+      | Le -> Float.le
+      | Gt -> Float.gt
+      | Ge -> Float.ge
     in fun v1 v2 -> f (Float.of_value 1 v1) (Float.of_value 2 v2)
 
   let cvt op =
@@ -229,13 +259,13 @@ struct
       | ConvertSInt64 -> fun v -> Int64.to_float (Int64X.of_value 1 v)
       | ConvertUInt64 -> fun v ->
         Big_int.float_of_big_int (Int64X.to_big_int_u (Int64X.of_value 1 v))
-      | PromoteFloat32 -> fun v -> Float32X.of_value 1 v
-      | DemoteFloat64 -> fun v -> Float64X.of_value 1 v
+      | PromoteFloat32 -> fun v -> (Float32.to_float (Float32X.of_value 1 v))
+      | DemoteFloat64 -> fun v -> (Float64.to_float (Float64X.of_value 1 v))
       | ReinterpretInt -> fun v ->
         if Float.size = 32
         then Int32.float_of_bits (Int32X.of_value 1 v)
         else Int64.float_of_bits (Int64X.of_value 1 v)
-    in fun v -> Float.to_value (f v)
+    in fun v -> (Float.to_value (Float.of_float (f v)))
 end
 
 module Float32Op = FloatOp (Ast.Float32Op) (Float32X)
diff --git a/ml-proto/src/spec/memory.ml b/ml-proto/src/spec/memory.ml
index 70218938f8..00f3f745ec 100644
--- a/ml-proto/src/spec/memory.ml
+++ b/ml-proto/src/spec/memory.ml
@@ -32,8 +32,8 @@ type uint8_view = (int, int8_unsigned_elt, c_layout) Array1.t
 type uint16_view = (int, int16_unsigned_elt, c_layout) Array1.t
 type uint32_view = (int32, int32_elt, c_layout) Array1.t
 type uint64_view = (int64, int64_elt, c_layout) Array1.t
-type float32_view = (float, float32_elt, c_layout) Array1.t
-type float64_view = (float, float64_elt, c_layout) Array1.t
+type float32_view = (int32, int32_elt, c_layout) Array1.t
+type float64_view = (int64, int64_elt, c_layout) Array1.t
 
 let view : memory -> ('c, 'd, c_layout) Array1.t = Obj.magic
 
@@ -94,8 +94,8 @@ let load mem a memty ext =
     | Int16Mem, ZX -> Int32 (Int32.of_int (view buf : uint16_view).{0})
     | Int32Mem, NX -> Int32 (view buf : sint32_view).{0}
     | Int64Mem, NX -> Int64 (view buf : sint64_view).{0}
-    | Float32Mem, NX -> Float32 (view buf : float32_view).{0}
-    | Float64Mem, NX -> Float64 (view buf : float64_view).{0}
+    | Float32Mem, NX -> Float32 (Float32.of_bits (view buf : float32_view).{0})
+    | Float64Mem, NX -> Float64 (Float64.of_bits (view buf : float64_view).{0})
     | _ -> raise Type
   with Invalid_argument _ -> raise Bounds
 
@@ -107,8 +107,8 @@ let store mem a memty v =
     | Int16Mem, Int32 x -> (view buf : sint16_view).{0} <- Int32.to_int x
     | Int32Mem, Int32 x -> (view buf : sint32_view).{0} <- x
     | Int64Mem, Int64 x -> (view buf : sint64_view).{0} <- x
-    | Float32Mem, Float32 x -> (view buf : float32_view).{0} <- x
-    | Float64Mem, Float64 x -> (view buf : float64_view).{0} <- x
+    | Float32Mem, Float32 x -> (view buf : float32_view).{0} <- Float32.to_bits x
+    | Float64Mem, Float64 x -> (view buf : float64_view).{0} <- Float64.to_bits x
     | _ -> raise Type);
     Array1.blit (Array1.sub buf 0 sz) (Array1.sub mem a sz)
   with Invalid_argument _ -> raise Bounds
diff --git a/ml-proto/src/spec/types.ml b/ml-proto/src/spec/types.ml
index 548e1cc859..71b04a0801 100644
--- a/ml-proto/src/spec/types.ml
+++ b/ml-proto/src/spec/types.ml
@@ -2,14 +2,6 @@
  * (c) 2015 Andreas Rossberg
  *)
 
-(* Number formats *)
-
-type uint32 = int32   (* approximate *)
-type uint64 = int64   (* approximate *)
-type float32 = float  (* approximate *)
-type float64 = float
-
-
 (* Types *)
 
 type value_type = Int32Type | Int64Type | Float32Type | Float64Type
diff --git a/ml-proto/src/spec/values.ml b/ml-proto/src/spec/values.ml
index 81a425a205..fcb426d685 100644
--- a/ml-proto/src/spec/values.ml
+++ b/ml-proto/src/spec/values.ml
@@ -10,7 +10,7 @@ open Types
 type ('i32, 'i64, 'f32, 'f64) op =
   Int32 of 'i32 | Int64 of 'i64 | Float32 of 'f32 | Float64 of 'f64
 
-type value = (int32, int64, float32, float64) op
+type value = (int32, int64, Float32.t, Float64.t) op
 
 
 (* Typing *)
@@ -24,8 +24,8 @@ let type_of = function
 let default_value = function
   | Int32Type -> Int32 Int32.zero
   | Int64Type -> Int64 Int64.zero
-  | Float32Type -> Float32 0.0
-  | Float64Type -> Float64 0.0
+  | Float32Type -> Float32 Float32.zero
+  | Float64Type -> Float64 Float64.zero
 
 
 (* String conversion *)
@@ -33,13 +33,9 @@ let default_value = function
 let string_of_value = function
   | Int32 i -> Int32.to_string i
   | Int64 i -> Int64.to_string i
-  | Float32 z | Float64 z -> string_of_float z
+  | Float32 z -> Float32.to_string z
+  | Float64 z -> Float64.to_string z
 
 let string_of_values = function
   | [v] -> string_of_value v
   | vs -> "(" ^ String.concat " " (List.map string_of_value vs) ^ ")"
-
-
-(* Float32 truncation *)
-
-let float32 x = Int32.float_of_bits (Int32.bits_of_float x)

From 9a5e057596543ceb60bf2794286fd35f335b83d7 Mon Sep 17 00:00:00 2001
From: Dan Gohman <sunfish@mozilla.com>
Date: Tue, 15 Sep 2015 14:20:29 -0700
Subject: [PATCH 2/2] Refactor the Float32 and Float64 modules into a Float
 functor.

---
 ml-proto/src/Makefile             |   2 +-
 ml-proto/src/given/basicfloat.ml  | 154 ++++++++++++++++++++++++++++++
 ml-proto/src/given/basicfloat.mli |  41 ++++++++
 ml-proto/src/given/basicint.ml    |  64 +++++++++++++
 ml-proto/src/given/basicint.mli   |  36 +++++++
 ml-proto/src/given/float32.ml     |  95 ------------------
 ml-proto/src/given/float32.mli    |  34 -------
 ml-proto/src/given/float64.ml     |  95 ------------------
 ml-proto/src/given/float64.mli    |  34 -------
 ml-proto/src/spec/arithmetic.ml   |   2 +
 10 files changed, 298 insertions(+), 259 deletions(-)
 create mode 100644 ml-proto/src/given/basicfloat.ml
 create mode 100644 ml-proto/src/given/basicfloat.mli
 create mode 100644 ml-proto/src/given/basicint.ml
 create mode 100644 ml-proto/src/given/basicint.mli
 delete mode 100644 ml-proto/src/given/float32.ml
 delete mode 100644 ml-proto/src/given/float32.mli
 delete mode 100644 ml-proto/src/given/float64.ml
 delete mode 100644 ml-proto/src/given/float64.mli

diff --git a/ml-proto/src/Makefile b/ml-proto/src/Makefile
index 864e47b5c7..314f3565bd 100644
--- a/ml-proto/src/Makefile
+++ b/ml-proto/src/Makefile
@@ -5,7 +5,7 @@
 NAME = wasm
 INCLUDES = -I host -I given -I spec
 MODULES = \
-  host/flags given/lib given/source given/float32 given/float64 spec/error \
+  host/flags given/lib given/source given/basicint given/basicfloat spec/error \
   spec/types spec/values spec/memory spec/ast \
   spec/check spec/arithmetic spec/eval \
   host/print host/builtins host/script \
diff --git a/ml-proto/src/given/basicfloat.ml b/ml-proto/src/given/basicfloat.ml
new file mode 100644
index 0000000000..9b56d9cfad
--- /dev/null
+++ b/ml-proto/src/given/basicfloat.ml
@@ -0,0 +1,154 @@
+(* WebAssembly-compatible floating point implementation *)
+
+module type BASIC_FLOAT = sig
+  type t
+  type bits
+
+  val size : int
+
+  val of_float : float -> t
+  val to_float : t -> float
+  val of_bits : bits -> t
+  val to_bits : t -> bits
+  val of_string : string -> t
+  val to_string : t -> string
+
+  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 ceil : t -> t
+  val floor : t -> t
+  val trunc : t -> t
+  val nearest : t -> t
+  val min : t -> t -> t
+  val max : t -> 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
+end
+
+module type FLOAT_TRAITS = sig
+  type t
+  val size : int
+  val nondeterministic_nan : t
+end
+
+module Float32Traits : FLOAT_TRAITS = struct
+  type t = int32
+  let size = 32
+
+  (* TODO: Do something meaningful with nondeterminism *)
+  let nondeterministic_nan = 0x7fc0f0f0l
+end
+
+module Float64Traits : FLOAT_TRAITS = struct
+  type t = int64
+  let size = 64
+
+  (* TODO: Do something meaningful with nondeterminism *)
+  let nondeterministic_nan = 0x7fff0f0f0f0f0f0fL
+end
+
+module Float (Traits : FLOAT_TRAITS) (Int : Basicint.BASIC_INT with type t = Traits.t) : BASIC_FLOAT = struct
+  include Traits
+
+  type bits = Int.t
+
+  let of_bits x = x
+  let to_bits x = x
+  let of_float x = of_bits (Int.bits_of_float x)
+  let to_float x = to_bits (Int.float_of_bits x)
+
+  (* 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)
+
+  let zero = of_float 0.0
+
+  (* 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 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) && (mod_float u 2.0 = 0.0)) 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 = 0.0 && yf = 0.0 then (Int.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 = 0.0 && yf = 0.0 then (Int.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 =
+    Int.logand x Int.max_int
+
+  let neg x =
+    Int.logxor x Int.min_int
+
+  let copysign x y =
+    Int.logor (abs x) (Int.logand y Int.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)
+end
+
+module BasicFloat32 : BASIC_FLOAT = struct
+  include Float(Float32Traits) (Basicint.BasicInt32)
+end
+
+module BasicFloat64 : BASIC_FLOAT = struct
+  include Float(Float64Traits) (Basicint.BasicInt64)
+end
diff --git a/ml-proto/src/given/basicfloat.mli b/ml-proto/src/given/basicfloat.mli
new file mode 100644
index 0000000000..b14cd0f9eb
--- /dev/null
+++ b/ml-proto/src/given/basicfloat.mli
@@ -0,0 +1,41 @@
+(* WebAssembly-compatible floating point implementation *)
+
+module type BASIC_FLOAT = sig
+  type t
+  type bits
+
+  val size : int
+
+  val of_float : float -> t
+  val to_float : t -> float
+  val of_bits : bits -> t
+  val to_bits : t -> bits
+  val of_string : string -> t
+  val to_string : t -> string
+
+  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 ceil : t -> t
+  val floor : t -> t
+  val trunc : t -> t
+  val nearest : t -> t
+  val min : t -> t -> t
+  val max : t -> 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
+end
+
+module BasicFloat32 : BASIC_FLOAT
+module BasicFloat64 : BASIC_FLOAT
diff --git a/ml-proto/src/given/basicint.ml b/ml-proto/src/given/basicint.ml
new file mode 100644
index 0000000000..7466560314
--- /dev/null
+++ b/ml-proto/src/given/basicint.ml
@@ -0,0 +1,64 @@
+(* WebAssembly-compatible integer implementation *)
+
+module type BASIC_INT =
+sig
+  type t
+  val size : int
+  val max_int : t
+  val min_int : t
+  val neg : t -> t
+  val abs : t -> t
+  val lognot : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mul : t -> t -> t
+  val div : t -> t -> t
+  val rem : t -> t -> t
+  val logand : t -> t -> t
+  val logor : t -> t -> t
+  val logxor : t -> t -> t
+  (* TODO: type should be t -> t -> t for wasm *)
+  val shift_left : t -> int -> t
+  val shift_right : t -> int -> t
+  val shift_right_logical : t -> int -> t
+
+  (* TODO obviate these *)
+  val to_float : t -> float
+  val of_float : float -> t
+  val bits_of_float : float -> t
+  val float_of_bits : t -> float
+
+  val to_big_int_u : t -> Big_int.big_int
+  val of_big_int_u : Big_int.big_int -> t
+end
+
+let to_big_int_u_for size to_big_int i =
+  let open Big_int in
+  let value_range = Big_int.power_int_positive_int 2 size in
+  let i' = to_big_int i in
+  if ge_big_int i' zero_big_int then i' else add_big_int i' value_range
+
+let of_big_int_u_for size of_big_int i =
+  let open Big_int in
+  let value_range = Big_int.power_int_positive_int 2 size in
+  let i' = if ge_big_int i zero_big_int then i else sub_big_int i value_range
+  in of_big_int i'
+
+module BasicInt32 =
+struct
+  include Int32
+  let size = 32
+  let of_int32 i = i
+  let of_int64 = Int64.to_int32
+  let to_big_int_u = to_big_int_u_for size Big_int.big_int_of_int32
+  let of_big_int_u = of_big_int_u_for size Big_int.int32_of_big_int
+end
+
+module BasicInt64 =
+struct
+  include Int64
+  let size = 64
+  let of_int64 i = i
+  let to_big_int_u = to_big_int_u_for size Big_int.big_int_of_int64
+  let of_big_int_u = of_big_int_u_for size Big_int.int64_of_big_int
+end
diff --git a/ml-proto/src/given/basicint.mli b/ml-proto/src/given/basicint.mli
new file mode 100644
index 0000000000..f5c8ce3a00
--- /dev/null
+++ b/ml-proto/src/given/basicint.mli
@@ -0,0 +1,36 @@
+(* WebAssembly-compatible integer implementation *)
+
+module type BASIC_INT =
+sig
+  type t
+  val size : int
+  val max_int : t
+  val min_int : t
+  val neg : t -> t
+  val abs : t -> t
+  val lognot : t -> t
+  val add : t -> t -> t
+  val sub : t -> t -> t
+  val mul : t -> t -> t
+  val div : t -> t -> t
+  val rem : t -> t -> t
+  val logand : t -> t -> t
+  val logor : t -> t -> t
+  val logxor : t -> t -> t
+  (* TODO: type should be t -> t -> t for wasm *)
+  val shift_left : t -> int -> t
+  val shift_right : t -> int -> t
+  val shift_right_logical : t -> int -> t
+
+  (* TODO obviate these *)
+  val to_float : t -> float
+  val of_float : float -> t
+  val bits_of_float : float -> t
+  val float_of_bits : t -> float
+
+  val to_big_int_u : t -> Big_int.big_int
+  val of_big_int_u : Big_int.big_int -> t
+end
+
+module BasicInt32 : BASIC_INT
+module BasicInt64 : BASIC_INT
diff --git a/ml-proto/src/given/float32.ml b/ml-proto/src/given/float32.ml
deleted file mode 100644
index 3991d56de3..0000000000
--- a/ml-proto/src/given/float32.ml
+++ /dev/null
@@ -1,95 +0,0 @@
-(* WebAssembly-compatible float32 implementation *)
-
-(*
- * We represent float32 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
-
-(* 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)
-
-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) && (mod_float u 2.0 = 0.0)) 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 = 0.0 && yf = 0.0 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 = 0.0 && yf = 0.0 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: type conversion functions *)
diff --git a/ml-proto/src/given/float32.mli b/ml-proto/src/given/float32.mli
deleted file mode 100644
index 126caf4453..0000000000
--- a/ml-proto/src/given/float32.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(* WebAssembly-compatible float32 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 of_string : string -> t
-val to_string : t -> string
-
-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
diff --git a/ml-proto/src/given/float64.ml b/ml-proto/src/given/float64.ml
deleted file mode 100644
index da49d36dc8..0000000000
--- a/ml-proto/src/given/float64.ml
+++ /dev/null
@@ -1,95 +0,0 @@
-(* WebAssembly-compatible float64 implementation *)
-
-(*
- * We represent float64 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
-
-(* 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)
-
-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) && (mod_float u 2.0 = 0.0)) 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 = 0.0 && yf = 0.0 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 = 0.0 && yf = 0.0 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: type conversion functions *)
diff --git a/ml-proto/src/given/float64.mli b/ml-proto/src/given/float64.mli
deleted file mode 100644
index fef07a86a1..0000000000
--- a/ml-proto/src/given/float64.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-(* WebAssembly-compatible float64 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 of_string : string -> t
-val to_string : t -> string
-
-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
diff --git a/ml-proto/src/spec/arithmetic.ml b/ml-proto/src/spec/arithmetic.ml
index 7c9daf104d..587567794d 100644
--- a/ml-proto/src/spec/arithmetic.ml
+++ b/ml-proto/src/spec/arithmetic.ml
@@ -13,6 +13,7 @@ exception TypeError of int * value * value_type
 
 (* Int traits *)
 
+(* TODO: Replace this with BASIC_INT *)
 module type INT =
 sig
   type t
@@ -84,6 +85,7 @@ end
 
 (* Float traits *)
 
+(* TODO: Replace this with BASIC_FLOAT *)
 module type FLOAT =
 sig
   type t