diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 57f86177df749df23f6f531f1f8a5390eb9ca48d..a2639a1e1aeae8d19e58c2bae2dbeadaf539e4c2 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -660,7 +660,7 @@ and js_of_expression ctx dest e =
let binders = List.mapi bind el in
let ids = List.map fst binders in
let sdecl = ppf_match_binders binders in
- (ids, sdecl)
+ (ids, sintro ^ sdecl)
| [ { vb_pat = { pat_desc = Tpat_record (args, closed_flag) }; vb_expr = obj } ] -> (* binding records *)
(* args : (Longident.t loc * label_description * pattern) list *)
let (sintro, seobj) = js_of_expression_naming_argument_if_non_variable ctx obj "_record_arg_" in
@@ -676,7 +676,7 @@ and js_of_expression ctx dest e =
let binders = List.map bind args in
let ids = List.map fst binders in
let sdecl = ppf_match_binders binders in
- (ids, sdecl)
+ (ids, sintro ^ sdecl)
| _ -> (* other cases *)
let (ids,sdecls) = List.split (List.map (fun vb -> show_value_binding ctx vb) @@ vb_l) in
let sdecl = String.concat lin1 @@ sdecls in
@@ -993,92 +993,3 @@ let to_javascript basename module_name typedtree =
Format.flush_str_formatter ()
-(****************************************************************)
-(* COMMENTS *)
-
-(*
-ctx_empty
-ctx_push(ctx, bindings) where bindings = [ { key: "ls", val: ls}, { key:"xs", val:xs } ]
-
-push("ls", ls, push("v", v, push("y", y, ctx314));
-
-example:
- ctx321 = ctx_push(ctx320, bindings); log(|line|, ctx321, "ctx_push")
-
-
- enter (or call) => arguments of the call + name of new ctx
- return (was exit) => return value
- let (on the "in") => new binding + name of new ctx
- case => bound variables + name of new ctx
-
-
-
-
-
-
-
- type token_info = ctx_operation * current ctx
-
-
- if ==> viewed as match with case true/false.
-
-
-ctx_empty is passed on each structure_item
-on each ctx extension, we need a fresh name (enter, let, match_branch)
-(for return values, do the extension on the fly)
-
-
- return f(x);
-translates as
- var v213 = f(x);
- log(|line|, ctx_push(ctx320, {key: "return", val: v213}), "return")
-
-
-
- match v with | None -> x | Some y -> y
-translates as
- function() {
-
-
-
-----------------------
- let f ... =
- match ...
-
-=>
- switch
- case:
- return;
-
-----------------------
- let f ... =
- match .. ->
- match ...
-
-=>
- return
-
-----------------------
- let x = match ... in ...
-=>
- switch ...
- case:
- x = ..; break;
- case:
- x = ..; break;
-
-
-----------------------
- let x =
- match .. ->
- match .. ->
-=>
- would not work without wrapping
-
-----------------------
-
- f (match ...)
-=>
- requires A-normalization
-
-*)
diff --git a/generator/stdlib_ml/stdlib.js b/generator/stdlib_ml/stdlib.js
index 5e3f1e1718a43c5fcb72ebc497bf6fd1c338c309..b1eba5d9016b6ca3b4a6a0e0c6976c51905a6a6a 100644
--- a/generator/stdlib_ml/stdlib.js
+++ b/generator/stdlib_ml/stdlib.js
@@ -60,7 +60,12 @@ var of_int = function(x) { return x; };
//----------------------------------------------------------------------------
-var number_comparable = function(x, y) { return x === y; };
+var number_comparable = function(x, y) {
+ if (typeof(x) != "number" || typeof(y) != "number")
+ throw "string_eq invalid arguments";
+ return x === y;
+};
+
//----------------------------------------------------------------------------
@@ -71,13 +76,29 @@ var not = function(x) { return !x; };
//----------------------------------------------------------------------------
-var string_eq = function(x, y) { return x === y; };
+var string_eq = function(x, y) {
+ if (typeof(x) != "string" || typeof(y) != "string")
+ throw "string_eq invalid arguments";
+ return x === y;
+};
-var strappend = function(x, y) { return x + y; };
+var strappend = function(x, y) {
+ if (typeof(x) != "string" || typeof(y) != "string")
+ throw "strappend invalid arguments";
+ return x + y;
+};
-var strlength = function(x) { return x.length; };
+var strlength = function(x) {
+ if (typeof(x) != "string")
+ throw "strlength invalid arguments";
+ return x.length;
+};
-var substring = function(n, m, s) { return s.slice(n, n+m); };
+var substring = function(n, m, s) {
+ if (typeof(s) != "string")
+ throw "strlength invalid arguments";
+ return s.slice(n, n+m);
+};
//----------------------------------------------------------------------------
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 2e8f9182ef3cc23154f213aea2a9fb3fe4ca6ba4..a113b07da931c443a3404b7f0938afda5b7bf0d7 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -18,9 +18,6 @@ open LibString
open LibTactics
open List0
open Shared
-(*open String0*)
-let append x y = strappend x y (* hack for compatibility, to do cleanup *)
-let length x = strlength x (* hack for compatibility, to do cleanup *)
@@ -1939,221 +1936,221 @@ let run_construct_prealloc runs0 s c b args =
match b with
| Coq_prealloc_global ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_eval ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_parse_int ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_parse_float ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_is_finite ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_is_nan ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_decode_uri ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_decode_uri_component ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_encode_uri ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_global_encode_uri_component ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object ->
let_binding (get_arg 0 args) (fun v -> call_object_new s v)
| Coq_prealloc_object_get_proto_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_get_own_prop_descriptor ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_get_own_prop_name ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_create ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_define_prop ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_define_props ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_seal ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_freeze ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_prevent_extensions ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_is_sealed ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_is_frozen ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_is_extensible ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_keys ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_keys_call ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto_value_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto_has_own_prop ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto_is_prototype_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_object_proto_prop_is_enumerable ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function_proto_apply ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function_proto_call ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_function_proto_bind ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_bool ->
result_out
@@ -2171,21 +2168,21 @@ let run_construct_prealloc runs0 s c b args =
Coq_out_ter (s', (res_val (Coq_value_object l)))))))))
| Coq_prealloc_bool_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_bool_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_bool_proto_value_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number ->
let_binding (fun s' v ->
@@ -2204,39 +2201,39 @@ let run_construct_prealloc runs0 s c b args =
follow x (Coq_value_prim (Coq_prim_number x0)))))
| Coq_prealloc_number_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number_proto_value_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number_proto_to_fixed ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number_proto_to_exponential ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_number_proto_to_precision ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array ->
let_binding
@@ -2324,39 +2321,39 @@ let run_construct_prealloc runs0 s c b args =
(fun s1 -> res_ter s1 (res_val (Coq_value_object l)))))))))
| Coq_prealloc_array_is_array ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array_proto_join ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array_proto_pop ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_array_proto_push ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_string ->
let_binding
@@ -2388,57 +2385,57 @@ let run_construct_prealloc runs0 s c b args =
follow s0 s1))))))
| Coq_prealloc_string_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_string_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_string_proto_value_of ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_string_proto_char_at ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_string_proto_char_code_at ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_math ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_mathop m ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_date ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_regexp ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_error ->
let_binding (get_arg 0 args) (fun v ->
@@ -2446,9 +2443,9 @@ let run_construct_prealloc runs0 s c b args =
Coq_prealloc_error_proto)) v)
| Coq_prealloc_error_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_native_error ne ->
let_binding (get_arg 0 args) (fun v ->
@@ -2456,27 +2453,27 @@ let run_construct_prealloc runs0 s c b args =
(Coq_prealloc_native_error_proto ne))) v)
| Coq_prealloc_native_error_proto n ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_error_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_throw_type_error ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
| Coq_prealloc_json ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Construct prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented.")))
(** val run_construct_default :
@@ -2712,8 +2709,8 @@ let rec binding_inst_function_decls runs0 s c l fds str bconfig =
let make_arg_getter runs0 s c x x0 =
let xbd =
- append ("return ")
- (append x (";"))
+ strappend ("return ")
+ (strappend x (";"))
in
let bd = Coq_funcbody_intro ((Coq_prog_intro (true, ((Coq_element_stat
(Coq_stat_return (Some (Coq_expr_identifier x)))) :: []))), xbd)
@@ -2724,9 +2721,9 @@ let make_arg_getter runs0 s c x x0 =
runs_type -> state -> execution_ctx -> prop_name -> lexical_env -> result **)
let make_arg_setter runs0 s c x x0 =
- let xparam = append x ("_arg") in
+ let xparam = strappend x ("_arg") in
let xbd =
- append x (append (" = ") (append xparam ";"))
+ strappend x (strappend (" = ") (strappend xparam ";"))
in
let bd = Coq_funcbody_intro ((Coq_prog_intro (true, ((Coq_element_stat
(Coq_stat_expr (Coq_expr_assign ((Coq_expr_identifier x), None,
@@ -3451,7 +3448,7 @@ let run_binary_op runs0 s c op v1 v2 =
(Coq_value_prim w2)) (fun s2 ss ->
let (s3, s4) = ss in
res_out (Coq_out_ter (s2,
- (res_val (Coq_value_prim (Coq_prim_string (append s3 s4)))))))
+ (res_val (Coq_value_prim (Coq_prim_string (strappend s3 s4)))))))
else if_spec
(convert_twice_number runs0 s1 c (Coq_value_prim w1)
(Coq_value_prim w2)) (fun s2 nn ->
@@ -5007,10 +5004,10 @@ let valueToStringForJoin runs0 s c l k =
let run_array_join_elements runs0 s c l k length0 sep sR =
if k < length0
- then let_binding (append sR sep) (fun ss ->
+ then let_binding (strappend sR sep) (fun ss ->
let_binding (valueToStringForJoin runs0 s c l k) (fun sE ->
if_spec sE (fun s0 element ->
- let_binding (append ss element) (fun sR0 ->
+ let_binding (strappend ss element) (fun sR0 ->
runs0.runs_type_array_join_elements s0 c l (k +. 1.)
length0 sep sR0))))
else res_ter s (res_val (Coq_value_prim (Coq_prim_string sR)))
@@ -5023,27 +5020,27 @@ let run_call_prealloc runs0 s c b vthis args =
match b with
| Coq_prealloc_global ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_eval ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_parse_int ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_parse_float ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_is_finite ->
let_binding (get_arg 0 args) (fun v ->
@@ -5062,27 +5059,27 @@ let run_call_prealloc runs0 s c b vthis args =
(number_comparable n JsNumber.nan))))))
| Coq_prealloc_global_decode_uri ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_decode_uri_component ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_encode_uri ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_global_encode_uri_component ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object ->
let_binding (get_arg 0 args) (fun value0 ->
@@ -5113,15 +5110,15 @@ let run_call_prealloc runs0 s c b vthis args =
from_prop_descriptor runs0 s2 c d)))
| Coq_prealloc_object_get_own_prop_name ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_create ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_define_prop ->
let_binding (get_arg 0 args) (fun o ->
@@ -5137,9 +5134,9 @@ let run_call_prealloc runs0 s c b vthis args =
(fun s3 x -> res_ter s3 (res_val (Coq_value_object l))))))))
| Coq_prealloc_object_define_props ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_seal ->
let_binding (get_arg 0 args) (fun v ->
@@ -5187,21 +5184,21 @@ let run_call_prealloc runs0 s c b vthis args =
res_ter s (res_val (Coq_value_prim (Coq_prim_bool r)))))
| Coq_prealloc_object_keys ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_keys_call ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_object_proto_to_string ->
(match vthis with
@@ -5220,33 +5217,33 @@ let run_call_prealloc runs0 s c b vthis args =
if_some (run_object_method object_class_ s1 l) (fun s0 ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_string
- (append
+ (strappend
("[object ")
- (append s0 ("]"))))))))
+ (strappend s0 ("]"))))))))
| Coq_prim_number n ->
if_object (to_object s vthis) (fun s1 l ->
if_some (run_object_method object_class_ s1 l) (fun s0 ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_string
- (append
+ (strappend
("[object ")
- (append s0 ("]"))))))))
+ (strappend s0 ("]"))))))))
| Coq_prim_string s0 ->
if_object (to_object s vthis) (fun s1 l ->
if_some (run_object_method object_class_ s1 l) (fun s2 ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_string
- (append
+ (strappend
("[object ")
- (append s2 ("]")))))))))
+ (strappend s2 ("]")))))))))
| Coq_value_object o ->
if_object (to_object s vthis) (fun s1 l ->
if_some (run_object_method object_class_ s1 l) (fun s0 ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_string
- (append
+ (strappend
("[object ")
- (append s0 ("]")))))))))
+ (strappend s0 ("]")))))))))
| Coq_prealloc_object_proto_value_of -> to_object s vthis
| Coq_prealloc_object_proto_has_own_prop ->
let_binding (get_arg 0 args) (fun v ->
@@ -5281,9 +5278,9 @@ let run_call_prealloc runs0 s c b vthis args =
(attributes_enumerable a))))))))
| Coq_prealloc_function ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_function_proto ->
result_out (Coq_out_ter (s, (res_val (Coq_value_prim Coq_prim_undef))))
@@ -5437,9 +5434,9 @@ let run_call_prealloc runs0 s c b vthis args =
(convert_value_to_boolean v)))))))
| Coq_prealloc_bool_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_bool_proto_to_string ->
(match vthis with
@@ -5519,15 +5516,15 @@ let run_call_prealloc runs0 s c b vthis args =
else let v = get_arg 0 args in to_number runs0 s c v
| Coq_prealloc_number_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_number_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_number_proto_value_of ->
(match vthis with
@@ -5563,21 +5560,21 @@ let run_call_prealloc runs0 s c b vthis args =
else run_error s Coq_native_error_type))
| Coq_prealloc_number_proto_to_fixed ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_number_proto_to_exponential ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_number_proto_to_precision ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_array ->
run_construct_prealloc runs0 s c Coq_prealloc_array args
@@ -5593,9 +5590,9 @@ let run_call_prealloc runs0 s c b vthis args =
else res_ter s (res_val (Coq_value_prim (Coq_prim_bool false)))))
| Coq_prealloc_array_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_array_proto_to_string ->
if_object (to_object s vthis) (fun s0 array ->
@@ -5676,9 +5673,9 @@ let run_call_prealloc runs0 s c b vthis args =
res_ter s0 (res_val (Coq_value_prim (Coq_prim_string s1)))))
| Coq_prealloc_string_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_string_proto_to_string ->
(match vthis with
@@ -5704,39 +5701,39 @@ let run_call_prealloc runs0 s c b vthis args =
else run_error s Coq_native_error_type))
| Coq_prealloc_string_proto_char_at ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_string_proto_char_code_at ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_math ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_mathop m ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_date ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_regexp ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_error ->
let_binding (get_arg 0 args) (fun v ->
@@ -5744,9 +5741,9 @@ let run_call_prealloc runs0 s c b vthis args =
Coq_prealloc_error_proto)) v)
| Coq_prealloc_error_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_native_error ne ->
let_binding (get_arg 0 args) (fun v ->
@@ -5754,22 +5751,22 @@ let run_call_prealloc runs0 s c b vthis args =
(Coq_prealloc_native_error_proto ne))) v)
| Coq_prealloc_native_error_proto n ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_error_proto_to_string ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_throw_type_error -> run_error s Coq_native_error_type
| Coq_prealloc_json ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
- (append
+ (strappend
("Call prealloc_")
- (append (string_of_prealloc b)
+ (strappend (string_of_prealloc b)
(" not yet implemented")))
(** val run_call :
diff --git a/navig-driver.js b/navig-driver.js
index dec8e080a2ef3fc1c8336e8a198c60fcc01fd9c9..7fb1d8dbcc35ea54d587123b60b6489d5a085c4f 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -80,7 +80,7 @@ var source_file = '{}';
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;})()';
// --------------- Initialization ----------------
@@ -360,6 +360,32 @@ function html_escape(stringToEncode) {
// --------------- Views for JS state/context ----------------
+function array_of_heap(heap) {
+ var items_list = Heap.to_list(LibString.string_comparable, heap);
+ return encoded_list_to_array(items_list);
+}
+
+
+function string_of_prealloc(prealloc) {
+ return (prealloc.tag).slice("Coq_prealloc_".length);
+ //TODO:
+ // Coq_prealloc_mathop [@f mathop] of mathop
+ // Coq_prealloc_native_error [@f error] of native_error
+ // Coq_prealloc_native_error_proto [@f error] of native_error
+}
+
+function string_of_loc(loc) {
+ switch (loc.tag) {
+ case "Coq_object_loc_normal":
+ return loc.address;
+ case "Coq_object_loc_prealloc":
+ return string_of_prealloc(loc.prealloc);
+ default:
+ throw "unrecognized tag in string_of_loc";
+ }
+}
+
+
function string_of_default(v) {
return "<pre style='margin:0; padding: 0; margin-left:1em'>" + JSON.stringify(v, null, 2) + "</pre>";
}
@@ -441,15 +467,17 @@ function string_of_mutability(mutability) {
attributes_accessor_configurable : bool }
*/
-
function show_object(state, loc, target, depth) {
var t = $("#" + target);
+ if (depth == 0) {
+ t.append("<hidden>");
+ return;
+ }
var obj_opt = JsCommonAux.object_binds_pickable_option(state, loc);
if (obj_opt.tag != "Some") throw "show_object: unbound object";
var obj = obj_opt.value;
var props = obj.object_properties_;
- var key_value_pair_list = Heap.to_list(string_comparable, props);
- var key_value_pair_array = encoded_list_to_array(key_value_pair_list);
+ var key_value_pair_array = array_of_heap(props);
for (var i = 0; i < key_value_pair_array.length; i++) {
var prop_name = key_value_pair_array[i][0];
var attribute = key_value_pair_array[i][1];
@@ -461,13 +489,13 @@ function show_object(state, loc, target, depth) {
switch (attribute.tag) {
case "Coq_attributes_data_of":
var attr = attribute.value;
- var prop_value = attribute.attributes_data_value;
+ var prop_value = attr.attributes_data_value;
show_value(state, prop_value, targetsub, depth-1);
break;
case "Coq_attributes_accessor_of":
var attr = attribute.value;
- $("#" + targetsub).append(" <accessor> ");
+ $("#" + targetsub).append(" <accessor> ");
// TODO: complete
break;
@@ -482,7 +510,6 @@ function show_object(state, loc, target, depth) {
}
}
-
function show_value(state, v, target, depth) {
var t = $("#" + target);
switch (v.tag) {
@@ -493,7 +520,7 @@ function show_value(state, v, target, depth) {
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>(" + loc + ")</a></span>";
+ 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;
function handler_close() {
handlers[target] = handler_open;
@@ -517,28 +544,27 @@ function show_value(state, v, target, depth) {
}
}
-function show_lexical_env(state, env_record_decl, items_target) {
+function show_decl_env_record(state, env_record_decl, target) {
// env_record_decl : (string, mutability * value) Heap.heap
var t = $("#" + target);
- var items_list = Heap.to_list(string_comparable, env_record_decl);
- var items_array = encoded_list_to_array(items_list);
+ 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];
var mutability = items_array[i][1][0];
var value = items_array[i][1][1];
var value_target = fresh_id();
- t.append("<div id='" + value_target + "'>" + html_escape(varname) + " (" + string_of_mutability(mutability) + "):</div>");
+ t.append("<div id='" + value_target + "'>" + html_escape(var_name) + " (" + string_of_mutability(mutability) + "):</div>");
show_value(state, value, value_target, 1);
}
}
function show_lexical_env(state, lexical_env, target) {
var t = $("#" + target);
- var env_record_heap = state.state_env_record_heap;
+ // var env_record_heap = state.state_env_record_heap;
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.object_binds_pickable_option(env_record_heap, env_loc);
+ 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;
@@ -550,12 +576,11 @@ function show_lexical_env(state, lexical_env, target) {
show_decl_env_record(state, env_record_decl, items_target)
break;
case "Coq_env_record_object":
- var env_record_object = env_record.value;
- var object_loc = env_record_object.value;
- var provide_this = env_record_object.provide_this;
+ var object_loc = env_record.value;
+ var provide_this = env_record.provide_this;
var obj_target = fresh_id();
t.append("with (" + ((provide_this) ? "" : "not ") + "providing 'this'): <div id='" + obj_target + "'></div>");
- show_value(state, object_loc, obj_target, 0);
+ show_object(state, object_loc, obj_target, 0);
break;
default:
@@ -574,15 +599,18 @@ function show_execution_ctx(state, execution_ctx, target) {
// this object
var this_target = fresh_id();
t.append("<div id='" + this_target + "'>this: </div>");
+ //TODO
show_value(state, execution_ctx.execution_ctx_this_binding, this_target, 0);
// lexical env
var lexical_env_target = fresh_id();
t.append("<div><div>lexical-env:</div> <div style='margin-left:0.5em' id='" + lexical_env_target + "'></div></div>");
show_lexical_env(state, execution_ctx.execution_ctx_lexical_env, lexical_env_target);
-
+
// variable env -- TODO, like above
- // execution_ctx.execution_ctx_variable_env
+ var variable_env_target = fresh_id();
+ t.append("<div><div>variable-env:</div> <div style='margin-left:0.5em' id='" + variable_env_target + "'></div></div>");
+ show_lexical_env(state, execution_ctx.execution_ctx_variable_env, variable_env_target);
}
@@ -629,6 +657,10 @@ function itemToHtml(item) {
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);
+ // s += htmlDiv("state: " + item.type);
+ // s += JSON.stringify(item.state);
return s;
}
@@ -681,7 +713,7 @@ function updateSelection() {
$("#disp_env").html("<undefined state or context>");
} else {
$("#disp_env").html("");
- // show_execution_ctx(item.state, item.execution_ctx, "disp_env");
+ show_execution_ctx(item.state, item.execution_ctx, "disp_env");
}
// interpreter ctx panel
@@ -780,6 +812,9 @@ function assignExtraInfosInTrace() {
var bindings = item.ctx.bindings;
for (var i = 0; i < bindings.length; i++) {
var binding = bindings[i];
+ if (binding.val === undefined) {
+ continue; // might happen on run with errors
+ }
if (binding.key === "_term_") {
var t = binding.val;
if (t.loc != undefined) {