cleanup

navig-driver.js

-// ----------- 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 },
+// ----------- Types ----------------
+
+// type loc
+// e.g.  {file: "foo.js", start: {line: 12, col: 9}, stop: {line: 13, col: 2} };
+//   Locations are generated by the translation from the parser to the AST
+
+// type event_type = 'enter' | 'return' | 'case' | 'let'
+//   Events are generated by the *.log.js files, themselves produced by the generator.
+
+// 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 
+//   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, 
+//                     state: JsSyntax.state, env: JsSyntax.env,
+//                     source_loc: loc }
+//   Event items are created on every call to the "log_event" function.
+//   Such calls are located in the *.log.js files.
+//   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". 
+
+// type trace = [event_item]
+//   In this file, "datalog" and "tracer_items" have type trace.
+
+// ----------- Datalog ----------------
 
 var datalog = [];
 
@@ -15,14 +39,11 @@ function log_event(loc, ctx, type) {
 
 // ----------- 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};
 }
@@ -41,6 +62,19 @@ function ctx_to_array(ctx) {
   return a;
 }
 
+// --------------- Representation for predicate evaluation ----------------
+
+function env_to_jsobject(env) {
+      // TODO implement
+   throw "unimplemented env_to_jsobject"; 
+};
+
+function ctx_to_jsobject(env) {
+      // TODO implement
+   throw "unimplemented ctx_to_jsobject"; 
+};
+
+
 // --------------- Handlers ----------------
 
 // callback functions to open and close objects displayed in the environment
@@ -51,16 +85,32 @@ var parsedTree;
 
 (function(check_pred){
 
-  // why do we need this in addition to datalog?
-  var tracer_items = [];
+   // --------------- Variables ----------------
 
+  // file currently displayed
+  var curfile = '';
+
+  // object of type loc describing the text currenctly selected
+  var source_loc_selected = undefined;
+
+  // current trace being displayed
+     // TODO: do we need tracer_iterms in addition to datalog? 
+  var tracer_items = [];
   var tracer_length = 0;
   var tracer_pos = 0;
 
+  // Core Mirror objects
+  var source = null;
+  var interpreter = null;
+
+  // --------------- Initialization ----------------
+
   // file displayed initially
   $("#source_code").val(source_file);
 
 
+  // --------------- Methods ----------------
+
   function stepTo(step) {
     tracer_pos = step;
     updateSelection();
@@ -74,13 +124,11 @@ var parsedTree;
       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
@@ -234,7 +282,8 @@ var parsedTree;
   function previous() { shared_next(-1, 0); }
   function finish() { shared_next(+1, -1); }
 
-  var curfile = '';
+
+  // --------------- Methods ----------------
 
   // load files in CodeMirror view
   var docs = {};
@@ -244,14 +293,11 @@ var parsedTree;
     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();
+      interpreter.swapDoc(docs[curfile]);
+      interpreter.focus();
       updateFileList();
     }
   }
@@ -277,8 +323,8 @@ var parsedTree;
     }
   }
 
+  // fresh name generated used for handlers of interactively-explorable values
   var next_fresh_id = 0;
-
   function fresh_id() {
     return "fresh_id_" + (next_fresh_id++);
   }
@@ -297,7 +343,7 @@ var parsedTree;
       function handler_close() {
         handlers[target] = handler_open;
         $("#" + target).html(contents_default);
-        editor.focus();
+        interpreter.focus();
       }
       function handler_open() {
         handlers[target] = handler_close;
@@ -313,7 +359,7 @@ var parsedTree;
         }
         if (count === 0)
           $("#" + target).append("<div style='margin-left:1em'>(empty object)</div>");
-        editor.focus();
+        interpreter.focus();
       };
       handlers[target] = handler_open;
       $("#" + target).html(contents_default);
@@ -345,25 +391,20 @@ var parsedTree;
     });
   }
 
