From be3f8513eff2ef936d6acf59927120d3f7b7af65 Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Tue, 29 Mar 2016 16:00:08 +0200
Subject: [PATCH] disp_obj
---
driver.html | 12 ++-
generator/stdlib_ml/stdlib.js | 8 +-
navig-driver.js | 189 ++++++++++++++++++++++++++++------
3 files changed, 171 insertions(+), 38 deletions(-)
diff --git a/driver.html b/driver.html
index 886aa0b..fd454b9 100644
--- a/driver.html
+++ b/driver.html
@@ -70,6 +70,10 @@
color: red;
}
+#disp_env {
+ margin-top: 0.5em;
+}
+
.CodeMirror-selected { background: #F3F781; }
.CodeMirror-focused .CodeMirror-selected { background: #F3F781; }
@@ -136,11 +140,13 @@ Navigation:
<div id='file_list'></div>
<textarea id='interpreter_code' class='source' rows='30' cols='60'></textarea>
</td>
-<td width='600'>
- <div id='disp_ctx'>ctx here</div>
-</td>
+<!--<td width='600'>
+ <div id='disp_ctx'></div>
+</td>-->
</tr></table>
</div>
+<div id='disp_ctx'></div>
+<hr>
<div id='disp_infos'></div>
<script src="tools.js"></script>
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index b1eba5d..62d1f9a 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -2,21 +2,21 @@
//----------------------------------------------------------------------------
var None = function() {
- return { type: "option", tag: "None" };
+ return { /*type: "option",*/ tag: "None" };
};
var Some = function(value) {
- return { type: "option", tag: "Some", value: value };
+ return { /*type: "option",*/ tag: "Some", value: value };
};
//----------------------------------------------------------------------------
var mk_nil = function() {
- return { type: "list", tag: "[]" };
+ return { /*type: "list",*/ tag: "[]" };
};
var mk_cons = function(head, tail) {
- return { type: "list", tag: "::", head: head, tail: tail };
+ return { /*type: "list",*/ tag: "::", head: head, tail: tail };
};
//----------------------------------------------------------------------------
diff --git a/navig-driver.js b/navig-driver.js
index 4de5c3e..1bb136c 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -81,6 +81,9 @@ var source_file = '{} + {}';
var source_file = 'var x = { a : 1, b : 2 }; ';
var source_file = 'x = 1;\nx = 2;\nx = 3';
var source_file = '(function (x) {return 1;})()';
+var source_file = 'var x = { a : 1 };\n x.b = 2;\nx';
+var source_file = 'var x = { a : { c: 1 } };\n x.a.b = 2;\nx';
+
// --------------- Initialization ----------------
@@ -357,6 +360,9 @@ function html_escape(stringToEncode) {
return entityMap[s]; });
}
+function string_of_any(v) {
+ return "<pre style='margin:0; padding: 0; margin-left:1em'>" + JSON.stringify(v, null, 2) + "</pre>";
+}
// --------------- Views for JS state/context ----------------
@@ -365,7 +371,6 @@ function array_of_heap(heap) {
return encoded_list_to_array(items_list);
}
-
function string_of_prealloc(prealloc) {
return (prealloc.tag).slice("Coq_prealloc_".length);
//TODO:
@@ -385,11 +390,6 @@ function string_of_loc(loc) {
}
}
-
-function string_of_default(v) {
- return "<pre style='margin:0; padding: 0; margin-left:1em'>" + JSON.stringify(v, null, 2) + "</pre>";
-}
-
function string_of_prim(v) {
switch (v.tag) {
case "Coq_prim_undef":
@@ -401,7 +401,7 @@ function string_of_prim(v) {
case "Coq_prim_number":
return "" + v.value;
case "Coq_prim_string":
- return "\"" + v.value + "\"";
+ return "\"" + html_escape(v.value) + "\"";
default:
throw "unrecognized tag in string_of_prim";
}
@@ -484,7 +484,7 @@ function show_object(state, loc, target, depth) {
var targetsub = fresh_id();
t.append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
- $("#" + targetsub).html(html_escape(prop_name) + ": ");
+ $("#" + targetsub).html("– " + html_escape(prop_name) + ": ");
switch (attribute.tag) {
case "Coq_attributes_data_of":
@@ -506,7 +506,7 @@ function show_object(state, loc, target, depth) {
// special display for empty objects
if (key_value_pair_array.length === 0) {
- t.append("<div style='margin-left:1em'>(empty object)</div>");
+ t.append("(empty object)");
}
}
@@ -519,24 +519,24 @@ function show_value(state, v, target, depth) {
return;
case "Coq_value_object":
var loc = v.value;
- var contents_init = $("#" + target).html();
- var contents_rest = "<span class='heap_link'><a onclick=\"handlers['" + target + "']()\"><Object>(" + string_of_loc(loc) + ")</a></span>";
- var contents_default = contents_init + contents_rest;
+ var obj_target = fresh_id();
+ t.append("<span class='heap_link'><a onclick=\"handlers['" + obj_target + "']()\" ><Object>(" + string_of_loc(loc) + ")</a><span id='" + obj_target + "'></span></span>");
function handler_close() {
- handlers[target] = handler_open;
- t.html(contents_default);
+ handlers[obj_target] = handler_open;
+ $("#" + obj_target).html("");
interpreter.focus();
}
function handler_open() {
- handlers[target] = handler_close;
- show_object(state, loc, target, depth);
+ handlers[obj_target] = handler_close;
+ show_object(state, loc, obj_target, 1);
interpreter.focus();
};
- handlers[target] = handler_open;
// initial opening of the object
- t.append(contents_default);
if (depth > 0) {
- handler_open();
+ handlers[obj_target] = handler_close;
+ show_object(state, loc, obj_target, depth);
+ } else {
+ handler_close();
}
return;
default:
@@ -635,6 +635,129 @@ function updateContext(targetid, state, env) {
}
*/
+function has_tag_in_set(value, array_tags) {
+ return (value.tag !== undefined &&
+ array_tags.indexOf(value.tag) != -1);
+}
+
+function interp_val_is_base_value(val) {
+ var t = typeof(val);
+ return t == "string" ||
+ t == "number" ||
+ t == "boolean" ||
+ t == "undefined" ||
+ t == "null";
+}
+
+function interp_val_is_js_prim(v) {
+ return has_tag_in_set(v, [ "Coq_prim_undef", "Coq_prim_null", "Coq_prim_bool", "Coq_prim_number", "Coq_prim_string" ]);
+}
+
+function interp_val_is_js_value(v) {
+ return has_tag_in_set(v, [ "Coq_value_prim", "Coq_value_object" ]);
+}
+
+function interp_val_is_loc(v) {
+ return has_tag_in_set(v, [ "Coq_object_loc_normal", "Coq_object_loc_prealloc" ]);
+}
+
+function interp_val_is_list(v) {
+ return has_tag_in_set(v, [ "::", "[]" ]);
+}
+
+function interp_val_is_syntax(v) {
+ return has_tag_in_set(v, [ "Coq_expr_this", "Coq_expr_identifier", "Coq_expr_literal", "Coq_expr_object", "Coq_expr_array", "Coq_expr_function", "Coq_expr_access", "Coq_expr_member", "Coq_expr_new", "Coq_expr_call", "Coq_expr_unary_op", "Coq_expr_binary_op", "Coq_expr_conditional", "Coq_expr_assign", "Coq_propbody_val", "Coq_propbody_get", "Coq_propbody_set", "Coq_funcbody_intro", "Coq_stat_expr", "Coq_stat_label", "Coq_stat_block", "Coq_stat_var_decl", "Coq_stat_if", "Coq_stat_do_while", "Coq_stat_while", "Coq_stat_with", "Coq_stat_throw", "Coq_stat_return", "Coq_stat_break", "Coq_stat_continue", "Coq_stat_try", "Coq_stat_for", "Coq_stat_for_var", "Coq_stat_for_in", "Coq_stat_for_in_var", "Coq_stat_debugger", "Coq_stat_switch", "Coq_switchbody_nodefault", "Coq_switchbody_withdefault", "Coq_switchclause_intro", "Coq_prog_intro", "Coq_element_stat", "Coq_element_func_decl" ]);
+}
+
+function interp_val_is_state(v) {
+ // Assume "has a state_object_heap" field iff "is a state"
+ return v.state_object_heap !== undefined;
+}
+
+function interp_val_is_execution_ctx(v) {
+ // Assume "has a execution_ctx_lexical_env" field iff "is a state"
+ return v.execution_ctx_lexical_env !== undefined;
+}
+
+
+function show_interp_val(state, v, target, depth) {
+ if (depth == 0) {
+ t.append("< ... >");
+ }
+ var t = $("#" + target);
+ if (interp_val_is_base_value(v)) {
+ t.append(html_escape("" + v));
+ } else if (interp_val_is_js_value(v)) {
+ show_value(state, v, target, 1);
+ } else if (interp_val_is_loc(v)) {
+ show_object(state, v, target, 1);
+ } else if (interp_val_is_js_prim(v)) {
+ t.append(string_of_prim(v));
+ } else if (interp_val_is_state(v)) {
+ t.append("< state-object >");
+ } else if (interp_val_is_execution_ctx(v)) {
+ t.append("< execution-ctx-object >");
+ } else if (interp_val_is_syntax(v)) {
+ t.append("< syntax-object >");
+ } else if (interp_val_is_list(v)) {
+ var items = encoded_list_to_array(v)
+ t.append("List:");
+ for (var i = 0; i < items.length; i++) {
+ var vi = items[i];
+ var targetsub = fresh_id();
+ t.append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
+ $("#" + targetsub).html("• ");
+ show_interp_val(state, vi, targetsub, depth-1);
+ }
+ } else if (v.tag !== undefined) { // data constructor
+ var constr = html_escape(v.tag); // TODO: rename constructor prefix
+ var hasArgs = (function() {
+ for (var key in v) {
+ if (key !== "tag") {
+ return true;
+ }
+ }
+ return false;
+ })();
+ t.append(constr + ((hasArgs) ? " with:" : ""));
+ for (var key in v) {
+ if (key !== "tag") {
+ var targetsub = fresh_id();
+ t.append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
+ $("#" + targetsub).html(html_escape(key) + ": ");
+ show_interp_val(state, v[key], targetsub, depth-1);
+ }
+ }
+ } else { // record
+ var items_target = fresh_id();
+ t.append("Struct with:");
+ for (var key in v) {
+ var targetsub = fresh_id();
+ t.append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
+ $("#" + targetsub).html(html_escape(key) + ": ");
+ show_interp_val(state, v[key], targetsub, depth-1);
+ }
+ }
+ // t.append(string_of_any(v));
+}
+
+function show_interp_ctx(state, ctx, target) {
+ var depth = 1000;
+ var t = $("#" + target);
+ var a = ctx_to_array(ctx);
+ for (var i = 0; i < a.length; i++) {
+ var key = a[i].key;
+ var val = a[i].val;
+ if (val.runs_type_expr !== undefined) // runs0
+ continue;
+ var targetsub = fresh_id();
+ t.append("<div style='margin-left:1em' id='" + targetsub + "'></div>");
+ $("#" + targetsub).html(html_escape(key) + ": ");
+ show_interp_val(state, val, targetsub, depth);
+ }
+}
+
+
// --------------- Debugging view ----------------
function htmlDiv(s) {
@@ -645,13 +768,15 @@ function ctxToHtml(ctx) {
var s = '';
var a = ctx_to_array(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;
+ var key = a[i].key;
+ var val = a[i].val;
+ // Uncomment next line for debug:
+ // s += "<div style='white-space: nowrap;'><b>" + b.key + "</b>: " + JSON.stringify(b.val) + "</div>";
+ if (key == "#RETURN_VALUE#" &&
+ val.value !== undefined &&
+ val.value.out !== undefined &&
+ val.value.out.res !== undefined) {
+ var res = 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
@@ -666,14 +791,15 @@ function ctxToHtml(ctx) {
return s;
}
-
function itemToHtml(item) {
var s = '';
s += htmlDiv("token: " + item.token + JSON.stringify(item.locByExt));
s += htmlDiv("type: " + item.type);
s += ctxToHtml(item.ctx);
s += htmlDiv("execution_ctx: " + item.type);
- s += JSON.stringify(item.execution_ctx);
+ // For debug, use:
+ // s += JSON.stringify(item.execution_ctx);
+
// s += htmlDiv("state: " + item.type);
// s += JSON.stringify(item.state);
return s;
@@ -737,7 +863,7 @@ function updateSelection() {
}
// interpreter ctx panel
- // updateContext("#disp_ctx", item.heap, item.ctx);
+ show_interp_ctx(item.state, item.ctx, "disp_ctx");
// interpreter code panel
// TEMPORARILY DISABLED BECAUSE ONLY SINGLE FILE TO TRACE
@@ -840,10 +966,10 @@ function assignExtraInfosInTrace() {
if (t.loc != undefined) {
last_loc = t.loc;
}
- } else if (binding.val.state_object_heap != undefined) {
+ } else if (interp_val_is_state(binding.val)) {
// assuming: 'is an state object' iff 'has a state_object_heap field'
last_state = binding.val;
- } else if (binding.val.execution_ctx_lexical_env != undefined) {
+ } else if (interp_val_is_execution_ctx(binding.val)) {
// assuming: 'is an execution_ctx' iff 'has a execution_ctx_lexical_env field'
last_execution_ctx = binding.val;
}
@@ -930,6 +1056,7 @@ function testLineof(filename, token) {
// for easy debugging, launch at startup:
readSourceParseAndRun();
+stepTo(3772);
function showCurrent() {
--
GitLab