Nicer handling of eval, closer to ES6.

Author: tilk

coq/JsCorrectness.v

@@ -3165,9 +3165,11 @@ Proof.
       M vthis = o ->
       red_expr S0 C (expr_call_5 l is_eval_direct vs (out_ter S3 vthis)) o).
     clear HR S o. introv HR. subst M.
-    case_if.
-      subst. applys red_expr_call_5_eval. applys* run_eval_correct.
-      applys* red_expr_call_5_not_eval. apply* IH.
+    case_if as a.
+      destruct a as (a1&a2). apply bool_eq_true in a2. rewrite a2. subst_hyp a1.
+        applys red_expr_call_5_eval. applys* run_eval_correct.
+      applys* red_expr_call_5_not_eval. rew_logic in *. rew_reflect. eassumption.
+        apply* IH.
     clear EQM.
   subst. destruct rv; tryfalse.
     applys* red_expr_call_4_not_ref.
@@ -4991,7 +4993,8 @@ Proof.
   (* prealloc_global *)
   discriminate.
   (* prealloc_global_eval *)
-  discriminate.
+  apply red_spec_call_prealloc_global_eval.
+  applys* run_eval_correct.
   (* prealloc_global_parse_int *)
   discriminate.
   (* prealloc_global_parse_float *)

coq/JsInterpreter.v

@@ -2083,8 +2083,8 @@ Definition run_expr_call runs S C e1 e2s : result :=
           *)
           ifb (is_callable S3 l) then
             'let follow := fun vthis =>
-              ifb l = prealloc_global_eval then
-                run_eval runs S3 C is_eval_direct vs
+              ifb l = prealloc_global_eval /\ is_eval_direct then
+                run_eval runs S3 C true vs
               else runs_type_call runs S3 C l vthis vs in
             match rv with
             | resvalue_value v => follow undef
@@ -2638,6 +2638,9 @@ Definition run_array_join_elements runs S C l (k length : int) (sep : string) sR
 Definition run_call_prealloc runs S C B vthis (args : list value) : result :=
   match B with
 
+  | prealloc_global_eval =>
+     run_eval runs S C false args
+
   | prealloc_global_is_nan =>
     'let v := get_arg 0 args in
     if_number (to_number runs S C v) (fun S0 n =>

coq/JsPrettyRules.v

@@ -1050,12 +1050,12 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
       red_expr S C (expr_call_5  l is_eval_direct vs (out_ter S undef)) o ->
       red_expr S C (expr_call_4 (resvalue_value v) l is_eval_direct vs) o
 
-  | red_expr_call_5_eval : forall S0 S C is_eval_direct vs v o, (* Step 8, special for eval *)
-      red_expr S C (spec_call_global_eval is_eval_direct vs) o ->
-      red_expr S0 C (expr_call_5 prealloc_global_eval is_eval_direct vs (out_ter S v)) o
+  | red_expr_call_5_eval : forall S0 S C vs v o, (* Step 8, special for eval *)
+      red_expr S C (spec_call_global_eval true vs) o ->
+      red_expr S0 C (expr_call_5 prealloc_global_eval true vs (out_ter S v)) o
 
    | red_expr_call_5_not_eval : forall S0 S C l is_eval_direct vs v o, (* Step 8 *)
-      l <> prealloc_global_eval ->
+      l <> prealloc_global_eval \/ !is_eval_direct ->
       red_expr S C (spec_call l v vs) o ->
       red_expr S0 C (expr_call_5 l is_eval_direct vs (out_ter S v)) o
 
@@ -3278,6 +3278,12 @@ with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=
 (*------------------------------------------------------------*)
 (** ** Global object builtin functions (15.1) *)
 
+  (** Calling eval as a function *)
+
+  | red_spec_call_prealloc_global_eval : forall S C o vthis args,
+      red_expr S C (spec_call_global_eval false args) o ->
+      red_expr S C (spec_call_prealloc prealloc_global_eval vthis args) o
+
   (** Eval (returns value)  (15.1.2) *)
 
   | red_spec_call_global_eval : forall S C bdirect args v o,