diff --git a/generator/Makefile b/generator/Makefile
index 5d917ef0fbd76d8f054d6573a30353af4223ecad..241fabee9e99322356e32eeb0a8355f7d46fb157 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -47,7 +47,6 @@ ASSEMBLY_JS_FILES := \
JsSyntax.unlog.js \
JsSyntaxAux.unlog.js \
Translate_syntax.js \
- JsSyntaxInfos.unlog.js \
JsCommon.unlog.js \
JsCommonAux.unlog.js \
JsPreliminary.unlog.js \
diff --git a/generator/TODO b/generator/TODO
index 2dc8f3a93030e487a205f33c48b11b838d9c2dff..d03fb727451661cd67888d1a9651129cd7f67639 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -18,8 +18,8 @@ CURRENT TODO
*) Arthur: inline let_binding
-*) Alan/Thomas: test "eval", might need pieces of JsCommon for it (parsePickable)
-
+*) Alan/Thomas: test "eval"
+ Still need to implement parsing with a given strictness
*) ?
update the ML code for: type_compare mutability_compare prim_compare
@@ -35,7 +35,7 @@ CURRENT TODO
*) [thomas]
- bigger test262 testing.
-- Flat to force esprima to parse in strict mode
+- Flag to force esprima to parse in strict mode
*) LATER: remove useless files such as LibReflect LibString etc...
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index b36efa4032d65c794a7e601048e7de61791accb7..da300106cb3833eba62ba9fb7f5e3ffbde609609 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -582,11 +582,8 @@ let elision_tail_remove ol =
(** val parse_pickable : string -> bool -> prog coq_Pickable_option **)
let parse_pickable = (fun s strict ->
- let str = s in
- (* try ARTHUR HACK *)
- let parserExp = Translate_syntax.Parser_main.exp_from_string ~force_strict:strict str in
- Some (JsSyntaxInfos.add_infos_prog strict
- (Translate_syntax.exp_to_prog parserExp))
+ Translate_syntax.parse_esprima strict s
+ (*Translate_syntax.parse_esprima strict s*)
(* with
(* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
| Parser.ParserFailure _ [@f] (** Auto Generated Attributes **)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 9172f29356edd2cd2f5e7059eb0389da69918622..fc2f6f0157d4fdd96867b91517ffbbd3862b689a 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -7,7 +7,6 @@ open JsInterpreterMonads
open JsPreliminary
open JsSyntax
open JsSyntaxAux
-open JsSyntaxInfos
open LibBool
open LibFunc
open LibList
@@ -4576,8 +4575,7 @@ and run_call s c l vthis args =
(** val run_javascript : prog -> result **)
and run_javascript p =
- let p_2 = add_infos_prog strictness_false p in
- let c = execution_ctx_initial (prog_intro_strictness p_2) in
+ let c = execution_ctx_initial (prog_intro_strictness p) in
if_void
(execution_ctx_binding_inst state_initial c Coq_codetype_global
- None p_2 []) (fun s_2 -> run_prog s_2 c p_2)
+ None p []) (fun s_2 -> run_prog s_2 c p)
diff --git a/generator/tests/jsref/JsSyntaxInfos.ml b/generator/tests/jsref/JsSyntaxInfos.ml
deleted file mode 100644
index fd1aaaeb590603bb8d4dd13224150f28c307907e..0000000000000000000000000000000000000000
--- a/generator/tests/jsref/JsSyntaxInfos.ml
+++ /dev/null
@@ -1,117 +0,0 @@
-open JsSyntax
-open JsSyntaxAux
-open LibBool
-open List0
-
-
-(** val add_infos_exp : strictness_flag -> expr -> expr **)
-
-let rec add_infos_exp str e =
- let f e = add_infos_exp str e in
- (match e with
- | Coq_expr_this -> e
- | Coq_expr_identifier s -> e
- | Coq_expr_literal l -> e
- | Coq_expr_object l -> e
- | Coq_expr_array oes ->
- Coq_expr_array
- (map (fun oe ->
- match oe with
- | Some e0 -> Some (f e0)
- | None -> None) oes)
- | Coq_expr_function (so, ss, fb) ->
- Coq_expr_function (so, ss, (add_infos_funcbody str fb))
- | Coq_expr_access (e1, e2) -> Coq_expr_access ((f e1), (f e2))
- | Coq_expr_member (e0, s) -> Coq_expr_member ((f e0), s)
- | Coq_expr_new (e0, es) -> Coq_expr_new ((f e0), (map f es))
- | Coq_expr_call (e0, es) -> Coq_expr_call ((f e0), (map f es))
- | Coq_expr_unary_op (op, e0) -> Coq_expr_unary_op (op, (f e0))
- | Coq_expr_binary_op (e1, op, e2) ->
- Coq_expr_binary_op ((f e1), op, (f e2))
- | Coq_expr_conditional (e1, e2, e3) ->
- Coq_expr_conditional ((f e1), (f e2), (f e3))
- | Coq_expr_assign (e1, op, e2) -> Coq_expr_assign ((f e1), op, (f e2)))
-
-(** val add_infos_funcbody : strictness_flag -> funcbody -> funcbody **)
-
-and add_infos_funcbody str fb = match fb with
-| Coq_funcbody_intro (p, s) -> Coq_funcbody_intro ((add_infos_prog str p), s)
-
-(** val add_infos_stat : strictness_flag -> label_set -> stat -> stat **)
-
-and add_infos_stat str labs t =
- let opt f smth = match smth with
- | Some smth0 -> Some (f smth0)
- | None -> None
- in
- let f e = add_infos_stat str label_set_empty e in
- let fe e = add_infos_exp str e in
- let fsb e = add_infos_switchbody str e in
- (match t with
- | Coq_stat_expr e -> Coq_stat_expr (fe e)
- | Coq_stat_label (l, t0) ->
- Coq_stat_label (l,
- (add_infos_stat str (label_set_add (Coq_label_string l) labs) t0))
- | Coq_stat_block ts -> Coq_stat_block (map f ts)
- | Coq_stat_var_decl vars ->
- Coq_stat_var_decl
- (map (fun x -> let (s, eo) = x in (s, (opt fe eo))) vars)
- | Coq_stat_if (e, t0, to0) -> Coq_stat_if ((fe e), (f t0), (opt f to0))
- | Coq_stat_do_while (l, t0, e) ->
- Coq_stat_do_while ((label_set_add_empty labs), (f t0), (fe e))
- | Coq_stat_while (l, e, t0) ->
- Coq_stat_while ((label_set_add_empty labs), (fe e), (f t0))
- | Coq_stat_with (e, t0) -> Coq_stat_with ((fe e), (f t0))
- | Coq_stat_throw e -> Coq_stat_throw (fe e)
- | Coq_stat_return eo -> Coq_stat_return (opt fe eo)
- | Coq_stat_break lopt -> Coq_stat_break lopt
- | Coq_stat_continue lopt -> Coq_stat_continue lopt
- | Coq_stat_try (t0, catch_stat, to0) ->
- Coq_stat_try ((f t0),
- (opt (fun c -> let (cs, t1) = c in (cs, (f t1))) catch_stat), (opt f to0))
- | Coq_stat_for (l, eo1, eo2, eo3, t0) ->
- Coq_stat_for ((label_set_add_empty labs), (opt fe eo1), (opt fe eo2),
- (opt fe eo3), (f t0))
- | Coq_stat_for_var (l, vars, eo2, eo3, t0) ->
- Coq_stat_for_var ((label_set_add_empty labs),
- (map (fun x -> let (s, eo) = x in (s, (opt fe eo))) vars), (opt fe eo2),
- (opt fe eo3), (f t0))
- | Coq_stat_for_in (l, e1, e2, t0) ->
- Coq_stat_for_in ((label_set_add_empty labs), (fe e1), (fe e2), (f t0))
- | Coq_stat_for_in_var (l, str0, eo, e, t0) ->
- Coq_stat_for_in_var ((label_set_add_empty labs), str0, (opt fe eo),
- (fe e), (f t0))
- | Coq_stat_debugger -> Coq_stat_debugger
- | Coq_stat_switch (labs0, e, ts) ->
- Coq_stat_switch ((label_set_add_empty labs0), (fe e), (fsb ts)))
-
-(** val add_infos_switchbody :
- strictness_flag -> switchbody -> switchbody **)
-
-and add_infos_switchbody str ts =
- let fe e = add_infos_exp str e in
- let fs e = add_infos_stat str label_set_empty e in
- let f sc = match sc with
- | Coq_switchclause_intro (e, l) ->
- Coq_switchclause_intro ((fe e), (map fs l))
- in
- (match ts with
- | Coq_switchbody_nodefault l -> Coq_switchbody_nodefault (map f l)
- | Coq_switchbody_withdefault (l1, s, l2) ->
- Coq_switchbody_withdefault ((map f l1), (map fs s), (map f l2)))
-
-(** val add_infos_prog : strictness_flag -> prog -> prog **)
-
-and add_infos_prog str p = match p with
-| Coq_prog_intro (str', els) ->
- let str'' = coq_or str str' in
- Coq_prog_intro (str'', (map (fun e -> add_infos_element str'' e) els))
-
-(** val add_infos_element : strictness_flag -> element -> element **)
-
-and add_infos_element str el = match el with
-| Coq_element_stat t ->
- Coq_element_stat (add_infos_stat str label_set_empty t)
-| Coq_element_func_decl (s, ss, fb) ->
- Coq_element_func_decl (s, ss, (add_infos_funcbody str fb))
-
diff --git a/generator/tests/jsref/Translate_syntax.js b/generator/tests/jsref/Translate_syntax.js
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..32f88b0d365bc9c8bfca162c6e42a53605e31441 100644
--- a/generator/tests/jsref/Translate_syntax.js
+++ b/generator/tests/jsref/Translate_syntax.js
@@ -0,0 +1,10 @@
+var Translate_syntax = {
+ parse_esprima: function (strictness, src) {
+ try {
+ // TODO Fixup line numbers for eval context
+ return Some(esprimaToAST(esprima.parse(src, {loc: true, range: true}), src));
+ } catch (e) {
+ return None();
+ }
+ }
+};
diff --git a/generator/tests/jsref/Translate_syntax.mli b/generator/tests/jsref/Translate_syntax.mli
index 0566761ab9023fc602d433808690b4af9400bdee..c3e2a37b7a7c24897227c71bfaa35c7bfb8cb178 100644
--- a/generator/tests/jsref/Translate_syntax.mli
+++ b/generator/tests/jsref/Translate_syntax.mli
@@ -1,40 +1,2 @@
-
-module Parser_syntax : sig (* needed by translate_syntax.mli and by parser_main (below) *)
- type unary_op
- type arith_op
- type bin_op
- type exp
-end
-
-module Parser_main : sig
- val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp
-end
-
-
-
-exception CoqSyntaxDoesNotSupport of string
-exception Empty_list
-
-val string_to_coq : string -> char list
-
-val unary_op_to_coq : Parser_syntax.unary_op -> JsSyntax.unary_op
-val arith_op_to_coq : Parser_syntax.arith_op -> JsSyntax.binary_op
-val bin_op_to_coq : Parser_syntax.bin_op -> JsSyntax.binary_op
-
-val exp_to_literal : Parser_syntax.exp -> JsSyntax.literal
-
-val exp_to_exp : Parser_syntax.exp -> JsSyntax.expr
-val exp_to_stat : Parser_syntax.exp -> JsSyntax.stat
-val exp_to_prog : Parser_syntax.exp -> JsSyntax.prog
-val exp_to_elem : Parser_syntax.exp -> JsSyntax.element
-val exp_to_funcbody :
- Parser_syntax.exp -> JsSyntax.strictness_flag -> JsSyntax.funcbody
-
-val coq_syntax_from_file : ?init:bool -> string -> JsSyntax.prog
-val coq_syntax_from_string : string -> JsSyntax.prog
-val coq_syntax_from_main : string -> JsSyntax.prog
-
-(*
-module Translate_syntax : sig (* ARTHUR: to implement *)
-end
-*)
\ No newline at end of file
+(* parse_esprima strictness source *)
+val parse_esprima : bool -> string -> JsSyntax.prog option
diff --git a/navig-driver.js b/navig-driver.js
index 63b1dc1059e0326b84ceb8c8968c44508da76771..44f39a8580d6af49c746d338461c57bfa266cf53 100644
--- a/navig-driver.js
+++ b/navig-driver.js
@@ -85,6 +85,7 @@ var source_files = [
'var x = { a : { c: 1 } };\n x.a.b = 2;\nx',
'(function (x) {return 1;})()',
'(function (x) {\nreturn 1;\n})({a:{b:2}})',
+ 'eval("var x = { a : 1 }; x.b = 2; x");',
];
source_files.reduce((select, file_content) => {
@@ -1073,14 +1074,14 @@ function readSourceParseAndRun() {
//console.log(code);
// TODO handle parsing error
try {
- parsedTree = esprima.parse(code, {loc:true});
+ parsedTree = esprima.parse(code, {loc: true, range: true});
} catch (e) {
return "Parse error";
}
// console.log(parsedTree);
// TODO handle out of scope errors
- program = esprimaToAST(parsedTree);
+ program = esprimaToAST(parsedTree, code);
// console.log(program);
return run();
}