diff --git a/generator/TODO b/generator/TODO
index f4c040020156c0359f6a6a6ce573e2c6297a73fa..2dc8f3a93030e487a205f33c48b11b838d9c2dff 100644
--- a/generator/TODO
+++ b/generator/TODO
@@ -16,20 +16,6 @@ CURRENT TODO
*) Alan: proof read JSNumber
-*) Thomas: factorize branches such as:
-
-
- | Coq_prim_bool b0 ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s
- ("[run_object_method] returned a primitive in [object_proto_is_prototype_of_body].")
- | Coq_prim_number n ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s
- ("[run_object_method] returned a primitive in [object_proto_is_prototype_of_body].")
-
-
-
*) Arthur: inline let_binding
*) Alan/Thomas: test "eval", might need pieces of JsCommon for it (parsePickable)
diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 0491cda6aa9abb9a40f0e4361e2be58b00ea2c04..9172f29356edd2cd2f5e7059eb0389da69918622 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -2994,50 +2994,6 @@ and run_unary_op s c op e =
if r.ref_strict
then run_error s0 Coq_native_error_syntax
else env_record_delete_binding s0 c l r.ref_name))
- | Coq_unary_op_void ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
| Coq_unary_op_typeof ->
if_success (run_expr s c e) (fun s1 rv ->
match rv with
@@ -3059,211 +3015,11 @@ and run_unary_op s c op e =
res_ter s2
(res_val (Coq_value_prim (Coq_prim_string
(run_typeof_value s2 v))))))
- | Coq_unary_op_post_incr ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_post_decr ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_pre_incr ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_pre_decr ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_add ->
+ | _ ->
if_spec (run_expr_get_value s c e) (fun s1 v ->
match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
| Coq_unary_op_void ->
res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
| Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
if_number (to_number s1 c v) (fun s2 n ->
@@ -3278,139 +3034,11 @@ and run_unary_op s c op e =
| Coq_unary_op_not ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_neg ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
+ (neg (convert_value_to_boolean v)))))
+ | _ ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_bitwise_not ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v))))))
- | Coq_unary_op_not ->
- if_spec (run_expr_get_value s c e) (fun s1 v ->
- match op with
- | Coq_unary_op_delete ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_void ->
- res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
- | Coq_unary_op_typeof ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_post_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_incr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_pre_decr ->
- (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
- s1
- ("Undealt regular operator in [run_unary_op].")
- | Coq_unary_op_add -> to_number s1 c v
- | Coq_unary_op_neg ->
- if_number (to_number s1 c v) (fun s2 n ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (JsNumber.neg n)))))
- | Coq_unary_op_bitwise_not ->
- if_spec (to_int32 s1 c v) (fun s2 k ->
- res_ter s2
- (res_val (Coq_value_prim (Coq_prim_number
- (of_int (JsNumber.int32_bitwise_not k))))))
- | Coq_unary_op_not ->
- res_ter s1
- (res_val (Coq_value_prim (Coq_prim_bool
- (neg (convert_value_to_boolean v)))))))
+ ("Undealt regular operator in [run_unary_op].")))
(** val create_new_function_in :
state -> execution_ctx -> string list -> funcbody ->