From 2e19e572d950a91b6862bf02faa6bb2a5375dd4f Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Thu, 3 Mar 2016 18:39:30 +0100
Subject: [PATCH] jsnumber_cleanup
---
generator/TODO | 26 ++++----
generator/lineof.ml | 2 +-
generator/stdlib_ml/stdlib.mli | 10 +++
generator/tests/jsref/JsCommon.ml | 6 +-
generator/tests/jsref/JsCommonAux.ml | 12 ++--
generator/tests/jsref/JsInit.ml | 24 ++++----
generator/tests/jsref/JsInterpreter.ml | 52 ++++++++--------
generator/tests/jsref/JsInterpreterMonads.ml | 2 +-
generator/tests/jsref/JsNumber.ml | 24 +++-----
generator/tests/jsref/JsPreliminary.ml | 64 ++++++++++----------
generator/tests/jsref/JsSyntax.ml | 8 +--
generator/tests/jsref/JsSyntaxAux.ml | 2 +-
12 files changed, 117 insertions(+), 115 deletions(-)
diff --git a/generator/TODO b/generator/TODO
index 8aae88f..f76fe9c 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -16,30 +16,32 @@ ARTHUR
- remove "open JsNumber" to more easily trace occurences
-- generate "type: " in smart contsructors
+- generate "type: " in smart constructors [optional until display is needed]
- generate the escaped source code
- control which file should feature logging
-- lineof_temp["5"] => 5 should be int
-[arthur will do a first pass]
-- clean up stdlib.ml
+
+=========================================================
+NEXT
+
+[arthur did a first pass on JsNumber.ml to make explicit paths
+ and on stdlib.ml]
+- continue cleaning up stdlib.ml
- implement stdlib.js
- remove unused functions
- sort out remaining ones
- need to have one function for each one of stdlib.ml
- - number related functions are implemented with JS counterpart directly
- JsNumber.ml should be replaced by JsNumber.mli (we might want to keep
- JsNumber.ml for future use, though), and we implement by hand JsNumber.js,
- which would then be included directly in assembly.js.
- - Int32 and Int64 implem [alan] directly in JS
+ - replace JsNumber by a corresponding JsNumber.mli
+ (keep JsNumber saved somewhere else for future use)
+ - implement JsNumber.js by hand to match signature of JsNumber.mli,
+ by implementing number related functions using JS counterpart directly
+ (ask Alan for Int32 and Int64 implementation tricks)
+ - include JsNumber.js in assembly.js by modifying ASSEMBLY_JS in Makefile
-=========================================================
-NEXT
-
[thomas, biggest piece, ask if anything problematic]
- fill in the "esprima-to-ast.js" file, following the template
(throw an exception, caught and displayed as an alert message,
diff --git a/generator/lineof.ml b/generator/lineof.ml
index ebfe32c..3a9b947 100644
--- a/generator/lineof.ml
+++ b/generator/lineof.ml
@@ -155,7 +155,7 @@ let generate_lineof_function put =
let pos_stop = try Hashtbl.find tokens_stop key
with Not_found -> Printf.printf "Warning (error): unclosed token %d in file %s; using pos_start instead.\n" key filename; pos_start
in
- put (Printf.sprintf " lineof_temp[\"%d\"] = [%d,%d,%d,%d];"
+ put (Printf.sprintf " lineof_temp[%d] = [%d,%d,%d,%d];"
key pos_start.pos_line pos_start.pos_col
pos_stop.pos_line pos_stop.pos_col);
);
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index f34242f..6e28740 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -73,9 +73,19 @@ val float_eq : float -> float -> bool
val float_lt : float -> float -> bool
val float_le : float -> float -> bool
val float_compare : float -> float -> int
+(** val number_comparable : number coq_Comparable **)
+val number_comparable : float -> float -> bool (* = (fun n1 n2 -> int_eq 0 (float_compare n1 n2)) *)
+
+(** val of_int : float -> number **)
+val of_int : float -> float (* = fun x -> x *)
+
+val number_of_int : int -> float (* = fun x -> float_of_int x *)
+
val string_concat : string -> string -> string
+val nat_eq : int -> int -> bool (* nat_eq x y = int_eq x y *)
+
val pi : float
val e : float
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index de739b0..daf1621 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -1,6 +1,6 @@
open Datatypes
-open JsNumber
+(*open JsNumber*)
open JsSyntax
open JsSyntaxAux
open LibList
@@ -520,12 +520,12 @@ let throw_irrelevant =
(** val add_one : number -> number **)
let add_one n =
- add n one
+ add n JsNumber.one
(** val sub_one : number -> number **)
let sub_one n =
- sub n one
+ sub n JsNumber.one
(** val is_syntactic_eval : expr -> bool **)
diff --git a/generator/tests/jsref/JsCommonAux.ml b/generator/tests/jsref/JsCommonAux.ml
index c8a5ef1..7214ae8 100644
--- a/generator/tests/jsref/JsCommonAux.ml
+++ b/generator/tests/jsref/JsCommonAux.ml
@@ -1,6 +1,6 @@
open Datatypes
open JsCommon
-open JsNumber
+(*open JsNumber*)
open JsSyntax
open JsSyntaxAux
open LibList
@@ -43,7 +43,7 @@ let same_value_dec v1 v2 =
let h2 =
and_decidable
(value_comparable v1 (Coq_value_prim (Coq_prim_number
- nan)))
+ JsNumber.nan)))
(value_comparable v2 (Coq_value_prim (Coq_prim_number
nan)))
in
@@ -53,9 +53,9 @@ let same_value_dec v1 v2 =
let h3 =
and_decidable
(value_comparable v1 (Coq_value_prim
- (Coq_prim_number zero)))
+ (Coq_prim_number JsNumber.zero)))
(value_comparable v2 (Coq_value_prim
- (Coq_prim_number neg_zero)))
+ (Coq_prim_number JsNumber.neg_zero)))
in
(if h3
then (fun _ -> false_decidable)
@@ -63,9 +63,9 @@ let same_value_dec v1 v2 =
let h4 =
and_decidable
(value_comparable v1 (Coq_value_prim
- (Coq_prim_number neg_zero)))
+ (Coq_prim_number JsNumber.neg_zero)))
(value_comparable v2 (Coq_value_prim
- (Coq_prim_number zero)))
+ (Coq_prim_number JsNumber.zero)))
in
(if h4
then (fun _ -> false_decidable)
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index 5b5d8c3..a399d9f 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -1,5 +1,5 @@
open JsCommon
-open JsNumber
+(*open JsNumber*)
open JsPreliminary
open JsSyntax
open JsSyntaxAux
@@ -79,12 +79,12 @@ let object_prealloc_global_class = "GlobalClass"
let object_prealloc_global_properties =
let p =
write_constant Heap.empty ("NaN") (Coq_value_prim
- (Coq_prim_number nan))
+ (Coq_prim_number JsNumber.nan))
in
let p0 =
write_constant p
("Infinity")
- (Coq_value_prim (Coq_prim_number infinity))
+ (Coq_value_prim (Coq_prim_number JsNumber.infinity))
in
let p1 =
write_constant p0
@@ -601,27 +601,27 @@ let object_prealloc_number =
in
let p0 =
write_constant p ("NaN") (Coq_value_prim (Coq_prim_number
- nan))
+ JsNumber.nan))
in
let p1 =
write_constant p0
("NEGATIVE_INFINITY")
- (Coq_value_prim (Coq_prim_number neg_infinity))
+ (Coq_value_prim (Coq_prim_number JsNumber.neg_infinity))
in
let p2 =
write_constant p1
("POSITIVE_INFINITY")
- (Coq_value_prim (Coq_prim_number infinity))
+ (Coq_value_prim (Coq_prim_number JsNumber.infinity))
in
let p3 =
write_constant p2
("MAX_VALUE")
- (Coq_value_prim (Coq_prim_number max_value))
+ (Coq_value_prim (Coq_prim_number JsNumber.max_value))
in
let p4 =
write_constant p3
("MIN_VALUE")
- (Coq_value_prim (Coq_prim_number min_value))
+ (Coq_value_prim (Coq_prim_number JsNumber.min_value))
in
object_create_prealloc_constructor Coq_prealloc_number (Coq_value_prim
(Coq_prim_number 1.0)) p4
@@ -649,7 +649,7 @@ let object_prealloc_number_proto =
Coq_prealloc_object_proto))
("Number") p1
in
- object_with_primitive_value o (Coq_value_prim (Coq_prim_number zero))
+ object_with_primitive_value o (Coq_value_prim (Coq_prim_number JsNumber.zero))
(** val number_proto_to_string_function_object : coq_object **)
@@ -847,12 +847,12 @@ let bool_proto_value_of_function_object =
let object_prealloc_math =
let p =
write_constant Heap.empty ("PI") (Coq_value_prim
- (Coq_prim_number pi))
+ (Coq_prim_number JsNumber.pi))
in
- let p0 = write_constant p ("E") (Coq_value_prim (Coq_prim_number e)) in
+ let p0 = write_constant p ("E") (Coq_value_prim (Coq_prim_number JsNumber.e)) in
let p1 =
write_constant p0 ("LN2") (Coq_value_prim
- (Coq_prim_number ln2))
+ (Coq_prim_number JsNumber.ln2))
in
object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
Coq_prealloc_object_proto)) ("Math") p1
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 6b81d97..672ee7d 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -3,7 +3,7 @@ open JsCommon
open JsCommonAux
open JsInit
open JsInterpreterMonads
-open JsNumber
+(*open JsNumber*)
open JsPreliminary
open JsSyntax
open JsSyntaxAux
@@ -520,13 +520,13 @@ let to_integer runs0 s c v =
runs_type -> state -> execution_ctx -> value -> float specres **)
let to_int32 runs0 s c v =
- if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (to_int32 n))
+ if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (JsNumber.to_int32 n))
(** val to_uint32 :
runs_type -> state -> execution_ctx -> value -> float specres **)
let to_uint32 runs0 s c v =
- if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (to_uint32 n))
+ if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (JsNumber.to_uint32 n))
(** val to_string :
runs_type -> state -> execution_ctx -> value -> result **)
@@ -2150,7 +2150,7 @@ let run_construct_prealloc runs0 s c b args =
result_out (Coq_out_ter (s1, (res_val (Coq_value_object l)))))))
(fun follow ->
if list_eq_nil_decidable args
- then follow s (Coq_value_prim (Coq_prim_number zero))
+ then follow s (Coq_value_prim (Coq_prim_number JsNumber.zero))
else let_binding (get_arg 0 args) (fun v ->
if_number (to_number runs0 s c v) (fun x x0 ->
follow x (Coq_value_prim (Coq_prim_number x0)))))
@@ -3330,9 +3330,9 @@ let get_shift_op _foo_ = match _foo_ with
| Coq_binary_op_mod -> None
| Coq_binary_op_add -> None
| Coq_binary_op_sub -> None
-| Coq_binary_op_left_shift -> Some (false, int32_left_shift)
-| Coq_binary_op_right_shift -> Some (false, int32_right_shift)
-| Coq_binary_op_unsigned_right_shift -> Some (true, uint32_right_shift)
+| Coq_binary_op_left_shift -> Some (false, JsNumber.int32_left_shift)
+| Coq_binary_op_right_shift -> Some (false, JsNumber.int32_right_shift)
+| Coq_binary_op_unsigned_right_shift -> Some (true, JsNumber.uint32_right_shift)
| Coq_binary_op_lt -> None
| Coq_binary_op_gt -> None
| Coq_binary_op_le -> None
@@ -3371,9 +3371,9 @@ let get_bitwise_op _foo_ = match _foo_ with
| Coq_binary_op_disequal -> None
| Coq_binary_op_strict_equal -> None
| Coq_binary_op_strict_disequal -> None
-| Coq_binary_op_bitwise_and -> Some int32_bitwise_and
-| Coq_binary_op_bitwise_or -> Some int32_bitwise_or
-| Coq_binary_op_bitwise_xor -> Some int32_bitwise_xor
+| Coq_binary_op_bitwise_and -> Some JsNumber.int32_bitwise_and
+| Coq_binary_op_bitwise_or -> Some JsNumber.int32_bitwise_or
+| Coq_binary_op_bitwise_xor -> Some JsNumber.int32_bitwise_xor
| Coq_binary_op_and -> None
| Coq_binary_op_or -> None
| Coq_binary_op_coma -> None
@@ -3508,7 +3508,7 @@ let run_binary_op runs0 s c op v1 v2 =
((if b_unsigned then to_uint32 else to_int32) runs0 s c
v1) (fun s1 k1 ->
if_spec (to_uint32 runs0 s1 c v2) (fun s2 k2 ->
- let k2' = modulo_32 k2 in
+ let k2' = JsNumber.modulo_32 k2 in
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
(of_int (f k1 k2'))))))))
@@ -3740,7 +3740,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -3826,7 +3826,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -3888,7 +3888,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -3950,7 +3950,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -4012,7 +4012,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -4074,7 +4074,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -4136,7 +4136,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -4198,7 +4198,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -4260,7 +4260,7 @@ let run_unary_op runs0 s c op e =
if_spec (to_int32 runs0 s1 c v) (fun s2 k ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
- (of_int (int32_bitwise_not k))))))
+ (of_int (JsNumber.int32_bitwise_not k))))))
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
@@ -5310,15 +5310,15 @@ let run_call_prealloc runs0 s c b vthis args =
res_ter s0
(res_val (Coq_value_prim (Coq_prim_bool
(neg
- (or_decidable (number_comparable n nan)
- (or_decidable (number_comparable n infinity)
- (number_comparable n neg_infinity)))))))))
+ (or_decidable (number_comparable n JsNumber.nan)
+ (or_decidable (number_comparable n JsNumber.infinity)
+ (number_comparable n JsNumber.neg_infinity)))))))))
| Coq_prealloc_global_is_nan ->
let_binding (get_arg 0 args) (fun v ->
if_number (to_number runs0 s c v) (fun s0 n ->
res_ter s0
(res_val (Coq_value_prim (Coq_prim_bool
- (number_comparable n nan))))))
+ (number_comparable n JsNumber.nan))))))
| Coq_prealloc_global_decode_uri ->
(fun s ->
print_endline (__LOC__ ^ ": Not implemented because: " ^ Prheap.string_of_char_list s) ;
@@ -5809,7 +5809,7 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_prealloc_number ->
if list_eq_nil_decidable args
then result_out (Coq_out_ter (s,
- (res_val (Coq_value_prim (Coq_prim_number zero)))))
+ (res_val (Coq_value_prim (Coq_prim_number JsNumber.zero)))))
else let v = get_arg 0 args in to_number runs0 s c v
| Coq_prealloc_number_proto ->
(fun s ->
@@ -5952,7 +5952,7 @@ let run_call_prealloc runs0 s c b vthis args =
then if_not_throw
(object_put runs0 s2 c l
("length")
- (Coq_value_prim (Coq_prim_number zero)) throw_true)
+ (Coq_value_prim (Coq_prim_number JsNumber.zero)) throw_true)
(fun s3 x ->
result_out (Coq_out_ter (s3,
(res_val (Coq_value_prim Coq_prim_undef)))))
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index 186f367..e4368fd 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -1,5 +1,5 @@
open JsCommon
-open JsNumber
+(*open JsNumber*)
open JsSyntax
open JsSyntaxAux
open LibList
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index ddf3c9a..29383d1 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -1,8 +1,6 @@
open Fappli_IEEE_bits
open LibReflect
-let nat_eq x y = int_eq x y
-
type number = binary64
(** val nan : number **)
@@ -37,20 +35,19 @@ let max_value = max_float
let min_value = min_float (* (Int64.float_of_bits Int64.one) *)
-(*
- (** val pi : number **)
- let pi = (4. *. atan 1.)
+(** val pi : number **)
- (** val e : number **)
+let pi = 3.141592654 (* (4. *. atan 1.) *)
- let e = (exp 1.)
+(** val e : number **)
- (** val ln2 : number **)
+let e = 2.718281828 (* (exp 1.) *)
- let ln2 = (log 2.)
+(** val ln2 : number **)
+
+let ln2 = 0.693147181 (* (log 2.) *)
-*)
(** val from_string : string -> number **)
@@ -129,15 +126,8 @@ let sign = (fun x -> float_of_int (float_compare x 0.))
*)
-(** val number_comparable : number coq_Comparable **)
-
-let number_comparable = (fun n1 n2 -> int_eq 0 (float_compare n1 n2))
-
-(** val of_int : float -> number **)
-let of_int = fun x -> x
-let number_of_int = fun x -> float_of_int x
(** val to_int32 : number -> float **)
diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml
index 2b060b8..e396aeb 100644
--- a/generator/tests/jsref/JsPreliminary.ml
+++ b/generator/tests/jsref/JsPreliminary.ml
@@ -1,5 +1,5 @@
open JsCommon
-open JsNumber
+(*open JsNumber*)
open JsSyntax
open JsSyntaxAux
open LibReflect
@@ -9,9 +9,9 @@ open Shared
(** val convert_number_to_bool : number -> bool **)
let convert_number_to_bool n =
- if or_decidable (number_comparable n zero)
- (or_decidable (number_comparable n neg_zero)
- (number_comparable n nan))
+ if or_decidable (number_comparable n JsNumber.zero)
+ (or_decidable (number_comparable n JsNumber.neg_zero)
+ (number_comparable n JsNumber.nan))
then false
else true
@@ -39,23 +39,23 @@ let convert_value_to_boolean _foo_ = match _foo_ with
(** val convert_prim_to_number : prim -> number **)
let convert_prim_to_number _foo_ = match _foo_ with
-| Coq_prim_undef -> nan
-| Coq_prim_null -> zero
-| Coq_prim_bool b -> if b then one else zero
+| Coq_prim_undef -> JsNumber.nan
+| Coq_prim_null -> JsNumber.zero
+| Coq_prim_bool b -> if b then JsNumber.one else JsNumber.zero
| Coq_prim_number n -> n
-| Coq_prim_string s -> from_string s
+| Coq_prim_string s -> JsNumber.from_string s
(** val convert_number_to_integer : number -> number **)
let convert_number_to_integer n =
- if number_comparable n nan
- then zero
- else if or_decidable (number_comparable n zero)
- (or_decidable (number_comparable n neg_zero)
- (or_decidable (number_comparable n infinity)
- (number_comparable n neg_infinity)))
+ if number_comparable n JsNumber.nan
+ then JsNumber.zero
+ else if or_decidable (number_comparable n JsNumber.zero)
+ (or_decidable (number_comparable n JsNumber.neg_zero)
+ (or_decidable (number_comparable n JsNumber.infinity)
+ (number_comparable n JsNumber.neg_infinity)))
then n
- else mult (sign n) (floor (absolute n))
+ else mult (JsNumber.sign n) (floor (JsNumber.absolute n))
(** val convert_bool_to_string : bool -> string **)
@@ -70,7 +70,7 @@ let convert_prim_to_string _foo_ = match _foo_ with
"undefined"
| Coq_prim_null -> "null"
| Coq_prim_bool b -> convert_bool_to_string b
-| Coq_prim_number n -> to_string n
+| Coq_prim_number n -> JsNumber.to_string n
| Coq_prim_string s -> s
(** val equality_test_for_same_type : coq_type -> value -> value -> bool **)
@@ -95,16 +95,16 @@ let equality_test_for_same_type ty v1 v2 =
| Coq_prim_null -> false
| Coq_prim_bool b -> false
| Coq_prim_number n2 ->
- if number_comparable n1 nan
+ if number_comparable n1 JsNumber.nan
then false
- else if number_comparable n2 nan
+ else if number_comparable n2 JsNumber.nan
then false
- else if and_decidable (number_comparable n1 zero)
- (number_comparable n2 neg_zero)
+ else if and_decidable (number_comparable n1 JsNumber.zero)
+ (number_comparable n2 JsNumber.neg_zero)
then true
else if and_decidable
- (number_comparable n1 neg_zero)
- (number_comparable n2 zero)
+ (number_comparable n1 JsNumber.neg_zero)
+ (number_comparable n2 JsNumber.zero)
then true
else number_comparable n1 n2
| Coq_prim_string s -> false)
@@ -126,23 +126,23 @@ let strict_equality_test v1 v2 =
(** val inequality_test_number : number -> number -> prim **)
let inequality_test_number n1 n2 =
- if or_decidable (number_comparable n1 nan) (number_comparable n2 nan)
+ if or_decidable (number_comparable n1 JsNumber.nan) (number_comparable n2 nan)
then Coq_prim_undef
else if number_comparable n1 n2
then Coq_prim_bool false
- else if and_decidable (number_comparable n1 zero)
- (number_comparable n2 neg_zero)
+ else if and_decidable (number_comparable n1 JsNumber.zero)
+ (number_comparable n2 JsNumber.neg_zero)
then Coq_prim_bool false
- else if and_decidable (number_comparable n1 neg_zero)
- (number_comparable n2 zero)
+ else if and_decidable (number_comparable n1 JsNumber.neg_zero)
+ (number_comparable n2 JsNumber.zero)
then Coq_prim_bool false
- else if number_comparable n1 infinity
+ else if number_comparable n1 JsNumber.infinity
then Coq_prim_bool false
- else if number_comparable n2 infinity
+ else if number_comparable n2 JsNumber.infinity
then Coq_prim_bool true
- else if number_comparable n2 neg_infinity
+ else if number_comparable n2 JsNumber.neg_infinity
then Coq_prim_bool false
- else if number_comparable n1 neg_infinity
+ else if number_comparable n1 JsNumber.neg_infinity
then Coq_prim_bool true
else Coq_prim_bool (lt_bool n1 n2)
@@ -213,7 +213,7 @@ let typeof_prim _foo_ = match _foo_ with
let string_of_propname _foo_ = match _foo_ with
| Coq_propname_identifier s -> s
| Coq_propname_string s -> s
-| Coq_propname_number n -> to_string n
+| Coq_propname_number n -> JsNumber.to_string n
(** val string_of_native_error : native_error -> string **)
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index 41c64f5..75aa477 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -1,4 +1,4 @@
-open JsNumber
+(*open JsNumber*)
open Heap
open LibReflect
open Shared
@@ -45,7 +45,7 @@ type binary_op =
type literal =
| Coq_literal_null [@f] (** Auto Generated Attributes **)
| Coq_literal_bool [@f value] of bool (** Auto Generated Attributes **)
-| Coq_literal_number [@f value] of number (** Auto Generated Attributes **)
+| Coq_literal_number [@f value] of JsNumber.number (** Auto Generated Attributes **)
| Coq_literal_string [@f value] of string (** Auto Generated Attributes **)
type label =
@@ -64,7 +64,7 @@ let strictness_false =
type propname =
| Coq_propname_identifier [@f value] of string (** Auto Generated Attributes **)
| Coq_propname_string [@f value] of string (** Auto Generated Attributes **)
-| Coq_propname_number [@f value] of number (** Auto Generated Attributes **)
+| Coq_propname_number [@f value] of JsNumber.number (** Auto Generated Attributes **)
type expr =
| Coq_expr_this [@f] (** Auto Generated Attributes **)
@@ -279,7 +279,7 @@ type prim =
| Coq_prim_undef [@f] (** Auto Generated Attributes **)
| Coq_prim_null [@f] (** Auto Generated Attributes **)
| Coq_prim_bool [@f value] of bool (** Auto Generated Attributes **)
-| Coq_prim_number [@f value] of number (** Auto Generated Attributes **)
+| Coq_prim_number [@f value] of JsNumber.number (** Auto Generated Attributes **)
| Coq_prim_string [@f value] of string (** Auto Generated Attributes **)
type value =
diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml
index 4b5e221..81da2a8 100644
--- a/generator/tests/jsref/JsSyntaxAux.ml
+++ b/generator/tests/jsref/JsSyntaxAux.ml
@@ -1,4 +1,4 @@
-open JsNumber
+(*open JsNumber*)
open JsSyntax
open LibList
open LibReflect
--
GitLab