From 54a7139467b60b23808b47cef8becc0c4b61510c Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 1 Mar 2016 15:02:59 +0100
Subject: [PATCH] number to int
---
generator/Makefile | 2 +
generator/TODO | 6 ++
generator/stdlib_ml/stdlib.mli | 2 +
generator/tests/jsref/JsInit.ml | 114 ++++++++++++-------------
generator/tests/jsref/JsInterpreter.ml | 68 +++++++--------
generator/tests/jsref/JsNumber.ml | 2 +
generator/tests/jsref/LibInt.ml | 35 --------
generator/tests/jsref/Shared.ml | 4 +-
8 files changed, 103 insertions(+), 130 deletions(-)
diff --git a/generator/Makefile b/generator/Makefile
index bf11852..9cf4775 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -111,6 +111,8 @@ $(JSREF_PATH)/lineof.js: lineof.byte $(JSREF_ML:.ml=.token.js)
main: main.byte
+cmi: $(JSREF_ML:.ml=.cmi) $(JSREF_MLI:.mli=.cmi)
+
full: $(JSREF_ML:.ml=.log.js) $(JSREF_ML:.ml=.unlog.js) $(JSREF_ML:.ml=.token.js)
unlog: $(JSREF_ML:.ml=.unlog.js)
diff --git a/generator/TODO b/generator/TODO
index 71be890..1fb4388 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -7,7 +7,13 @@
+- check in Shared.ml whether we need to take absolute values
+ let string_sub s n l =
+ substring (int_abs n) (int_abs l) s
+-
+ string_sub str (int_of_float k0) 1
+ => TODO: check k0 is not negative
=========================================================
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index 2e10c91..eadaf32 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -36,6 +36,8 @@ val min : float -> float -> float
val max : float -> float -> float
val classify_float : float -> fpclass
+val int_abs : int -> int
+
val float_of_int : int -> float
val float_of_string : string -> float
val int_of_char : char -> int
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index a218c6c..56d2c22 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -232,58 +232,58 @@ let object_prealloc_global =
let global_eval_function_object =
object_create_prealloc_call Coq_prealloc_global_eval (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_parse_int_function_object : coq_object **)
let global_parse_int_function_object =
object_create_prealloc_call Coq_prealloc_global_parse_int (Coq_value_prim
(Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ (Pervasives.succ 0)))))) Heap.empty
+ 2.0)) Heap.empty
(** val global_parse_float_function_object : coq_object **)
let global_parse_float_function_object =
object_create_prealloc_call Coq_prealloc_global_parse_float (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_is_nan_function_object : coq_object **)
let global_is_nan_function_object =
object_create_prealloc_call Coq_prealloc_global_is_nan (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_is_finite_function_object : coq_object **)
let global_is_finite_function_object =
object_create_prealloc_call Coq_prealloc_global_is_finite (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_decode_uri_function_object : coq_object **)
let global_decode_uri_function_object =
object_create_prealloc_call Coq_prealloc_global_decode_uri (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_decode_uri_component_function_object : coq_object **)
let global_decode_uri_component_function_object =
object_create_prealloc_call Coq_prealloc_global_decode_uri_component
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val global_encode_uri_function_object : coq_object **)
let global_encode_uri_function_object =
object_create_prealloc_call Coq_prealloc_global_encode_uri (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val global_encode_uri_component_function_object : coq_object **)
let global_encode_uri_component_function_object =
object_create_prealloc_call Coq_prealloc_global_encode_uri_component
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_prealloc_object : coq_object **)
@@ -360,43 +360,41 @@ let object_prealloc_object =
Coq_prealloc_object_is_extensible))
in
object_create_prealloc_constructor Coq_prealloc_object (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p11
+ (Coq_prim_number 1.0)) p11
(** val object_get_proto_of_function_object : coq_object **)
let object_get_proto_of_function_object =
object_create_prealloc_call Coq_prealloc_object_get_proto_of
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_get_own_prop_descriptor_function_object : coq_object **)
let object_get_own_prop_descriptor_function_object =
object_create_prealloc_call Coq_prealloc_object_get_own_prop_descriptor
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_get_own_prop_name_function_object : coq_object **)
let object_get_own_prop_name_function_object =
object_create_prealloc_call Coq_prealloc_object_get_own_prop_name
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_create_function_object : coq_object **)
let object_create_function_object =
object_create_prealloc_call Coq_prealloc_object_create (Coq_value_prim
(Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ (Pervasives.succ 0)))))) Heap.empty
+ 2.0)) Heap.empty
(** val object_define_prop_function_object : coq_object **)
let object_define_prop_function_object =
object_create_prealloc_call Coq_prealloc_object_define_prop (Coq_value_prim
- (Coq_prim_number
- (of_int
- (my_Z_of_nat (Pervasives.succ (Pervasives.succ (Pervasives.succ 0)))))))
+ (Coq_prim_number 2.0))
Heap.empty
(** val object_define_props_function_object : coq_object **)
@@ -404,45 +402,45 @@ let object_define_prop_function_object =
let object_define_props_function_object =
object_create_prealloc_call Coq_prealloc_object_define_props
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ (Pervasives.succ 0)))))) Heap.empty
+ 2.0)) Heap.empty
(** val object_seal_function_object : coq_object **)
let object_seal_function_object =
object_create_prealloc_call Coq_prealloc_object_seal (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_freeze_function_object : coq_object **)
let object_freeze_function_object =
object_create_prealloc_call Coq_prealloc_object_freeze (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_prevent_extensions_function_object : coq_object **)
let object_prevent_extensions_function_object =
object_create_prealloc_call Coq_prealloc_object_prevent_extensions
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_is_sealed_function_object : coq_object **)
let object_is_sealed_function_object =
object_create_prealloc_call Coq_prealloc_object_is_sealed (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_is_frozen_function_object : coq_object **)
let object_is_frozen_function_object =
object_create_prealloc_call Coq_prealloc_object_is_frozen (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_is_extensible_function_object : coq_object **)
let object_is_extensible_function_object =
object_create_prealloc_call Coq_prealloc_object_is_extensible
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_prealloc_object_proto : coq_object **)
@@ -487,33 +485,33 @@ let object_prealloc_object_proto =
let object_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_object_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_proto_value_of_function_object : coq_object **)
let object_proto_value_of_function_object =
object_create_prealloc_call Coq_prealloc_object_proto_value_of
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_proto_has_own_prop_function_object : coq_object **)
let object_proto_has_own_prop_function_object =
object_create_prealloc_call Coq_prealloc_object_proto_has_own_prop
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_proto_is_prototype_of_function_object : coq_object **)
let object_proto_is_prototype_of_function_object =
object_create_prealloc_call Coq_prealloc_object_proto_is_prototype_of
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_proto_prop_is_enumerable_function_object : coq_object **)
let object_proto_prop_is_enumerable_function_object =
object_create_prealloc_call Coq_prealloc_object_proto_prop_is_enumerable
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val object_prealloc_function : coq_object **)
@@ -525,7 +523,7 @@ let object_prealloc_function =
Coq_prealloc_function_proto))
in
object_create_prealloc_constructor Coq_prealloc_function (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p
+ (Coq_prim_number 1.0)) p
(** val object_prealloc_function_proto : coq_object **)
@@ -539,7 +537,7 @@ let object_prealloc_function_proto =
Heap.write p ("length")
(Coq_attributes_data_of
(attrib_constant (Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat 0))))))
+ 0.0))))
in
let p1 =
write_native p0
@@ -571,28 +569,28 @@ let object_prealloc_function_proto =
let function_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_function_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val function_proto_call_function_object : coq_object **)
let function_proto_call_function_object =
object_create_prealloc_call Coq_prealloc_function_proto_call
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val function_proto_bind_function_object : coq_object **)
let function_proto_bind_function_object =
object_create_prealloc_call Coq_prealloc_function_proto_bind
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ 1.0)) Heap.empty
(** val function_proto_apply_function_object : coq_object **)
let function_proto_apply_function_object =
object_create_prealloc_call Coq_prealloc_function_proto_apply
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ (Pervasives.succ 0)))))) Heap.empty
+ 2.0)) Heap.empty
(** val object_prealloc_number : coq_object **)
@@ -627,7 +625,7 @@ let object_prealloc_number =
(Coq_value_prim (Coq_prim_number min_value))
in
object_create_prealloc_constructor Coq_prealloc_number (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p4
+ (Coq_prim_number 1.0)) p4
(** val object_prealloc_number_proto : coq_object **)
@@ -658,13 +656,13 @@ let object_prealloc_number_proto =
let number_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_number_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val number_proto_value_of_function_object : coq_object **)
let number_proto_value_of_function_object =
object_create_prealloc_call Coq_prealloc_number_proto_value_of
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_prealloc_array : coq_object **)
@@ -682,16 +680,16 @@ let object_prealloc_array =
let p1 =
write_constant p0 ("length")
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0)))))
+ 1.0))
in
object_create_prealloc_constructor Coq_prealloc_array (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p1
+ (Coq_prim_number 1.0)) p1
(** val array_is_array_function_object : coq_object **)
let array_is_array_function_object =
object_create_prealloc_call Coq_prealloc_array_is_array (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_prealloc_array_proto : coq_object **)
@@ -720,7 +718,7 @@ let object_prealloc_array_proto =
in
let p4 =
write_constant p3 ("length")
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0))))
+ (Coq_value_prim (Coq_prim_number 0.0))
in
object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
Coq_prealloc_object_proto)) ("Array") p4
@@ -729,25 +727,25 @@ let object_prealloc_array_proto =
let array_proto_pop_function_object =
object_create_prealloc_call Coq_prealloc_array_proto_pop (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_prim_number 0.0)) Heap.empty
(** val array_proto_push_function_object : coq_object **)
let array_proto_push_function_object =
object_create_prealloc_call Coq_prealloc_array_proto_push (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val array_proto_to_string_function_object : coq_object **)
let array_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_array_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val array_proto_join_function_object : coq_object **)
let array_proto_join_function_object =
object_create_prealloc_call Coq_prealloc_array_proto_join (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_prealloc_string : coq_object **)
@@ -758,7 +756,7 @@ let object_prealloc_string =
(Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_string_proto))
in
object_create_prealloc_constructor Coq_prealloc_string (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p
+ (Coq_prim_number 1.0)) p
(** val object_prealloc_string_proto : coq_object **)
@@ -789,13 +787,13 @@ let object_prealloc_string_proto =
let string_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_string_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val string_proto_value_of_function_object : coq_object **)
let string_proto_value_of_function_object =
object_create_prealloc_call Coq_prealloc_string_proto_value_of
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_prealloc_bool : coq_object **)
@@ -806,7 +804,7 @@ let object_prealloc_bool =
(Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_bool_proto))
in
object_create_prealloc_constructor Coq_prealloc_bool (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p
+ (Coq_prim_number 1.0)) p
(** val object_prealloc_bool_proto : coq_object **)
@@ -837,13 +835,13 @@ let object_prealloc_bool_proto =
let bool_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_bool_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val bool_proto_value_of_function_object : coq_object **)
let bool_proto_value_of_function_object =
object_create_prealloc_call Coq_prealloc_bool_proto_value_of
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_prealloc_math : coq_object **)
@@ -864,13 +862,13 @@ let object_prealloc_math =
let object_prealloc_date =
object_create_prealloc_constructor Coq_prealloc_date (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_prealloc_regexp : coq_object **)
let object_prealloc_regexp =
object_create_prealloc_constructor Coq_prealloc_regexp (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) Heap.empty
+ (Coq_prim_number 1.0)) Heap.empty
(** val object_prealloc_error : coq_object **)
@@ -881,7 +879,7 @@ let object_prealloc_error =
(Coq_value_object (Coq_object_loc_prealloc Coq_prealloc_error_proto))
in
object_create_prealloc_constructor Coq_prealloc_error (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Pervasives.succ 0))))) p
+ (Coq_prim_number 1.0)) p
(** val object_prealloc_error_proto : coq_object **)
@@ -912,7 +910,7 @@ let object_prealloc_error_proto =
let error_proto_to_string_function_object =
object_create_prealloc_call Coq_prealloc_error_proto_to_string
- (Coq_value_prim (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_value_prim (Coq_prim_number 0.0)) Heap.empty
(** val object_prealloc_native_error : native_error -> coq_object **)
@@ -925,7 +923,7 @@ let object_prealloc_native_error ne =
in
object_create_prealloc_constructor (Coq_prealloc_native_error ne)
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (Pervasives.succ 0))))) p
+ 1.0)) p
(** val object_prealloc_native_error_proto : native_error -> coq_object **)
@@ -958,7 +956,7 @@ let object_prealloc_json =
let throw_type_error_object =
let o =
object_create_prealloc_call Coq_prealloc_throw_type_error (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat 0)))) Heap.empty
+ (Coq_prim_number 0.0)) Heap.empty
in
let o0 = object_with_scope o (Some lexical_env_initial) in
let o1 = object_with_formal_params o0 (Some []) in
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 0b5f927..1b1fcb3 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -632,7 +632,7 @@ let object_can_put runs0 s c l x =
let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc newWritable throw def =
if lt_int_decidable newLen oldLen
- then let_binding (Z.sub oldLen 1.) (fun oldLen' ->
+ then let_binding (oldLen -. 1.) (fun oldLen' ->
if_string
(to_string runs0 s c (Coq_value_prim (Coq_prim_number
(of_int oldLen')))) (fun s0 slen ->
@@ -641,7 +641,7 @@ let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc n
if not_decidable (bool_decidable deleteSucceeded)
then let_binding
(descriptor_with_value newLenDesc (Some (Coq_value_prim
- (Coq_prim_number (of_int (Z.add oldLen' 1.))))))
+ (Coq_prim_number (of_int (oldLen' +. 1.))))))
(fun newLenDesc0 ->
let_binding
(if not_decidable (bool_decidable newWritable)
@@ -872,7 +872,7 @@ let object_define_own_prop runs0 s c l x desc throw =
(fun s2 slen ->
if and_decidable (string_comparable x slen)
(not_decidable
- (int_comparable ilen
+ (float_eq ilen
((fun p -> 1. +. (2. *. p))
((fun p -> 1. +. (2. *. p))
((fun p -> 1. +. (2. *. p))
@@ -932,8 +932,7 @@ let object_define_own_prop runs0 s c l x desc throw =
(Coq_value_prim
(Coq_prim_number
(of_int
- (Z.add index
- 1.)))))
+ (index +. 1.)))))
in
default s4
("length")
@@ -1118,7 +1117,7 @@ let prim_new_object s _foo_ = match _foo_ with
Heap.write p ("length")
(Coq_attributes_data_of
(attributes_data_intro_constant (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (length s0)))))))))
+ (Coq_prim_number (number_of_int (length s0))))))))
(fun s' -> res_ter s' (res_val (Coq_value_object l))))))
(** val to_object : state -> value -> result **)
@@ -1672,7 +1671,7 @@ let rec array_args_map_loop runs0 s c l args ind =
(object_heap_map_properties_pickable_option s l (fun p ->
Heap.write p (JsNumber.to_string (of_int ind))
(Coq_attributes_data_of (attributes_data_intro_all_true h))))
- (fun s' -> array_args_map_loop runs0 s' c l rest (Z.add ind 1.))
+ (fun s' -> array_args_map_loop runs0 s' c l rest (ind +. 1.))
(** val string_of_prealloc : prealloc -> string **)
@@ -2238,7 +2237,7 @@ let run_construct_prealloc runs0 s c b args =
Heap.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v))))
(fun s0 ->
- follow s0 (my_Z_of_nat (Pervasives.succ 0)))
+ follow s0 1.0)
| Coq_prim_null ->
if_some
(object_heap_map_properties_pickable_option s' l
@@ -2246,7 +2245,7 @@ let run_construct_prealloc runs0 s c b args =
Heap.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v))))
(fun s0 ->
- follow s0 (my_Z_of_nat (Pervasives.succ 0)))
+ follow s0 1.0)
| Coq_prim_bool b0 ->
if_some
(object_heap_map_properties_pickable_option s' l
@@ -2254,7 +2253,7 @@ let run_construct_prealloc runs0 s c b args =
Heap.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v))))
(fun s0 ->
- follow s0 (my_Z_of_nat (Pervasives.succ 0)))
+ follow s0 1.0)
| Coq_prim_number vlen ->
if_spec
(to_uint32 runs0 s' c (Coq_value_prim
@@ -2269,14 +2268,14 @@ let run_construct_prealloc runs0 s c b args =
Heap.write p1 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v))))
(fun s1 ->
- follow s1 (my_Z_of_nat (Pervasives.succ 0))))
+ follow s1 1.0))
| Coq_value_object o0 ->
if_some
(object_heap_map_properties_pickable_option s' l
(fun p0 ->
Heap.write p0 ("0") (Coq_attributes_data_of
(attributes_data_intro_all_true v)))) (fun s0 ->
- follow s0 (my_Z_of_nat (Pervasives.succ 0))))
+ follow s0 1.0))
else if_some
(object_heap_map_properties_pickable_option s' l
(fun p0 ->
@@ -2284,7 +2283,7 @@ let run_construct_prealloc runs0 s c b args =
("length")
(Coq_attributes_data_of { attributes_data_value =
(Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat arg_len))));
+ (number_of_int arg_len)));
attributes_data_writable = true;
attributes_data_enumerable = false;
attributes_data_configurable = false }))) (fun s0 ->
@@ -2353,7 +2352,7 @@ let run_construct_prealloc runs0 s c b args =
let (l, s2) = object_alloc s0 o in
let_binding
(attributes_data_intro_constant (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (length s1))))))
+ (Coq_prim_number (number_of_int (length s1)))))
(fun lenDesc ->
if_some
(object_heap_map_properties_pickable_option s2 l (fun p ->
@@ -2594,7 +2593,7 @@ let creating_function_object runs0 s c names bd x str =
let (l, s1) = p in
let_binding { attributes_data_value = (Coq_value_prim
(Coq_prim_number
- (of_int (my_Z_of_nat (LibList.length names)))));
+ (number_of_int (LibList.length names))));
attributes_data_writable = false; attributes_data_enumerable =
false; attributes_data_configurable = false } (fun a1 ->
if_bool
@@ -2772,7 +2771,7 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
if_bool
(object_define_own_prop runs0 s c l
(convert_prim_to_string (Coq_prim_number
- (of_int (my_Z_of_nat len'))))
+ (number_of_int len')))
(descriptor_of_attributes (Coq_attributes_data_of a)) false)
(fun s1 b ->
if ge_nat_decidable len' (LibList.length xs)
@@ -2795,7 +2794,7 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
if_bool
(object_define_own_prop runs0 s3 c lmap
(convert_prim_to_string (Coq_prim_number
- (of_int (my_Z_of_nat len'))))
+ (number_of_int len')))
(descriptor_of_attributes
(Coq_attributes_accessor_of a')) false)
(fun s4 b' ->
@@ -2825,7 +2824,7 @@ let create_arguments_object runs0 s c lf xs args x str =
let_binding (object_alloc s o) (fun p ->
let (l, s') = p in
let_binding { attributes_data_value = (Coq_value_prim (Coq_prim_number
- (of_int (my_Z_of_nat (LibList.length args)))));
+ (number_of_int (LibList.length args))));
attributes_data_writable = true; attributes_data_enumerable = false;
attributes_data_configurable = true } (fun a ->
if_bool
@@ -3080,7 +3079,7 @@ let run_object_get_own_prop runs0 s c l x =
(fun s1 k ->
if_string
(runs0.runs_type_to_string s1 c (Coq_value_prim
- (Coq_prim_number (of_int (my_Z_of_nat (Z.abs_nat k))))))
+ (Coq_prim_number (abs_float k))))
(fun s2 s3 ->
if not_decidable (string_comparable x s3)
then res_spec s2 Coq_full_descriptor_undef
@@ -3088,12 +3087,12 @@ let run_object_get_own_prop runs0 s c l x =
if_spec
(to_int32 runs0 s4 c (Coq_value_prim
(Coq_prim_string x))) (fun s5 k0 ->
- let_binding (Z.of_nat (length str)) (fun len ->
+ let_binding (number_of_int (length str)) (fun len ->
if le_int_decidable len k0
then res_spec s5 Coq_full_descriptor_undef
else let resultStr =
- string_sub str k0
- (my_Z_of_nat (Pervasives.succ 0))
+ string_sub str (int_of_float k0) 1
+ (* TODO: check k0 is not negative *)
in
let a = { attributes_data_value =
(Coq_value_prim (Coq_prim_string
@@ -4335,7 +4334,7 @@ let run_array_element_list runs0 s c l oes n =
if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
if_string
(to_string runs0 s2 c (Coq_value_prim (Coq_prim_number
- (of_int (Z.add ilen n))))) (fun s3 slen ->
+ (ilen +. n)))) (fun s3 slen ->
let_binding { attributes_data_value = v;
attributes_data_writable = true;
attributes_data_enumerable = true;
@@ -4349,7 +4348,7 @@ let run_array_element_list runs0 s c l oes n =
| None ->
let_binding (elision_head_count (None :: oes')) (fun firstIndex ->
runs0.runs_type_array_element_list s c l
- (elision_head_remove (None :: oes')) (my_Z_of_nat firstIndex)))
+ (elision_head_remove (None :: oes')) (number_of_int firstIndex)))
(** val init_array :
runs_type -> state -> execution_ctx -> object_loc -> expr option list ->
@@ -4366,7 +4365,7 @@ let init_array runs0 s c l oes =
if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
if_spec
(to_uint32 runs0 s2 c (Coq_value_prim (Coq_prim_number
- (of_int (Z.add ilen (my_Z_of_nat elisionLength))))))
+ (ilen +. number_of_int elisionLength))))
(fun s3 len ->
if_not_throw
(object_put runs0 s3 c l0
@@ -5085,7 +5084,7 @@ let rec push runs0 s c l args ilen =
if_string (to_string runs0 s c (Coq_value_prim (Coq_prim_number vlen)))
(fun s0 slen ->
if_not_throw (object_put runs0 s0 c l slen v throw_true) (fun s1 x ->
- push runs0 s1 c l vs (Z.add ilen 1.))))
+ push runs0 s1 c l vs (ilen +. 1.))))
(** val run_object_is_sealed :
runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
@@ -5228,7 +5227,7 @@ let run_get_args_for_apply runs0 s c l index n =
(of_int index)))) (fun s0 sindex ->
if_value (run_object_get runs0 s0 c l sindex) (fun s1 v ->
let_binding
- (runs0.runs_type_get_args_for_apply s1 c l (Z.add index 1.) n)
+ (runs0.runs_type_get_args_for_apply s1 c l (index +. 1.) n)
(fun tail_args ->
if_spec tail_args (fun s2 tail -> res_spec s2 (v :: tail)))))
else res_spec s []
@@ -5266,7 +5265,7 @@ let run_array_join_elements runs0 s c l k length0 sep sR =
let_binding (valueToStringForJoin runs0 s c l k) (fun sE ->
if_spec sE (fun s0 element ->
let_binding (append ss element) (fun sR0 ->
- runs0.runs_type_array_join_elements s0 c l (Z.add k 1.)
+ runs0.runs_type_array_join_elements s0 c l (k +. 1.)
length0 sep sR0))))
else res_ter s (res_val (Coq_value_prim (Coq_prim_string sR)))
@@ -5679,12 +5678,11 @@ let run_call_prealloc runs0 s c b vthis args =
(Coq_prim_number n)))
(fun s'1 ilen ->
if lt_int_decidable ilen
- (my_Z_of_nat (LibList.length a))
+ (number_of_int (LibList.length a))
then res_spec s'1 0.
else res_spec s'1
- (Z.sub ilen
- (my_Z_of_nat
- (LibList.length a)))))
+ (ilen -.
+ (number_of_int (LibList.length a)))))
else res_spec s' 0.)) (fun vlength ->
if_spec vlength (fun s'0 length0 ->
let_binding { attributes_data_value =
@@ -5940,7 +5938,7 @@ let run_call_prealloc runs0 s c b vthis args =
then vsep
else Coq_value_prim (Coq_prim_string (","))) (fun rsep ->
if_string (to_string runs0 s2 c rsep) (fun s3 sep ->
- if int_comparable ilen (my_Z_of_nat 0)
+ if float_eq ilen 0.0
then res_ter s3
(res_val (Coq_value_prim (Coq_prim_string "")))
else let_binding (valueToStringForJoin runs0 s3 c l 0.)
@@ -5953,7 +5951,7 @@ let run_call_prealloc runs0 s c b vthis args =
(run_object_get runs0 s0 c l
("length")) (fun s1 vlen ->
if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
- if int_comparable ilen (my_Z_of_nat 0)
+ if float_eq ilen 0.0
then if_not_throw
(object_put runs0 s2 c l
("length")
@@ -5963,7 +5961,7 @@ let run_call_prealloc runs0 s c b vthis args =
(res_val (Coq_value_prim Coq_prim_undef)))))
else if_string
(to_string runs0 s2 c (Coq_value_prim (Coq_prim_number
- (of_int (Z.sub ilen 1.))))) (fun s3 sindx ->
+ (of_int (ilen -. 1.))))) (fun s3 sindx ->
if_value (run_object_get runs0 s3 c l sindx)
(fun s4 velem ->
if_not_throw
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index 3c4fd4f..03f3be5 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -129,6 +129,8 @@ let number_comparable = (fun n1 n2 -> int_eq 0 (float_compare n1 n2))
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/LibInt.ml b/generator/tests/jsref/LibInt.ml
index fae323b..4688e5b 100644
--- a/generator/tests/jsref/LibInt.ml
+++ b/generator/tests/jsref/LibInt.ml
@@ -2,38 +2,3 @@ open BinInt
open Datatypes
open LibReflect
-(** val my_Z_of_nat : int -> float **)
-
-let my_Z_of_nat =
- Z.of_nat
-
-(** val comparison_compare : comparison -> comparison -> bool **)
-
-let comparison_compare c1 c2 =
- match c1 with
- | Eq ->
- (match c2 with
- | Eq -> true
- | Lt -> false
- | Gt -> false)
- | Lt ->
- (match c2 with
- | Eq -> false
- | Lt -> true
- | Gt -> false)
- | Gt ->
- (match c2 with
- | Eq -> false
- | Lt -> false
- | Gt -> true)
-
-(** val comparison_comparable : comparison coq_Comparable **)
-
-let comparison_comparable x y =
- comparison_compare x y
-
-(** val int_comparable : float coq_Comparable **)
-
-let int_comparable x y =
- comparison_comparable (Z.compare x y) Eq
-
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index b7a0f92..74fe425 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -18,10 +18,10 @@ let int_of_char = (fun c -> float_of_int (int_of_char c))
let ascii_comparable = (=)
-(** val string_sub : string -> float -> float -> string **)
+(** val string_sub : string -> int -> int -> string **)
let string_sub s n l =
- substring (Z.abs_nat n) (Z.abs_nat l) s
+ substring n l s
(** val lt_int_decidable : float -> float -> coq_Decidable **)
--
GitLab