diff --git a/generator/TODO b/generator/TODO
index f44a80038cf7d6d9bd0e7661d58c68c9924d38de..ab0b734433fa2ac56e48051bf3f2fa995336ed4d 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -1,3 +1,49 @@
+ let%if_spec (s,x) = expr in cont
+becomes
+ if_spec expr (fun s x -> cont)
+
+and in pseudo:
+ Let%spec x = expr in
+ cont
+
+
+------------
+
+
+ Let (x,y) = ...
+
+
+------------
+
+ return (
+ if_run(
+ convert_twice_string(Coq_value_prim(w1), Coq_value_prim(w2)),
+ function (ss) {
+ var s3 = ss[0], s4 = ss[1];
+ return (
+ res_out(
+ Coq_out_ter(s2,
+ res_val(
+ Coq_value_prim(Coq_prim_string(strappend(s3, s4)))))));
+ }));
+
+
+
+
+ let%run (s3,s4) = convert_twice_string(Coq_value_prim(w1), Coq_value_prim(w2)) in
+ if_run(
+ ,
+ function (ss) {
+ var s3 = ss[0], s4 = ss[1];
+ return (
+ res_out(
+ Coq_out_ter(s2,
+ res_val(
+ Coq_value_prim(Coq_prim_string(strappend(s3, s4)))))));
+ }));
+
+
+
--------------
@@ -20,10 +66,6 @@ BECOMES IN PSEUDO
------------------
-enlever les mlloc
-
-
diff --git a/generator/monad_ppx.ml b/generator/monad_ppx.ml
index b3d529d9d98ba00265210ac506ec061ab688306b..7ff1572a014ab15db124c3ba12811d3bf58d2b09 100644
--- a/generator/monad_ppx.ml
+++ b/generator/monad_ppx.ml
@@ -30,6 +30,10 @@ becomes
becomes
if_spec expr (fun s x -> cont)
+and in pseudo:
+ Let%spec x = expr in
+ cont
+
*)
diff --git a/navig-driver.js b/navig-driver.js
index 8fe663bbc045977d3afc2d903f2cf5e0bc249225..0a4702e5c50f06f163aed0b1bf7f19c472e51845 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -96,6 +96,8 @@ var source_files = [
'eval("var x = { a : 1 };\\nx.b = 2;\\nx");',
'var f = function() {return "f"}; eval("var g = function() {return \\"g\\"}; eval(\\"var h = function() {return \\\\\\"h\\\\\\"}; f(); g(); h()\\"); h();"); g(); h(); f();',
'var t = {};\nfor (var i = 0; i < 3; i++) {\n t[i] = eval("i + " + i); \n};\nt; ',
+ 'function f() {\n var x = 2;\n function g() { var x = 3; return x; };\n return g(); \n};\nf()',
+ 'f()' // bug? return 0 on the value thrown
];
source_files.reduce((select, file_content) => {
@@ -211,12 +213,20 @@ function jsvalue_of_value(v) {
}
function lookup_var_in_record_decl(name, env_record_decl) {
- // TODO : replace with
- // Heap.find name env_record_decl
- /// --> mutability_flag * value
- // return value
- // si not found, return undefined
-
+ var ro = Heap.read_option(string_eq, env_record_decl, name);
+ switch (ro.tag) {
+ case "None":
+ return undefined;
+ case "Some":
+ var r = ro.value;
+ var mutability = r[0];
+ var value = r[1];
+ return value;
+ default:
+ throw "unrecognized tag in lookup_var_in_record_decl";
+ }
+}
+ /* DEPRECATED, naive code for lookup_var_in_record_decl:
var items_array = array_of_heap(env_record_decl);
for (var i = 0; i < items_array.length; i++) {
var var_name = items_array[i][0];
@@ -227,7 +237,7 @@ function lookup_var_in_record_decl(name, env_record_decl) {
}
}
return undefined;
-}
+ */
function lookup_var_in_object(state, name, loc) {
var obj_opt = JsCommonAux.object_binds_pickable_option(state, loc);
@@ -261,53 +271,43 @@ function lookup_var_in_object(state, name, loc) {
// todo : handle objects
function lookup_var_in_lexical_env(state, name, lexical_env) {
// var env_record_heap = state.state_env_record_heap;
- var env_loc_array = encoded_list_to_array(lexical_env);
- // TODO: walk step by step the lexical env
- /* var r = [];
- while (list.tag == "::") {
- r.push(list.head);
- list = list.tail;
- }
- return r;
-
- function f() {
- var x = 2;
- var g = function() {
- var x = 3;
- breakpoint ==> S_core(x) == 3
- }
- }
- */
- for (var i = 0; i < env_loc_array.length; i++) {
+ /* DEPRECATED: naive processing of the loop
+ var env_loc_array = encoded_list_to_array(lexical_env);
+ for (var i = 0; i < env_loc_array.length; i++) {
var env_loc = env_loc_array[i];
- var env_record_opt = JsCommonAux.env_record_binds_pickable_option(state, env_loc);
- if (env_record_opt.tag != "Some") throw "show_object: unbound object";
- var env_record = env_record_opt.value;
-
- switch (env_record.tag) {
- case "Coq_env_record_decl":
- var env_record_decl = env_record.value;
- var r = lookup_var_in_record_decl(name, env_record_decl);
- if (r !== undefined) {
- return r;
- }
- break;
- case "Coq_env_record_object":
- var object_loc = env_record.value;
- var r = lookup_var_in_object(state, name, object_loc);
- if (r !== undefined) {
- return r;
- }
- /*
- var obj_value = { tag: "Coq_value_object", value: object_loc };
- var provide_this = env_record.provide_this;
- */
- break;
- default:
- throw "invalid env_record.tag";
- }
- }
- return undefined;
+ */
+ var list = lexical_env;
+ while (list.tag == "::") {
+ var env_loc = list.head;
+ list = list.tail;
+ var env_record_opt = JsCommonAux.env_record_binds_pickable_option(state, env_loc);
+ if (env_record_opt.tag != "Some") throw "show_object: unbound object";
+ var env_record = env_record_opt.value;
+
+ switch (env_record.tag) {
+ case "Coq_env_record_decl":
+ var env_record_decl = env_record.value;
+ var r = lookup_var_in_record_decl(name, env_record_decl);
+ if (r !== undefined) {
+ return r;
+ }
+ break;
+ case "Coq_env_record_object":
+ var object_loc = env_record.value;
+ var r = lookup_var_in_object(state, name, object_loc);
+ if (r !== undefined) {
+ return r;
+ }
+ /*
+ var obj_value = { tag: "Coq_value_object", value: object_loc };
+ var provide_this = env_record.provide_this;
+ */
+ break;
+ default:
+ throw "invalid env_record.tag";
+ }
+ }
+ return undefined;
}
function evalPred(item, pred) {
@@ -682,7 +682,7 @@ function string_of_any(v) {
// --------------- Views for JS state/context ----------------
function array_of_heap(heap) {
- var items_list = Heap.to_list(LibString.string_comparable, heap);
+ var items_list = Heap.to_list(string_eq, heap);
return encoded_list_to_array(items_list);
}
@@ -1322,6 +1322,11 @@ function assignExtraInfosInTrace() {
var t = binding.val;
if (t.loc != undefined) {
last_loc = t.loc;
+ /*console.log("found source loc: " +
+ last_loc.start.line + "," +
+ last_loc.start.column + " --> " +
+ last_loc.end.line + "," +
+ last_loc.end.column);*/
}
} else if (interp_val_is_state(binding.val)) {
// assuming: 'is an state object' iff 'has a state_object_heap field'
@@ -1420,7 +1425,6 @@ readSourceParseAndRun();
// stepTo(2466);
-// $("#reach_condition").val("S('x') == 2");
// button_reach_handler();
// $("#reach_condition").val("S_raw('x')");
// button_test_handler();
@@ -1430,7 +1434,9 @@ readSourceParseAndRun();
//
//stepTo(5873);
-setExample(3);
+setExample(20);
+$("#reach_condition").val("S('x') == 2");
+
function showCurrent() {
console.log(tracer_items[tracer_pos]);