-
-  var source_select = undefined;
-
-  function updateSourceSelection() {
-    if (source_select === undefined) {
+  // --------------- Selection view ----------------
+  
+  function updateSelection(codeMirrorObj, loc) {
+    if (loc === 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 } */;
+    var anchor = {line: loc.start.line-1 , ch: loc.start.column };
+    var head = {line: loc.stop.line-1, ch: loc.stop.column };
+    codeMirrorObj.setSelection(anchor, head);
   }
 
   function updateSelection() {
     var item = tracer_items[tracer_pos];
-    source.setSelection({line: 0, ch:0}, {line: 0, ch:0}); // TODO: fct reset
+    source.setSelection({line: 0, ch:0}, {line: 0, ch:0}); // TODO: introduce a fct reset
 
     if (item !== undefined) {
       // console.log(item);
@@ -372,34 +413,36 @@ var parsedTree;
         alert("missing line in log event");
 
       // source panel
-      source_select = item.source_select;
-      // console.log(source_select);
-      updateSourceSelection();
+      source_loc_selected = item.source_loc;
+      updateSelection(source, source_loc_selected);
+      // console.log(source_loc_selected);
+
+      // source heap/env panel
+      updateContext("#disp_env", item.heap, item.env);
 
-      // ctx panel
+      // interpreter ctx panel
       updateContext("#disp_ctx", item.heap, item.ctx);
 
-      // file panel
+      // interpreter code panel
       viewFile(item.file);
       //console.log("pos: " + tracer_pos);
-      // var color = (item.type === 'enter') ? '#F3F781' : '#CCCCCC';
+
       var color = '#F3F781';
+         // possible to use different colors depending on event type
+         // var color = (item.type === 'enter') ? '#F3F781' : '#CCCCCC';
       $('.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);
+      updateSelection(interpreter, item.loc);
 
       // navig panel
       $("#navigation_step").val(tracer_pos);
     }
     updateFileList();
-    editor.focus();
+    interpreter.focus();
   }
 
+  // --------------- CodeMirror ----------------
+
   source = CodeMirror.fromTextArea(document.getElementById('source_code'), {
     mode: 'js',
     lineNumbers: true,
@@ -407,7 +450,7 @@ var parsedTree;
   });
   source.setSize(300, 150);
 
-  editor = CodeMirror.fromTextArea(document.getElementById('interpreter_code'), {
+  interpreter = CodeMirror.fromTextArea(document.getElementById('interpreter_code'), {
     mode: 'js',
     lineNumbers: true,
     lineWrapping: true,
@@ -421,20 +464,20 @@ var parsedTree;
       'F': function(cm) { finish(); updateSelection(); }
     },
   });
-  editor.setSize(600,250);
+  interpreter.setSize(600,250);
 
   /* ==> try in new version of codemirror*/
   try {
-    $(editor.getWrapperElement()).resizable({
+    $(interpreter.getWrapperElement()).resizable({
       resize: function() {
-        editor.setSize($(this).width(), $(this).height());
+        interpreter.setSize($(this).width(), $(this).height());
       }
     });
   } catch(e) { }
 
-  editor.on('dblclick', function() {
-    var line = editor.getCursor().line;
-    var txt = editor.getLine(line);
+  interpreter.on('dblclick', function() {
+    var line = interpreter.getCursor().line;
+    var txt = interpreter.getLine(line);
     var prefix = "#sec-";
     var pos_start = txt.indexOf(prefix);
     if (pos_start === -1)
@@ -447,23 +490,22 @@ var parsedTree;
     window.open(url, '_blank');
   });
 
-  editor.focus();
-
+  interpreter.focus();
 
+  // --------------- Main run method ----------------
 
-  // used to ensure that most events have an associated term
-  function completeTermsInDatalog(items) {
+  function assignSourceLogInTrace(items) {
     var last = undefined;
     for (var k = 0; k < datalog.length; k++) {
       var item = datalog[k];
-      item.source_select = last;
+      item.source_loc = 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;
+            item.source_loc = t.loc;
             // t.loc = {start : int, end : int}
             last = t;
           }
@@ -472,11 +514,9 @@ var parsedTree;
     }
   }
 
-
-
   function run() {
     JsInterpreter.run_javascript(JsInterpreter.runs, program);
-    completeTermsInDatalog(datalog);
+    assignSourceLogInTrace(datalog);
     tracer_items = datalog;
     tracer_length = tracer_items.length;
     $("#navigation_total").html(tracer_length - 1);