Simpler env_record_write_decl_env.

coq/JsCommon.v

@@ -871,13 +871,9 @@ Definition decl_env_record_rem Ed x : decl_env_record :=
 
 (** LATER: Change the following definition to a relation. *)
 
-Definition env_record_write_decl_env S L x mu v :=
-  match Heap.read (state_env_record_heap S) L with
-  | env_record_decl Ed =>
-     let env' := decl_env_record_write Ed x mu v in
-     env_record_write S L (env_record_decl env')
-  | env_record_object _ _ => S (* It should never happen *)
-  end.
+Definition env_record_write_decl_env S L Ed x mu v :=
+  env_record_write S L (env_record_decl 
+    (decl_env_record_write Ed x mu v)).
 
 
 (**************************************************************)
@@ -1219,7 +1215,6 @@ Inductive value_viewable_as : string -> state -> value -> prim -> Prop :=
 Definition is_syntactic_eval e :=
   match e with
   | expr_identifier s => decide (s = "eval")
-  | expr_literal (literal_string s) => decide (s = "eval")
   | _ => false
   end.
 

coq/JsCorrectness.v

@@ -2800,10 +2800,10 @@ Proof.
 Qed.
 
 
-Lemma binding_inst_function_decls_correct : forall runs S C args L fds str bconfig o,
+Lemma binding_inst_function_decls_correct : forall runs S C L fds str bconfig o,
   runs_type_correct runs ->
   binding_inst_function_decls runs S C L fds str bconfig = o ->
-  red_expr S C (spec_binding_inst_function_decls args L fds str bconfig) o.
+  red_expr S C (spec_binding_inst_function_decls L fds str bconfig) o.
 Proof.
   introv IH HR. gen S o. induction fds; introv HR.
   simpls. run_inv. applys* red_spec_binding_inst_function_decls_nil.
@@ -2813,7 +2813,7 @@ Proof.
   let_name as M. rename a into fd. rename l into fo.
   asserts M_correct: (forall S o,
       M S = o ->
-      red_expr S C (spec_binding_inst_function_decls_5 args L fd fds str fo bconfig) o).
+      red_expr S C (spec_binding_inst_function_decls_5 L fd fds str fo bconfig) o).
     clears HR S o. introv HR. subst M.
     subst fname. run red_spec_binding_inst_function_decls_5
       using env_record_set_mutable_binding_correct.
@@ -2981,12 +2981,12 @@ Proof.
     clear EQA. apply~ red_spec_create_arguments_object_4.
 Qed.
 
-Lemma binding_inst_arg_obj_correct : forall runs S C lf p xs args L o,
+Lemma binding_inst_arg_obj_correct : forall runs S C lf str xs args L o,
   runs_type_correct runs ->
-  binding_inst_arg_obj runs S C lf p xs args L = o ->
-  red_expr S C (spec_binding_inst_arg_obj lf p xs args L) o.
+  binding_inst_arg_obj runs S C lf xs args L str = o ->
+  red_expr S C (spec_binding_inst_arg_obj lf xs args L str) o.
 Proof.
-  introv IH HR. unfolds in HR. let_name.
+  introv IH HR. unfolds in HR.
   run~ red_spec_binding_inst_arg_obj using create_arguments_object_correct.
   cases_if.
    run red_spec_binding_inst_arg_obj_1_strict
@@ -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

@@ -878,7 +878,7 @@ Definition env_record_set_mutable_binding runs S C L x v str : result_void :=
       if_some (Heap.read_option Ed x) (fun rm =>
         let '(mu, v_old) := rm in
         ifb mutability_is_mutable mu then
-          res_void (env_record_write_decl_env S L x mu v)
+          res_void (env_record_write_decl_env S L Ed x mu v)
         else out_error_or_void S str native_error_type)
     | env_record_object l pt =>
       object_put runs S C l x v str
@@ -934,7 +934,7 @@ Definition env_record_create_mutable_binding runs S C L x (deletable_opt : optio
       ifb decl_env_record_indom Ed x then
         impossible_with_heap_because S "Already declared environnment record in [env_record_create_mutable_binding]."
       else
-        'let S' := env_record_write_decl_env S L x (mutability_of_bool deletable) undef in
+        'let S' := env_record_write_decl_env S L Ed x (mutability_of_bool deletable) undef in
         res_void S'
     | env_record_object l pt =>
       if_bool (object_has_prop runs S C l x) (fun S1 has =>
@@ -957,7 +957,7 @@ Definition env_record_create_immutable_binding S L x : result_void :=
       ifb decl_env_record_indom Ed x then
         impossible_with_heap_because S "Already declared environnment record in [env_record_create_immutable_binding]."
       else
-        res_void (env_record_write_decl_env S L x mutability_uninitialized_immutable undef)
+        res_void (env_record_write_decl_env S L Ed x mutability_uninitialized_immutable undef)
     | env_record_object _ _ =>
         impossible_with_heap_because S "[env_record_create_immutable_binding] received an environnment record object."
     end).
@@ -968,7 +968,7 @@ Definition env_record_initialize_immutable_binding S L x v : result_void :=
     | env_record_decl Ed =>
       if_some (pick_option (Heap.binds Ed x)) (fun evs =>
         ifb evs = (mutability_uninitialized_immutable, undef) then
-          'let S' := env_record_write_decl_env S L x mutability_immutable v in
+          'let S' := env_record_write_decl_env S L Ed x mutability_immutable v in
           res_void S'
         else
           impossible_with_heap_because S "Non suitable binding in [env_record_initialize_immutable_binding].")
@@ -1356,16 +1356,15 @@ Definition create_arguments_object runs S C lf xs args X str : result :=
         if_bool (object_define_own_prop runs S2 C l "callee" A false) (fun S3 b' =>
           res_ter S3 l)))).
 
