diff --git a/generator/TODO b/generator/TODO
index 5f6b1e6240377af7f23eadceecf588038c15dec8..44730b755c04885d1ddb7452d84be16bc50d66cc 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -39,17 +39,18 @@ NEW TODO
=========================================================
-BROWSER LIMIT WITH STACK SIZE:
+HERE IS HOW TO PRINT BROWSER STACK SIZE LIMIT:
-execute:
- var i=0;
- function inc() {
- i++;
- inc();
- }
- inc();
+ in the console, execute:
-then print value of "i".
+ var i=0;
+ function inc() {
+ i++;
+ inc();
+ }
+ inc();
+
+ then print value of "i".
=========================================================
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index a2639a1e1aeae8d19e58c2bae2dbeadaf539e4c2..a1c593c2048d7688cc74044c9e7af3277c3f9a3e 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -237,8 +237,11 @@ let ppf_field_access expr field =
Printf.sprintf "%s.%s" expr field
(* ' is not permitted in JS identifier names, and $ is not permitted in OCaml ones *)
-let ppf_ident_name =
- String.map (function '\'' -> '$' | c -> c)
+let ppf_ident_name x =
+ if List.mem x ["arguments"]
+ then unsupported ("use of reserved keyword: " ^ x);
+ (* TODO: complete the list *)
+ String.map (function '\'' -> '$' | c -> c) x
let ppf_ident i =
i |> Ident.name |> ppf_ident_name
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index a113b07da931c443a3404b7f0938afda5b7bf0d7..45135288997352f279f838fab0be79f143eb834d 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -2517,8 +2517,8 @@ let run_construct runs0 s c co l args =
| Some co0 ->
if_some (run_object_method object_bound_args_ s l) (fun oarg ->
if_some oarg (fun boundArgs ->
- let_binding (LibList.append boundArgs args) (fun arguments ->
- runs0.runs_type_construct s c co0 target arguments)))
+ let_binding (LibList.append boundArgs args) (fun arguments_ ->
+ runs0.runs_type_construct s c co0 target arguments_)))
| None -> run_error s Coq_native_error_type)))
| Coq_construct_prealloc b -> run_construct_prealloc runs0 s c b args
@@ -2857,7 +2857,7 @@ let create_arguments_object runs0 s c lf xs args x str =
list -> value list -> env_loc -> result_void **)
let binding_inst_arg_obj runs0 s c lf p xs args l =
- let arguments =
+ let arguments_ =
"arguments"
in
let_binding (prog_intro_strictness p) (fun str ->
@@ -2865,11 +2865,11 @@ let binding_inst_arg_obj runs0 s c lf p xs args l =
(create_arguments_object runs0 s c lf xs args
c.execution_ctx_variable_env str) (fun s1 largs ->
if str
- then if_void (env_record_create_immutable_binding s1 l arguments)
+ then if_void (env_record_create_immutable_binding s1 l arguments_)
(fun s2 ->
- env_record_initialize_immutable_binding s2 l arguments
+ env_record_initialize_immutable_binding s2 l arguments_
(Coq_value_object largs))
- else env_record_create_set_mutable_binding runs0 s1 c l arguments None
+ else env_record_create_set_mutable_binding runs0 s1 c l arguments_ None
(Coq_value_object largs) false))
(** val binding_inst_var_decls :
@@ -5317,8 +5317,8 @@ let run_call_prealloc runs0 s c b vthis args =
if_spec (to_uint32 runs0 s0 c v) (fun s1 ilen ->
if_spec
(run_get_args_for_apply runs0 s1 c array 0. ilen)
- (fun s2 arguments ->
- runs0.runs_type_call s2 c thisobj thisArg arguments)))))
+ (fun s2 arguments_ ->
+ runs0.runs_type_call s2 c thisobj thisArg arguments_)))))
else run_error s Coq_native_error_type))
| Coq_prealloc_function_proto_call ->
if is_callable_dec s vthis
@@ -5787,8 +5787,8 @@ let run_call runs0 s c l vthis args =
(fun otrg ->
if_some otrg (fun target ->
let_binding (LibList.append boundArgs args)
- (fun arguments ->
- runs0.runs_type_call s c target boundThis arguments)))))))
+ (fun arguments_ ->
+ runs0.runs_type_call s c target boundThis arguments_)))))))
| Coq_call_prealloc b -> run_call_prealloc runs0 s c b vthis args))
(** val run_javascript : runs_type -> prog -> result **)
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index 47b47bb83dbfc5477a5f4ace539c0f40f752b68a..3912e4fc4202d07b45d1617f5443bfb059b9441d 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -9,10 +9,10 @@ open Shared
type __ = unit
type 't resultof =
-| Coq_result_some [@f label0] of 't (** Auto Generated Attributes **)
+| Coq_result_some [@f value] of 't (** Auto Generated Attributes **)
| Coq_result_not_yet_implemented [@f] (** Auto Generated Attributes **)
| Coq_result_impossible [@f] (** Auto Generated Attributes **)
-| Coq_result_bottom [@f label0] of state (** Auto Generated Attributes **)
+| Coq_result_bottom [@f state] of state (** Auto Generated Attributes **)
type 't specres = 't specret resultof
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index 9749b2f7a824bbc1382ab9d08d812c5081e75367..d3c8199e85df2d61d00affe94ff0e10bdb99a199 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -592,7 +592,7 @@ type restype =
type resvalue =
| Coq_resvalue_empty [@f]
| Coq_resvalue_value [@f value] of value
-| Coq_resvalue_ref [@f value] of ref
+| Coq_resvalue_ref [@f ref] of ref
type res = { res_type : restype; res_value : resvalue; res_label : label }
diff --git a/navig-driver.js b/navig-driver.js
index 7fb1d8dbcc35ea54d587123b60b6489d5a085c4f..4de5c3ee07b092de547d3d4e1cab761d80f7d203 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -647,6 +647,21 @@ function ctxToHtml(ctx) {
for (var i = 0; i < a.length; i++) {
var b = a[i];
s += "<div style='white-space: nowrap;'><b>" + b.key + "</b>: " + JSON.stringify(b.val) + "</div>";
+ if (b.key == "#RETURN_VALUE#" &&
+ b.val.value !== undefined &&
+ b.val.value.out !== undefined &&
+ b.val.value.out.res !== undefined) {
+ var res = b.val.value.out.res;
+ // Coq_result_some [@f value] of 't
+ // Coq_specret_out [@f value] of out
+ // Coq_out_ter [@f state, res] of state * res
+ s += "<div style='white-space: nowrap;'><b>#RES#</b>: " + JSON.stringify(res) + "</div>";
+ if (res.res_value !== undefined &&
+ res.res_value.value !== undefined) {
+ var value = res.res_value.value;
+ s += "<div style='white-space: nowrap;'><b>#RESVALUE#: " + JSON.stringify(value) + "</b></div>";
+ }
+ }
}
return s;
}
@@ -690,13 +705,19 @@ function updateSelectionInCodeMirrorAccordingToExt(codeMirrorObj, locByExt) {
updateSelectionInCodeMirror(codeMirrorObj, loc);
}
+function clearFeedback() {
+ $("#disp_infos").html("");
+ $("#disp_env").html("");
+ $("#disp_ctx").html("");
+}
+
function updateSelection() {
- var item = tracer_items[tracer_pos];
- source.setSelection({line: 0, ch:0}, {line: 0, ch:0}); // TODO: introduce a fct reset
+ clearFeedback();
+ var item = tracer_items[tracer_pos];
+ source.setSelection({line: 0, ch:0}, {line: 0, ch:0}); // TODO: introduce a fct reset
if (item !== undefined) {
// console.log(item);
- $("#disp_infos").html("");
$("#disp_infos").html(itemToHtml(item));
if (item.source_loc === undefined) {
console.log("Error: missing line in log event");
@@ -712,7 +733,6 @@ function updateSelection() {
if (item.state === undefined || item.execution_ctx === undefined) {
$("#disp_env").html("<undefined state or context>");
} else {
- $("#disp_env").html("");
show_execution_ctx(item.state, item.execution_ctx, "disp_env");
}