diff --git a/generator/Makefile b/generator/Makefile index 316e8d85eba10035ccfa126edb96ad09f8a183ba..fe9ee04e95b7b5bb1dceb803acdd5c1c9dc2dd20 100644 --- a/generator/Makefile +++ b/generator/Makefile @@ -47,7 +47,7 @@ tests/jsref/%.ml: ../../convert-ml-strings.pl tests/jsref/*.ml cd $(@D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml -tests/%.ml.d: tests/%.ml +tests/%.ml.d: tests/%.ml tests/%.mli $(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@ tests/%.cmi tests/%.unlog.js: tests/%.ml main.byte stdlib diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli index 2f9f1c9bdf5507343458d772f6b0762cdefcd8d6..c427c4542d4d35558553dc0b2aed17126b419c9f 100644 --- a/generator/stdlib_ml/stdlib.mli +++ b/generator/stdlib_ml/stdlib.mli @@ -95,6 +95,9 @@ module List : sig end module String : sig + val length : string -> int + val append : string -> string -> string + val sub : string -> int -> int -> string val concat : string -> string list -> string val iter : (char -> unit) -> string -> unit val make : int -> char -> string @@ -106,3 +109,17 @@ val raise : exn -> 'a (* JSRef specific functions *) 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 + type bin_op + type exp +end + diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml index 6bc57c3be58ceb97f77345f8cb15872c64533e8c..dbdcf5a6610b771329eba4bbfac2c3a04368e33b 100644 --- a/generator/tests/jsref/JsCommon.ml +++ b/generator/tests/jsref/JsCommon.ml @@ -429,7 +429,7 @@ let element_funcdecl = function let prog_funcdecl p = concat (LibList.map element_funcdecl (prog_elements p)) -(** val stat_vardecl : stat -> char list list **) +(** val stat_vardecl : stat -> string list **) let rec stat_vardecl = function | Coq_stat_expr e -> [] @@ -460,7 +460,7 @@ let rec stat_vardecl = function | Coq_stat_debugger -> [] | Coq_stat_switch (l, e, sb) -> switchbody_vardecl sb -(** val switchbody_vardecl : switchbody -> char list list **) +(** val switchbody_vardecl : switchbody -> string list **) and switchbody_vardecl = function | Coq_switchbody_nodefault scl -> concat (map switchclause_vardecl scl) @@ -469,18 +469,18 @@ and switchbody_vardecl = function (append (concat (map stat_vardecl sl)) (concat (map switchclause_vardecl scl2))) -(** val switchclause_vardecl : switchclause -> char list list **) +(** val switchclause_vardecl : switchclause -> string list **) and switchclause_vardecl = function | Coq_switchclause_intro (e, sl) -> concat (map stat_vardecl sl) -(** val element_vardecl : element -> char list list **) +(** val element_vardecl : element -> string list **) let element_vardecl = function | Coq_element_stat t -> stat_vardecl t | Coq_element_func_decl (name, args, bd) -> [] -(** val prog_vardecl : prog -> char list list **) +(** val prog_vardecl : prog -> string list **) let prog_vardecl p = concat (LibList.map element_vardecl (prog_elements p)) @@ -489,7 +489,7 @@ type preftype = | Coq_preftype_number [@f] (** Auto Generated Attributes **) | Coq_preftype_string [@f] (** Auto Generated Attributes **) -(** val method_of_preftype : preftype -> char list **) +(** val method_of_preftype : preftype -> string **) let method_of_preftype = function | Coq_preftype_number -> "valueOf" @@ -579,7 +579,7 @@ let elision_tail_count ol = let elision_tail_remove ol = rev (elision_head_remove (rev ol)) -(** val parse_pickable : char list -> bool -> prog coq_Pickable_option **) +(** val parse_pickable : string -> bool -> prog coq_Pickable_option **) let parse_pickable = (fun s strict -> let str = String.concat "" (List.map (String.make 1) s) in diff --git a/generator/tests/jsref/JsInit.ml b/generator/tests/jsref/JsInit.ml index ab615d419f33dff2e14f5d98c0aa1f37c6fcb25e..2e8e88a7f5c410e06f43cc7c75e06e0c08e53882 100644 --- a/generator/tests/jsref/JsInit.ml +++ b/generator/tests/jsref/JsInit.ml @@ -71,7 +71,7 @@ let write_constant p name value0 = let object_prealloc_global_proto = (Coq_value_prim Coq_prim_null) -(** val object_prealloc_global_class : char list **) +(** val object_prealloc_global_class : string **) let object_prealloc_global_class = ( let rec aux s = function diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml index 9098c6505067bb573c4c1bc9f70cdc568246d49f..1be8e42b8e221970ec7c3797f650707f0955dffe 100644 --- a/generator/tests/jsref/JsInterpreter.ml +++ b/generator/tests/jsref/JsInterpreter.ml @@ -148,8 +148,8 @@ let run_object_heap_set_extensible b s l = result); runs_type_array_join_elements : (state -> execution_ctx -> object_loc -> float -> - float -> char list -> - char list -> result); + float -> string -> + string -> result); runs_type_array_element_list : (state -> execution_ctx -> object_loc -> expr option list -> float -> result); @@ -285,7 +285,7 @@ let runs_type_to_string x = x.runs_type_to_string (** val runs_type_array_join_elements : runs_type -> state -> execution_ctx -> object_loc -> float -> float -> - char list -> char list -> result **) + string -> string -> result **) let runs_type_array_join_elements x = x.runs_type_array_join_elements @@ -1665,7 +1665,7 @@ let rec array_args_map_loop runs0 s c l args 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.)) -(** val string_of_prealloc : prealloc -> char list **) +(** val string_of_prealloc : prealloc -> string **) let string_of_prealloc = function | Coq_prealloc_global -> "global" @@ -2565,7 +2565,7 @@ let creating_function_object_proto runs0 s c l = (descriptor_of_attributes (Coq_attributes_data_of a2)) false)))) (** val creating_function_object : - runs_type -> state -> execution_ctx -> char list list -> funcbody -> + runs_type -> state -> execution_ctx -> string list -> funcbody -> lexical_env -> strictness_flag -> result **) let creating_function_object runs0 s c names bd x str = @@ -2619,7 +2619,7 @@ let creating_function_object runs0 s c names bd x str = res_ter s5 (res_val (Coq_value_object l)))))))))))))) (** val binding_inst_formal_params : - runs_type -> state -> execution_ctx -> env_loc -> value list -> char list + runs_type -> state -> execution_ctx -> env_loc -> value list -> string list -> strictness_flag -> result_void **) let rec binding_inst_formal_params runs0 s c l args names str = @@ -2737,9 +2737,9 @@ let make_arg_setter runs0 s c x x0 = creating_function_object runs0 s c (xparam :: []) bd x0 true (** val arguments_object_map_loop : - runs_type -> state -> execution_ctx -> object_loc -> char list list -> + runs_type -> state -> execution_ctx -> object_loc -> string list -> int -> value list -> lexical_env -> strictness_flag -> object_loc -> - char list list -> result_void **) + string list -> result_void **) let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap = (fun fO fS n -> if n=0 then fO () else fS (n-1)) @@ -2794,7 +2794,7 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap = len (** val arguments_object_map : - runs_type -> state -> execution_ctx -> object_loc -> char list list -> + runs_type -> state -> execution_ctx -> object_loc -> string list -> value list -> lexical_env -> strictness_flag -> result_void **) let arguments_object_map runs0 s c l xs args x str = @@ -2804,7 +2804,7 @@ let arguments_object_map runs0 s c l xs args x str = str lmap []) (** val create_arguments_object : - runs_type -> state -> execution_ctx -> object_loc -> char list list -> + runs_type -> state -> execution_ctx -> object_loc -> string list -> value list -> lexical_env -> strictness_flag -> result **) let create_arguments_object runs0 s c lf xs args x str = @@ -2858,7 +2858,7 @@ let create_arguments_object runs0 s c lf xs args x str = res_ter s3 (res_val (Coq_value_object l))))))))) (** val binding_inst_arg_obj : - runs_type -> state -> execution_ctx -> object_loc -> prog -> char list + runs_type -> state -> execution_ctx -> object_loc -> prog -> string list -> value list -> env_loc -> result_void **) let binding_inst_arg_obj runs0 s c lf p xs args l = @@ -2878,7 +2878,7 @@ let binding_inst_arg_obj runs0 s c lf p xs args l = (Coq_value_object largs) false)) (** val binding_inst_var_decls : - runs_type -> state -> execution_ctx -> env_loc -> char list list -> bool + runs_type -> state -> execution_ctx -> env_loc -> string list -> bool -> strictness_flag -> result_void **) let rec binding_inst_var_decls runs0 s c l vds bconfig str = @@ -3456,7 +3456,7 @@ let convert_twice_number runs0 s c v1 v2 = (** val convert_twice_string : runs_type -> state -> execution_ctx -> value -> value -> - (char list * char list) specres **) + (string * string) specres **) let convert_twice_string runs0 s c v1 v2 = convert_twice if_string (fun s0 v -> to_string runs0 s0 c v) s v1 v2 @@ -3628,7 +3628,7 @@ let run_prepost_op = function | Coq_unary_op_bitwise_not -> None | Coq_unary_op_not -> None -(** val run_typeof_value : state -> value -> char list **) +(** val run_typeof_value : state -> value -> string **) let run_typeof_value s = function | Coq_value_prim w -> typeof_prim w @@ -4262,7 +4262,7 @@ let run_unary_op runs0 s c op e = (neg (convert_value_to_boolean v))))))) (** val create_new_function_in : - runs_type -> state -> execution_ctx -> char list list -> funcbody -> + runs_type -> state -> execution_ctx -> string list -> funcbody -> result **) let create_new_function_in runs0 s c args bd = @@ -4479,7 +4479,7 @@ let run_expr_assign runs0 s c opo e1 e2 = follow x (Coq_resvalue_value x0)))) (** val run_expr_function : - runs_type -> state -> execution_ctx -> prop_name option -> char list list + runs_type -> state -> execution_ctx -> prop_name option -> string list -> funcbody -> result **) let run_expr_function runs0 s c fo args bd = @@ -4965,7 +4965,7 @@ let run_stat_for runs0 s c labs eo1 eo2 eo3 t = | None -> follows s) (** val run_stat_for_var : - runs_type -> state -> execution_ctx -> label_set -> (char list * expr + runs_type -> state -> execution_ctx -> label_set -> (string * expr option) list -> expr option -> expr option -> stat -> result **) let run_stat_for_var runs0 s c labs ds eo2 eo3 t = @@ -5225,7 +5225,7 @@ let run_get_args_for_apply runs0 s c l index n = else res_spec s [] (** val valueToStringForJoin : - runs_type -> state -> execution_ctx -> object_loc -> float -> char list + runs_type -> state -> execution_ctx -> object_loc -> float -> string specres **) let valueToStringForJoin runs0 s c l k = @@ -5249,7 +5249,7 @@ let valueToStringForJoin runs0 s c l k = (** val run_array_join_elements : runs_type -> state -> execution_ctx -> object_loc -> float -> float -> - char list -> char list -> result **) + string -> string -> result **) let run_array_join_elements runs0 s c l k length0 sep sR = if lt_int_decidable k length0 diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml index 7dff7901f6c2f2692d034ce7d3ef98abac4a7f02..e782bb98e14ec7d7005c24bfa6622720b96fa6eb 100644 --- a/generator/tests/jsref/JsInterpreterMonads.ml +++ b/generator/tests/jsref/JsInterpreterMonads.ml @@ -325,7 +325,7 @@ let if_object w k = | Coq_value_object l -> k s l) (** val if_string : - result -> (state -> char list -> 'a1 specres) -> 'a1 specres **) + result -> (state -> string -> 'a1 specres) -> 'a1 specres **) let if_string w k = if_value w (fun s v -> diff --git a/generator/tests/jsref/JsNumber.ml b/generator/tests/jsref/JsNumber.ml index 213e70576166aa79de651de978c6986eb21fa196..a2322bebc19a93060a58823142cba5a2a7c0173c 100644 --- a/generator/tests/jsref/JsNumber.ml +++ b/generator/tests/jsref/JsNumber.ml @@ -47,7 +47,7 @@ let e = (exp 1.) let ln2 = (log 2.) -(** val from_string : char list -> number **) +(** val from_string : string -> number **) let from_string = (fun s -> (*try*) @@ -58,7 +58,7 @@ let from_string = (fun s -> behavior than JavaScript. For instance it will read "022" as 22 instead of 18, which should be the JavaScript result for it. *) -(** val to_string : number -> char list **) +(** val to_string : number -> string **) let to_string = (fun f -> prerr_string ("Warning: JsNumber.to_string called. This might be responsible for errors. Argument value: " ^ string_of_float f ^ "."); diff --git a/generator/tests/jsref/JsPreliminary.ml b/generator/tests/jsref/JsPreliminary.ml index ea315b8129e684fc2252969fdfc3e63eac46d8c4..116ce1b6b4adfd95180ceeb349811882cea3230a 100644 --- a/generator/tests/jsref/JsPreliminary.ml +++ b/generator/tests/jsref/JsPreliminary.ml @@ -15,7 +15,7 @@ let convert_number_to_bool n = then false else true -(** val convert_string_to_bool : char list -> bool **) +(** val convert_string_to_bool : string -> bool **) let convert_string_to_bool s = if string_comparable s [] then false else true @@ -56,13 +56,13 @@ let convert_number_to_integer n = then n else mult (sign n) (floor (absolute n)) -(** val convert_bool_to_string : bool -> char list **) +(** val convert_bool_to_string : bool -> string **) let convert_bool_to_string = function | true -> "true" | false -> "false" -(** val convert_prim_to_string : prim -> char list **) +(** val convert_prim_to_string : prim -> string **) let convert_prim_to_string = function | Coq_prim_undef -> @@ -145,7 +145,7 @@ let inequality_test_number n1 n2 = then Coq_prim_bool true else Coq_prim_bool (lt_bool n1 n2) -(** val inequality_test_string : char list -> char list -> bool **) +(** val inequality_test_string : string -> string -> bool **) let rec inequality_test_string s1 s2 = match s1 with @@ -193,7 +193,7 @@ let inequality_test_primitive w1 w2 = (convert_prim_to_number w2) | Coq_prim_string s2 -> Coq_prim_bool (inequality_test_string s1 s2)) -(** val typeof_prim : prim -> char list **) +(** val typeof_prim : prim -> string **) let typeof_prim = function | Coq_prim_undef -> @@ -210,7 +210,7 @@ let string_of_propname = function | Coq_propname_string s -> s | Coq_propname_number n -> to_string n -(** val string_of_native_error : native_error -> char list **) +(** val string_of_native_error : native_error -> string **) let string_of_native_error = function | Coq_native_error_eval -> diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml index 7be0ddc03addec1ef7f40a032a3fe833b1d76dd2..a1fe1421e02b378c246bf7e194962fd7478f54dd 100644 --- a/generator/tests/jsref/JsSyntax.ml +++ b/generator/tests/jsref/JsSyntax.ml @@ -49,11 +49,11 @@ type literal = | Coq_literal_null [@f] (** Auto Generated Attributes **) | Coq_literal_bool [@f label0] of bool (** Auto Generated Attributes **) | Coq_literal_number [@f label0] of number (** Auto Generated Attributes **) -| Coq_literal_string [@f label0] of char list (** Auto Generated Attributes **) +| Coq_literal_string [@f label0] of string (** Auto Generated Attributes **) type label = | Coq_label_empty [@f] (** Auto Generated Attributes **) -| Coq_label_string [@f label0] of char list (** Auto Generated Attributes **) +| Coq_label_string [@f label0] of string (** Auto Generated Attributes **) type label_set = label list @@ -65,19 +65,19 @@ let strictness_false = false type propname = -| Coq_propname_identifier [@f label0] of char list (** Auto Generated Attributes **) -| Coq_propname_string [@f label0] of char list (** Auto Generated Attributes **) +| Coq_propname_identifier [@f label0] of string (** Auto Generated Attributes **) +| Coq_propname_string [@f label0] of string (** Auto Generated Attributes **) | Coq_propname_number [@f label0] of number (** Auto Generated Attributes **) type expr = | Coq_expr_this [@f] (** Auto Generated Attributes **) -| Coq_expr_identifier [@f label0] of char list (** Auto Generated Attributes **) +| Coq_expr_identifier [@f label0] of string (** Auto Generated Attributes **) | Coq_expr_literal [@f label0] of literal (** Auto Generated Attributes **) | Coq_expr_object [@f label0] of (propname * propbody) list (** Auto Generated Attributes **) | Coq_expr_array [@f label0] of expr option list (** Auto Generated Attributes **) -| Coq_expr_function [@f label0, label1, label2] of char list option * char list list * funcbody (** Auto Generated Attributes **) +| Coq_expr_function [@f label0, label1, label2] of string option * string list * funcbody (** Auto Generated Attributes **) | Coq_expr_access [@f label0, label1] of expr * expr (** Auto Generated Attributes **) -| Coq_expr_member [@f label0, label1] of expr * char list (** Auto Generated Attributes **) +| Coq_expr_member [@f label0, label1] of expr * string (** Auto Generated Attributes **) | Coq_expr_new [@f label0, label1] of expr * expr list (** Auto Generated Attributes **) | Coq_expr_call [@f label0, label1] of expr * expr list (** Auto Generated Attributes **) | Coq_expr_unary_op [@f label0, label1] of unary_op * expr (** Auto Generated Attributes **) @@ -87,14 +87,14 @@ type expr = and propbody = | Coq_propbody_val [@f label0] of expr (** Auto Generated Attributes **) | Coq_propbody_get [@f label0] of funcbody (** Auto Generated Attributes **) -| Coq_propbody_set [@f label0, label1] of char list list * funcbody (** Auto Generated Attributes **) +| Coq_propbody_set [@f label0, label1] of string list * funcbody (** Auto Generated Attributes **) and funcbody = -| Coq_funcbody_intro [@f label0, label1] of prog * char list (** Auto Generated Attributes **) +| Coq_funcbody_intro [@f label0, label1] of prog * string (** Auto Generated Attributes **) and stat = | Coq_stat_expr [@f label0] of expr (** Auto Generated Attributes **) -| Coq_stat_label [@f label0, label1] of char list * stat (** Auto Generated Attributes **) +| Coq_stat_label [@f label0, label1] of string * stat (** Auto Generated Attributes **) | Coq_stat_block [@f label0] of stat list (** Auto Generated Attributes **) -| Coq_stat_var_decl [@f label0] of (char list * expr option) list (** Auto Generated Attributes **) +| Coq_stat_var_decl [@f label0] of (string * expr option) list (** Auto Generated Attributes **) | Coq_stat_if [@f label0, label1, label2] of expr * stat * stat option (** Auto Generated Attributes **) | Coq_stat_do_while [@f label0, label1, label2] of label_set * stat * expr (** Auto Generated Attributes **) | Coq_stat_while [@f label0, label1, label2] of label_set * expr * stat (** Auto Generated Attributes **) @@ -103,11 +103,11 @@ and stat = | Coq_stat_return [@f label0] of expr option (** Auto Generated Attributes **) | Coq_stat_break [@f label0] of label (** Auto Generated Attributes **) | Coq_stat_continue [@f label0] of label (** Auto Generated Attributes **) -| Coq_stat_try [@f label0, label1, label2] of stat * (char list * stat) option * stat option (** Auto Generated Attributes **) +| Coq_stat_try [@f label0, label1, label2] of stat * (string * stat) option * stat option (** Auto Generated Attributes **) | Coq_stat_for [@f label0, label1, label2, label3, label4] of label_set * expr option * expr option * expr option * stat (** Auto Generated Attributes **) -| Coq_stat_for_var [@f label0, label1, label2, label3, label4] of label_set * (char list * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **) +| Coq_stat_for_var [@f label0, label1, label2, label3, label4] of label_set * (string * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **) | Coq_stat_for_in [@f label0, label1, label2, label3] of label_set * expr * expr * stat (** Auto Generated Attributes **) -| Coq_stat_for_in_var [@f label0, label1, label2, label3, label4] of label_set * char list * expr option * expr * stat (** Auto Generated Attributes **) +| Coq_stat_for_in_var [@f label0, label1, label2, label3, label4] of label_set * string * expr option * expr * stat (** Auto Generated Attributes **) | Coq_stat_debugger [@f] (** Auto Generated Attributes **) | Coq_stat_switch [@f label0, label1, label2] of label_set * expr * switchbody (** Auto Generated Attributes **) and switchbody = @@ -119,21 +119,21 @@ and prog = | Coq_prog_intro [@f label0, label1] of strictness_flag * element list (** Auto Generated Attributes **) and element = | Coq_element_stat [@f label0] of stat (** Auto Generated Attributes **) -| Coq_element_func_decl [@f label0, label1, label2] of char list * char list list * funcbody (** Auto Generated Attributes **) +| Coq_element_func_decl [@f label0, label1, label2] of string * string list * funcbody (** Auto Generated Attributes **) type propdefs = (propname * propbody) list type elements = element list -type funcdecl = { funcdecl_name : char list; - funcdecl_parameters : char list list; +type funcdecl = { funcdecl_name : string; + funcdecl_parameters : string list; funcdecl_body : funcbody } -(** val funcdecl_name : funcdecl -> char list **) +(** val funcdecl_name : funcdecl -> string **) let funcdecl_name x = x.funcdecl_name -(** val funcdecl_parameters : funcdecl -> char list list **) +(** val funcdecl_parameters : funcdecl -> string list **) let funcdecl_parameters x = x.funcdecl_parameters @@ -283,7 +283,7 @@ type prim = | Coq_prim_null [@f] (** Auto Generated Attributes **) | Coq_prim_bool [@f label0] of bool (** Auto Generated Attributes **) | Coq_prim_number [@f label0] of number (** Auto Generated Attributes **) -| Coq_prim_string [@f label0] of char list (** Auto Generated Attributes **) +| Coq_prim_string [@f label0] of string (** Auto Generated Attributes **) type value = | Coq_value_prim [@f label0] of prim (** Auto Generated Attributes **) @@ -384,7 +384,7 @@ type mutability = | Coq_mutability_nondeletable [@f] (** Auto Generated Attributes **) | Coq_mutability_deletable [@f] (** Auto Generated Attributes **) -type decl_env_record = (char list, mutability * value) Heap.heap +type decl_env_record = (string, mutability * value) Heap.heap type provide_this_flag = bool @@ -421,7 +421,7 @@ let execution_ctx_this_binding x = x.execution_ctx_this_binding let execution_ctx_strict x = x.execution_ctx_strict -type prop_name = char list +type prop_name = string type ref_base_type = | Coq_ref_base_type_value [@f label0] of value (** Auto Generated Attributes **) @@ -442,7 +442,7 @@ let ref_name x = x.ref_name let ref_strict x = x.ref_strict -type class_name = char list +type class_name = string type object_properties_type = (prop_name, attributes) Heap.heap @@ -463,7 +463,7 @@ type coq_object = { object_proto_ : value; object_class_ : class_name; object_call_ : call option; object_has_instance_ : builtin_has_instance option; object_scope_ : lexical_env option; - object_formal_parameters_ : char list list option; + object_formal_parameters_ : string list option; object_code_ : funcbody option; object_target_function_ : object_loc option; object_bound_this_ : value option; @@ -542,7 +542,7 @@ let object_has_instance_ x = x.object_has_instance_ let object_scope_ x = x.object_scope_ -(** val object_formal_parameters_ : coq_object -> char list list option **) +(** val object_formal_parameters_ : coq_object -> string list option **) let object_formal_parameters_ x = x.object_formal_parameters_ diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml index a06330b03ed1a6ae320f9635f377fe0b4e508efa..9ebfaf52fc3f68e5287aae57f767e6052515b2bc 100644 --- a/generator/tests/jsref/JsSyntaxAux.ml +++ b/generator/tests/jsref/JsSyntaxAux.ml @@ -260,7 +260,7 @@ let object_with_scope o scope = object_bound_args_ = x23; object_parameter_map_ = x24 } (** val object_with_formal_params : - coq_object -> char list list option -> coq_object **) + coq_object -> string list option -> coq_object **) let object_with_formal_params o params = let { object_proto_ = x1; object_class_ = x2; object_extensible_ = x3; @@ -284,7 +284,7 @@ let object_with_formal_params o params = object_bound_args_ = x23; object_parameter_map_ = x24 } (** val object_with_details : - coq_object -> lexical_env option -> char list list option -> funcbody + coq_object -> lexical_env option -> string list option -> funcbody option -> object_loc option -> value option -> value list option -> object_loc option -> coq_object **) diff --git a/generator/tests/jsref/LibString.ml b/generator/tests/jsref/LibString.ml index ee203769138cda4372d7b7521972cb76b80395bc..7e8433eca07a48ae658d272fc6b8fd07683138d6 100644 --- a/generator/tests/jsref/LibString.ml +++ b/generator/tests/jsref/LibString.ml @@ -1,7 +1,7 @@ open LibReflect open String0 -(** val string_comparable : char list coq_Comparable **) +(** val string_comparable : string coq_Comparable **) let string_comparable x y = comparable_of_dec string_dec x y diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml index 932621cb09bf38953cb152298c45a0dd196f3d90..002d695cc51aca5f1eaa7e0003c361f283d489ac 100644 --- a/generator/tests/jsref/Shared.ml +++ b/generator/tests/jsref/Shared.ml @@ -18,7 +18,7 @@ let int_of_char = (fun c -> float_of_int (int_of_char c)) let ascii_comparable = (=) -(** val string_sub : char list -> float -> float -> char list **) +(** val string_sub : string -> float -> float -> string **) let string_sub s n l = substring (Z.abs_nat n) (Z.abs_nat l) s diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml index e802a8f30c82b421aa13425a4f95913f27679d7c..fdd7e9f90d2f605624e9c689fca91068edcd87c4 100644 --- a/generator/tests/jsref/String0.ml +++ b/generator/tests/jsref/String0.ml @@ -1,4 +1,17 @@ -(** val string_dec : char list -> char list -> bool **) + +(* ARTHUR: hacked this file *) + +let string_dec s1 s2 = (s1 = s2) + +let append s1 s2 = String.append s1 s2 + +let length s = String.length s + +let substring n m s = String.sub s n m + +(* + +(** val string_dec : string -> string -> bool **) let rec string_dec s1 s2 = match s1 with | [] -> (match s2 with @@ -8,20 +21,20 @@ let rec string_dec s1 s2 = match s1 with | [] -> false | a0::s4 -> if (=) a a0 then string_dec s0 s4 else false) -(** val append : char list -> char list -> char list **) +(** val append : string -> string -> string **) let rec append s1 s2 = match s1 with | [] -> s2 | c::s1' -> c::(append s1' s2) -(** val length : char list -> int **) +(** val length : string -> int **) let rec length l = match l with | [] -> 0 | c::s' -> Pervasives.succ (length s') -(** val substring : int -> int -> char list -> char list **) +(** val substring : int -> int -> string -> string **) let rec substring n m s = if n=0 then @@ -33,3 +46,6 @@ let rec substring n m s = else match s with | [] -> s | c::s' -> substring (n-1) m s' + + +*) \ No newline at end of file