From 7df93a803de66ac88e39a162e0a8684c8ba36a8f Mon Sep 17 00:00:00 2001
From: Alan Schmitt <alan.schmitt@polytechnique.org>
Date: Tue, 1 Mar 2016 09:16:15 +0100
Subject: [PATCH] it compiles !
---
generator/tests/jsref/JsSyntax.ml | 8 ++++----
navig-driver.js | 24 ++++++++++++------------
2 files changed, 16 insertions(+), 16 deletions(-)
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index ba7a38d..ac9e48e 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -101,10 +101,10 @@ and stat =
| Coq_stat_break [@f label] of label (** Auto Generated Attributes **)
| Coq_stat_continue [@f label] of label (** Auto Generated Attributes **)
| Coq_stat_try [@f body, catch_stats_opt, finally_opt] of stat * (string * stat) option * stat option (** Auto Generated Attributes **)
-| Coq_stat_for [@f labels, TODO_opt1, TODO_opt2, TODO_opt3, body] of label_set * expr option * expr option * expr option * stat (** Auto Generated Attributes **)
-| Coq_stat_for_var [@f labels, TODO_list1, TODO_opt2, TODO_opt3, body] of label_set * (string * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **)
-| Coq_stat_for_in [@f labels, TODO_exp1, TODO_exp2, body] of label_set * expr * expr * stat (** Auto Generated Attributes **)
-| Coq_stat_for_in_var [@f labels, TODO_str1, TODO_exp2, TODO_exp3, body] of label_set * string * expr option * expr * stat (** Auto Generated Attributes **)
+| Coq_stat_for [@f labels, init, cond, step, body] of label_set * expr option * expr option * expr option * stat (** Auto Generated Attributes **)
+| Coq_stat_for_var [@f labels, init, cond, step, body] of label_set * (string * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **)
+| Coq_stat_for_in [@f labels, id, obj, body] of label_set * expr * expr * stat (** Auto Generated Attributes **)
+| Coq_stat_for_in_var [@f labels, id, init, obj, body] of label_set * string * expr option * expr * stat (** Auto Generated Attributes **)
| Coq_stat_debugger [@f] (** Auto Generated Attributes **)
| Coq_stat_switch [@f labels, arg, body] of label_set * expr * switchbody (** Auto Generated Attributes **)
and switchbody =
diff --git a/navig-driver.js b/navig-driver.js
index 2902b00..d37f275 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -10,11 +10,11 @@
// type ctx = {tag: "ctx_nil"} | {tag: "ctx_cons", next: ctx, bindings: bindings};
// type bindings = [{key: string, val: any}]
-// A context is a linked list of arrays, with the top of stack located at the
+// A context is a linked list of arrays, with the top of stack located at the
// head of the list, and where each array stores a set of bindings, with the
// more recent binding at the tail of the array.
-// type event_item = { type: event_type, loc: loc, ctx: ctx,
+// type event_item = { type: event_type, loc: loc, ctx: ctx,
// state: JsSyntax.state, env: JsSyntax.env,
// source_loc: loc }
// Event items are created on every call to the "log_event" function.
@@ -22,7 +22,7 @@
// Fields "state" and "env" are snapshots of the state at the time of the event.
// Field "ctx" describes the state of the variables from the interpreter,
// and this description is constructed by the instrumented code in "*.log.js".
-// The "source_loc" fields are filled in by function "assignSourceLogInTrace".
+// The "source_loc" fields are filled in by function "assignSourceLocInTrace".
// type trace = [event_item]
// In this file, "datalog" and "tracer_items" have type trace.
@@ -120,7 +120,7 @@ var parsedTree;
function goToPred(pred) {
function check(i){
- var item = datalog[i];
+ var item = tracer_items[i];
var state = item.state;
// the goal here is to take the environment and make it available to the
// user
@@ -151,19 +151,19 @@ var parsedTree;
var error = 0;
- if (datalog.length === 0)
+ if (tracer_items.length === 0)
return false;
- for (var i = (tracer_pos + 1) % datalog.length, current = tracer_pos;
+ for (var i = (tracer_pos + 1) % tracer_items.length, current = tracer_pos;
i !== current;
- i++, i %= datalog.length)
+ i++, i %= tracer_items.length)
if (check(i))
return true;
if (check(tracer_pos))
return true;
- if (error === datalog.length)
+ if (error === tracer_items.length)
return "There was an execution error at every execution of your condition: are you sure that this is a valid JavaScript code?";
return "Not found";
@@ -494,10 +494,10 @@ var parsedTree;
// --------------- Main run method ----------------
- function assignSourceLogInTrace(items) {
+ function assignSourceLocInTrace(items) {
var last = undefined;
- for (var k = 0; k < datalog.length; k++) {
- var item = datalog[k];
+ for (var k = 0; k < tracer_items.length; k++) {
+ var item = tracer_items[k];
item.source_loc = last;
if (item.ctx !== undefined) {
var ctx_as_array = array_of_env(item.ctx);
@@ -516,7 +516,7 @@ var parsedTree;
function run() {
JsInterpreter.run_javascript(JsInterpreter.runs, program);
- assignSourceLogInTrace(datalog);
+ assignSourceLocInTrace(datalog);
tracer_items = datalog;
tracer_length = tracer_items.length;
$("#navigation_total").html(tracer_length - 1);
--
GitLab