From 1b4d665569fc89dd9bc2049065a040ebaa0c7c6a Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Tue, 29 Mar 2016 20:42:33 +0100
Subject: [PATCH] Factor out excess cases in run_unary_op
---
generator/TODO | 14 -
generator/tests/jsref/JsInterpreter.ml | 380 +------------------------
2 files changed, 4 insertions(+), 390 deletions(-)
diff --git a/generator/TODO b/generator/TODO
index f4c0400..2dc8f3a 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 0491cda..9172f29 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 ->
--
GitLab