diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml index 61f5a4c25ead09d4b59ad6cb75b9fb17ce3d860d..7be0ddc03addec1ef7f40a032a3fe833b1d76dd2 100644 --- a/generator/tests/jsref/JsSyntax.ml +++ b/generator/tests/jsref/JsSyntax.ml @@ -73,7 +73,7 @@ type expr = | Coq_expr_this [@f] (** Auto Generated Attributes **) | Coq_expr_identifier [@f label0] of char list (** Auto Generated Attributes **) | Coq_expr_literal [@f label0] of literal (** Auto Generated Attributes **) -| Coq_expr_object [@f label0, label1] of (propname * propbody) list (** 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_access [@f label0, label1] of expr * expr (** Auto Generated Attributes **) @@ -94,7 +94,7 @@ 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_block [@f label0] of stat list (** Auto Generated Attributes **) -| Coq_stat_var_decl [@f label0, label1] of (char list * expr option) list (** Auto Generated Attributes **) +| Coq_stat_var_decl [@f label0] of (char list * 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,18 +103,16 @@ 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, label3] of stat * (char list * stat) option * stat option (** Auto Generated Attributes **) +| Coq_stat_try [@f label0, label1, label2] of stat * (char list * 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] of label_set * (char list * expr option) list (** Auto Generated Attributes **) - * expr option * expr option * stat +| 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_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_debugger [@f] (** Auto Generated Attributes **) | Coq_stat_switch [@f label0, label1, label2] of label_set * expr * switchbody (** Auto Generated Attributes **) and switchbody = | Coq_switchbody_nodefault [@f label0] of switchclause list (** Auto Generated Attributes **) -| Coq_switchbody_withdefault [@f label0, label1] of switchclause list * stat list (** Auto Generated Attributes **) - * switchclause list +| Coq_switchbody_withdefault [@f label0, label1, label2] of switchclause list * stat list * switchclause list (** Auto Generated Attributes **) and switchclause = | Coq_switchclause_intro [@f label0, label1] of expr * stat list (** Auto Generated Attributes **) and prog = @@ -570,7 +568,7 @@ let object_parameter_map_ x = x.object_parameter_map_ type event = | Coq_delete_event [@f label0, label1, label2] of object_loc * prop_name * object_loc option (** Auto Generated Attributes **) -| Coq_mutateproto_event [@f label0, label1, label2] of object_loc * (object_loc * prop_name) list (** Auto Generated Attributes **) +| Coq_mutateproto_event [@f label0, label1] of object_loc * (object_loc * prop_name) list (** Auto Generated Attributes **) * (object_loc * prop_name) list | Coq_enumchange_event [@f label0, label1] of object_loc * prop_name (** Auto Generated Attributes **) diff --git a/generator/tests/jsref/JsSyntaxAux.ml b/generator/tests/jsref/JsSyntaxAux.ml index b23b5c9ce70d0bd2b2b64410a62a0febf5e4f015..a06330b03ed1a6ae320f9635f377fe0b4e508efa 100644 --- a/generator/tests/jsref/JsSyntaxAux.ml +++ b/generator/tests/jsref/JsSyntaxAux.ml @@ -361,7 +361,10 @@ let object_for_args_object o paramsmap get getownproperty defineownproperty dele (** val mathop_compare : mathop -> mathop -> bool **) let mathop_compare m1 m2 = - let Coq_mathop_abs = m1 in let Coq_mathop_abs = m2 in true + match m1 with + | Coq_mathop_abs -> + match m2 with + | Coq_mathop_abs -> true (** val mathop_comparable : mathop coq_Comparable **) @@ -6634,24 +6637,25 @@ let binary_op_comparable x y = (** val prog_intro_strictness : prog -> strictness_flag **) -let prog_intro_strictness = function +let prog_intro_strictness p = match p with | Coq_prog_intro (str, els) -> str (** val prog_elements : prog -> element list **) -let prog_elements = function +let prog_elements p = match p with | Coq_prog_intro (str, els) -> els (** val funcbody_prog : funcbody -> prog **) -let funcbody_prog = function +let funcbody_prog fb = match fb with | Coq_funcbody_intro (p, s) -> p (** val funcbody_is_strict : funcbody -> strictness_flag **) -let funcbody_is_strict = function +let funcbody_is_strict fb = match fb with | Coq_funcbody_intro (p, s) -> - let Coq_prog_intro (b_strict, l) = p in b_strict + match p with + | Coq_prog_intro (b_strict, l) -> b_strict (** val restype_compare : restype -> restype -> bool **) diff --git a/generator/tests/jsref/JsSyntaxInfos.ml b/generator/tests/jsref/JsSyntaxInfos.ml index 3c63dd6ecfa108279b26769fe23bce3193d39648..7ef6cd1bbfc34ef306715a9b60da17e6fe093208 100644 --- a/generator/tests/jsref/JsSyntaxInfos.ml +++ b/generator/tests/jsref/JsSyntaxInfos.ml @@ -3,7 +3,9 @@ open JsSyntaxAux open LibBool open List0 +(* let __ = let rec f _ = Obj.repr f in Obj.repr f +*) (** val add_infos_exp : strictness_flag -> expr -> expr **) @@ -35,21 +37,18 @@ let rec add_infos_exp str e = (** val add_infos_funcbody : strictness_flag -> funcbody -> funcbody **) -and add_infos_funcbody str = function +and add_infos_funcbody str fb = match fb with | Coq_funcbody_intro (p, s) -> Coq_funcbody_intro ((add_infos_prog str p), s) (** val add_infos_stat : strictness_flag -> label_set -> stat -> stat **) and add_infos_stat str labs t = - let opt = fun _ f smth -> - match smth with + let opt f smth = match smth with | Some smth0 -> Some (f smth0) | None -> None in let f = add_infos_stat str label_set_empty in - let fo = opt __ f in let fe = add_infos_exp str in - let feo = opt __ fe in let fsb = add_infos_switchbody str in (match t with | Coq_stat_expr e -> Coq_stat_expr (fe e) @@ -59,31 +58,31 @@ and add_infos_stat str labs t = | Coq_stat_block ts -> Coq_stat_block (map f ts) | Coq_stat_var_decl vars -> Coq_stat_var_decl - (map (fun var -> let (s, eo) = var in (s, (feo eo))) vars) - | Coq_stat_if (e, t0, to0) -> Coq_stat_if ((fe e), (f t0), (fo to0)) + (map (fun var -> let (s, eo) = var in (s, (opt fe eo))) vars) + | Coq_stat_if (e, t0, to0) -> Coq_stat_if ((fe e), (f t0), (opt f to0)) | Coq_stat_do_while (l, t0, e) -> Coq_stat_do_while ((label_set_add_empty labs), (f t0), (fe e)) | Coq_stat_while (l, e, t0) -> Coq_stat_while ((label_set_add_empty labs), (fe e), (f t0)) | Coq_stat_with (e, t0) -> Coq_stat_with ((fe e), (f t0)) | Coq_stat_throw e -> Coq_stat_throw (fe e) - | Coq_stat_return eo -> Coq_stat_return (feo eo) + | Coq_stat_return eo -> Coq_stat_return (opt fe eo) | Coq_stat_break lopt -> Coq_stat_break lopt | Coq_stat_continue lopt -> Coq_stat_continue lopt | Coq_stat_try (t0, catch, to0) -> Coq_stat_try ((f t0), - (opt __ (fun c -> let (cs, t1) = c in (cs, (f t1))) catch), (fo to0)) + (opt (fun c -> let (cs, t1) = c in (cs, (f t1))) catch), (opt f to0)) | Coq_stat_for (l, eo1, eo2, eo3, t0) -> - Coq_stat_for ((label_set_add_empty labs), (feo eo1), (feo eo2), - (feo eo3), (f t0)) + Coq_stat_for ((label_set_add_empty labs), (opt fe eo1), (opt fe eo2), + (opt fe eo3), (f t0)) | Coq_stat_for_var (l, vars, eo2, eo3, t0) -> Coq_stat_for_var ((label_set_add_empty labs), - (map (fun var -> let (s, eo) = var in (s, (feo eo))) vars), (feo eo2), - (feo eo3), (f t0)) + (map (fun var -> let (s, eo) = var in (s, (opt fe eo))) vars), (opt fe eo2), + (opt fe eo3), (f t0)) | Coq_stat_for_in (l, e1, e2, t0) -> Coq_stat_for_in ((label_set_add_empty labs), (fe e1), (fe e2), (f t0)) | Coq_stat_for_in_var (l, str0, eo, e, t0) -> - Coq_stat_for_in_var ((label_set_add_empty labs), str0, (feo eo), + Coq_stat_for_in_var ((label_set_add_empty labs), str0, (opt fe eo), (fe e), (f t0)) | Coq_stat_debugger -> Coq_stat_debugger | Coq_stat_switch (labs0, e, ts) -> @@ -95,8 +94,8 @@ and add_infos_stat str labs t = and add_infos_switchbody str ts = let fe = add_infos_exp str in let fs = add_infos_stat str label_set_empty in - let f = fun sc -> - let Coq_switchclause_intro (e, l) = sc in + let f sc = match sc with + | Coq_switchclause_intro (e, l) -> Coq_switchclause_intro ((fe e), (map fs l)) in (match ts with @@ -106,14 +105,14 @@ and add_infos_switchbody str ts = (** val add_infos_prog : strictness_flag -> prog -> prog **) -and add_infos_prog str = function +and add_infos_prog str p = match p with | Coq_prog_intro (str', els) -> let str'' = coq_or str str' in Coq_prog_intro (str'', (map (add_infos_element str'') els)) (** val add_infos_element : strictness_flag -> element -> element **) -and add_infos_element str = function +and add_infos_element str el = match el with | Coq_element_stat t -> Coq_element_stat (add_infos_stat str label_set_empty t) | Coq_element_func_decl (s, ss, fb) ->