From 51831c845ff5079a151cfb7cd0afbdd7328c20c0 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Thu, 26 Nov 2015 18:30:21 +0100
Subject: [PATCH] progress

---
 generator/Makefile                           | 19 ++++--
 generator/stdlib_ml/stdlib.mli               | 30 +++++++--
 generator/tests/jsref/JsCommon.ml            | 49 ++++++++-------
 generator/tests/jsref/JsInit.ml              |  2 +-
 generator/tests/jsref/JsInterpreter.ml       | 66 ++++++++++----------
 generator/tests/jsref/JsInterpreterMonads.ml |  2 +-
 generator/tests/jsref/JsNumber.ml            | 10 ++-
 generator/tests/jsref/JsPreliminary.ml       | 23 ++++---
 8 files changed, 120 insertions(+), 81 deletions(-)

diff --git a/generator/Makefile b/generator/Makefile
index fe9ee04..eee7b24 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -41,18 +41,22 @@ tests/%.ml: tests/%.v
 	cd $(@D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
 
 .PRECIOUS: tests/jsref/%.ml
-tests/jsref/%.ml:
-	$(MAKE) -C $(CURDIR)/../../.. interpreter
-	cp ../../../interp/src/extract/*.ml tests/jsref/
-	../../convert-ml-strings.pl tests/jsref/*.ml
-	cd $(@D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
+#tests/jsref/%.ml:
+#	$(MAKE) -C $(CURDIR)/../../.. interpreter
+#	cp ../../../interp/src/extract/*.ml tests/jsref/
+#	../../convert-ml-strings.pl tests/jsref/*.ml
+#	cd $(@D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
 
-tests/%.ml.d: tests/%.ml tests/%.mli
+tests/%.ml.d: tests/%.ml
 	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
 
 tests/%.cmi tests/%.unlog.js: tests/%.ml main.byte stdlib
 	./main.byte -mode unlog -I $(<D) $<
 
+tests/%.cmi tests/%.unlog.js: tests/%.mli stdlib
+	ocamlc -I stdlib_ml -open Stdlib -I $(<D) $<
+
+
 tests/%.log.js: tests/%.ml tests/%.cmi main.byte stdlib
 	./main.byte -mode log -I $(<D) $<
 
@@ -100,3 +104,6 @@ endif
 # records -> replace warning with code
 # lazy -> use a function for fresh locations in copied extracted code
 # replace "char list" with strings.
+# fix functor translation
+# missing return in:    funcdecl_name: function (x) { x.funcdecl_name},
+# change extraction of:   native_error_compare
\ No newline at end of file
diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli
index c427c45..d430fc0 100644
--- a/generator/stdlib_ml/stdlib.mli
+++ b/generator/stdlib_ml/stdlib.mli
@@ -44,6 +44,7 @@ val string_of_float : float -> string
 val string_of_int : int -> string
 
 val ( === ) : 'a -> 'a -> bool
+val ( <> ) : 'a -> 'a -> bool
 val ( < ) : 'a -> 'a -> bool
 val ( > ) : 'a -> 'a -> bool
 val ( <= ) : 'a -> 'a -> bool 
@@ -111,11 +112,6 @@ val prerr_string : string -> unit
 val prerr_newline : unit -> unit
 
 
-module Parser_main : sig 
-  val exp_from_string : ?force_strict:bool -> string -> string
-end 
-
-
 module Parser_syntax : sig (* ARTHUR: to implement *)
   type unary_op
   type arith_op
@@ -123,3 +119,27 @@ module Parser_syntax : sig (* ARTHUR: to implement *)
   type exp
 end
 
+module Parser_main : sig 
+  val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp
+end 
+
+(* ARTHUR: not needed
+module Parser : sig
+  exception ParserFailure of string
+  exception InvalidArgument
+end
+
+*)
+
+module Obj : sig
+  type t
+end
+
+val print_endline : string -> unit
+
+val __LOC__ : string
+
+module Prheap : sig
+  val prstate : bool -> string -> string
+  val string_of_char_list : string -> string
+end
\ No newline at end of file
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index dbdcf5a..ff70f85 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -25,7 +25,7 @@ let res_label_in r labs =
 
 (** val convert_literal_to_prim : literal -> prim **)
 
-let convert_literal_to_prim = function
+let convert_literal_to_prim _foo_ = match _foo_ with
 | Coq_literal_null -> Coq_prim_null
 | Coq_literal_bool b -> Coq_prim_bool b
 | Coq_literal_number n -> Coq_prim_number n
@@ -33,7 +33,7 @@ let convert_literal_to_prim = function
 
 (** val type_of_prim : prim -> coq_type **)
 
-let type_of_prim = function
+let type_of_prim _foo_ = match _foo_ with
 | Coq_prim_undef -> Coq_type_undef
 | Coq_prim_null -> Coq_type_null
 | Coq_prim_bool b -> Coq_type_bool
@@ -42,7 +42,7 @@ let type_of_prim = function
 
 (** val type_of : value -> coq_type **)
 
-let type_of = function
+let type_of _foo_ = match _foo_ with
 | Coq_value_prim w -> type_of_prim w
 | Coq_value_object o -> Coq_type_object
 
@@ -132,7 +132,7 @@ let attributes_accessor_of_descriptor desc =
 
 (** val descriptor_of_attributes : attributes -> descriptor **)
 
-let descriptor_of_attributes = function
+let descriptor_of_attributes _foo_ = match _foo_ with
 | Coq_attributes_data_of ad ->
   { descriptor_value = (Some ad.attributes_data_value); descriptor_writable =
     (Some ad.attributes_data_writable); descriptor_get = None;
@@ -148,13 +148,13 @@ let descriptor_of_attributes = function
 
 (** val attributes_configurable : attributes -> bool **)
 
-let attributes_configurable = function
+let attributes_configurable _foo_ = match _foo_ with
 | Coq_attributes_data_of ad -> ad.attributes_data_configurable
 | Coq_attributes_accessor_of aa -> aa.attributes_accessor_configurable
 
 (** val attributes_enumerable : attributes -> bool **)
 
-let attributes_enumerable = function
+let attributes_enumerable _foo_ = match _foo_ with
 | Coq_attributes_data_of ad -> ad.attributes_data_enumerable
 | Coq_attributes_accessor_of aa -> aa.attributes_accessor_enumerable
 
@@ -209,7 +209,7 @@ let object_new vproto sclass =
 
 (** val attributes_writable : attributes -> bool **)
 
-let attributes_writable = function
+let attributes_writable _foo_ = match _foo_ with
 | Coq_attributes_data_of ad -> ad.attributes_data_writable
 | Coq_attributes_accessor_of aa -> false
 
@@ -278,7 +278,7 @@ let ref_create_env_loc l x strict =
 
 (** val mutability_of_bool : bool -> mutability **)
 
-let mutability_of_bool = function
+let mutability_of_bool _foo_ = match _foo_ with
 | true -> Coq_mutability_deletable
 | false -> Coq_mutability_nondeletable
 
@@ -418,7 +418,7 @@ let execution_ctx_initial str =
 
 (** val element_funcdecl : element -> funcdecl list **)
 
-let element_funcdecl = function
+let element_funcdecl _foo_ = match _foo_ with
 | Coq_element_stat s -> []
 | Coq_element_func_decl (name, args, bd) ->
   { funcdecl_name = name; funcdecl_parameters = args; funcdecl_body =
@@ -431,7 +431,7 @@ let prog_funcdecl p =
 
 (** val stat_vardecl : stat -> string list **)
 
-let rec stat_vardecl = function
+let rec stat_vardecl _foo_ = match _foo_ with
 | Coq_stat_expr e -> []
 | Coq_stat_label (s0, s) -> stat_vardecl s
 | Coq_stat_block ts -> concat (map stat_vardecl ts)
@@ -462,7 +462,7 @@ let rec stat_vardecl = function
 
 (** val switchbody_vardecl : switchbody -> string list **)
 
-and switchbody_vardecl = function
+and switchbody_vardecl _foo_ = match _foo_ with
 | Coq_switchbody_nodefault scl -> concat (map switchclause_vardecl scl)
 | Coq_switchbody_withdefault (scl1, sl, scl2) ->
   append (concat (map switchclause_vardecl scl1))
@@ -471,12 +471,12 @@ and switchbody_vardecl = function
 
 (** val switchclause_vardecl : switchclause -> string list **)
 
-and switchclause_vardecl = function
+and switchclause_vardecl _foo_ = match _foo_ with
 | Coq_switchclause_intro (e, sl) -> concat (map stat_vardecl sl)
 
 (** val element_vardecl : element -> string list **)
 
-let element_vardecl = function
+let element_vardecl _foo_ = match _foo_ with
 | Coq_element_stat t -> stat_vardecl t
 | Coq_element_func_decl (name, args, bd) -> []
 
@@ -491,14 +491,14 @@ type preftype =
 
 (** val method_of_preftype : preftype -> string **)
 
-let method_of_preftype = function
+let method_of_preftype _foo_ = match _foo_ with
 | Coq_preftype_number -> "valueOf"
 | Coq_preftype_string ->
   "toString"
 
 (** val other_preftypes : preftype -> preftype **)
 
-let other_preftypes = function
+let other_preftypes _foo_ = match _foo_ with
 | Coq_preftype_number -> Coq_preftype_string
 | Coq_preftype_string -> Coq_preftype_number
 
@@ -529,7 +529,7 @@ let sub_one n =
 
 (** val is_syntactic_eval : expr -> bool **)
 
-let is_syntactic_eval = function
+let is_syntactic_eval _foo_ = match _foo_ with
 | Coq_expr_this -> false
 | Coq_expr_identifier s -> string_comparable s ("eval")
 | Coq_expr_literal l ->
@@ -553,7 +553,7 @@ let is_syntactic_eval = function
 
 (** val elision_head_count : 'a1 option list -> int **)
 
-let rec elision_head_count = function
+let rec elision_head_count _foo_ = match _foo_ with
 | [] -> 0
 | o :: ol' ->
   (match o with
@@ -583,15 +583,16 @@ let elision_tail_remove ol =
 
 let parse_pickable = (fun s strict ->
     let str = String.concat "" (List.map (String.make 1) s) in
-    try
+    (* try  ARTHUR HACK *)
       let parserExp = Parser_main.exp_from_string ~force_strict:strict str in
       Some (JsSyntaxInfos.add_infos_prog strict
         (Translate_syntax.exp_to_prog parserExp))
-    with
-    (* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
-    | Parser.ParserFailure _ [@f]  (** Auto Generated Attributes **)
-    | Parser.InvalidArgument ->
-      prerr_string ("Warning:  Parser error on eval.  Input string:  \"" ^ str ^ "\"\n");
-      None
+    (* with
+      (* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
+      | Parser.ParserFailure _ [@f]  (** Auto Generated Attributes **)
+      | Parser.InvalidArgument ->
+        prerr_string ("Warning:  Parser error on eval.  Input string:  \"" ^ str ^ "\"\n");
+        None
+    *)
   )
 
diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml
index 2e8e88a..046ec3f 100644
--- a/generator/tests/jsref/JsInit.ml
+++ b/generator/tests/jsref/JsInit.ml
@@ -74,7 +74,7 @@ let object_prealloc_global_proto = (Coq_value_prim Coq_prim_null)
 (** val object_prealloc_global_class : string **)
 
 let object_prealloc_global_class = (
-  let rec aux s = function
+  let rec aux s _foo_ = match _foo_ with
   | 0 -> []
   | n -> let n' = n - 1 in
     s.[n'] :: aux s n'
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 1be8e42..992914b 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -499,7 +499,7 @@ let to_primitive runs0 s c v prefo =
 (** val to_number :
     runs_type -> state -> execution_ctx -> value -> result **)
 
-let to_number runs0 s c = function
+let to_number runs0 s c _foo_ = match _foo_ with
 | Coq_value_prim w ->
   result_out (Coq_out_ter (s,
     (res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w))))))
@@ -534,7 +534,7 @@ let to_uint32 runs0 s c v =
 (** val to_string :
     runs_type -> state -> execution_ctx -> value -> result **)
 
-let to_string runs0 s c = function
+let to_string runs0 s c _foo_ = match _foo_ with
 | Coq_value_prim w ->
   result_out (Coq_out_ter (s,
     (res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w))))))
@@ -995,7 +995,7 @@ let object_define_own_prop runs0 s c l x desc throw =
 (** val run_to_descriptor :
     runs_type -> state -> execution_ctx -> value -> descriptor specres **)
 
-let run_to_descriptor runs0 s c = function
+let run_to_descriptor runs0 s c _foo_ = match _foo_ with
 | Coq_value_prim p -> throw_result (run_error s Coq_native_error_type)
 | Coq_value_object l ->
   let sub0 = fun s0 desc name conv k ->
@@ -1064,7 +1064,7 @@ let run_to_descriptor runs0 s c = function
 
 (** val prim_new_object : state -> prim -> result **)
 
-let prim_new_object s = function
+let prim_new_object s _foo_ = match _foo_ with
 | Coq_prim_undef ->
   (fun s message ->
   print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
@@ -1123,7 +1123,7 @@ let prim_new_object s = function
 
 (** val to_object : state -> value -> result **)
 
-let to_object s = function
+let to_object s _foo_ = match _foo_ with
 | Coq_value_prim w ->
   (match w with
    | Coq_prim_undef -> run_error s Coq_native_error_type
@@ -1293,7 +1293,7 @@ let env_record_get_binding_value runs0 s c l x str =
 (** val ref_get_value :
     runs_type -> state -> execution_ctx -> resvalue -> value specres **)
 
-let ref_get_value runs0 s c = function
+let ref_get_value runs0 s c _foo_ = match _foo_ with
 | Coq_resvalue_empty ->
   (fun s message ->
   print_endline (__LOC__ ^ ": Stuck!\nState:  " ^ Prheap.prstate true s
@@ -1667,7 +1667,7 @@ let rec array_args_map_loop runs0 s c l args ind =
 
 (** val string_of_prealloc : prealloc -> string **)
 
-let string_of_prealloc = function
+let string_of_prealloc _foo_ = match _foo_ with
 | Coq_prealloc_global -> "global"
 | Coq_prealloc_global_eval ->
   "global_eval"
@@ -3099,7 +3099,7 @@ let run_object_get_own_prop runs0 s c l x =
 (** val run_function_has_instance :
     runs_type -> state -> object_loc -> value -> result **)
 
-let run_function_has_instance runs0 s lv = function
+let run_function_has_instance runs0 s lv _foo_ = match _foo_ with
 | Coq_value_prim p -> run_error s Coq_native_error_type
 | Coq_value_object lo ->
   if_some (run_object_method object_proto_ s lv) (fun vproto ->
@@ -3174,7 +3174,7 @@ let run_object_has_instance runs0 s c b l v =
 (** val from_prop_descriptor :
     runs_type -> state -> execution_ctx -> full_descriptor -> result **)
 
-let from_prop_descriptor runs0 s c = function
+let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
 | Coq_full_descriptor_undef ->
   result_out (Coq_out_ter (s, (res_val (Coq_value_prim Coq_prim_undef))))
 | Coq_full_descriptor_some a ->
@@ -3233,7 +3233,7 @@ let from_prop_descriptor runs0 s c = function
 
 (** val is_lazy_op : binary_op -> bool option **)
 
-let is_lazy_op = function
+let is_lazy_op _foo_ = match _foo_ with
 | Coq_binary_op_mult -> None
 | Coq_binary_op_div -> None
 | Coq_binary_op_mod -> None
@@ -3262,7 +3262,7 @@ let is_lazy_op = function
 (** val get_puremath_op :
     binary_op -> (number -> number -> number) option **)
 
-let get_puremath_op = function
+let get_puremath_op _foo_ = match _foo_ with
 | Coq_binary_op_mult -> Some mult
 | Coq_binary_op_div -> Some div
 | Coq_binary_op_mod -> Some fmod
@@ -3290,7 +3290,7 @@ let get_puremath_op = function
 
 (** val get_inequality_op : binary_op -> (bool * bool) option **)
 
-let get_inequality_op = function
+let get_inequality_op _foo_ = match _foo_ with
 | Coq_binary_op_mult -> None
 | Coq_binary_op_div -> None
 | Coq_binary_op_mod -> None
@@ -3319,7 +3319,7 @@ let get_inequality_op = function
 (** val get_shift_op :
     binary_op -> (bool * (float -> float -> float)) option **)
 
-let get_shift_op = function
+let get_shift_op _foo_ = match _foo_ with
 | Coq_binary_op_mult -> None
 | Coq_binary_op_div -> None
 | Coq_binary_op_mod -> None
@@ -3347,7 +3347,7 @@ let get_shift_op = function
 
 (** val get_bitwise_op : binary_op -> (float -> float -> float) option **)
 
-let get_bitwise_op = function
+let get_bitwise_op _foo_ = match _foo_ with
 | Coq_binary_op_mult -> None
 | Coq_binary_op_div -> None
 | Coq_binary_op_mod -> None
@@ -3463,7 +3463,7 @@ let convert_twice_string runs0 s c v1 v2 =
 
 (** val issome : 'a1 option -> bool **)
 
-let issome = function
+let issome _foo_ = match _foo_ with
 | Some t -> true
 | None -> false
 
@@ -3615,7 +3615,7 @@ let run_binary_op runs0 s c op v1 v2 =
 
 (** val run_prepost_op : unary_op -> ((number -> number) * bool) option **)
 
-let run_prepost_op = function
+let run_prepost_op _foo_ = match _foo_ with
 | Coq_unary_op_delete -> None
 | Coq_unary_op_void -> None
 | Coq_unary_op_typeof -> None
@@ -3630,7 +3630,7 @@ let run_prepost_op = function
 
 (** val run_typeof_value : state -> value -> string **)
 
-let run_typeof_value s = function
+let run_typeof_value s _foo_ = match _foo_ with
 | Coq_value_prim w -> typeof_prim w
 | Coq_value_object l ->
   if is_callable_dec s (Coq_value_object l)
@@ -4272,7 +4272,7 @@ let create_new_function_in runs0 s c args bd =
 (** val init_object :
     runs_type -> state -> execution_ctx -> object_loc -> propdefs -> result **)
 
-let rec init_object runs0 s c l = function
+let rec init_object runs0 s c l _foo_ = match _foo_ with
 | [] -> result_out (Coq_out_ter (s, (res_val (Coq_value_object l))))
 | p :: pds' ->
   let (pn, pb) = p in
@@ -4370,7 +4370,7 @@ let init_array runs0 s c l oes =
 (** val run_var_decl_item :
     runs_type -> state -> execution_ctx -> prop_name -> expr option -> result **)
 
-let run_var_decl_item runs0 s c x = function
+let run_var_decl_item runs0 s c x _foo_ = match _foo_ with
 | Some e ->
   if_spec (identifier_resolution runs0 s c x) (fun s1 ir ->
     if_spec (run_expr_get_value runs0 s1 c e) (fun s2 v ->
@@ -4385,7 +4385,7 @@ let run_var_decl_item runs0 s c x = function
     runs_type -> state -> execution_ctx -> (prop_name * expr option) list ->
     result **)
 
-let rec run_var_decl runs0 s c = function
+let rec run_var_decl runs0 s c _foo_ = match _foo_ with
 | [] -> result_out (Coq_out_ter (s, res_empty))
 | y :: xeos' ->
   let (x, eo) = y in
@@ -4396,7 +4396,7 @@ let rec run_var_decl runs0 s c = function
     runs_type -> state -> execution_ctx -> value list -> expr list -> value
     list specres **)
 
-let rec run_list_expr runs0 s1 c vs = function
+let rec run_list_expr runs0 s1 c vs _foo_ = match _foo_ with
 | [] -> res_spec s1 (rev vs)
 | e :: es' ->
   if_spec (run_expr_get_value runs0 s1 c e) (fun s2 v ->
@@ -4405,7 +4405,7 @@ let rec run_list_expr runs0 s1 c vs = function
 (** val run_block :
     runs_type -> state -> execution_ctx -> stat list -> result **)
 
-let rec run_block runs0 s c = function
+let rec run_block runs0 s c _foo_ = match _foo_ with
 | [] -> res_ter s (res_normal Coq_resvalue_empty)
 | t :: ts_rev' ->
   if_success (run_block runs0 s c ts_rev') (fun s0 rv0 ->
@@ -4745,7 +4745,7 @@ let run_stat_while runs0 s c rv labs e1 t2 =
     runs_type -> state -> execution_ctx -> resvalue -> switchclause list ->
     result **)
 
-let rec run_stat_switch_end runs0 s c rv = function
+let rec run_stat_switch_end runs0 s c rv _foo_ = match _foo_ with
 | [] -> result_out (Coq_out_ter (s, (res_normal rv)))
 | y :: scs' ->
   let Coq_switchclause_intro (e, ts) = y in
@@ -4756,7 +4756,7 @@ let rec run_stat_switch_end runs0 s c rv = function
     runs_type -> state -> execution_ctx -> value -> resvalue -> switchclause
     list -> result **)
 
-let rec run_stat_switch_no_default runs0 s c vi rv = function
+let rec run_stat_switch_no_default runs0 s c vi rv _foo_ = match _foo_ with
 | [] -> result_out (Coq_out_ter (s, (res_normal rv)))
 | y :: scs' ->
   let Coq_switchclause_intro (e, ts) = y in
@@ -4908,7 +4908,7 @@ let run_stat_throw runs0 s c e =
 (** val run_stat_return :
     runs_type -> state -> execution_ctx -> expr option -> result **)
 
-let run_stat_return runs0 s c = function
+let run_stat_return runs0 s c _foo_ = match _foo_ with
 | Some e ->
   if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
     res_ter s1 (res_return (Coq_resvalue_value v1)))
@@ -4974,7 +4974,7 @@ let run_stat_for_var runs0 s c labs ds eo2 eo3 t =
 
 (** val run_expr : runs_type -> state -> execution_ctx -> expr -> result **)
 
-let run_expr runs0 s c = function
+let run_expr runs0 s c _foo_ = match _foo_ with
 | Coq_expr_this ->
   result_out (Coq_out_ter (s, (res_val c.execution_ctx_this_binding)))
 | Coq_expr_identifier x ->
@@ -5004,7 +5004,7 @@ let run_expr runs0 s c = function
 
 (** val run_stat : runs_type -> state -> execution_ctx -> stat -> result **)
 
-let run_stat runs0 s c = function
+let run_stat runs0 s c _foo_ = match _foo_ with
 | Coq_stat_expr e ->
   if_spec (run_expr_get_value runs0 s c e) (fun s0 r ->
     res_ter s0 (res_val r))
@@ -5043,7 +5043,7 @@ let run_stat runs0 s c = function
 (** val run_elements :
     runs_type -> state -> execution_ctx -> elements -> result **)
 
-let rec run_elements runs0 s c = function
+let rec run_elements runs0 s c _foo_ = match _foo_ with
 | [] -> result_out (Coq_out_ter (s, (res_normal Coq_resvalue_empty)))
 | el :: els_rev' ->
   if_success (run_elements runs0 s c els_rev') (fun s0 rv0 ->
@@ -5056,7 +5056,7 @@ let rec run_elements runs0 s c = function
 
 (** val run_prog : runs_type -> state -> execution_ctx -> prog -> result **)
 
-let run_prog runs0 s c = function
+let run_prog runs0 s c _foo_ = match _foo_ with
 | Coq_prog_intro (str, els) -> run_elements runs0 s c (rev els)
 
 (** val push :
@@ -5082,7 +5082,7 @@ let rec push runs0 s c l args ilen =
     runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
     result **)
 
-let rec run_object_is_sealed runs0 s c l = function
+let rec run_object_is_sealed runs0 s c l _foo_ = match _foo_ with
 | [] ->
   if_some (run_object_method object_extensible_ s l) (fun ext ->
     res_ter s (res_val (Coq_value_prim (Coq_prim_bool (neg ext)))))
@@ -5105,7 +5105,7 @@ let rec run_object_is_sealed runs0 s c l = function
     runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
     result **)
 
-let rec run_object_seal runs0 s c l = function
+let rec run_object_seal runs0 s c l _foo_ = match _foo_ with
 | [] ->
   if_some (run_object_heap_set_extensible false s l) (fun s0 ->
     res_ter s0 (res_val (Coq_value_object l)))
@@ -5138,7 +5138,7 @@ let rec run_object_seal runs0 s c l = function
     runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
     result **)
 
-let rec run_object_freeze runs0 s c l = function
+let rec run_object_freeze runs0 s c l _foo_ = match _foo_ with
 | [] ->
   if_some (run_object_heap_set_extensible false s l) (fun s0 ->
     res_ter s0 (res_val (Coq_value_object l)))
@@ -5181,7 +5181,7 @@ let rec run_object_freeze runs0 s c l = function
     runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
     result **)
 
-let rec run_object_is_frozen runs0 s c l = function
+let rec run_object_is_frozen runs0 s c l _foo_ = match _foo_ with
 | [] ->
   if_some (run_object_method object_extensible_ s l) (fun ext ->
     res_ter s (res_val (Coq_value_prim (Coq_prim_bool (neg ext)))))
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index e782bb9..9e7c9fc 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -44,7 +44,7 @@ let res_void s =
 
 (** val out_from_retn : retn -> out **)
 
-let out_from_retn = function
+let out_from_retn _foo_ = match _foo_ with
 | Coq_specret_val (s, _) -> assert false (* absurd case *)
 | Coq_specret_out o -> o
 
diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml
index a2322be..e552789 100644
--- a/generator/tests/jsref/JsNumber.ml
+++ b/generator/tests/jsref/JsNumber.ml
@@ -51,7 +51,7 @@ let ln2 = (log 2.)
 
 let from_string = (fun s ->
     (*try*)
-      let s = (String.concat "" (List.map (String.make 1) s)) in
+     (* let s = (String.concat "" (List.map (String.make 1) s)) in ARTHUR hack*)
       if s = "" then 0. else float_of_string s
     (* FIXME: with Failure "float_of_string" -> nan *) )
    (* Note that we're using `float_of_string' there, which does not have the same
@@ -70,11 +70,17 @@ let to_string = (fun f ->
        if (sfn = "nan") then "NaN" else
        let inum = int_of_float n in
        if (float_of_int inum = n) then (string_of_int inum) else (string_of_float n)) in
+    string_of_number f
+
+    (* ARTHUR hack
     let ret = ref [] in (* Ugly, but the API for OCaml string is not very functional... *)
     String.iter (fun c -> ret := c :: !ret) (string_of_number f);
-    List.rev !ret)
+    List.rev !ret
+    *)
+    )
    (* Note that this is ugly, we should use the spec of JsNumber.to_string here (9.8.1). *)
 
+
 (** val neg : number -> number **)
 
 let neg = (~-.)
diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml
index 116ce1b..7a284e8 100644
--- a/generator/tests/jsref/JsPreliminary.ml
+++ b/generator/tests/jsref/JsPreliminary.ml
@@ -18,11 +18,12 @@ let convert_number_to_bool n =
 (** val convert_string_to_bool : string -> bool **)
 
 let convert_string_to_bool s =
-  if string_comparable s [] then false else true
+  if string_comparable s "" then false else true
+  (* Arthur hack string.empty *)
 
 (** val convert_prim_to_boolean : prim -> bool **)
 
-let convert_prim_to_boolean = function
+let convert_prim_to_boolean _foo_ = match _foo_ with
 | Coq_prim_undef -> false
 | Coq_prim_null -> false
 | Coq_prim_bool b -> b
@@ -31,13 +32,13 @@ let convert_prim_to_boolean = function
 
 (** val convert_value_to_boolean : value -> bool **)
 
-let convert_value_to_boolean = function
+let convert_value_to_boolean _foo_ = match _foo_ with
 | Coq_value_prim p -> convert_prim_to_boolean p
 | Coq_value_object o -> true
 
 (** val convert_prim_to_number : prim -> number **)
 
-let convert_prim_to_number = function
+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
@@ -58,13 +59,13 @@ let convert_number_to_integer n =
 
 (** val convert_bool_to_string : bool -> string **)
 
-let convert_bool_to_string = function
+let convert_bool_to_string _foo_ = match _foo_ with
 | true -> "true"
 | false -> "false"
 
 (** val convert_prim_to_string : prim -> string **)
 
-let convert_prim_to_string = function
+let convert_prim_to_string _foo_ = match _foo_ with
 | Coq_prim_undef ->
   "undefined"
 | Coq_prim_null -> "null"
@@ -147,6 +148,7 @@ let inequality_test_number n1 n2 =
 
 (** val inequality_test_string : string -> string -> bool **)
 
+(* ARTHUR hack 
 let rec inequality_test_string s1 s2 =
   match s1 with
   | [] ->
@@ -160,6 +162,9 @@ let rec inequality_test_string s1 s2 =
        if ascii_comparable c1 c2
        then inequality_test_string s1' s2'
        else lt_int_decidable (int_of_char c1) (int_of_char c2))
+*)
+let inequality_test_string s1 s2 = (s1 <> s2)
+
 
 (** val inequality_test_primitive : prim -> prim -> prim **)
 
@@ -195,7 +200,7 @@ let inequality_test_primitive w1 w2 =
 
 (** val typeof_prim : prim -> string **)
 
-let typeof_prim = function
+let typeof_prim _foo_ = match _foo_ with
 | Coq_prim_undef ->
   "undefined"
 | Coq_prim_null -> "object"
@@ -205,14 +210,14 @@ let typeof_prim = function
 
 (** val string_of_propname : propname -> prop_name **)
 
-let string_of_propname = function
+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
 
 (** val string_of_native_error : native_error -> string **)
 
-let string_of_native_error = function
+let string_of_native_error _foo_ = match _foo_ with
 | Coq_native_error_eval ->
   "EvalError"
 | Coq_native_error_range ->
-- 
GitLab