-Definition binding_inst_arg_obj runs S C lf p xs args L : result_void :=
+Definition binding_inst_arg_obj runs S C lf xs args L str : result_void :=
   let arguments := "arguments" in
-  'let str := prog_intro_strictness p in
-    if_object (create_arguments_object runs S C lf xs args
-                   (execution_ctx_variable_env C) str) (fun S1 largs =>
-      if str then
-        if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
-          env_record_initialize_immutable_binding S2 L arguments largs)
-      else
-        env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
+  if_object (create_arguments_object runs S C lf xs args
+                 (execution_ctx_variable_env C) str) (fun S1 largs =>
+    if str then
+      if_void (env_record_create_immutable_binding S1 L arguments) (fun S2 =>
+        env_record_initialize_immutable_binding S2 L arguments largs)
+    else
+      env_record_create_set_mutable_binding runs S1 C L arguments None largs false).
 
 Fixpoint binding_inst_var_decls runs S C L (vds : list string) bconfig str : result_void :=
   match vds with
@@ -1396,7 +1395,7 @@ Definition execution_ctx_binding_inst runs S C (ct : codetype) (funco : option o
             in
           match ct, funco, bdefined with
           | codetype_func, Some func, false =>
-            if_void (binding_inst_arg_obj runs S2 C func p names args L) follow2
+            if_void (binding_inst_arg_obj runs S2 C func names args L str) follow2
           | codetype_func, _, false =>
             impossible_with_heap_because S2 "Weird `arguments' object in [execution_ctx_binding_inst]."
           | _, _, _ => follow2 S2
@@ -2083,8 +2082,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 +2637,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/JsPrettyInterm.v

@@ -336,17 +336,17 @@ Inductive ext_expr :=
   | spec_binding_inst_formal_params_2 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> out -> ext_expr
   | spec_binding_inst_formal_params_3 : list value -> env_loc -> string -> list string -> strictness_flag -> value -> ext_expr
   | spec_binding_inst_formal_params_4 : list value -> env_loc -> list string -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_function_decls :  list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
-  | spec_binding_inst_function_decls_1 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_2 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_3 : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_3a : list value -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
-  | spec_binding_inst_function_decls_4 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
-  | spec_binding_inst_function_decls_5 : list value -> env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
-  | spec_binding_inst_function_decls_6 : list value -> env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
-  | spec_binding_inst_arg_obj :   object_loc -> prog -> list string -> list value -> env_loc -> ext_expr
-  | spec_binding_inst_arg_obj_1 : prog -> env_loc -> strictness_flag -> out -> ext_expr
-  | spec_binding_inst_arg_obj_2 : prog -> env_loc -> object_loc -> out -> ext_expr
+  | spec_binding_inst_function_decls :  env_loc -> list funcdecl -> strictness_flag -> bool -> ext_expr
+  | spec_binding_inst_function_decls_1 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_2 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_3 : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> specret full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_3a : funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> full_descriptor -> ext_expr
+  | spec_binding_inst_function_decls_4 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> out -> ext_expr
+  | spec_binding_inst_function_decls_5 : env_loc -> funcdecl -> list funcdecl -> strictness_flag -> object_loc -> bool -> ext_expr
+  | spec_binding_inst_function_decls_6 : env_loc -> list funcdecl -> strictness_flag -> bool -> out -> ext_expr
+  | spec_binding_inst_arg_obj :   object_loc -> list string -> list value -> env_loc -> strictness_flag -> ext_expr
+  | spec_binding_inst_arg_obj_1 : env_loc -> strictness_flag -> out -> ext_expr
+  | spec_binding_inst_arg_obj_2 : env_loc -> object_loc -> out -> ext_expr
   | spec_binding_inst_var_decls : env_loc -> list string -> bool -> strictness_flag -> ext_expr
   | spec_binding_inst_var_decls_1 : env_loc -> string -> list string -> bool -> strictness_flag -> out -> ext_expr
   | spec_binding_inst_var_decls_2 : env_loc -> list string -> bool -> strictness_flag -> out -> ext_expr
@@ -1148,17 +1148,17 @@ Definition out_of_ext_expr (e : ext_expr) : option out :=
   | spec_binding_inst_formal_params_2 _ _ _ _ _ _ o => Some o
   | spec_binding_inst_formal_params_3 _ _ _ _ _ _ => None
   | spec_binding_inst_formal_params_4 _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_1 _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_3 _ _ _ _ _ _ y => out_of_specret y
-  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ _ o => Some o
-  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ _ => None
-  | spec_binding_inst_function_decls_6 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls _ _ _ _ => None
+  | spec_binding_inst_function_decls_1 _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_2 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_3 _ _ _ _ _ y => out_of_specret y
+  | spec_binding_inst_function_decls_3a _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_4 _ _ _ _ _ _ o => Some o
+  | spec_binding_inst_function_decls_5 _ _ _ _ _ _ => None
+  | spec_binding_inst_function_decls_6 _ _ _ _ o => Some o
   | spec_binding_inst_arg_obj   object_loc _ _ _ _ => None
-  | spec_binding_inst_arg_obj_1 _ _ _ o => Some o
-  | spec_binding_inst_arg_obj_2 _ _ _ o => Some o
+  | spec_binding_inst_arg_obj_1 _ _ o => Some o
+  | spec_binding_inst_arg_obj_2 _ _ o => Some o
   | spec_binding_inst_var_decls _ _ _ _ => None
   | spec_binding_inst_var_decls_1 _ _ _ _ _ o => Some o
   | spec_binding_inst_var_decls_2 _ _ _ _ o => Some o