diff --git a/driver.html b/driver.html
new file mode 100644
index 0000000000000000000000000000000000000000..e89594708c6162c4525bc75e1aead90e27b2ea7c
--- /dev/null
+++ b/driver.html
@@ -0,0 +1,179 @@
+<!doctype html>
+<html>
+<head>
+<meta charset="utf-8">
+<title>JavaScript Reference Tracer</title>
+
+<script src="../../interp/tracer/jquery-2.1.1.min.js"></script>
+
+<link rel=stylesheet href="../../interp/tracer/codemirror/lib/codemirror.css">
+<script src="../../interp/tracer/codemirror/lib/codemirror.js"></script>
+
+
+<!-- styles needed by jScrollPane - include in your own sites -->
+<link type="text/css" href="jquery_scroll/jquery.jscrollpane.css" rel="stylesheet" media="all" />
+<!-- the mousewheel plugin -->
+<script type="text/javascript" src="jquery_scroll/jquery.mousewheel.js"></script>
+<!-- the jScrollPane script -->
+<script type="text/javascript" src="jquery_scroll/jquery.jscrollpane.min.js"></script>
+
+<link rel="stylesheet" href="jquery-ui-1.11.4.custom/jquery-ui.css">
+<script src="jquery-ui-1.11.4.custom/jquery-ui.js"></script>
+
+<script src="https://cdn.rawgit.com/jquery/esprima/1.2/esprima.js"></script>
+<script type = "text/javascript" src="source-driver.js"></script>
+<!-- <script src="interp-poc.js"></script> -->
+
+<!-- <style> -->
+<!-- .source_div { -->
+<!-- border-top: 1px solid black; -->
+<!-- border-bottom: 1px solid black; -->
+<!-- } -->
+
+<!-- .heap_link { -->
+<!-- color: black; -->
+<!-- } -->
+
+<!-- #file_list { -->
+<!-- height: 1em; -->
+<!-- padding-top: 8px; -->
+<!-- padding-bottom: 8px; -->
+<!-- border-bottom: 1px solid black; -->
+<!-- } -->
+
+<!-- .file_item, .file_item_current { -->
+<!-- margin-right: 5px; -->
+<!-- padding: 5px; -->
+<!-- text-decoration: underline; -->
+<!-- } -->
+
+<!-- .file_item, .file_item_current:hover { -->
+<!-- cursor: pointer; -->
+<!-- cursor: hand; -->
+<!-- } -->
+
+<!-- .file_item { -->
+<!-- background-color: #FAFAFA; -->
+<!-- } -->
+
+<!-- .file_item_current { -->
+<!-- background-color: #FFCCCC; -->
+<!-- } -->
+
+<!-- #main_table td { -->
+<!-- vertical-align: top; -->
+<!-- border: 1px solid black; -->
+<!-- } -->
+
+<!-- .CodeMirror-selected { background: #F3F781; } -->
+<!-- .CodeMirror-focused .CodeMirror-selected { background: #F3F781; } -->
+
+
+<!-- .scroll-pane -->
+<!-- { -->
+<!-- width: 100%; -->
+<!-- height: 200px; -->
+<!-- overflow: auto; -->
+<!-- } -->
+<!-- </style> -->
+
+
+</head>
+<body>
+
+<h2>Mini-ML Interpreter</h2>
+
+
+<!-- <div class='source_div'> -->
+
+<!-- <table id='main_table'><tr> -->
+<!-- <td> -->
+<!-- <textarea id='source_code' class='source' rows='6' cols='60'>source code here</textarea> -->
+<!-- </td> -->
+<!-- <td width='600'> -->
+<!-- <div class="scroll-pane" style="height: 10em"> -->
+<!-- <div id='disp_env'>ctx here</div> -->
+<!-- </div> -->
+<!-- </td> -->
+<!-- </tr></table> -->
+<!-- </div> -->
+
+
+
+<!-- <br/> -->
+<!-- <div> -->
+<!-- <input type="button" id="button_run" value="RUN" /> -->
+<!-- Navigation: -->
+<!-- <input type="textbox" id='navigation_step' style="width:3em" value="0"/> -->
+<!-- / <span id="navigation_total"></span> -->
+<!-- <input type="button" id='button_reset' value="Reset" /> -->
+<!-- <input type="button" id='button_prev' value="Prev" /> -->
+<!-- <input type="button" id='button_next' value="Next" /> -->
+<!-- Reach condition: -->
+<!-- <input type="textbox" id='text_condition' style="width:30em" /> -->
+<!-- <input type="button" id='button_reach' value="Reach" /> -->
+<!-- <span id="reach_output"></span> -->
+<!-- </div> -->
+
+<!-- <div id="action_output"></div> -->
+<!-- <br/> -->
+
+<!-- <div class='source_div'> -->
+
+<!-- <table id='main_table'><tr> -->
+<!-- <td> -->
+<!-- <div id='file_list'></div> -->
+<!-- <textarea id='interpreter_code' class='source' rows='20' cols='60'></textarea> -->
+<!-- </td> -->
+<!-- <td width='600'> -->
+<!-- <div id='disp_infos'></div> -->
+<!-- <div id='disp_ctx'>ctx here</div> -->
+<!-- </td> -->
+<!-- </tr></table> -->
+<!-- </div> -->
+
+
+<!-- <script src="navig-poc.js"></script> -->
+
+<!-- <\!-- -->
+<!-- <script language="javascript"> -->
+<!-- $(function() { -->
+<!-- $('.scroll-pane').jScrollPane(); -->
+<!-- }); -->
+<!-- </script> -->
+<!-- -\-> -->
+
+<!-- <\!--div style="font-size:0.8em">Instructions: from console, the variable "h" denotes the current heap.</div-\-> -->
+
+<!-- <div style="font-size:0.8em">Instructions: type 'S' for step (next function call), 'N' for next (next call at same level), 'B' for backstep (symmetric to step), 'P' for previous (symmetric to next), 'F' for finish (next call at upper level), 'R' for restart.</div> -->
+
+<!-- <div style="font-size:0.8em">Examples of conditions: -->
+<!-- <ul> -->
+<!-- <li><pre style = "display:inline">X.type === "fun" && (X.v1, true)</pre> (we are at the beginning of a function and v1 is defined in the local interpreter context),</li> -->
+<!-- <li><pre style = "display:inline">X.line === 32 && X.t.tag === "trm_set" && X.t.field === "bar"</pre> (we are at line 32 and we are setting the field “bar†of the current location),</li> -->
+<!-- <li><pre style = "display:inline">y.foo === 12</pre> (the program variable “y†points to an object whose field “foo†is equal to 12),</li> -->
+<!-- <li><pre style = "display:inline">X.heap[0].bar === 12</pre> (the first cell of the heap has a field “bar†defined equal to 12).</li> -->
+<!-- </ul></div> -->
+<!-- Â -->
+
+</body>
+</html>
+
+
+
+<!---
+$timeout(function() {codeMirror.refresh();});
+
+this.codeMirrorInstance.setValue(content);
+var that = this;
+setTimeout(function() {
+ that.codeMirrorInstance.refresh();
+},1);
+
+http://codemirror.net/demo/buffers.html
+
+//CodeMirror.Doc(text
+---->
+
+
+
diff --git a/navig-driver.js b/navig-driver.js
new file mode 100644
index 0000000000000000000000000000000000000000..91808dc5a3e072b466c4c9643b7a680c5b76573e
--- /dev/null
+++ b/navig-driver.js
@@ -0,0 +1,491 @@
+// ----------- Datalog ----------------
+
+// Definition of loc is in lineof.ml
+// event_type is 'enter', 'return', 'case', 'let'
+// Assumes datalog and tracer_items to be an array with items, e.g.:
+// { type: event_type, loc: loc, ctx: ctx },
+
+var datalog = [];
+
+function log_event(loc, ctx, type) {
+ // TODO populate state with object_heap, env_record_heap, fresh_locations, and populate env
+ var event = {loc : loc, ctx : ctx, type : type, state: {}, env: {}};
+ datalog.push(event);
+}
+
+// ----------- Context ----------------
+
+// chained list of arrays, top of stack as the head of the list, each array
+// stores bindings in reverse order
+
+function ctx_empty() {
+ return {tag: "ctx_nil"};
+}
+
+// bindings: [{key: string, val: any?}]
+function ctx_push(ctx, bindings) {
+ return {tag: "ctx_cons", next: ctx, bindings: bindings};
+}
+
+function ctx_to_array(ctx) {
+ var a = [];
+
+ while (ctx.tag === "ctx_cons") {
+ var b = ctx.bindings;
+ for (var i = b.length - 1; i >= 0; i--) {
+ a.push(b[i]);
+ }
+ ctx = ctx.next;
+ }
+
+ return a;
+}
+
+// --------------- Handlers ----------------
+
+// callback functions to open and close objects displayed in the environment
+// view
+var handlers = [];
+
+var parsedTree;
+
+(function(check_pred){
+
+ // why do we need this in addition to datalog?
+ var tracer_items = [];
+
+ var tracer_length = 0;
+ var tracer_pos = 0;
+
+ // file displayed initially
+ $("#source_code").val(source_file);
+
+
+ function stepTo(step) {
+ tracer_pos = step;
+ updateSelection();
+ }
+
+ // Take a predicate in form of a JavaScript code (string) and returns either true or an error message (string).
+ function goToPred(pred) {
+
+ function check(i){
+ var item = datalog[i];
+ var state = item.state;
+ // the goal here is to take the environment and make it available to the
+ // user
+ // TODO implement
+ var obj = env_to_jsobject(state, item.env);
+ // the goal here is to take the local variable of the interpreter and make
+ // them available to the user
+ var objX = {};
+ if (item.ctx !== undefined){
+ // TODO implement
+ objX = ctx_to_jsobject(state, item.ctx);
+ }
+ // TODO bind loc
+ objX.line = item.loc.start.line;
+ objX.type = item.type;
+ // TODO bind other fields of the state
+ objX.heap = state.object_heap;
+ obj.X = objX; // If we want to change the “X†identifier, just change this line.
+ try {
+ if (check_pred(pred, obj)){
+ stepTo(i);
+ return true;
+ }
+ } catch(e){
+ error++;
+ }
+
+ return false;
+ }
+
+ var error = 0;
+
+ if (datalog.length === 0)
+ return false;
+
+ for (var i = (tracer_pos + 1) % datalog.length, current = tracer_pos;
+ i !== current;
+ i++, i %= datalog.length)
+ if (check(i))
+ return true;
+
+ if (check(tracer_pos))
+ return true;
+
+ if (error === datalog.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";
+ }
+
+ function button_reach_handler() {
+ var pred = $("#text_condition").val();
+ var res = goToPred(pred);
+ if (res !== true){
+ $("#action_output").html(res);
+ var timeoutID =
+ window.setTimeout(function() {
+ $("#action_output").html(""); }, 3000);
+ }
+ };
+
+ $('#text_condition').keypress(function(e){
+ var keycode = (e.keyCode ? e.keyCode : e.which);
+ if (keycode == '13') {
+ button_reach_handler();
+ }
+ });
+
+ $("#button_reach").click(button_reach_handler);
+
+
+ $("#navigation_step").change(function(e) {
+ var n = + $("#navigation_step").val();
+ n = Math.max(0, Math.min(tracer_length - 1, n));
+ stepTo(n);
+ });
+
+ $("#button_run").click(function() {
+ try {
+ var code = source.getValue();
+ //console.log(code);
+ // TODO handle parsing error
+ parsedTree = esprima.parse(code, {loc:true});
+ // console.log(parsedTree);
+ // TODO write the parser
+ program = esprimaToAST(parsedTree);
+ // console.log(program);
+ run();
+ $("#action_output").html("Run successful!");
+ } catch(_){
+ $("#action_output").html("Error during the run.");
+ };
+ var timeoutID = window.setTimeout(function() { $("#run_output").html(""); }, 1000);
+ });
+
+ $("#button_reset").click(function() {
+ stepTo(0);
+ });
+
+ $("#button_prev").click(function() {
+ stepTo(Math.max(0, tracer_pos-1));
+ });
+
+ $("#button_next").click(function() {
+ stepTo(Math.min(tracer_length-1, tracer_pos+1));
+ });
+
+
+ // Assumes tracer_files to be an array of objects with two field:
+ // - file, containing the name of the file,
+ // - contents, a string containing its source code
+
+ function tracer_valid_pos(i) {
+ return (i >= 0 && i < tracer_length);
+ }
+
+ // dir is -1 or +1
+ function shared_step(dir) {
+ var i = tracer_pos;
+ i += dir;
+ if (! tracer_valid_pos(i))
+ return; // not found, we don’t update the tracer position.
+ tracer_pos = i;
+ }
+
+ // dir is -1 or +1,
+ // target (= target depth) is 0 for (next/prev) or -1 (finish)
+ function shared_next(dir, target) {
+ var i = tracer_pos;
+ var depth = 0;
+ var ty = tracer_items[i].type;
+ // TODO check if this works
+ if (dir === +1 && ty === 'return') {
+ depth = 1;
+ } else if (dir === -1 && ty === 'enter') {
+ depth = -1;
+ }
+ while (true) {
+ if (! tracer_valid_pos(i)) {
+ tracer_pos = i - dir; // just before out of range
+ return; // not found
+ }
+ if (i !== tracer_pos && depth === target) {
+ tracer_pos = i;
+ return;
+ }
+ var ty = tracer_items[i].type;
+ if (ty === 'enter') {
+ depth++;
+ } else if (ty === 'return') {
+ depth--;
+ }
+ i += dir;
+ }
+ }
+
+ function restart() { tracer_pos = 0; }
+ function step() { shared_step(+1); }
+ function backstep() { shared_step(-1); }
+ function next() { shared_next(+1, 0); }
+ function previous() { shared_next(-1, 0); }
+ function finish() { shared_next(+1, -1); }
+
+ var curfile = '';
+
+ // load files in CodeMirror view
+ var docs = {};
+ for (var i = 0; i < tracer_files.length; i++) {
+ var file = tracer_files[i].file;
+ var txt = tracer_files[i].contents;
+ docs[file] = CodeMirror.Doc(txt, 'js');
+ }
+
+ var editor = null;
+ var source = null;
+
+ function viewFile(file) {
+ if (curfile !== file) {
+ curfile = file;
+ editor.swapDoc(docs[curfile]);
+ editor.focus();
+ updateFileList();
+ }
+ }
+
+ function updateFileList() {
+ var s = '';
+ for (var i = 0; i < tracer_files.length; i++) {
+ var file = tracer_files[i].file;
+ s += "<span class=\"file_item" + ((curfile == file) ? '_current' : '') + "\" onclick=\"viewFile('" + file + "')\">" + file + "</span> ";
+ }
+ $('#file_list').html(s);
+ }
+
+ // TODO adapt to values from JsSyntax
+ function text_of_cst(c) {
+ switch (c.tag) {
+ case "cst_bool":
+ return c.bool + "";
+ case "cst_number":
+ return c.number + "";
+ default:
+ return "unrecognized cst";
+ }
+ }
+
+ var next_fresh_id = 0;
+
+ function fresh_id() {
+ return "fresh_id_" + (next_fresh_id++);
+ }
+
+ // TODO deal with the heap here
+ function show_value(heap, v, target, depth) {
+ var contents_init = $("#" + target).html();
+ var s = "";
+ switch (v.tag) {
+ case "val_cst":
+ s = text_of_cst(v.cst);
+ break;
+ case "val_loc":
+ var contents_rest = "<span class='heap_link'><a onclick=\"handlers['" + target + "']()\"><Object>(" + v.loc + ")</a></span>";
+ var contents_default = contents_init + contents_rest;
+ function handler_close() {
+ handlers[target] = handler_open;
+ $("#" + target).html(contents_default);
+ editor.focus();
+ }
+ function handler_open() {
+ handlers[target] = handler_close;
+ var obj = heap.get(v.loc).asReadOnlyArray(); // type object
+ var count = 0;
+ for (var x in obj) {
+ if (obj[x] === undefined) continue; // LATER remove!
+ count++;
+ var targetsub = fresh_id();
+ $("#" + target).append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
+ $("#" + targetsub).html(x + ": ");
+ show_value(heap, obj[x], targetsub, depth-1);
+ }
+ if (count === 0)
+ $("#" + target).append("<div style='margin-left:1em'>(empty object)</div>");
+ editor.focus();
+ };
+ handlers[target] = handler_open;
+ $("#" + target).html(contents_default);
+ if (depth > 0)
+ handler_open();
+ return;
+ case "val_abs":
+ s = "<Closure>";
+ break;
+ default:
+ s = "<pre style='margin:0; padding: 0; margin-left:1em'>" + JSON.stringify(v, null, 2) + "</pre>";
+ break;
+ }
+ $("#" + target).append(s);
+ }
+
+ function updateContext(targetid, heap, env) {
+ $(targetid).html("");
+ if (env === undefined)
+ return;
+ if (heap === undefined)
+ return;
+ array_of_env(env).map(function(env){
+ var target = fresh_id();
+ $(targetid).append("<div id='" + target + "'></div>");
+ $("#" + target).html(env.name + ": ");
+ var depth = 1;
+ show_value(heap, env.val, target, depth);
+ });
+ }
+
+
+ var source_select = undefined;
+
+ function updateSourceSelection() {
+ if (source_select === undefined) {
+ return;
+ }
+ // TODO: adapt to new structure
+ var anchor = {line: source_select.start.line-1 , ch: source_select.start.column };
+ var head = {line: source_select.end.line-1, ch: source_select.end.column };
+ source.setSelection(anchor, head);
+ /* deprecated:
+ var anchor = {line: source_select-1, ch: 0 };
+ var head = {line: source_select-1, ch: 100 } */;
+ }
+
+ function updateSelection() {
+ var item = tracer_items[tracer_pos];
+ source.setSelection({line: 0, ch:0}, {line: 0, ch:0}); // TODO: fct reset
+
+ if (item !== undefined) {
+ // console.log(item);
+ // $("#disp_infos").html();
+ if (item.line === undefined)
+ alert("missing line in log event");
+
+ // source panel
+ source_select = item.source_select;
+ // console.log(source_select);
+ updateSourceSelection();
+
+ // ctx panel
+ updateContext("#disp_ctx", item.heap, item.ctx);
+
+ // file panel
+ viewFile(item.file);
+ //console.log("pos: " + tracer_pos);
+ // var color = (item.type === 'enter') ? '#F3F781' : '#CCCCCC';
+ var color = '#F3F781';
+ $('.CodeMirror-selected').css({ background: color });
+ $('.CodeMirror-focused .CodeMirror-selected').css({ background: color });
+ var anchor = {line: item.start_line-1 , ch: item.start_col };
+ var head = {line: item.end_line-1, ch: item.end_col };
+ editor.setSelection(anchor, head);
+
+ // env panel
+ updateContext("#disp_env", item.heap, item.env);
+
+ // navig panel
+ $("#navigation_step").val(tracer_pos);
+ }
+ updateFileList();
+ editor.focus();
+ }
+
+ source = CodeMirror.fromTextArea(document.getElementById('source_code'), {
+ mode: 'js',
+ lineNumbers: true,
+ lineWrapping: true
+ });
+ source.setSize(300, 150);
+
+ editor = CodeMirror.fromTextArea(document.getElementById('interpreter_code'), {
+ mode: 'js',
+ lineNumbers: true,
+ lineWrapping: true,
+ readOnly: true,
+ extraKeys: {
+ 'R': function(cm) { restart(); updateSelection(); },
+ 'S': function(cm) { step(); updateSelection(); },
+ 'B': function(cm) { backstep(); updateSelection(); },
+ 'N': function(cm) { next(); updateSelection(); },
+ 'P': function(cm) { previous(); updateSelection(); },
+ 'F': function(cm) { finish(); updateSelection(); }
+ },
+ });
+ editor.setSize(600,250);
+
+ /* ==> try in new version of codemirror*/
+ try {
+ $(editor.getWrapperElement()).resizable({
+ resize: function() {
+ editor.setSize($(this).width(), $(this).height());
+ }
+ });
+ } catch(e) { }
+
+ editor.on('dblclick', function() {
+ var line = editor.getCursor().line;
+ var txt = editor.getLine(line);
+ var prefix = "#sec-";
+ var pos_start = txt.indexOf(prefix);
+ if (pos_start === -1)
+ return;
+ var pos_end = txt.indexOf("*", pos_start);
+ if (pos_end === -1)
+ return;
+ var sec = txt.substring(pos_start, pos_end);
+ var url = "http://www.ecma-international.org/ecma-262/5.1/" + sec;
+ window.open(url, '_blank');
+ });
+
+ editor.focus();
+
+
+
+ // used to ensure that most events have an associated term
+ function completeTermsInDatalog(items) {
+ var last = undefined;
+ for (var k = 0; k < datalog.length; k++) {
+ var item = datalog[k];
+ item.source_select = last;
+ if (item.ctx !== undefined) {
+ var ctx_as_array = array_of_env(item.ctx);
+ // only considers _term_ as top of ctx
+ if (ctx_as_array.length > 0 && ctx_as_array[0].key === "_term_") {
+ var t = ctx_as_array[0].val;
+ if (! (t === undefined || t.loc === undefined)) {
+ item.source_select = t.loc;
+ // t.loc = {start : int, end : int}
+ last = t;
+ }
+ }
+ }
+ }
+ }
+
+
+
+ function run() {
+ JsInterpreter.run_javascript(JsInterpreter.runs, program);
+ completeTermsInDatalog(datalog);
+ tracer_items = datalog;
+ tracer_length = tracer_items.length;
+ $("#navigation_total").html(tracer_length - 1);
+ stepTo(0); // calls updateSelection();
+ }
+
+}(function check_pred(p, obj) {
+ with (obj){
+ return eval(p)
+ }
+}));
+
diff --git a/source-driver.js b/source-driver.js
new file mode 100644
index 0000000000000000000000000000000000000000..cbc45443b2916d5969d87c90b4a2ad48d6e25491
--- /dev/null
+++ b/source-driver.js
@@ -0,0 +1,9 @@
+var source_file = 'var x = 2;\n';
+
+var tracer_files = [
+ // the tracer files
+];
+
+// stdlib
+
+// the logged files