diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml
index 45135288997352f279f838fab0be79f143eb834d..53f429bf17f2e6d2471f80396988ab4849ef3f54 100644
--- a/generator/tests/jsref/JsInterpreter.ml
+++ b/generator/tests/jsref/JsInterpreter.ml
@@ -317,239 +317,25 @@ let run_object_heap_set_extensible b s l =
LibOption.map (fun o -> object_write s l (object_set_extensible o b)) opt
*)
- type runs_type = { runs_type_expr : (state -> execution_ctx -> expr ->
- result);
- runs_type_stat : (state -> execution_ctx -> stat ->
- result);
- runs_type_prog : (state -> execution_ctx -> prog ->
- result);
- runs_type_call : (state -> execution_ctx -> object_loc ->
- value -> value list -> result);
- runs_type_call_prealloc : (state -> execution_ctx ->
- prealloc -> value -> value list
- -> result);
- runs_type_construct : (state -> execution_ctx -> construct
- -> object_loc -> value list ->
- result);
- runs_type_function_has_instance : (state -> object_loc ->
- value -> result);
- runs_type_object_has_instance : (state -> execution_ctx ->
- builtin_has_instance ->
- object_loc -> value ->
- result);
- runs_type_get_args_for_apply : (state -> execution_ctx ->
- object_loc -> float ->
- float -> value list
- specres);
- runs_type_stat_while : (state -> execution_ctx -> resvalue
- -> label_set -> expr -> stat ->
- result);
- runs_type_stat_do_while : (state -> execution_ctx ->
- resvalue -> label_set -> expr ->
- stat -> result);
- runs_type_stat_for_loop : (state -> execution_ctx ->
- label_set -> resvalue -> expr
- option -> expr option -> stat ->
- result);
- runs_type_object_delete : (state -> execution_ctx ->
- object_loc -> prop_name -> bool
- -> result);
- runs_type_object_get_own_prop : (state -> execution_ctx ->
- object_loc -> prop_name ->
- full_descriptor specres);
- runs_type_object_get_prop : (state -> execution_ctx ->
- object_loc -> prop_name ->
- full_descriptor specres);
- runs_type_object_get : (state -> execution_ctx ->
- object_loc -> prop_name -> result);
- runs_type_object_proto_is_prototype_of : (state ->
- object_loc ->
- object_loc ->
- result);
- runs_type_object_put : (state -> execution_ctx ->
- object_loc -> prop_name -> value ->
- strictness_flag -> result);
- runs_type_equal : (state -> execution_ctx -> value ->
- value -> result);
- runs_type_to_integer : (state -> execution_ctx -> value ->
- result);
- runs_type_to_string : (state -> execution_ctx -> value ->
- result);
- runs_type_array_join_elements : (state -> execution_ctx ->
- object_loc -> float ->
- float -> string ->
- string -> result);
- runs_type_array_element_list : (state -> execution_ctx ->
- object_loc -> expr option
- list -> float -> result);
- runs_type_object_define_own_prop_array_loop : (state ->
- execution_ctx
- ->
- object_loc
- -> float ->
- float ->
- descriptor
- -> bool ->
- bool ->
- (state ->
- prop_name ->
- descriptor
- ->
- strictness_flag
- -> __
- specres) ->
- result) }
-
-(** val runs_type_expr :
- runs_type -> state -> execution_ctx -> expr -> result **)
-
-let runs_type_expr x = x.runs_type_expr
-
-(** val runs_type_stat :
- runs_type -> state -> execution_ctx -> stat -> result **)
-
-let runs_type_stat x = x.runs_type_stat
-
-(** val runs_type_prog :
- runs_type -> state -> execution_ctx -> prog -> result **)
-
-let runs_type_prog x = x.runs_type_prog
-
-(** val runs_type_call :
- runs_type -> state -> execution_ctx -> object_loc -> value -> value list
- -> result **)
-
-let runs_type_call x = x.runs_type_call
-
-(** val runs_type_call_prealloc :
- runs_type -> state -> execution_ctx -> prealloc -> value -> value list ->
- result **)
-
-let runs_type_call_prealloc x = x.runs_type_call_prealloc
-
-(** val runs_type_construct :
- runs_type -> state -> execution_ctx -> construct -> object_loc -> value
- list -> result **)
-
-let runs_type_construct x = x.runs_type_construct
-
-(** val runs_type_function_has_instance :
- runs_type -> state -> object_loc -> value -> result **)
-
-let runs_type_function_has_instance x = x.runs_type_function_has_instance
-
-(** val runs_type_object_has_instance :
- runs_type -> state -> execution_ctx -> builtin_has_instance -> object_loc
- -> value -> result **)
-
-let runs_type_object_has_instance x = x.runs_type_object_has_instance
-
-(** val runs_type_get_args_for_apply :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
- value list specres **)
-
-let runs_type_get_args_for_apply x = x.runs_type_get_args_for_apply
-
-(** val runs_type_stat_while :
- runs_type -> state -> execution_ctx -> resvalue -> label_set -> expr ->
- stat -> result **)
-
-let runs_type_stat_while x = x.runs_type_stat_while
-
-(** val runs_type_stat_do_while :
- runs_type -> state -> execution_ctx -> resvalue -> label_set -> expr ->
- stat -> result **)
-
-let runs_type_stat_do_while x = x.runs_type_stat_do_while
-
-(** val runs_type_stat_for_loop :
- runs_type -> state -> execution_ctx -> label_set -> resvalue -> expr
- option -> expr option -> stat -> result **)
-
-let runs_type_stat_for_loop x = x.runs_type_stat_for_loop
-
-(** val runs_type_object_delete :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> bool ->
- result **)
-
-let runs_type_object_delete x = x.runs_type_object_delete
-
-(** val runs_type_object_get_own_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
- full_descriptor specres **)
-
-let runs_type_object_get_own_prop x = x.runs_type_object_get_own_prop
-
-(** val runs_type_object_get_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
- full_descriptor specres **)
-
-let runs_type_object_get_prop x = x.runs_type_object_get_prop
-
-(** val runs_type_object_get :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> result **)
-
-let runs_type_object_get x = x.runs_type_object_get
-
-(** val runs_type_object_proto_is_prototype_of :
- runs_type -> state -> object_loc -> object_loc -> result **)
-
-let runs_type_object_proto_is_prototype_of x = x.runs_type_object_proto_is_prototype_of
-
-(** val runs_type_object_put :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> value
- -> strictness_flag -> result **)
-
-let runs_type_object_put x = x.runs_type_object_put
-
-(** val runs_type_equal :
- runs_type -> state -> execution_ctx -> value -> value -> result **)
-
-let runs_type_equal x = x.runs_type_equal
-
-(** val runs_type_to_string :
- runs_type -> state -> execution_ctx -> value -> result **)
-
-let runs_type_to_string x = x.runs_type_to_string
-
-(** val runs_type_array_join_elements :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
- string -> string -> result **)
-
-let runs_type_array_join_elements x = x.runs_type_array_join_elements
-
-(** val runs_type_array_element_list :
- runs_type -> state -> execution_ctx -> object_loc -> expr option list ->
- float -> result **)
-
-let runs_type_array_element_list x = x.runs_type_array_element_list
-
-(** val runs_type_object_define_own_prop_array_loop :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
- descriptor -> bool -> bool -> (state -> prop_name -> descriptor ->
- strictness_flag -> __ specres) -> result **)
-
-let runs_type_object_define_own_prop_array_loop x = x.runs_type_object_define_own_prop_array_loop
-
(** val object_has_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> result **)
+ state -> execution_ctx -> object_loc -> prop_name -> result **)
-let object_has_prop runs0 s c l x =
+let rec object_has_prop s c l x =
if_some (run_object_method object_has_prop_ s l) (fun b ->
match b with Coq_builtin_has_prop_default ->
- if_spec (runs0.runs_type_object_get_prop s c l x) (fun s1 d ->
+ if_spec (run_object_get_prop s c l x) (fun s1 d ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_bool
(not_decidable
(full_descriptor_comparable d Coq_full_descriptor_undef)))))))
(** val object_get_builtin :
- runs_type -> state -> execution_ctx -> builtin_get -> value -> object_loc
+ state -> execution_ctx -> builtin_get -> value -> object_loc
-> prop_name -> result **)
-let object_get_builtin runs0 s c b vthis l x =
+and object_get_builtin s c b vthis l x =
let_binding (fun s0 l0 ->
- if_spec (runs0.runs_type_object_get_prop s0 c l0 x) (fun s1 d ->
+ if_spec (run_object_get_prop s0 c l0 x) (fun s1 d ->
match d with
| Coq_full_descriptor_undef ->
res_ter s1 (res_val (Coq_value_prim Coq_prim_undef))
@@ -567,7 +353,7 @@ let object_get_builtin runs0 s c b vthis l x =
| Coq_prim_bool b0 -> Coq_result_impossible
| Coq_prim_number n -> Coq_result_impossible
| Coq_prim_string s2 -> Coq_result_impossible)
- | Coq_value_object lf -> runs0.runs_type_call s1 c lf vthis []))))
+ | Coq_value_object lf -> run_call s1 c lf vthis []))))
(fun def ->
let_binding (fun s0 ->
if_value (def s0 l) (fun s' v ->
@@ -580,28 +366,28 @@ let object_get_builtin runs0 s c b vthis l x =
| Coq_builtin_get_args_obj ->
if_some (run_object_method object_parameter_map_ s l) (fun lmapo ->
if_some lmapo (fun lmap ->
- if_spec (runs0.runs_type_object_get_own_prop s c lmap x)
+ if_spec (run_object_get_own_prop s c lmap x)
(fun s0 d ->
match d with
| Coq_full_descriptor_undef -> function0 s0
| Coq_full_descriptor_some a ->
- runs0.runs_type_object_get s0 c lmap x)))))
+ run_object_get s0 c lmap x)))))
(** val run_object_get :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> result **)
+ state -> execution_ctx -> object_loc -> prop_name -> result **)
-let run_object_get runs0 s c l x =
+and run_object_get s c l x =
if_some (run_object_method object_get_ s l) (fun b ->
- object_get_builtin runs0 s c b (Coq_value_object l) l x)
+ object_get_builtin s c b (Coq_value_object l) l x)
(** val run_object_get_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
+ state -> execution_ctx -> object_loc -> prop_name ->
full_descriptor specres **)
-let run_object_get_prop runs0 s c l x =
+and run_object_get_prop s c l x =
if_some (run_object_method object_get_prop_ s l) (fun b ->
match b with Coq_builtin_get_prop_default ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s1 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s1 d ->
if full_descriptor_comparable d Coq_full_descriptor_undef
then if_some (run_object_method object_proto_ s1 l) (fun proto ->
match proto with
@@ -625,13 +411,13 @@ let run_object_get_prop runs0 s c l x =
s1
("Found a non-null primitive value as a prototype in [run_object_get_prop]."))
| Coq_value_object lproto ->
- runs0.runs_type_object_get_prop s1 c lproto x)
+ run_object_get_prop s1 c lproto x)
else res_spec s1 d))
(** val object_proto_is_prototype_of :
- runs_type -> state -> object_loc -> object_loc -> result **)
+ state -> object_loc -> object_loc -> result **)
-let object_proto_is_prototype_of runs0 s l0 l =
+and object_proto_is_prototype_of s l0 l =
if_some (run_object_method object_proto_ s l) (fun b ->
match b with
| Coq_value_prim p ->
@@ -659,26 +445,26 @@ let object_proto_is_prototype_of runs0 s l0 l =
if object_loc_comparable l' l0
then result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_bool true)))))
- else runs0.runs_type_object_proto_is_prototype_of s l0 l')
+ else object_proto_is_prototype_of s l0 l')
(** val object_default_value :
- runs_type -> state -> execution_ctx -> object_loc -> preftype option ->
+ state -> execution_ctx -> object_loc -> preftype option ->
result **)
-let object_default_value runs0 s c l prefo =
+and object_default_value s c l prefo =
if_some (run_object_method object_default_value_ s l) (fun b ->
match b with Coq_builtin_default_value_default ->
let gpref = unsome_default Coq_preftype_number prefo in
let lpref = other_preftypes gpref in
let sub0 = (fun s' x k -> (* this was a let_binding *)
- if_value (run_object_get runs0 s' c l x) (fun s1 vfo ->
+ if_value (run_object_get s' c l x) (fun s1 vfo ->
if_some (run_callable s1 vfo) (fun co ->
match co with
| Some b0 ->
if_object (result_out (Coq_out_ter (s1, (res_val vfo))))
(fun s2 lfunc ->
if_value
- (runs0.runs_type_call s2 c lfunc (Coq_value_object l) [])
+ (run_call s2 c lfunc (Coq_value_object l) [])
(fun s3 v ->
match v with
| Coq_value_prim w ->
@@ -691,72 +477,72 @@ let object_default_value runs0 s c l prefo =
sub0 s' lmeth (fun s'' -> run_error s'' Coq_native_error_type))))
(** val to_primitive :
- runs_type -> state -> execution_ctx -> value -> preftype option -> result **)
+ state -> execution_ctx -> value -> preftype option -> result **)
-let to_primitive runs0 s c v prefo =
+and to_primitive s c v prefo =
match v with
| Coq_value_prim w ->
result_out (Coq_out_ter (s, (res_val (Coq_value_prim w))))
| Coq_value_object l ->
- if_prim (object_default_value runs0 s c l prefo) (fun s0 r ->
+ if_prim (object_default_value s c l prefo) (fun s0 r ->
res_ter s0 (res_val (Coq_value_prim r)))
(** val to_number :
- runs_type -> state -> execution_ctx -> value -> result **)
+ state -> execution_ctx -> value -> result **)
-let to_number runs0 s c _foo_ = match _foo_ with
+and to_number s c _foo_ = match _foo_ with
| Coq_value_prim w ->
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w))))))
| Coq_value_object l ->
if_prim
- (to_primitive runs0 s c (Coq_value_object l) (Some Coq_preftype_number))
+ (to_primitive s c (Coq_value_object l) (Some Coq_preftype_number))
(fun s1 w ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_number (convert_prim_to_number w)))))
(** val to_integer :
- runs_type -> state -> execution_ctx -> value -> result **)
+ state -> execution_ctx -> value -> result **)
-let to_integer runs0 s c v =
- if_number (to_number runs0 s c v) (fun s1 n ->
+and to_integer s c v =
+ if_number (to_number s c v) (fun s1 n ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_number
(convert_number_to_integer n)))))
(** val to_int32 :
- runs_type -> state -> execution_ctx -> value -> float specres **)
+ state -> execution_ctx -> value -> float specres **)
-let to_int32 runs0 s c v =
- if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (JsNumber.to_int32 n))
+and to_int32 s c v =
+ if_number (to_number s c v) (fun s' n -> res_spec s' (JsNumber.to_int32 n))
(** val to_uint32 :
- runs_type -> state -> execution_ctx -> value -> float specres **)
+ state -> execution_ctx -> value -> float specres **)
-let to_uint32 runs0 s c v =
- if_number (to_number runs0 s c v) (fun s' n -> res_spec s' (JsNumber.to_uint32 n))
+and to_uint32 s c v =
+ if_number (to_number s c v) (fun s' n -> res_spec s' (JsNumber.to_uint32 n))
(** val to_string :
- runs_type -> state -> execution_ctx -> value -> result **)
+ state -> execution_ctx -> value -> result **)
-let to_string runs0 s c _foo_ = match _foo_ with
+and to_string s c _foo_ = match _foo_ with
| Coq_value_prim w ->
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w))))))
| Coq_value_object l ->
if_prim
- (to_primitive runs0 s c (Coq_value_object l) (Some Coq_preftype_string))
+ (to_primitive s c (Coq_value_object l) (Some Coq_preftype_string))
(fun s1 w ->
res_ter s1
(res_val (Coq_value_prim (Coq_prim_string (convert_prim_to_string w)))))
(** val object_can_put :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> result **)
+ state -> execution_ctx -> object_loc -> prop_name -> result **)
-let object_can_put runs0 s c l x =
+and object_can_put s c l x =
if_some (run_object_method object_can_put_ s l) (fun b ->
match b with Coq_builtin_can_put_default ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s1 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s1 d ->
match d with
| Coq_full_descriptor_undef ->
if_some (run_object_method object_proto_ s1 l) (fun vproto ->
@@ -783,7 +569,7 @@ let object_can_put runs0 s c l x =
s1
("Non-null primitive get as a prototype value in [object_can_put]."))
| Coq_value_object lproto ->
- if_spec (run_object_get_prop runs0 s1 c lproto x) (fun s2 d' ->
+ if_spec (run_object_get_prop s1 c lproto x) (fun s2 d' ->
match d' with
| Coq_full_descriptor_undef ->
if_some (run_object_method object_extensible_ s2 l)
@@ -819,17 +605,17 @@ let object_can_put runs0 s c l x =
Coq_prim_undef)))))))))
(** val run_object_define_own_prop_array_loop :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
+ state -> execution_ctx -> object_loc -> float -> float ->
descriptor -> bool -> bool -> (state -> prop_name -> descriptor ->
strictness_flag -> __ specres) -> result **)
-let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc newWritable throwcont def =
+and run_object_define_own_prop_array_loop s c l newLen oldLen newLenDesc newWritable throwcont def =
if newLen < oldLen
then let_binding (oldLen -. 1.) (fun oldLen' ->
if_string
- (to_string runs0 s c (Coq_value_prim (Coq_prim_number
+ (to_string s c (Coq_value_prim (Coq_prim_number
(of_int oldLen')))) (fun s0 slen ->
- if_bool (runs0.runs_type_object_delete s0 c l slen false)
+ if_bool (object_delete s0 c l slen false)
(fun s1 deleteSucceeded ->
if not_decidable (bool_decidable deleteSucceeded)
then let_binding
@@ -845,7 +631,7 @@ let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc n
newLenDesc1 false) (fun s2 x ->
out_error_or_cst s2 throwcont Coq_native_error_type
(Coq_value_prim (Coq_prim_bool false)))))
- else runs0.runs_type_object_define_own_prop_array_loop s1 c l
+ else run_object_define_own_prop_array_loop s1 c l
newLen oldLen' newLenDesc newWritable throwcont def)))
else if not_decidable (bool_decidable newWritable)
then def s ("length")
@@ -856,15 +642,15 @@ let run_object_define_own_prop_array_loop runs0 s c l newLen oldLen newLenDesc n
else res_ter s (res_val (Coq_value_prim (Coq_prim_bool true)))
(** val object_define_own_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
+ state -> execution_ctx -> object_loc -> prop_name ->
descriptor -> strictness_flag -> result **)
-let object_define_own_prop runs0 s c l x desc throwcont =
+and object_define_own_prop s c l x desc throwcont =
let_binding (fun s0 throwcont0 ->
out_error_or_cst s0 throwcont0 Coq_native_error_type (Coq_value_prim
(Coq_prim_bool false))) (fun reject ->
let_binding (fun s0 x0 desc0 throwcont0 ->
- if_spec (runs0.runs_type_object_get_own_prop s0 c l x0) (fun s1 d ->
+ if_spec (run_object_get_own_prop s0 c l x0) (fun s1 d ->
if_some (run_object_method object_extensible_ s1 l) (fun ext ->
match d with
| Coq_full_descriptor_undef ->
@@ -957,7 +743,7 @@ let object_define_own_prop runs0 s c l x desc throwcont =
| Coq_builtin_define_own_prop_default -> def s x desc throwcont
| Coq_builtin_define_own_prop_array ->
if_spec
- (runs0.runs_type_object_get_own_prop s c l
+ (run_object_get_own_prop s c l
("length")) (fun s0 d ->
match d with
| Coq_full_descriptor_undef ->
@@ -978,9 +764,9 @@ let object_define_own_prop runs0 s c l x desc throwcont =
("length")
then (match descValueOpt with
| Some descValue ->
- if_spec (to_uint32 runs0 s0 c descValue)
+ if_spec (to_uint32 s0 c descValue)
(fun s1 newLen ->
- if_number (to_number runs0 s1 c descValue)
+ if_number (to_number s1 c descValue)
(fun s2 newLenN ->
if not_decidable
(number_comparable (of_int newLen)
@@ -1033,7 +819,7 @@ let object_define_own_prop runs0 s c l x desc throwcont =
(Coq_prim_bool
false)))
else run_object_define_own_prop_array_loop
- runs0 s3 c
+ s3 c
l newLen
oldLen0
newLenDesc0
@@ -1045,10 +831,10 @@ let object_define_own_prop runs0 s c l x desc throwcont =
("length")
desc throwcont)
else if_spec
- (to_uint32 runs0 s0 c (Coq_value_prim
+ (to_uint32 s0 c (Coq_value_prim
(Coq_prim_string x))) (fun s1 ilen ->
if_string
- (to_string runs0 s1 c (Coq_value_prim
+ (to_string s1 c (Coq_value_prim
(Coq_prim_number (of_int ilen))))
(fun s2 slen ->
if and_decidable (string_comparable x slen)
@@ -1087,7 +873,7 @@ let object_define_own_prop runs0 s c l x desc throwcont =
((fun p -> 1. +. (2. *. p))
1.)))))))))))))))))))))))))))))))))
then if_spec
- (to_uint32 runs0 s2 c
+ (to_uint32 s2 c
(Coq_value_prim (Coq_prim_string
x))) (fun s3 index ->
if and_decidable
@@ -1135,7 +921,7 @@ let object_define_own_prop runs0 s c l x desc throwcont =
| Coq_builtin_define_own_prop_args_obj ->
if_some (run_object_method object_parameter_map_ s l) (fun lmapo ->
if_some lmapo (fun lmap ->
- if_spec (runs0.runs_type_object_get_own_prop s c lmap x)
+ if_spec (run_object_get_own_prop s c lmap x)
(fun s0 d ->
if_bool (def s0 x desc false) (fun s1 b0 ->
if b0
@@ -1148,35 +934,35 @@ let object_define_own_prop runs0 s c l x desc throwcont =
| Coq_full_descriptor_some a ->
if descriptor_is_accessor_dec desc
then if_bool
- (runs0.runs_type_object_delete s1 c lmap x
+ (object_delete s1 c lmap x
false) (fun s2 x0 -> follow s2)
else let_binding (fun s2 ->
if option_comparable bool_comparable
desc.descriptor_writable (Some false)
then if_bool
- (runs0.runs_type_object_delete s2 c
+ (object_delete s2 c
lmap x false) (fun s3 x0 ->
follow s3)
else follow s2) (fun follow0 ->
match desc.descriptor_value with
| Some v ->
if_void
- (runs0.runs_type_object_put s1 c lmap x
+ (object_put s1 c lmap x
v throwcont) (fun s2 -> follow0 s2)
| None -> follow0 s1))
else reject s1 throwcont)))))))
(** val run_to_descriptor :
- runs_type -> state -> execution_ctx -> value -> descriptor specres **)
+ state -> execution_ctx -> value -> descriptor specres **)
-let run_to_descriptor runs0 s c _foo_ = match _foo_ with
+and run_to_descriptor s c _foo_ = match _foo_ with
| Coq_value_prim p -> throw_result (run_error s Coq_native_error_type)
| Coq_value_object l ->
let sub0 = fun s0 desc name conv k ->
- if_bool (object_has_prop runs0 s0 c l name) (fun s1 has ->
+ if_bool (object_has_prop s0 c l name) (fun s1 has ->
if neg has
then k s1 desc
- else if_value (run_object_get runs0 s1 c l name) (fun s2 v0 ->
+ else if_value (run_object_get s1 c l name) (fun s2 v0 ->
if_spec (conv s2 v0 desc) k))
in
sub0 s descriptor_intro_empty
@@ -1238,7 +1024,7 @@ let run_to_descriptor runs0 s c _foo_ = match _foo_ with
(** val prim_new_object : state -> prim -> result **)
-let prim_new_object s _foo_ = match _foo_ with
+and prim_new_object s _foo_ = match _foo_ with
| Coq_prim_undef ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
@@ -1291,7 +1077,7 @@ let prim_new_object s _foo_ = match _foo_ with
(** val to_object : state -> value -> result **)
-let to_object s _foo_ = match _foo_ with
+and to_object s _foo_ = match _foo_ with
| Coq_value_prim w ->
(match w with
| Coq_prim_undef -> run_error s Coq_native_error_type
@@ -1304,49 +1090,49 @@ let to_object s _foo_ = match _foo_ with
(** val run_object_prim_value : state -> object_loc -> result **)
-let run_object_prim_value s l =
+and run_object_prim_value s l =
if_some (run_object_method object_prim_value_ s l) (fun ov ->
if_some ov (fun v -> res_ter s (res_val v)))
(** val prim_value_get :
- runs_type -> state -> execution_ctx -> value -> prop_name -> result **)
+ state -> execution_ctx -> value -> prop_name -> result **)
-let prim_value_get runs0 s c v x =
+and prim_value_get s c v x =
if_object (to_object s v) (fun s' l ->
- object_get_builtin runs0 s' c Coq_builtin_get_default v l x)
+ object_get_builtin s' c Coq_builtin_get_default v l x)
(** val env_record_has_binding :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name -> result **)
+ state -> execution_ctx -> env_loc -> prop_name -> result **)
-let env_record_has_binding runs0 s c l x =
+and env_record_has_binding s c l x =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_bool
(Heap.indom_decidable string_comparable ed x))))))
- | Coq_env_record_object (l0, pt) -> object_has_prop runs0 s c l0 x)
+ | Coq_env_record_object (l0, pt) -> object_has_prop s c l0 x)
(** val lexical_env_get_identifier_ref :
- runs_type -> state -> execution_ctx -> lexical_env -> prop_name ->
+ state -> execution_ctx -> lexical_env -> prop_name ->
strictness_flag -> ref specres **)
-let rec lexical_env_get_identifier_ref runs0 s c x x0 str =
+and lexical_env_get_identifier_ref s c x x0 str =
match x with
| [] ->
res_spec s (ref_create_value (Coq_value_prim Coq_prim_undef) x0 str)
| l :: x' ->
- if_bool (env_record_has_binding runs0 s c l x0) (fun s1 has ->
+ if_bool (env_record_has_binding s c l x0) (fun s1 has ->
if has
then res_spec s1 (ref_create_env_loc l x0 str)
- else lexical_env_get_identifier_ref runs0 s1 c x' x0 str)
+ else lexical_env_get_identifier_ref s1 c x' x0 str)
(** val object_delete_default :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
+ state -> execution_ctx -> object_loc -> prop_name ->
strictness_flag -> result **)
-let object_delete_default runs0 s c l x str =
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s1 d ->
+and object_delete_default s c l x str =
+ if_spec (run_object_get_own_prop s c l x) (fun s1 d ->
match d with
| Coq_full_descriptor_undef ->
res_ter s1 (res_val (Coq_value_prim (Coq_prim_bool true)))
@@ -1360,34 +1146,34 @@ let object_delete_default runs0 s c l x str =
(Coq_prim_bool false)))
(** val object_delete :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
+ state -> execution_ctx -> object_loc -> prop_name ->
strictness_flag -> result **)
-let object_delete runs0 s c l x str =
+and object_delete s c l x str =
if_some (run_object_method object_delete_ s l) (fun b ->
match b with
- | Coq_builtin_delete_default -> object_delete_default runs0 s c l x str
+ | Coq_builtin_delete_default -> object_delete_default s c l x str
| Coq_builtin_delete_args_obj ->
if_some (run_object_method object_parameter_map_ s l) (fun mo ->
if_some mo (fun m ->
- if_spec (runs0.runs_type_object_get_own_prop s c m x) (fun s1 d ->
- if_bool (object_delete_default runs0 s1 c l x str) (fun s2 b0 ->
+ if_spec (run_object_get_own_prop s c m x) (fun s1 d ->
+ if_bool (object_delete_default s1 c l x str) (fun s2 b0 ->
if b0
then (match d with
| Coq_full_descriptor_undef ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_bool b0)))
| Coq_full_descriptor_some a ->
- if_bool (runs0.runs_type_object_delete s2 c m x false)
+ if_bool (object_delete s2 c m x false)
(fun s3 b' ->
res_ter s3
(res_val (Coq_value_prim (Coq_prim_bool b0)))))
else res_ter s2 (res_val (Coq_value_prim (Coq_prim_bool b0))))))))
(** val env_record_delete_binding :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name -> result **)
+ state -> execution_ctx -> env_loc -> prop_name -> result **)
-let env_record_delete_binding runs0 s c l x =
+and env_record_delete_binding s c l x =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
@@ -1415,11 +1201,11 @@ let env_record_delete_binding runs0 s c l x =
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_bool true))))))
| Coq_env_record_object (l0, pt) ->
- runs0.runs_type_object_delete s c l0 x throw_false)
+ object_delete s c l0 x throw_false)
(** val env_record_implicit_this_value : state -> env_loc -> value option **)
-let env_record_implicit_this_value s l =
+and env_record_implicit_this_value s l =
if_some_or_default (env_record_binds_pickable_option s l) None (fun e ->
Some
(match e with
@@ -1430,18 +1216,18 @@ let env_record_implicit_this_value s l =
else Coq_value_prim Coq_prim_undef))
(** val identifier_resolution :
- runs_type -> state -> execution_ctx -> prop_name -> ref specres **)
+ state -> execution_ctx -> prop_name -> ref specres **)
-let identifier_resolution runs0 s c x =
+and identifier_resolution s c x =
let x0 = c.execution_ctx_lexical_env in
let str = c.execution_ctx_strict in
- lexical_env_get_identifier_ref runs0 s c x0 x str
+ lexical_env_get_identifier_ref s c x0 x str
(** val env_record_get_binding_value :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name ->
+ state -> execution_ctx -> env_loc -> prop_name ->
strictness_flag -> result **)
-let env_record_get_binding_value runs0 s c l x str =
+and env_record_get_binding_value s c l x str =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
@@ -1452,16 +1238,16 @@ let env_record_get_binding_value runs0 s c l x str =
Coq_prim_undef)
else res_ter s (res_val v))
| Coq_env_record_object (l0, pt) ->
- if_bool (object_has_prop runs0 s c l0 x) (fun s1 has ->
+ if_bool (object_has_prop s c l0 x) (fun s1 has ->
if has
- then run_object_get runs0 s1 c l0 x
+ then run_object_get s1 c l0 x
else out_error_or_cst s1 str Coq_native_error_ref (Coq_value_prim
Coq_prim_undef)))
(** val ref_get_value :
- runs_type -> state -> execution_ctx -> resvalue -> value specres **)
+ state -> execution_ctx -> resvalue -> value specres **)
-let ref_get_value runs0 s c _foo_ = match _foo_ with
+and ref_get_value s c _foo_ = match _foo_ with
| Coq_resvalue_empty ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
@@ -1472,14 +1258,14 @@ let ref_get_value runs0 s c _foo_ = match _foo_ with
match r.ref_base with
| Coq_ref_base_type_value v ->
if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_primitive_base
- then if_value (prim_value_get runs0 s c v r.ref_name) res_spec
+ then if_value (prim_value_get s c v r.ref_name) res_spec
else (match v with
| Coq_value_prim p ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
("[ref_get_value] received a primitive value whose kind is not primitive.")
| Coq_value_object l ->
- if_value (run_object_get runs0 s c l r.ref_name) res_spec)
+ if_value (run_object_get s c l r.ref_name) res_spec)
| Coq_ref_base_type_env_loc l ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
@@ -1501,11 +1287,11 @@ let ref_get_value runs0 s c _foo_ = match _foo_ with
("[ref_get_value] received a reference to an environnment record whose base type is a value.")
| Coq_ref_base_type_env_loc l ->
if_value
- (env_record_get_binding_value runs0 s c l r.ref_name r.ref_strict)
+ (env_record_get_binding_value s c l r.ref_name r.ref_strict)
res_spec))
(* DEBUG
-let ref_get_value runs s c r =
+and ref_get_value runs s c r =
let res = ref_get_value runs s c r in match res with
| JsInterpreterMonads.Coq_result_some crs ->
begin match crs with
@@ -1525,23 +1311,23 @@ let ref_get_value runs s c r =
(** val run_expr_get_value :
- runs_type -> state -> execution_ctx -> expr -> value specres **)
+ state -> execution_ctx -> expr -> value specres **)
-let run_expr_get_value runs0 s c e =
- if_success (runs0.runs_type_expr s c e) (fun s0 rv ->
- ref_get_value runs0 s0 c rv)
+and run_expr_get_value s c e =
+ if_success (run_expr s c e) (fun s0 rv ->
+ ref_get_value s0 c rv)
(** val object_put_complete :
- runs_type -> builtin_put -> state -> execution_ctx -> value -> object_loc
+ builtin_put -> state -> execution_ctx -> value -> object_loc
-> prop_name -> value -> strictness_flag -> result_void **)
-let object_put_complete runs0 b s c vthis l x v str =
+and object_put_complete b s c vthis l x v str =
match b with Coq_builtin_put_default ->
- if_bool (object_can_put runs0 s c l x) (fun s1 b0 ->
+ if_bool (object_can_put s c l x) (fun s1 b0 ->
if b0
- then if_spec (runs0.runs_type_object_get_own_prop s1 c l x) (fun s2 d ->
+ then if_spec (run_object_get_own_prop s1 c l x) (fun s2 d ->
let_binding (fun x0 ->
- if_spec (run_object_get_prop runs0 s2 c l x) (fun s3 d' ->
+ if_spec (run_object_get_prop s2 c l x) (fun s3 d' ->
let_binding (fun x1 ->
match vthis with
| Coq_value_prim wthis ->
@@ -1550,7 +1336,7 @@ let object_put_complete runs0 b s c vthis l x v str =
let_binding (descriptor_intro_data v true true true)
(fun desc ->
if_success
- (object_define_own_prop runs0 s3 c l x desc str)
+ (object_define_own_prop s3 c l x desc str)
(fun s4 rv -> res_void s4))) (fun follow' ->
match d' with
| Coq_full_descriptor_undef -> follow' ()
@@ -1565,7 +1351,7 @@ let object_put_complete runs0 b s c vthis l x v str =
("[object_put_complete] found a primitive in an `set\' accessor.")
| Coq_value_object lfsetter ->
if_success
- (runs0.runs_type_call s3 c lfsetter vthis
+ (run_call s3 c lfsetter vthis
(v :: [])) (fun s4 rv -> res_void s4))))))
(fun follow ->
match d with
@@ -1582,24 +1368,24 @@ let object_put_complete runs0 b s c vthis l x v str =
descriptor_set = None; descriptor_enumerable = None;
descriptor_configurable = None } (fun desc ->
if_success
- (object_define_own_prop runs0 s2 c l x desc str)
+ (object_define_own_prop s2 c l x desc str)
(fun s3 rv -> res_void s3)))
| Coq_attributes_accessor_of a0 -> follow ())))
else out_error_or_void s1 str Coq_native_error_type)
(** val object_put :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name -> value
+ state -> execution_ctx -> object_loc -> prop_name -> value
-> strictness_flag -> result_void **)
-let object_put runs0 s c l x v str =
+and object_put s c l x v str =
if_some (run_object_method object_put_ s l) (fun b ->
- object_put_complete runs0 b s c (Coq_value_object l) l x v str)
+ object_put_complete b s c (Coq_value_object l) l x v str)
(** val env_record_set_mutable_binding :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name -> value ->
+ state -> execution_ctx -> env_loc -> prop_name -> value ->
strictness_flag -> result_void **)
-let env_record_set_mutable_binding runs0 s c l x v str =
+and env_record_set_mutable_binding s c l x v str =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
@@ -1608,21 +1394,21 @@ let env_record_set_mutable_binding runs0 s c l x v str =
if not_decidable (mutability_comparable mu Coq_mutability_immutable)
then res_void (env_record_write_decl_env s l x mu v)
else out_error_or_void s str Coq_native_error_type)
- | Coq_env_record_object (l0, pt) -> object_put runs0 s c l0 x v str)
+ | Coq_env_record_object (l0, pt) -> object_put s c l0 x v str)
(** val prim_value_put :
- runs_type -> state -> execution_ctx -> prim -> prop_name -> value ->
+ state -> execution_ctx -> prim -> prop_name -> value ->
strictness_flag -> result_void **)
-let prim_value_put runs0 s c w x v str =
+and prim_value_put s c w x v str =
if_object (to_object s (Coq_value_prim w)) (fun s1 l ->
- object_put_complete runs0 Coq_builtin_put_default s1 c (Coq_value_prim w)
+ object_put_complete Coq_builtin_put_default s1 c (Coq_value_prim w)
l x v str)
(** val ref_put_value :
- runs_type -> state -> execution_ctx -> resvalue -> value -> result_void **)
+ state -> execution_ctx -> resvalue -> value -> result_void **)
-let ref_put_value runs0 s c rv v =
+and ref_put_value s c rv v =
match rv with
| Coq_resvalue_empty ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -1633,7 +1419,7 @@ let ref_put_value runs0 s c rv v =
if ref_kind_comparable (ref_kind_of r) Coq_ref_kind_undef
then if r.ref_strict
then run_error s Coq_native_error_ref
- else object_put runs0 s c (Coq_object_loc_prealloc
+ else object_put s c (Coq_object_loc_prealloc
Coq_prealloc_global) r.ref_name v throw_false
else if or_decidable
(ref_kind_comparable (ref_kind_of r)
@@ -1647,7 +1433,7 @@ let ref_put_value runs0 s c rv v =
Coq_ref_kind_primitive_base
then (match v' with
| Coq_value_prim w ->
- prim_value_put runs0 s c w r.ref_name v r.ref_strict
+ prim_value_put s c w r.ref_name v r.ref_strict
| Coq_value_object o ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
@@ -1658,7 +1444,7 @@ let ref_put_value runs0 s c rv v =
s
("[ref_put_value] impossible case")
| Coq_value_object l ->
- object_put runs0 s c l r.ref_name v r.ref_strict)
+ object_put s c l r.ref_name v r.ref_strict)
| Coq_ref_base_type_env_loc l ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s
@@ -1669,14 +1455,14 @@ let ref_put_value runs0 s c rv v =
s
("[ref_put_value] impossible spec")
| Coq_ref_base_type_env_loc l ->
- env_record_set_mutable_binding runs0 s c l r.ref_name v
+ env_record_set_mutable_binding s c l r.ref_name v
r.ref_strict)
(** val env_record_create_mutable_binding :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name -> bool
+ state -> execution_ctx -> env_loc -> prop_name -> bool
option -> result_void **)
-let env_record_create_mutable_binding runs0 s c l x deletable_opt =
+and env_record_create_mutable_binding s c l x deletable_opt =
let_binding (unsome_default false deletable_opt) (fun deletable ->
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
@@ -1690,7 +1476,7 @@ let env_record_create_mutable_binding runs0 s c l x deletable_opt =
(mutability_of_bool deletable) (Coq_value_prim
Coq_prim_undef)) (fun s' -> res_void s')
| Coq_env_record_object (l0, pt) ->
- if_bool (object_has_prop runs0 s c l0 x) (fun s1 has ->
+ if_bool (object_has_prop s c l0 x) (fun s1 has ->
if has
then (fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
s1
@@ -1700,22 +1486,22 @@ let env_record_create_mutable_binding runs0 s c l x deletable_opt =
attributes_data_enumerable = true;
attributes_data_configurable = deletable } (fun a ->
if_success
- (object_define_own_prop runs0 s1 c l0 x
+ (object_define_own_prop s1 c l0 x
(descriptor_of_attributes (Coq_attributes_data_of a))
throw_true) (fun s2 rv -> res_void s2)))))
(** val env_record_create_set_mutable_binding :
- runs_type -> state -> execution_ctx -> env_loc -> prop_name -> bool
+ state -> execution_ctx -> env_loc -> prop_name -> bool
option -> value -> strictness_flag -> result_void **)
-let env_record_create_set_mutable_binding runs0 s c l x deletable_opt v str =
- if_void (env_record_create_mutable_binding runs0 s c l x deletable_opt)
- (fun s0 -> env_record_set_mutable_binding runs0 s0 c l x v str)
+and env_record_create_set_mutable_binding s c l x deletable_opt v str =
+ if_void (env_record_create_mutable_binding s c l x deletable_opt)
+ (fun s0 -> env_record_set_mutable_binding s0 c l x v str)
(** val env_record_create_immutable_binding :
state -> env_loc -> prop_name -> result_void **)
-let env_record_create_immutable_binding s l x =
+and env_record_create_immutable_binding s l x =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
@@ -1735,7 +1521,7 @@ let env_record_create_immutable_binding s l x =
(** val env_record_initialize_immutable_binding :
state -> env_loc -> prop_name -> value -> result_void **)
-let env_record_initialize_immutable_binding s l x v =
+and env_record_initialize_immutable_binding s l x v =
if_some (env_record_binds_pickable_option s l) (fun e ->
match e with
| Coq_env_record_decl ed ->
@@ -1756,7 +1542,7 @@ let env_record_initialize_immutable_binding s l x v =
(** val call_object_new : state -> value -> result **)
-let call_object_new s v =
+and call_object_new s v =
match type_of v with
| Coq_type_undef ->
result_out
@@ -1780,10 +1566,10 @@ let call_object_new s v =
| Coq_type_object -> result_out (Coq_out_ter (s, (res_val v)))
(** val array_args_map_loop :
- runs_type -> state -> execution_ctx -> object_loc -> value list -> float
+ state -> execution_ctx -> object_loc -> value list -> float
-> result_void **)
-let rec array_args_map_loop runs0 s c l args ind =
+and array_args_map_loop s c l args ind =
match args with
| [] -> res_void s
| h :: rest ->
@@ -1791,11 +1577,11 @@ let rec array_args_map_loop runs0 s c l args ind =
(object_heap_map_properties_pickable_option s l (fun p ->
Heap.write p (JsNumber.to_string (of_int ind))
(Coq_attributes_data_of (attributes_data_intro_all_true h))))
- (fun s' -> array_args_map_loop runs0 s' c l rest (ind +. 1.))
+ (fun s' -> array_args_map_loop s' c l rest (ind +. 1.))
(** val string_of_prealloc : prealloc -> string **)
-let string_of_prealloc _foo_ = match _foo_ with
+and string_of_prealloc _foo_ = match _foo_ with
| Coq_prealloc_global -> "global"
| Coq_prealloc_global_eval ->
"global_eval"
@@ -1930,9 +1716,9 @@ let string_of_prealloc _foo_ = match _foo_ with
| Coq_prealloc_json -> "json"
(** val run_construct_prealloc :
- runs_type -> state -> execution_ctx -> prealloc -> value list -> result **)
+ state -> execution_ctx -> prealloc -> value list -> result **)
-let run_construct_prealloc runs0 s c b args =
+and run_construct_prealloc s c b args =
match b with
| Coq_prealloc_global ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -2197,7 +1983,7 @@ let run_construct_prealloc runs0 s c b args =
if list_eq_nil_decidable args
then follow s (Coq_value_prim (Coq_prim_number JsNumber.zero))
else let_binding (get_arg 0 args) (fun v ->
- if_number (to_number runs0 s c v) (fun x x0 ->
+ if_number (to_number s c v) (fun x x0 ->
follow x (Coq_value_prim (Coq_prim_number x0)))))
| Coq_prealloc_number_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -2286,7 +2072,7 @@ let run_construct_prealloc runs0 s c b args =
follow s0 1.0)
| Coq_prim_number vlen ->
if_spec
- (to_uint32 runs0 s' c (Coq_value_prim
+ (to_uint32 s' c (Coq_value_prim
(Coq_prim_number vlen))) (fun s0 ilen ->
if number_comparable (of_int ilen) vlen
then follow s0 ilen
@@ -2317,7 +2103,7 @@ let run_construct_prealloc runs0 s c b args =
attributes_data_writable = true;
attributes_data_enumerable = false;
attributes_data_configurable = false }))) (fun s0 ->
- if_void (array_args_map_loop runs0 s0 c l args 0.)
+ if_void (array_args_map_loop s0 c l args 0.)
(fun s1 -> res_ter s1 (res_val (Coq_value_object l)))))))))
| Coq_prealloc_array_is_array ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -2381,7 +2167,7 @@ let run_construct_prealloc runs0 s c b args =
if nat_eq arg_len 0
then follow s ""
else let_binding (get_arg 0 args) (fun arg ->
- if_string (to_string runs0 s c arg) (fun s0 s1 ->
+ if_string (to_string s c arg) (fun s0 s1 ->
follow s0 s1))))))
| Coq_prealloc_string_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -2477,12 +2263,12 @@ let run_construct_prealloc runs0 s c b args =
(" not yet implemented.")))
(** val run_construct_default :
- runs_type -> state -> execution_ctx -> object_loc -> value list -> __
+ state -> execution_ctx -> object_loc -> value list -> __
specres **)
-let run_construct_default runs0 s c l args =
+and run_construct_default s c l args =
if_value
- (run_object_get runs0 s c l
+ (run_object_get s c l
("prototype"))
(fun s1 v1 ->
let_binding
@@ -2495,7 +2281,7 @@ let run_construct_default runs0 s c l args =
(fun o ->
let_binding (object_alloc s1 o) (fun p ->
let (l', s2) = p in
- if_value (runs0.runs_type_call s2 c l (Coq_value_object l') args)
+ if_value (run_call s2 c l (Coq_value_object l') args)
(fun s3 v2 ->
let_binding
(if type_comparable (type_of v2) Coq_type_object
@@ -2503,12 +2289,12 @@ let run_construct_default runs0 s c l args =
else Coq_value_object l') (fun vr -> res_ter s3 (res_val vr)))))))
(** val run_construct :
- runs_type -> state -> execution_ctx -> construct -> object_loc -> value
+ state -> execution_ctx -> construct -> object_loc -> value
list -> result **)
-let run_construct runs0 s c co l args =
+and run_construct s c co l args =
match co with
- | Coq_construct_default -> run_construct_default runs0 s c l args
+ | Coq_construct_default -> run_construct_default s c l args
| Coq_construct_after_bind ->
if_some (run_object_method object_target_function_ s l) (fun otrg ->
if_some otrg (fun target ->
@@ -2518,14 +2304,14 @@ let run_construct runs0 s c co l args =
if_some (run_object_method object_bound_args_ s l) (fun oarg ->
if_some oarg (fun boundArgs ->
let_binding (LibList.append boundArgs args) (fun arguments_ ->
- runs0.runs_type_construct s c co0 target arguments_)))
+ run_construct s c co0 target arguments_)))
| None -> run_error s Coq_native_error_type)))
- | Coq_construct_prealloc b -> run_construct_prealloc runs0 s c b args
+ | Coq_construct_prealloc b -> run_construct_prealloc s c b args
(** val run_call_default :
- runs_type -> state -> execution_ctx -> object_loc -> result **)
+ state -> execution_ctx -> object_loc -> result **)
-let run_call_default runs0 s c lf =
+and run_call_default s c lf =
let_binding
(result_out (Coq_out_ter (s, (res_val (Coq_value_prim Coq_prim_undef)))))
(fun def ->
@@ -2535,38 +2321,38 @@ let run_call_default runs0 s c lf =
if list_eq_nil_decidable (prog_elements (funcbody_prog bd))
then def
else if_success_or_return
- (runs0.runs_type_prog s c (funcbody_prog bd)) (fun s' ->
+ (run_prog s c (funcbody_prog bd)) (fun s' ->
result_out (Coq_out_ter (s',
(res_val (Coq_value_prim Coq_prim_undef))))) (fun s' rv ->
result_out (Coq_out_ter (s', (res_normal rv))))
| None -> def))
(** val creating_function_object_proto :
- runs_type -> state -> execution_ctx -> object_loc -> result **)
+ state -> execution_ctx -> object_loc -> result **)
-let creating_function_object_proto runs0 s c l =
- if_object (run_construct_prealloc runs0 s c Coq_prealloc_object [])
+and creating_function_object_proto s c l =
+ if_object (run_construct_prealloc s c Coq_prealloc_object [])
(fun s1 lproto ->
let_binding { attributes_data_value = (Coq_value_object l);
attributes_data_writable = true; attributes_data_enumerable = false;
attributes_data_configurable = true } (fun a1 ->
if_bool
- (object_define_own_prop runs0 s1 c lproto
+ (object_define_own_prop s1 c lproto
("constructor")
(descriptor_of_attributes (Coq_attributes_data_of a1)) false)
(fun s2 b ->
let_binding { attributes_data_value = (Coq_value_object lproto);
attributes_data_writable = true; attributes_data_enumerable =
false; attributes_data_configurable = false } (fun a2 ->
- object_define_own_prop runs0 s2 c l
+ object_define_own_prop s2 c l
("prototype")
(descriptor_of_attributes (Coq_attributes_data_of a2)) false))))
(** val creating_function_object :
- runs_type -> state -> execution_ctx -> string list -> funcbody ->
+ state -> execution_ctx -> string list -> funcbody ->
lexical_env -> strictness_flag -> result **)
-let creating_function_object runs0 s c names bd x str =
+and creating_function_object s c names bd x str =
let_binding
(object_new (Coq_value_object (Coq_object_loc_prealloc
Coq_prealloc_function_proto))
@@ -2587,11 +2373,11 @@ let creating_function_object runs0 s c names bd x str =
attributes_data_writable = false; attributes_data_enumerable =
false; attributes_data_configurable = false } (fun a1 ->
if_bool
- (object_define_own_prop runs0 s1 c l
+ (object_define_own_prop s1 c l
("length")
(descriptor_of_attributes (Coq_attributes_data_of a1))
false) (fun s2 b2 ->
- if_bool (creating_function_object_proto runs0 s2 c l)
+ if_bool (creating_function_object_proto s2 c l)
(fun s3 b3 ->
if negb str
then res_ter s3 (res_val (Coq_value_object l))
@@ -2603,13 +2389,13 @@ let creating_function_object runs0 s c names bd x str =
attributes_accessor_configurable = false }
(fun a2 ->
if_bool
- (object_define_own_prop runs0 s3 c l
+ (object_define_own_prop s3 c l
("caller")
(descriptor_of_attributes
(Coq_attributes_accessor_of a2)) false)
(fun s4 b4 ->
if_bool
- (object_define_own_prop runs0 s4 c l
+ (object_define_own_prop s4 c l
("arguments")
(descriptor_of_attributes
(Coq_attributes_accessor_of a2)) false)
@@ -2617,33 +2403,33 @@ let creating_function_object runs0 s c names bd x str =
res_ter s5 (res_val (Coq_value_object l))))))))))))))
(** val binding_inst_formal_params :
- runs_type -> state -> execution_ctx -> env_loc -> value list -> string
+ state -> execution_ctx -> env_loc -> value list -> string
list -> strictness_flag -> result_void **)
-let rec binding_inst_formal_params runs0 s c l args names str =
+and binding_inst_formal_params s c l args names str =
match names with
| [] -> res_void s
| argname :: names' ->
let_binding (hd (Coq_value_prim Coq_prim_undef) args) (fun v ->
let_binding (tl args) (fun args' ->
- if_bool (env_record_has_binding runs0 s c l argname) (fun s1 hb ->
+ if_bool (env_record_has_binding s c l argname) (fun s1 hb ->
let_binding (fun s' ->
if_void
- (env_record_set_mutable_binding runs0 s' c l argname v str)
+ (env_record_set_mutable_binding s' c l argname v str)
(fun s'' ->
- binding_inst_formal_params runs0 s'' c l args' names' str))
+ binding_inst_formal_params s'' c l args' names' str))
(fun follow ->
if hb
then follow s1
else if_void
- (env_record_create_mutable_binding runs0 s1 c l argname
+ (env_record_create_mutable_binding s1 c l argname
None) follow))))
(** val binding_inst_function_decls :
- runs_type -> state -> execution_ctx -> env_loc -> funcdecl list ->
+ state -> execution_ctx -> env_loc -> funcdecl list ->
strictness_flag -> bool -> result_void **)
-let rec binding_inst_function_decls runs0 s c l fds str bconfig =
+and binding_inst_function_decls s c l fds str bconfig =
match fds with
| [] -> res_void s
| fd :: fds' ->
@@ -2652,20 +2438,20 @@ let rec binding_inst_function_decls runs0 s c l fds str bconfig =
let_binding fd.funcdecl_parameters (fun fparams ->
let_binding fd.funcdecl_name (fun fname ->
if_object
- (creating_function_object runs0 s c fparams fbd
+ (creating_function_object s c fparams fbd
c.execution_ctx_variable_env str_fd) (fun s1 fo ->
let_binding (fun s2 ->
if_void
- (env_record_set_mutable_binding runs0 s2 c l fname
+ (env_record_set_mutable_binding s2 c l fname
(Coq_value_object fo) str) (fun s3 ->
- binding_inst_function_decls runs0 s3 c l fds' str bconfig))
+ binding_inst_function_decls s3 c l fds' str bconfig))
(fun follow ->
- if_bool (env_record_has_binding runs0 s1 c l fname)
+ if_bool (env_record_has_binding s1 c l fname)
(fun s2 has ->
if has
then if nat_eq l env_loc_global_env_record
then if_spec
- (run_object_get_prop runs0 s2 c
+ (run_object_get_prop s2 c
(Coq_object_loc_prealloc Coq_prealloc_global)
fname) (fun s3 d ->
match d with
@@ -2682,7 +2468,7 @@ let rec binding_inst_function_decls runs0 s c l fds str bconfig =
attributes_data_configurable =
bconfig } (fun a' ->
if_bool
- (object_define_own_prop runs0 s3 c
+ (object_define_own_prop s3 c
(Coq_object_loc_prealloc
Coq_prealloc_global) fname
(descriptor_of_attributes
@@ -2701,13 +2487,13 @@ let rec binding_inst_function_decls runs0 s c l fds str bconfig =
else follow s3)
else follow s2
else if_void
- (env_record_create_mutable_binding runs0 s2 c l
+ (env_record_create_mutable_binding s2 c l
fname (Some bconfig)) follow)))))))
(** val make_arg_getter :
- runs_type -> state -> execution_ctx -> prop_name -> lexical_env -> result **)
+ state -> execution_ctx -> prop_name -> lexical_env -> result **)
-let make_arg_getter runs0 s c x x0 =
+and make_arg_getter s c x x0 =
let xbd =
strappend ("return ")
(strappend x (";"))
@@ -2715,12 +2501,12 @@ let make_arg_getter runs0 s c x x0 =
let bd = Coq_funcbody_intro ((Coq_prog_intro (true, ((Coq_element_stat
(Coq_stat_return (Some (Coq_expr_identifier x)))) :: []))), xbd)
in
- creating_function_object runs0 s c [] bd x0 true
+ creating_function_object s c [] bd x0 true
(** val make_arg_setter :
- runs_type -> state -> execution_ctx -> prop_name -> lexical_env -> result **)
+ state -> execution_ctx -> prop_name -> lexical_env -> result **)
-let make_arg_setter runs0 s c x x0 =
+and make_arg_setter s c x x0 =
let xparam = strappend x ("_arg") in
let xbd =
strappend x (strappend (" = ") (strappend xparam ";"))
@@ -2729,14 +2515,14 @@ let make_arg_setter runs0 s c x x0 =
(Coq_stat_expr (Coq_expr_assign ((Coq_expr_identifier x), None,
(Coq_expr_identifier xparam))))) :: []))), xbd)
in
- creating_function_object runs0 s c (xparam :: []) bd x0 true
+ creating_function_object s c (xparam :: []) bd x0 true
(** val arguments_object_map_loop :
- runs_type -> state -> execution_ctx -> object_loc -> string list ->
+ state -> execution_ctx -> object_loc -> string list ->
int -> value list -> lexical_env -> strictness_flag -> object_loc ->
string list -> result_void **)
-let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
+and arguments_object_map_loop s c l xs len args x str lmap xsmap =
(fun fO fS n -> if int_eq n 0 then fO () else fS (n-1))
(fun _ ->
if list_eq_nil_decidable xsmap
@@ -2752,11 +2538,11 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
let_binding (take_drop_last args) (fun tdl ->
let (rmlargs, largs) = tdl in
let_binding (fun s0 xsmap0 ->
- arguments_object_map_loop runs0 s0 c l xs len' rmlargs x str lmap
+ arguments_object_map_loop s0 c l xs len' rmlargs x str lmap
xsmap0) (fun arguments_object_map_loop' ->
let_binding (attributes_data_intro_all_true largs) (fun a ->
if_bool
- (object_define_own_prop runs0 s c l
+ (object_define_own_prop s c l
(convert_prim_to_string (Coq_prim_number
(number_of_int len')))
(descriptor_of_attributes (Coq_attributes_data_of a)) false)
@@ -2768,9 +2554,9 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
if or_decidable (bool_comparable str true)
(coq_Mem_decidable string_comparable x0 xsmap)
then arguments_object_map_loop' s1 xsmap
- else if_object (make_arg_getter runs0 s1 c x0 x)
+ else if_object (make_arg_getter s1 c x0 x)
(fun s2 lgetter ->
- if_object (make_arg_setter runs0 s2 c x0 x)
+ if_object (make_arg_setter s2 c x0 x)
(fun s3 lsetter ->
let_binding { attributes_accessor_get =
(Coq_value_object lgetter);
@@ -2779,7 +2565,7 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
false; attributes_accessor_configurable =
true } (fun a' ->
if_bool
- (object_define_own_prop runs0 s3 c lmap
+ (object_define_own_prop s3 c lmap
(convert_prim_to_string (Coq_prim_number
(number_of_int len')))
(descriptor_of_attributes
@@ -2789,20 +2575,20 @@ let rec arguments_object_map_loop runs0 s c l xs len args x str lmap xsmap =
len
(** val arguments_object_map :
- runs_type -> state -> execution_ctx -> object_loc -> string list ->
+ state -> execution_ctx -> object_loc -> string list ->
value list -> lexical_env -> strictness_flag -> result_void **)
-let arguments_object_map runs0 s c l xs args x str =
- if_object (run_construct_prealloc runs0 s c Coq_prealloc_object [])
+and arguments_object_map s c l xs args x str =
+ if_object (run_construct_prealloc s c Coq_prealloc_object [])
(fun s' lmap ->
- arguments_object_map_loop runs0 s' c l xs (LibList.length args) args x
+ arguments_object_map_loop s' c l xs (LibList.length args) args x
str lmap [])
(** val create_arguments_object :
- runs_type -> state -> execution_ctx -> object_loc -> string list ->
+ state -> execution_ctx -> object_loc -> string list ->
value list -> lexical_env -> strictness_flag -> result **)
-let create_arguments_object runs0 s c lf xs args x str =
+and create_arguments_object s c lf xs args x str =
let_binding
(object_create_builtin (Coq_value_object (Coq_object_loc_prealloc
Coq_prealloc_object_proto))
@@ -2815,11 +2601,11 @@ let create_arguments_object runs0 s c lf xs args x str =
attributes_data_writable = true; attributes_data_enumerable = false;
attributes_data_configurable = true } (fun a ->
if_bool
- (object_define_own_prop runs0 s' c l
+ (object_define_own_prop s' c l
("length")
(descriptor_of_attributes (Coq_attributes_data_of a)) false)
(fun s1 b ->
- if_void (arguments_object_map runs0 s1 c l xs args x str)
+ if_void (arguments_object_map s1 c l xs args x str)
(fun s2 ->
if str
then let_binding (Coq_value_object (Coq_object_loc_prealloc
@@ -2829,13 +2615,13 @@ let create_arguments_object runs0 s c lf xs args x str =
attributes_accessor_enumerable = false;
attributes_accessor_configurable = false } (fun a0 ->
if_bool
- (object_define_own_prop runs0 s2 c l
+ (object_define_own_prop s2 c l
("caller")
(descriptor_of_attributes
(Coq_attributes_accessor_of a0)) false)
(fun s3 b' ->
if_bool
- (object_define_own_prop runs0 s3 c l
+ (object_define_own_prop s3 c l
("callee")
(descriptor_of_attributes
(Coq_attributes_accessor_of a0)) false)
@@ -2846,54 +2632,54 @@ let create_arguments_object runs0 s c lf xs args x str =
attributes_data_enumerable = false;
attributes_data_configurable = true } (fun a0 ->
if_bool
- (object_define_own_prop runs0 s2 c l
+ (object_define_own_prop s2 c l
("callee")
(descriptor_of_attributes (Coq_attributes_data_of a0))
false) (fun s3 b' ->
res_ter s3 (res_val (Coq_value_object l)))))))))
(** val binding_inst_arg_obj :
- runs_type -> state -> execution_ctx -> object_loc -> prog -> string
+ state -> execution_ctx -> object_loc -> prog -> string
list -> value list -> env_loc -> result_void **)
-let binding_inst_arg_obj runs0 s c lf p xs args l =
+and binding_inst_arg_obj s c lf p xs args l =
let arguments_ =
"arguments"
in
let_binding (prog_intro_strictness p) (fun str ->
if_object
- (create_arguments_object runs0 s c lf xs args
+ (create_arguments_object s c lf xs args
c.execution_ctx_variable_env 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_
(Coq_value_object largs))
- else env_record_create_set_mutable_binding runs0 s1 c l arguments_ None
+ else env_record_create_set_mutable_binding s1 c l arguments_ None
(Coq_value_object largs) false))
(** val binding_inst_var_decls :
- runs_type -> state -> execution_ctx -> env_loc -> string list -> bool
+ state -> execution_ctx -> env_loc -> string list -> bool
-> strictness_flag -> result_void **)
-let rec binding_inst_var_decls runs0 s c l vds bconfig str =
+and binding_inst_var_decls s c l vds bconfig str =
match vds with
| [] -> res_void s
| vd :: vds' ->
let_binding (fun s0 ->
- binding_inst_var_decls runs0 s0 c l vds' bconfig str) (fun bivd ->
- if_bool (env_record_has_binding runs0 s c l vd) (fun s1 has ->
+ binding_inst_var_decls s0 c l vds' bconfig str) (fun bivd ->
+ if_bool (env_record_has_binding s c l vd) (fun s1 has ->
if has
then bivd s1
else if_void
- (env_record_create_set_mutable_binding runs0 s1 c l vd (Some
+ (env_record_create_set_mutable_binding s1 c l vd (Some
bconfig) (Coq_value_prim Coq_prim_undef) str) bivd))
(** val execution_ctx_binding_inst :
- runs_type -> state -> execution_ctx -> codetype -> object_loc option ->
+ state -> execution_ctx -> codetype -> object_loc option ->
prog -> value list -> result_void **)
-let execution_ctx_binding_inst runs0 s c ct funco p args =
+and execution_ctx_binding_inst s c ct funco p args =
match c.execution_ctx_variable_env with
| [] ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -2906,15 +2692,15 @@ let execution_ctx_binding_inst runs0 s c ct funco p args =
(fun bconfig ->
let_binding (prog_funcdecl p) (fun fds ->
if_void
- (binding_inst_function_decls runs0 s' c l fds str bconfig)
+ (binding_inst_function_decls s' c l fds str bconfig)
(fun s1 ->
if_bool
- (env_record_has_binding runs0 s1 c l
+ (env_record_has_binding s1 c l
("arguments"))
(fun s2 bdefined ->
let_binding (fun s'0 ->
let vds = prog_vardecl p in
- binding_inst_var_decls runs0 s'0 c l vds bconfig str)
+ binding_inst_var_decls s'0 c l vds bconfig str)
(fun follow2 ->
match ct with
| Coq_codetype_func ->
@@ -2923,7 +2709,7 @@ let execution_ctx_binding_inst runs0 s c ct funco p args =
if bdefined
then follow2 s2
else if_void
- (binding_inst_arg_obj runs0 s2 c func p names
+ (binding_inst_arg_obj s2 c func p names
args l) follow2
| None ->
if bdefined
@@ -2941,7 +2727,7 @@ let execution_ctx_binding_inst runs0 s c ct funco p args =
(fun nameso ->
if_some nameso (fun names ->
if_void
- (binding_inst_formal_params runs0 s c l args names str)
+ (binding_inst_formal_params s c l args names str)
(fun s' -> follow s' names)))
| None ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -2963,10 +2749,10 @@ let execution_ctx_binding_inst runs0 s c ct funco p args =
| None -> follow s [])))
(** val entering_func_code :
- runs_type -> state -> execution_ctx -> object_loc -> value -> value list
+ state -> execution_ctx -> object_loc -> value -> value list
-> result **)
-let entering_func_code runs0 s c lf vthis args =
+and entering_func_code s c lf vthis args =
if_some (run_object_method object_code_ s lf) (fun bdo ->
if_some bdo (fun bd ->
let_binding (funcbody_is_strict bd) (fun str ->
@@ -2978,9 +2764,9 @@ let entering_func_code runs0 s c lf vthis args =
let_binding (execution_ctx_intro_same lex' vthis' str)
(fun c' ->
if_void
- (execution_ctx_binding_inst runs0 s1 c' Coq_codetype_func
+ (execution_ctx_binding_inst s1 c' Coq_codetype_func
(Some lf) (funcbody_prog bd) args) (fun s2 ->
- run_call_default runs0 s2 c' lf)))))) (fun follow ->
+ run_call_default s2 c' lf)))))) (fun follow ->
if str
then follow s vthis
else (match vthis with
@@ -2999,10 +2785,10 @@ let entering_func_code runs0 s c lf vthis args =
| Coq_value_object lthis -> follow s vthis)))))
(** val run_object_get_own_prop :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name ->
+ state -> execution_ctx -> object_loc -> prop_name ->
full_descriptor specres **)
-let run_object_get_own_prop runs0 s c l x =
+and run_object_get_own_prop s c l x =
if_some (run_object_method object_get_own_prop_ s l) (fun b ->
let_binding (fun s' ->
if_some (run_object_method object_properties_ s' l) (fun p ->
@@ -3022,14 +2808,14 @@ let run_object_get_own_prop runs0 s c l x =
if_some (run_object_method object_parameter_map_ s1 l)
(fun lmapo ->
if_some lmapo (fun lmap ->
- if_spec (runs0.runs_type_object_get_own_prop s1 c lmap x)
+ if_spec (run_object_get_own_prop s1 c lmap x)
(fun s2 d0 ->
let_binding (fun s' a0 ->
res_spec s' (Coq_full_descriptor_some a0)) (fun follow ->
match d0 with
| Coq_full_descriptor_undef -> follow s2 a
| Coq_full_descriptor_some amap ->
- if_value (run_object_get runs0 s2 c lmap x)
+ if_value (run_object_get s2 c lmap x)
(fun s3 v ->
match a with
| Coq_attributes_data_of ad ->
@@ -3044,17 +2830,17 @@ let run_object_get_own_prop runs0 s c l x =
match d with
| Coq_full_descriptor_undef ->
if_spec
- (to_int32 runs0 s0 c (Coq_value_prim (Coq_prim_string x)))
+ (to_int32 s0 c (Coq_value_prim (Coq_prim_string x)))
(fun s1 k ->
if_string
- (runs0.runs_type_to_string s1 c (Coq_value_prim
+ (to_string s1 c (Coq_value_prim
(Coq_prim_number (JsNumber.absolute k))))
(fun s2 s3 ->
if not_decidable (string_comparable x s3)
then res_spec s2 Coq_full_descriptor_undef
else if_string (run_object_prim_value s2 l) (fun s4 str ->
if_spec
- (to_int32 runs0 s4 c (Coq_value_prim
+ (to_int32 s4 c (Coq_value_prim
(Coq_prim_string x))) (fun s5 k0 ->
let_binding (number_of_int (strlength str)) (fun len ->
if le_int_decidable len k0
@@ -3074,9 +2860,9 @@ let run_object_get_own_prop runs0 s c l x =
| Coq_full_descriptor_some a -> res_spec s0 d)))
(** val run_function_has_instance :
- runs_type -> state -> object_loc -> value -> result **)
+ state -> object_loc -> value -> result **)
-let run_function_has_instance runs0 s lv _foo_ = match _foo_ with
+and run_function_has_instance s lv _foo_ = match _foo_ with
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object lo ->
if_some (run_object_method object_proto_ s lv) (fun vproto ->
@@ -3104,14 +2890,14 @@ let run_function_has_instance runs0 s lv _foo_ = match _foo_ with
| Coq_value_object proto ->
if object_loc_comparable proto lo
then res_ter s (res_val (Coq_value_prim (Coq_prim_bool true)))
- else runs0.runs_type_function_has_instance s proto (Coq_value_object
+ else run_function_has_instance s proto (Coq_value_object
lo))
(** val run_object_has_instance :
- runs_type -> state -> execution_ctx -> builtin_has_instance -> object_loc
+ state -> execution_ctx -> builtin_has_instance -> object_loc
-> value -> result **)
-let run_object_has_instance runs0 s c b l v =
+and run_object_has_instance s c b l v =
match b with
| Coq_builtin_has_instance_function ->
(match v with
@@ -3120,37 +2906,37 @@ let run_object_has_instance runs0 s c b l v =
(res_val (Coq_value_prim (Coq_prim_bool false)))))
| Coq_value_object lv ->
if_value
- (run_object_get runs0 s c l
+ (run_object_get s c l
("prototype"))
(fun s1 vproto ->
match vproto with
| Coq_value_prim p -> run_error s1 Coq_native_error_type
| Coq_value_object lproto ->
- runs0.runs_type_function_has_instance s1 lv (Coq_value_object
+ run_function_has_instance s1 lv (Coq_value_object
lproto)))
| Coq_builtin_has_instance_after_bind ->
if_some (run_object_method object_target_function_ s l) (fun ol ->
if_some ol (fun l0 ->
if_some (run_object_method object_has_instance_ s l0) (fun ob ->
match ob with
- | Some b0 -> runs0.runs_type_object_has_instance s c b0 l0 v
+ | Some b0 -> run_object_has_instance s c b0 l0 v
| None -> run_error s Coq_native_error_type)))
(** val from_prop_descriptor :
- runs_type -> state -> execution_ctx -> full_descriptor -> result **)
+ state -> execution_ctx -> full_descriptor -> result **)
-let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
+and from_prop_descriptor s c _foo_ = match _foo_ with
| Coq_full_descriptor_undef ->
result_out (Coq_out_ter (s, (res_val (Coq_value_prim Coq_prim_undef))))
| Coq_full_descriptor_some a ->
- if_object (run_construct_prealloc runs0 s c Coq_prealloc_object [])
+ if_object (run_construct_prealloc s c Coq_prealloc_object [])
(fun s1 l ->
let_binding (fun s0 x ->
let_binding
(attributes_data_intro_all_true (Coq_value_prim (Coq_prim_bool
(attributes_enumerable a)))) (fun a1 ->
if_bool
- (object_define_own_prop runs0 s0 c l
+ (object_define_own_prop s0 c l
("enumerable")
(descriptor_of_attributes (Coq_attributes_data_of a1))
throw_false) (fun s0' x0 ->
@@ -3158,7 +2944,7 @@ let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
(attributes_data_intro_all_true (Coq_value_prim (Coq_prim_bool
(attributes_configurable a)))) (fun a2 ->
if_bool
- (object_define_own_prop runs0 s0' c l
+ (object_define_own_prop s0' c l
("configurable")
(descriptor_of_attributes (Coq_attributes_data_of a2))
throw_false) (fun s' x1 ->
@@ -3168,7 +2954,7 @@ let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
let_binding (attributes_data_intro_all_true ad.attributes_data_value)
(fun a1 ->
if_bool
- (object_define_own_prop runs0 s1 c l
+ (object_define_own_prop s1 c l
("value")
(descriptor_of_attributes (Coq_attributes_data_of a1))
throw_false) (fun s2 x ->
@@ -3176,7 +2962,7 @@ let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
(attributes_data_intro_all_true (Coq_value_prim (Coq_prim_bool
ad.attributes_data_writable))) (fun a2 ->
if_bool
- (object_define_own_prop runs0 s2 c l
+ (object_define_own_prop s2 c l
("writable")
(descriptor_of_attributes (Coq_attributes_data_of a2))
throw_false) follow)))
@@ -3185,20 +2971,20 @@ let from_prop_descriptor runs0 s c _foo_ = match _foo_ with
(attributes_data_intro_all_true aa.attributes_accessor_get)
(fun a1 ->
if_bool
- (object_define_own_prop runs0 s1 c l ("get")
+ (object_define_own_prop s1 c l ("get")
(descriptor_of_attributes (Coq_attributes_data_of a1))
throw_false) (fun s2 x ->
let_binding
(attributes_data_intro_all_true aa.attributes_accessor_set)
(fun a2 ->
if_bool
- (object_define_own_prop runs0 s2 c l ("set")
+ (object_define_own_prop s2 c l ("set")
(descriptor_of_attributes (Coq_attributes_data_of a2))
throw_false) follow)))))
(** val is_lazy_op : binary_op -> bool option **)
-let is_lazy_op _foo_ = match _foo_ with
+and is_lazy_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> None
| Coq_binary_op_div -> None
| Coq_binary_op_mod -> None
@@ -3227,7 +3013,7 @@ let is_lazy_op _foo_ = match _foo_ with
(** val get_puremath_op :
binary_op -> (number -> number -> number) option **)
-let get_puremath_op _foo_ = match _foo_ with
+and get_puremath_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> Some (fun x y -> x *. y)
| Coq_binary_op_div -> Some (fun x y -> x /. y)
| Coq_binary_op_mod -> Some JsNumber.fmod
@@ -3255,7 +3041,7 @@ let get_puremath_op _foo_ = match _foo_ with
(** val get_inequality_op : binary_op -> (bool * bool) option **)
-let get_inequality_op _foo_ = match _foo_ with
+and get_inequality_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> None
| Coq_binary_op_div -> None
| Coq_binary_op_mod -> None
@@ -3284,7 +3070,7 @@ let get_inequality_op _foo_ = match _foo_ with
(** val get_shift_op :
binary_op -> (bool * (float -> float -> float)) option **)
-let get_shift_op _foo_ = match _foo_ with
+and get_shift_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> None
| Coq_binary_op_div -> None
| Coq_binary_op_mod -> None
@@ -3312,7 +3098,7 @@ let get_shift_op _foo_ = match _foo_ with
(** val get_bitwise_op : binary_op -> (float -> float -> float) option **)
-let get_bitwise_op _foo_ = match _foo_ with
+and get_bitwise_op _foo_ = match _foo_ with
| Coq_binary_op_mult -> None
| Coq_binary_op_div -> None
| Coq_binary_op_mod -> None
@@ -3339,11 +3125,11 @@ let get_bitwise_op _foo_ = match _foo_ with
| Coq_binary_op_coma -> None
(** val run_equal :
- runs_type -> state -> execution_ctx -> value -> value -> result **)
+ state -> execution_ctx -> value -> value -> result **)
-let run_equal runs0 s c v1 v2 =
- let conv_number = fun s0 v -> to_number runs0 s0 c v in
- let conv_primitive = fun s0 v -> to_primitive runs0 s0 c v None in
+and run_equal s c v1 v2 =
+ let conv_number = fun s0 v -> to_number s0 c v in
+ let conv_primitive = fun s0 v -> to_primitive s0 c v None in
let_binding (fun s0 v3 v4 k ->
let ty1 = type_of v3 in
let ty2 = type_of v4 in
@@ -3354,7 +3140,7 @@ let run_equal runs0 s c v1 v2 =
else k ty1 ty2) (fun checkTypesThen ->
checkTypesThen s v1 v2 (fun ty1 ty2 ->
let_binding (fun v3 f v4 ->
- if_value (f s v4) (fun s0 v2' -> runs0.runs_type_equal s0 c v3 v2'))
+ if_value (f s v4) (fun s0 v2' -> run_equal s0 c v3 v2'))
(fun dc_conv ->
let so = fun b ->
result_out (Coq_out_ter (s,
@@ -3401,63 +3187,67 @@ let run_equal runs0 s c v1 v2 =
specres) -> (state -> value -> 'a2 resultof) -> state -> value -> value
-> ('a1 * 'a1) specres **)
-let convert_twice ifv kC s v1 v2 =
+and convert_twice :
+ 'a1 'a2 . ('a2 resultof -> (state -> 'a1 -> ('a1 * 'a1) specres) -> ('a1 * 'a1) specres) ->
+ (state -> value -> 'a2 resultof) -> state -> value -> value -> ('a1 * 'a1) specres
+ = fun ifv kC s v1 v2 ->
ifv (kC s v1) (fun s1 vc1 ->
ifv (kC s1 v2) (fun s2 vc2 -> res_spec s2 (vc1, vc2)))
(** val convert_twice_primitive :
- runs_type -> state -> execution_ctx -> value -> value -> (prim * prim)
+ state -> execution_ctx -> value -> value -> (prim * prim)
specres **)
-let convert_twice_primitive runs0 s c v1 v2 =
- convert_twice if_prim (fun s0 v -> to_primitive runs0 s0 c v None) s v1 v2
+and convert_twice_primitive s c v1 v2 =
+ convert_twice if_prim (fun s0 v -> to_primitive s0 c v None) s v1 v2
(** val convert_twice_number :
- runs_type -> state -> execution_ctx -> value -> value ->
+ state -> execution_ctx -> value -> value ->
(number * number) specres **)
-let convert_twice_number runs0 s c v1 v2 =
- convert_twice if_number (fun s0 v -> to_number runs0 s0 c v) s v1 v2
+and convert_twice_number s c v1 v2 =
+ convert_twice if_number (fun s0 v -> to_number s0 c v) s v1 v2
(** val convert_twice_string :
- runs_type -> state -> execution_ctx -> value -> value ->
+ state -> execution_ctx -> value -> value ->
(string * string) specres **)
-let convert_twice_string runs0 s c v1 v2 =
- convert_twice if_string (fun s0 v -> to_string runs0 s0 c v) s v1 v2
+and convert_twice_string s c v1 v2 =
+ convert_twice if_string (fun s0 v -> to_string s0 c v) s v1 v2
(** val issome : 'a1 option -> bool **)
-let issome _foo_ = match _foo_ with
+and issome : 'a1 . 'a1 option -> bool = fun _foo_ ->
+match _foo_ with
| Some t -> true
| None -> false
(** val run_binary_op :
- runs_type -> state -> execution_ctx -> binary_op -> value -> value ->
+ state -> execution_ctx -> binary_op -> value -> value ->
result **)
-let run_binary_op runs0 s c op v1 v2 =
+and run_binary_op s c op v1 v2 =
if binary_op_comparable op Coq_binary_op_add
- then if_spec (convert_twice_primitive runs0 s c v1 v2) (fun s1 ww ->
+ then if_spec (convert_twice_primitive s c v1 v2) (fun s1 ww ->
let (w1, w2) = ww in
if or_decidable
(type_comparable (type_of (Coq_value_prim w1)) Coq_type_string)
(type_comparable (type_of (Coq_value_prim w2)) Coq_type_string)
then if_spec
- (convert_twice_string runs0 s1 c (Coq_value_prim w1)
+ (convert_twice_string s1 c (Coq_value_prim w1)
(Coq_value_prim w2)) (fun s2 ss ->
let (s3, s4) = ss in
res_out (Coq_out_ter (s2,
(res_val (Coq_value_prim (Coq_prim_string (strappend s3 s4)))))))
else if_spec
- (convert_twice_number runs0 s1 c (Coq_value_prim w1)
+ (convert_twice_number s1 c (Coq_value_prim w1)
(Coq_value_prim w2)) (fun s2 nn ->
let (n1, n2) = nn in
res_out (Coq_out_ter (s2,
(res_val (Coq_value_prim (Coq_prim_number (n1 +. n2))))))))
else if issome (get_puremath_op op)
then if_some (get_puremath_op op) (fun mop ->
- if_spec (convert_twice_number runs0 s c v1 v2) (fun s1 nn ->
+ if_spec (convert_twice_number s c v1 v2) (fun s1 nn ->
let (n1, n2) = nn in
res_out (Coq_out_ter (s1,
(res_val (Coq_value_prim (Coq_prim_number (mop n1 n2))))))))
@@ -3465,17 +3255,17 @@ let run_binary_op runs0 s c op v1 v2 =
then if_some (get_shift_op op) (fun so ->
let (b_unsigned, f) = so in
if_spec
- ((if b_unsigned then to_uint32 else to_int32) runs0 s c
+ ((if b_unsigned then to_uint32 else to_int32) s c
v1) (fun s1 k1 ->
- if_spec (to_uint32 runs0 s1 c v2) (fun s2 k2 ->
+ if_spec (to_uint32 s1 c v2) (fun s2 k2 ->
let k2' = JsNumber.modulo_32 k2 in
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
(of_int (f k1 k2'))))))))
else if issome (get_bitwise_op op)
then if_some (get_bitwise_op op) (fun bo ->
- if_spec (to_int32 runs0 s c v1) (fun s1 k1 ->
- if_spec (to_int32 runs0 s1 c v2) (fun s2 k2 ->
+ if_spec (to_int32 s c v1) (fun s1 k1 ->
+ if_spec (to_int32 s1 c v2) (fun s2 k2 ->
res_ter s2
(res_val (Coq_value_prim (Coq_prim_number
(of_int (bo k1 k2))))))))
@@ -3483,7 +3273,7 @@ let run_binary_op runs0 s c op v1 v2 =
then if_some (get_inequality_op op) (fun io ->
let (b_swap, b_neg) = io in
if_spec
- (convert_twice_primitive runs0 s c v1 v2)
+ (convert_twice_primitive s c v1 v2)
(fun s1 ww ->
let (w1, w2) = ww in
let_binding
@@ -3522,23 +3312,23 @@ let run_binary_op runs0 s c op v1 v2 =
option_case (fun x ->
run_error s Coq_native_error_type)
(fun has_instance_id x ->
- run_object_has_instance runs0 s c
+ run_object_has_instance s c
has_instance_id l v1) b ()))
else if binary_op_comparable op Coq_binary_op_in
then (match v2 with
| Coq_value_prim p ->
run_error s Coq_native_error_type
| Coq_value_object l ->
- if_string (to_string runs0 s c v1)
+ if_string (to_string s c v1)
(fun s2 x ->
- object_has_prop runs0 s2 c l x))
+ object_has_prop s2 c l x))
else if binary_op_comparable op
Coq_binary_op_equal
- then runs0.runs_type_equal s c v1 v2
+ then run_equal s c v1 v2
else if binary_op_comparable op
Coq_binary_op_disequal
then if_bool
- (runs0.runs_type_equal s c
+ (run_equal s c
v1 v2) (fun s0 b0 ->
res_ter s0
(res_val (Coq_value_prim
@@ -3577,7 +3367,7 @@ let run_binary_op runs0 s c op v1 v2 =
(** val run_prepost_op : unary_op -> ((number -> number) * bool) option **)
-let run_prepost_op _foo_ = match _foo_ with
+and run_prepost_op _foo_ = match _foo_ with
| Coq_unary_op_delete -> None
| Coq_unary_op_void -> None
| Coq_unary_op_typeof -> None
@@ -3592,7 +3382,7 @@ let run_prepost_op _foo_ = match _foo_ with
(** val run_typeof_value : state -> value -> string **)
-let run_typeof_value s _foo_ = match _foo_ with
+and run_typeof_value s _foo_ = match _foo_ with
| Coq_value_prim w -> typeof_prim w
| Coq_value_object l ->
if is_callable_dec s (Coq_value_object l)
@@ -3600,26 +3390,26 @@ let run_typeof_value s _foo_ = match _foo_ with
else "object"
(** val run_unary_op :
- runs_type -> state -> execution_ctx -> unary_op -> expr -> result **)
+ state -> execution_ctx -> unary_op -> expr -> result **)
-let run_unary_op runs0 s c op e =
+and run_unary_op s c op e =
if prepost_unary_op_dec op
- then if_success (runs0.runs_type_expr s c e) (fun s1 rv1 ->
- if_spec (ref_get_value runs0 s1 c rv1) (fun s2 v2 ->
- if_number (to_number runs0 s2 c v2) (fun s3 n1 ->
+ then if_success (run_expr s c e) (fun s1 rv1 ->
+ if_spec (ref_get_value s1 c rv1) (fun s2 v2 ->
+ if_number (to_number s2 c v2) (fun s3 n1 ->
if_some (run_prepost_op op) (fun po ->
let (number_op, is_pre) = po in
let_binding (number_op n1) (fun n2 ->
let_binding (Coq_prim_number (if is_pre then n2 else n1))
(fun v ->
if_void
- (ref_put_value runs0 s3 c rv1 (Coq_value_prim
+ (ref_put_value s3 c rv1 (Coq_value_prim
(Coq_prim_number n2))) (fun s4 ->
result_out (Coq_out_ter (s4,
(res_val (Coq_value_prim v)))))))))))
else (match op with
| Coq_unary_op_delete ->
- if_success (runs0.runs_type_expr s c e) (fun s0 rv ->
+ if_success (run_expr s c e) (fun s0 rv ->
match rv with
| Coq_resvalue_empty ->
res_ter s0 (res_val (Coq_value_prim (Coq_prim_bool true)))
@@ -3634,14 +3424,14 @@ let run_unary_op runs0 s c op e =
else (match r.ref_base with
| Coq_ref_base_type_value v ->
if_object (to_object s0 v) (fun s1 l ->
- runs0.runs_type_object_delete s1 c l r.ref_name
+ object_delete s1 c l r.ref_name
r.ref_strict)
| Coq_ref_base_type_env_loc l ->
if r.ref_strict
then run_error s0 Coq_native_error_syntax
- else env_record_delete_binding runs0 s0 c l r.ref_name))
+ else env_record_delete_binding s0 c l r.ref_name))
| Coq_unary_op_void ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v ->
+ 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)
@@ -3669,14 +3459,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3685,7 +3475,7 @@ let run_unary_op runs0 s c op e =
(res_val (Coq_value_prim (Coq_prim_bool
(neg (convert_value_to_boolean v))))))
| Coq_unary_op_typeof ->
- if_success (runs0.runs_type_expr s c e) (fun s1 rv ->
+ if_success (run_expr s c e) (fun s1 rv ->
match rv with
| Coq_resvalue_empty ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -3700,13 +3490,13 @@ let run_unary_op runs0 s c op e =
then res_ter s1
(res_val (Coq_value_prim (Coq_prim_string
("undefined"))))
- else if_spec (ref_get_value runs0 s1 c (Coq_resvalue_ref r))
+ else if_spec (ref_get_value s1 c (Coq_resvalue_ref r))
(fun s2 v ->
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 runs0 s c e) (fun s1 v ->
+ 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)
@@ -3734,14 +3524,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3750,7 +3540,7 @@ let run_unary_op runs0 s c op e =
(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 runs0 s c e) (fun s1 v ->
+ 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)
@@ -3778,14 +3568,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3794,7 +3584,7 @@ let run_unary_op runs0 s c op e =
(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 runs0 s c e) (fun s1 v ->
+ 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)
@@ -3822,14 +3612,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3838,7 +3628,7 @@ let run_unary_op runs0 s c op e =
(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 runs0 s c e) (fun s1 v ->
+ 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)
@@ -3866,14 +3656,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3882,7 +3672,7 @@ let run_unary_op runs0 s c op e =
(res_val (Coq_value_prim (Coq_prim_bool
(neg (convert_value_to_boolean v))))))
| Coq_unary_op_add ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v ->
+ 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)
@@ -3910,14 +3700,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3926,7 +3716,7 @@ let run_unary_op runs0 s c op e =
(res_val (Coq_value_prim (Coq_prim_bool
(neg (convert_value_to_boolean v))))))
| Coq_unary_op_neg ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v ->
+ 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)
@@ -3954,14 +3744,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -3970,7 +3760,7 @@ let run_unary_op runs0 s c op e =
(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 runs0 s c e) (fun s1 v ->
+ 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)
@@ -3998,14 +3788,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -4014,7 +3804,7 @@ let run_unary_op runs0 s c op e =
(res_val (Coq_value_prim (Coq_prim_bool
(neg (convert_value_to_boolean v))))))
| Coq_unary_op_not ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v ->
+ 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)
@@ -4042,14 +3832,14 @@ let run_unary_op runs0 s c op e =
(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 runs0 s1 c v
+ | Coq_unary_op_add -> to_number s1 c v
| Coq_unary_op_neg ->
- if_number (to_number runs0 s1 c v) (fun s2 n ->
+ 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 runs0 s1 c v) (fun s2 k ->
+ 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))))))
@@ -4059,27 +3849,27 @@ let run_unary_op runs0 s c op e =
(neg (convert_value_to_boolean v)))))))
(** val create_new_function_in :
- runs_type -> state -> execution_ctx -> string list -> funcbody ->
+ state -> execution_ctx -> string list -> funcbody ->
result **)
-let create_new_function_in runs0 s c args bd =
- creating_function_object runs0 s c args bd c.execution_ctx_lexical_env
+and create_new_function_in s c args bd =
+ creating_function_object s c args bd c.execution_ctx_lexical_env
c.execution_ctx_strict
(** val init_object :
- runs_type -> state -> execution_ctx -> object_loc -> propdefs -> result **)
+ state -> execution_ctx -> object_loc -> propdefs -> result **)
-let rec init_object runs0 s c l _foo_ = match _foo_ with
+and init_object s c l _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_val (Coq_value_object l))))
| p :: pds' ->
let (pn, pb) = p in
let_binding (string_of_propname pn) (fun x ->
let_binding (fun s1 desc ->
- if_success (object_define_own_prop runs0 s1 c l x desc false)
- (fun s2 rv -> init_object runs0 s2 c l pds')) (fun follows ->
+ if_success (object_define_own_prop s1 c l x desc false)
+ (fun s2 rv -> init_object s2 c l pds')) (fun follows ->
match pb with
| Coq_propbody_val e0 ->
- if_spec (run_expr_get_value runs0 s c e0) (fun s1 v0 ->
+ if_spec (run_expr_get_value s c e0) (fun s1 v0 ->
let desc = { descriptor_value = (Some v0); descriptor_writable =
(Some true); descriptor_get = None; descriptor_set = None;
descriptor_enumerable = (Some true); descriptor_configurable =
@@ -4087,7 +3877,7 @@ let rec init_object runs0 s c l _foo_ = match _foo_ with
in
follows s1 desc)
| Coq_propbody_get bd ->
- if_value (create_new_function_in runs0 s c [] bd) (fun s1 v0 ->
+ if_value (create_new_function_in s c [] bd) (fun s1 v0 ->
let desc = { descriptor_value = None; descriptor_writable = None;
descriptor_get = (Some v0); descriptor_set = None;
descriptor_enumerable = (Some true); descriptor_configurable =
@@ -4095,7 +3885,7 @@ let rec init_object runs0 s c l _foo_ = match _foo_ with
in
follows s1 desc)
| Coq_propbody_set (args, bd) ->
- if_value (create_new_function_in runs0 s c args bd) (fun s1 v0 ->
+ if_value (create_new_function_in s c args bd) (fun s1 v0 ->
let desc = { descriptor_value = None; descriptor_writable = None;
descriptor_get = None; descriptor_set = (Some v0);
descriptor_enumerable = (Some true); descriptor_configurable =
@@ -4104,60 +3894,60 @@ let rec init_object runs0 s c l _foo_ = match _foo_ with
follows s1 desc)))
(** val run_array_element_list :
- runs_type -> state -> execution_ctx -> object_loc -> expr option list ->
+ state -> execution_ctx -> object_loc -> expr option list ->
float -> result **)
-let run_array_element_list runs0 s c l oes n =
+and run_array_element_list s c l oes n =
match oes with
| [] -> result_out (Coq_out_ter (s, (res_val (Coq_value_object l))))
| o :: oes' ->
(match o with
| Some e ->
let_binding (fun s0 ->
- runs0.runs_type_array_element_list s0 c l oes' 0.)
+ run_array_element_list s0 c l oes' 0.)
(fun loop_result ->
- if_spec (run_expr_get_value runs0 s c e) (fun s0 v ->
+ if_spec (run_expr_get_value s c e) (fun s0 v ->
if_value
- (run_object_get runs0 s0 c l
+ (run_object_get s0 c l
("length")) (fun s1 vlen ->
- if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
+ if_spec (to_uint32 s1 c vlen) (fun s2 ilen ->
if_string
- (to_string runs0 s2 c (Coq_value_prim (Coq_prim_number
+ (to_string s2 c (Coq_value_prim (Coq_prim_number
(ilen +. n)))) (fun s3 slen ->
let_binding { attributes_data_value = v;
attributes_data_writable = true;
attributes_data_enumerable = true;
attributes_data_configurable = true } (fun desc ->
if_bool
- (object_define_own_prop runs0 s3 c l slen
+ (object_define_own_prop s3 c l slen
(descriptor_of_attributes (Coq_attributes_data_of
desc)) false) (fun s4 x ->
if_object (loop_result s4) (fun s5 l0 ->
res_ter s5 (res_val (Coq_value_object l0))))))))))
| None ->
let_binding (elision_head_count (None :: oes')) (fun firstIndex ->
- runs0.runs_type_array_element_list s c l
+ run_array_element_list s c l
(elision_head_remove (None :: oes')) (number_of_int firstIndex)))
(** val init_array :
- runs_type -> state -> execution_ctx -> object_loc -> expr option list ->
+ state -> execution_ctx -> object_loc -> expr option list ->
result **)
-let init_array runs0 s c l oes =
+and init_array s c l oes =
let_binding (elision_tail_remove oes) (fun elementList ->
let_binding (elision_tail_count oes) (fun elisionLength ->
- if_object (run_array_element_list runs0 s c l elementList 0.)
+ if_object (run_array_element_list s c l elementList 0.)
(fun s0 l0 ->
if_value
- (run_object_get runs0 s0 c l0
+ (run_object_get s0 c l0
("length")) (fun s1 vlen ->
- if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
+ if_spec (to_uint32 s1 c vlen) (fun s2 ilen ->
if_spec
- (to_uint32 runs0 s2 c (Coq_value_prim (Coq_prim_number
+ (to_uint32 s2 c (Coq_value_prim (Coq_prim_number
(ilen +. number_of_int elisionLength))))
(fun s3 len ->
if_not_throw
- (object_put runs0 s3 c l0
+ (object_put s3 c l0
("length")
(Coq_value_prim (Coq_prim_number (of_int len)))
throw_false) (fun s4 x ->
@@ -4165,13 +3955,13 @@ let init_array runs0 s c l oes =
(res_val (Coq_value_object l0)))))))))))
(** val run_var_decl_item :
- runs_type -> state -> execution_ctx -> prop_name -> expr option -> result **)
+ state -> execution_ctx -> prop_name -> expr option -> result **)
-let run_var_decl_item runs0 s c x _foo_ = match _foo_ with
+and run_var_decl_item s c x _foo_ = match _foo_ with
| Some e ->
- if_spec (identifier_resolution runs0 s c x) (fun s1 ir ->
- if_spec (run_expr_get_value runs0 s1 c e) (fun s2 v ->
- if_void (ref_put_value runs0 s2 c (Coq_resvalue_ref ir) v) (fun s3 ->
+ if_spec (identifier_resolution s c x) (fun s1 ir ->
+ if_spec (run_expr_get_value s1 c e) (fun s2 v ->
+ if_void (ref_put_value s2 c (Coq_resvalue_ref ir) v) (fun s3 ->
result_out (Coq_out_ter (s3,
(res_val (Coq_value_prim (Coq_prim_string x))))))))
| None ->
@@ -4179,73 +3969,73 @@ let run_var_decl_item runs0 s c x _foo_ = match _foo_ with
(res_val (Coq_value_prim (Coq_prim_string x)))))
(** val run_var_decl :
- runs_type -> state -> execution_ctx -> (prop_name * expr option) list ->
+ state -> execution_ctx -> (prop_name * expr option) list ->
result **)
-let rec run_var_decl runs0 s c _foo_ = match _foo_ with
+and run_var_decl s c _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, res_empty))
| y :: xeos' ->
let (x, eo) = y in
- if_value (run_var_decl_item runs0 s c x eo) (fun s1 vname ->
- run_var_decl runs0 s1 c xeos')
+ if_value (run_var_decl_item s c x eo) (fun s1 vname ->
+ run_var_decl s1 c xeos')
(** val run_list_expr :
- runs_type -> state -> execution_ctx -> value list -> expr list -> value
+ state -> execution_ctx -> value list -> expr list -> value
list specres **)
-let rec run_list_expr runs0 s1 c vs _foo_ = match _foo_ with
+and run_list_expr s1 c vs _foo_ = match _foo_ with
| [] -> res_spec s1 (rev vs)
| e :: es' ->
- if_spec (run_expr_get_value runs0 s1 c e) (fun s2 v ->
- run_list_expr runs0 s2 c (v :: vs) es')
+ if_spec (run_expr_get_value s1 c e) (fun s2 v ->
+ run_list_expr s2 c (v :: vs) es')
(** val run_block :
- runs_type -> state -> execution_ctx -> stat list -> result **)
+ state -> execution_ctx -> stat list -> result **)
-let rec run_block runs0 s c _foo_ = match _foo_ with
+and run_block s c _foo_ = match _foo_ with
| [] -> res_ter s (res_normal Coq_resvalue_empty)
| t :: ts_rev' ->
- if_success (run_block runs0 s c ts_rev') (fun s0 rv0 ->
- if_success_state rv0 (runs0.runs_type_stat s0 c t) (fun x x0 ->
+ if_success (run_block s c ts_rev') (fun s0 rv0 ->
+ if_success_state rv0 (run_stat s0 c t) (fun x x0 ->
result_out (Coq_out_ter (x, (res_normal x0)))))
(** val run_expr_binary_op :
- runs_type -> state -> execution_ctx -> binary_op -> expr -> expr ->
+ state -> execution_ctx -> binary_op -> expr -> expr ->
result **)
-let run_expr_binary_op runs0 s c op e1 e2 =
+and run_expr_binary_op s c op e1 e2 =
match is_lazy_op op with
| Some b_ret ->
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
let_binding (convert_value_to_boolean v1) (fun b1 ->
if bool_comparable b1 b_ret
then res_ter s1 (res_val v1)
- else if_spec (run_expr_get_value runs0 s1 c e2) (fun s2 v ->
+ else if_spec (run_expr_get_value s1 c e2) (fun s2 v ->
res_ter s2 (res_val v))))
| None ->
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
- if_spec (run_expr_get_value runs0 s1 c e2) (fun s2 v2 ->
- run_binary_op runs0 s2 c op v1 v2))
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
+ if_spec (run_expr_get_value s1 c e2) (fun s2 v2 ->
+ run_binary_op s2 c op v1 v2))
(** val run_expr_access :
- runs_type -> state -> execution_ctx -> expr -> expr -> result **)
+ state -> execution_ctx -> expr -> expr -> result **)
-let run_expr_access runs0 s c e1 e2 =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
- if_spec (run_expr_get_value runs0 s1 c e2) (fun s2 v2 ->
+and run_expr_access s c e1 e2 =
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
+ if_spec (run_expr_get_value s1 c e2) (fun s2 v2 ->
if or_decidable (value_comparable v1 (Coq_value_prim Coq_prim_undef))
(value_comparable v1 (Coq_value_prim Coq_prim_null))
then run_error s2 Coq_native_error_type
- else if_string (to_string runs0 s2 c v2) (fun s3 x ->
+ else if_string (to_string s2 c v2) (fun s3 x ->
res_ter s3
(res_ref (ref_create_value v1 x c.execution_ctx_strict)))))
(** val run_expr_assign :
- runs_type -> state -> execution_ctx -> binary_op option -> expr -> expr
+ state -> execution_ctx -> binary_op option -> expr -> expr
-> result **)
-let run_expr_assign runs0 s c opo e1 e2 =
- if_success (runs0.runs_type_expr s c e1) (fun s1 rv1 ->
+and run_expr_assign s c opo e1 e2 =
+ if_success (run_expr s c e1) (fun s1 rv1 ->
let_binding (fun s0 rv' ->
match rv' with
| Coq_resvalue_empty ->
@@ -4253,7 +4043,7 @@ let run_expr_assign runs0 s c opo e1 e2 =
s0
("Non-value result in [run_expr_assign].")
| Coq_resvalue_value v ->
- if_void (ref_put_value runs0 s0 c rv1 v) (fun s' ->
+ if_void (ref_put_value s0 c rv1 v) (fun s' ->
result_out (Coq_out_ter (s', (res_val v))))
| Coq_resvalue_ref r ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4262,18 +4052,18 @@ let run_expr_assign runs0 s c opo e1 e2 =
(fun follow ->
match opo with
| Some op ->
- if_spec (ref_get_value runs0 s1 c rv1) (fun s2 v1 ->
- if_spec (run_expr_get_value runs0 s2 c e2) (fun s3 v2 ->
- if_success (run_binary_op runs0 s3 c op v1 v2) follow))
+ if_spec (ref_get_value s1 c rv1) (fun s2 v1 ->
+ if_spec (run_expr_get_value s2 c e2) (fun s3 v2 ->
+ if_success (run_binary_op s3 c op v1 v2) follow))
| None ->
- if_spec (run_expr_get_value runs0 s1 c e2) (fun x x0 ->
+ if_spec (run_expr_get_value s1 c e2) (fun x x0 ->
follow x (Coq_resvalue_value x0))))
(** val run_expr_function :
- runs_type -> state -> execution_ctx -> prop_name option -> string list
+ state -> execution_ctx -> prop_name option -> string list
-> funcbody -> result **)
-let run_expr_function runs0 s c fo args bd =
+and run_expr_function s c fo args bd =
match fo with
| Some fn ->
let_binding (lexical_env_alloc_decl s c.execution_ctx_lexical_env)
@@ -4283,7 +4073,7 @@ let run_expr_function runs0 s c fo args bd =
if_some (env_record_binds_pickable_option s' l) (fun e ->
if_void (env_record_create_immutable_binding s' l fn) (fun s1 ->
if_object
- (creating_function_object runs0 s1 c args bd lex'
+ (creating_function_object s1 c args bd lex'
(funcbody_is_strict bd)) (fun s2 l0 ->
if_void
(env_record_initialize_immutable_binding s2 l fn
@@ -4298,13 +4088,13 @@ let run_expr_function runs0 s c fo args bd =
(fun l x -> follow l) ())
| None ->
let lex = c.execution_ctx_lexical_env in
- creating_function_object runs0 s c args bd lex (funcbody_is_strict bd)
+ creating_function_object s c args bd lex (funcbody_is_strict bd)
(** val entering_eval_code :
- runs_type -> state -> execution_ctx -> bool -> funcbody -> (state ->
+ state -> execution_ctx -> bool -> funcbody -> (state ->
execution_ctx -> result) -> result **)
-let entering_eval_code runs0 s c direct bd k =
+and entering_eval_code s c direct bd k =
let_binding
(coq_or (funcbody_is_strict bd) ( direct && c.execution_ctx_strict))
(fun str ->
@@ -4318,13 +4108,13 @@ let entering_eval_code runs0 s c direct bd k =
(fun c1 ->
let_binding (funcbody_prog bd) (fun p0 ->
if_void
- (execution_ctx_binding_inst runs0 s' c1 Coq_codetype_eval None
+ (execution_ctx_binding_inst s' c1 Coq_codetype_eval None
p0 []) (fun s1 -> k s1 c1))))))
(** val run_eval :
- runs_type -> state -> execution_ctx -> bool -> value list -> result **)
+ state -> execution_ctx -> bool -> value list -> result **)
-let run_eval runs0 s c is_direct_call vs =
+and run_eval s c is_direct_call vs =
match get_arg 0 vs with
| Coq_value_prim p ->
(match p with
@@ -4344,9 +4134,9 @@ let run_eval runs0 s c is_direct_call vs =
(fun str ->
match parse_pickable s0 str with
| Some p0 ->
- entering_eval_code runs0 s c is_direct_call (Coq_funcbody_intro
+ entering_eval_code s c is_direct_call (Coq_funcbody_intro
(p0, s0)) (fun s1 c' ->
- if_ter (runs0.runs_type_prog s1 c' p0) (fun s2 r ->
+ if_ter (run_prog s1 c' p0) (fun s2 r ->
match r.res_type with
| Coq_restype_normal ->
if_empty_label s2 r (fun x ->
@@ -4376,13 +4166,13 @@ let run_eval runs0 s c is_direct_call vs =
result_out (Coq_out_ter (s, (res_val (Coq_value_object o))))
(** val run_expr_call :
- runs_type -> state -> execution_ctx -> expr -> expr list -> result **)
+ state -> execution_ctx -> expr -> expr list -> result **)
-let run_expr_call runs0 s c e1 e2s =
+and run_expr_call s c e1 e2s =
let_binding (is_syntactic_eval e1) (fun is_eval_direct ->
- if_success (runs0.runs_type_expr s c e1) (fun s1 rv ->
- if_spec (ref_get_value runs0 s1 c rv) (fun s2 f ->
- if_spec (run_list_expr runs0 s2 c [] e2s) (fun s3 vs ->
+ if_success (run_expr s c e1) (fun s1 rv ->
+ if_spec (ref_get_value s1 c rv) (fun s2 f ->
+ if_spec (run_list_expr s2 c [] e2s) (fun s3 vs ->
match f with
| Coq_value_prim p -> run_error s3 Coq_native_error_type
| Coq_value_object l ->
@@ -4390,8 +4180,8 @@ let run_expr_call runs0 s c e1 e2s =
then let_binding (fun vthis ->
if object_loc_comparable l (Coq_object_loc_prealloc
Coq_prealloc_global_eval)
- then run_eval runs0 s3 c is_eval_direct vs
- else runs0.runs_type_call s3 c l vthis vs) (fun follow ->
+ then run_eval s3 c is_eval_direct vs
+ else run_call s3 c l vthis vs) (fun follow ->
match rv with
| Coq_resvalue_empty ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4419,82 +4209,82 @@ let run_expr_call runs0 s c e1 e2s =
else run_error s3 Coq_native_error_type))))
(** val run_expr_conditionnal :
- runs_type -> state -> execution_ctx -> expr -> expr -> expr -> result **)
+ state -> execution_ctx -> expr -> expr -> expr -> result **)
-let run_expr_conditionnal runs0 s c e1 e2 e3 =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
+and run_expr_conditionnal s c e1 e2 e3 =
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
let_binding (convert_value_to_boolean v1) (fun b ->
let_binding (if b then e2 else e3) (fun e ->
- if_spec (run_expr_get_value runs0 s1 c e) (fun s0 r ->
+ if_spec (run_expr_get_value s1 c e) (fun s0 r ->
res_ter s0 (res_val r)))))
(** val run_expr_new :
- runs_type -> state -> execution_ctx -> expr -> expr list -> result **)
+ state -> execution_ctx -> expr -> expr list -> result **)
-let run_expr_new runs0 s c e1 e2s =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v ->
- if_spec (run_list_expr runs0 s1 c [] e2s) (fun s2 args ->
+and run_expr_new s c e1 e2s =
+ if_spec (run_expr_get_value s c e1) (fun s1 v ->
+ if_spec (run_list_expr s1 c [] e2s) (fun s2 args ->
match v with
| Coq_value_prim p -> run_error s2 Coq_native_error_type
| Coq_value_object l ->
if_some (run_object_method object_construct_ s2 l) (fun coo ->
match coo with
- | Some co -> run_construct runs0 s2 c co l args
+ | Some co -> run_construct s2 c co l args
| None -> run_error s2 Coq_native_error_type)))
(** val run_stat_label :
- runs_type -> state -> execution_ctx -> label -> stat -> result **)
+ state -> execution_ctx -> label -> stat -> result **)
-let run_stat_label runs0 s c lab t =
- if_break (runs0.runs_type_stat s c t) (fun s1 r1 ->
+and run_stat_label s c lab t =
+ if_break (run_stat s c t) (fun s1 r1 ->
result_out (Coq_out_ter (s1,
(if label_comparable r1.res_label lab
then res_normal r1.res_value
else r1))))
(** val run_stat_with :
- runs_type -> state -> execution_ctx -> expr -> stat -> result **)
+ state -> execution_ctx -> expr -> stat -> result **)
-let run_stat_with runs0 s c e1 t2 =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
+and run_stat_with s c e1 t2 =
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
if_object (to_object s1 v1) (fun s2 l ->
let_binding c.execution_ctx_lexical_env (fun lex ->
let_binding (lexical_env_alloc_object s2 lex l provide_this_true)
(fun p ->
let (lex', s3) = p in
let_binding (execution_ctx_with_lex c lex') (fun c' ->
- runs0.runs_type_stat s3 c' t2)))))
+ run_stat s3 c' t2)))))
(** val run_stat_if :
- runs_type -> state -> execution_ctx -> expr -> stat -> stat option ->
+ state -> execution_ctx -> expr -> stat -> stat option ->
result **)
-let run_stat_if runs0 s c e1 t2 to0 =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
+and run_stat_if s c e1 t2 to0 =
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
let_binding (convert_value_to_boolean v1) (fun b ->
if b
- then runs0.runs_type_stat s1 c t2
+ then run_stat s1 c t2
else (match to0 with
- | Some t3 -> runs0.runs_type_stat s1 c t3
+ | Some t3 -> run_stat s1 c t3
| None ->
result_out (Coq_out_ter (s1, (res_normal Coq_resvalue_empty))))))
(** val run_stat_while :
- runs_type -> state -> execution_ctx -> resvalue -> label_set -> expr ->
+ state -> execution_ctx -> resvalue -> label_set -> expr ->
stat -> result **)
-let run_stat_while runs0 s c rv labs e1 t2 =
- if_spec (run_expr_get_value runs0 s c e1) (fun s1 v1 ->
+and run_stat_while s c rv labs e1 t2 =
+ if_spec (run_expr_get_value s c e1) (fun s1 v1 ->
let_binding (convert_value_to_boolean v1) (fun b ->
if b
- then if_ter (runs0.runs_type_stat s1 c t2) (fun s2 r ->
+ then if_ter (run_stat s1 c t2) (fun s2 r ->
let_binding
(if not_decidable
(resvalue_comparable r.res_value Coq_resvalue_empty)
then r.res_value
else rv) (fun rv' ->
let_binding (fun x ->
- runs0.runs_type_stat_while s2 c rv' labs e1 t2) (fun loop ->
+ run_stat_while s2 c rv' labs e1 t2) (fun loop ->
if or_decidable
(not_decidable
(restype_comparable r.res_type Coq_restype_continue))
@@ -4512,85 +4302,85 @@ let run_stat_while runs0 s c rv labs e1 t2 =
else res_ter s1 (res_normal rv)))
(** val run_stat_switch_end :
- runs_type -> state -> execution_ctx -> resvalue -> switchclause list ->
+ state -> execution_ctx -> resvalue -> switchclause list ->
result **)
-let rec run_stat_switch_end runs0 s c rv _foo_ = match _foo_ with
+and run_stat_switch_end s c rv _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_normal rv)))
| y :: scs' ->
match y with Coq_switchclause_intro (e, ts) ->
- if_success_state rv (run_block runs0 s c (rev ts)) (fun s1 rv1 ->
- run_stat_switch_end runs0 s1 c rv1 scs')
+ if_success_state rv (run_block s c (rev ts)) (fun s1 rv1 ->
+ run_stat_switch_end s1 c rv1 scs')
(** val run_stat_switch_no_default :
- runs_type -> state -> execution_ctx -> value -> resvalue -> switchclause
+ state -> execution_ctx -> value -> resvalue -> switchclause
list -> result **)
-let rec run_stat_switch_no_default runs0 s c vi rv _foo_ = match _foo_ with
+and run_stat_switch_no_default s c vi rv _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_normal rv)))
| y :: scs' ->
match y with Coq_switchclause_intro (e, ts) ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
+ if_spec (run_expr_get_value s c e) (fun s1 v1 ->
let_binding (strict_equality_test v1 vi) (fun b ->
if b
- then if_success (run_block runs0 s1 c (rev ts)) (fun s2 rv2 ->
- run_stat_switch_end runs0 s2 c rv2 scs')
- else run_stat_switch_no_default runs0 s1 c vi rv scs'))
+ then if_success (run_block s1 c (rev ts)) (fun s2 rv2 ->
+ run_stat_switch_end s2 c rv2 scs')
+ else run_stat_switch_no_default s1 c vi rv scs'))
(** val run_stat_switch_with_default_default :
- runs_type -> state -> execution_ctx -> stat list -> switchclause list ->
+ state -> execution_ctx -> stat list -> switchclause list ->
result **)
-let run_stat_switch_with_default_default runs0 s c ts scs =
- if_success (run_block runs0 s c (rev ts)) (fun s1 rv ->
- run_stat_switch_end runs0 s1 c rv scs)
+and run_stat_switch_with_default_default s c ts scs =
+ if_success (run_block s c (rev ts)) (fun s1 rv ->
+ run_stat_switch_end s1 c rv scs)
(** val run_stat_switch_with_default_B :
- runs_type -> state -> execution_ctx -> value -> resvalue -> stat list ->
+ state -> execution_ctx -> value -> resvalue -> stat list ->
switchclause list -> result **)
-let rec run_stat_switch_with_default_B runs0 s c vi rv ts0 scs = match scs with
-| [] -> run_stat_switch_with_default_default runs0 s c ts0 scs
+and run_stat_switch_with_default_B s c vi rv ts0 scs = match scs with
+| [] -> run_stat_switch_with_default_default s c ts0 scs
| y :: scs' ->
match y with Coq_switchclause_intro (e, ts) ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
+ if_spec (run_expr_get_value s c e) (fun s1 v1 ->
let_binding (strict_equality_test v1 vi) (fun b ->
if b
- then if_success (run_block runs0 s1 c (rev ts)) (fun s2 rv2 ->
- run_stat_switch_end runs0 s2 c rv2 scs')
- else run_stat_switch_with_default_B runs0 s1 c vi rv ts0 scs'))
+ then if_success (run_block s1 c (rev ts)) (fun s2 rv2 ->
+ run_stat_switch_end s2 c rv2 scs')
+ else run_stat_switch_with_default_B s1 c vi rv ts0 scs'))
(** val run_stat_switch_with_default_A :
- runs_type -> state -> execution_ctx -> bool -> value -> resvalue ->
+ state -> execution_ctx -> bool -> value -> resvalue ->
switchclause list -> stat list -> switchclause list -> result **)
-let rec run_stat_switch_with_default_A runs0 s c found vi rv scs1 ts0 scs2 =
+and run_stat_switch_with_default_A s c found vi rv scs1 ts0 scs2 =
match scs1 with
| [] ->
if found
- then run_stat_switch_with_default_default runs0 s c ts0 scs2
- else run_stat_switch_with_default_B runs0 s c vi rv ts0 scs2
+ then run_stat_switch_with_default_default s c ts0 scs2
+ else run_stat_switch_with_default_B s c vi rv ts0 scs2
| y :: scs' ->
match y with Coq_switchclause_intro (e, ts) ->
let_binding (fun s0 ->
- if_success_state rv (run_block runs0 s0 c (rev ts)) (fun s1 rv0 ->
- run_stat_switch_with_default_A runs0 s1 c true vi rv0 scs' ts0 scs2))
+ if_success_state rv (run_block s0 c (rev ts)) (fun s1 rv0 ->
+ run_stat_switch_with_default_A s1 c true vi rv0 scs' ts0 scs2))
(fun follow ->
if found
then follow s
- else if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
+ else if_spec (run_expr_get_value s c e) (fun s1 v1 ->
let_binding (strict_equality_test v1 vi) (fun b ->
if b
then follow s1
- else run_stat_switch_with_default_A runs0 s1 c false vi rv
+ else run_stat_switch_with_default_A s1 c false vi rv
scs' ts0 scs2)))
(** val run_stat_switch :
- runs_type -> state -> execution_ctx -> label_set -> expr -> switchbody ->
+ state -> execution_ctx -> label_set -> expr -> switchbody ->
result **)
-let run_stat_switch runs0 s c labs e sb =
- if_spec (run_expr_get_value runs0 s c e) (fun s1 vi ->
+and run_stat_switch s c labs e sb =
+ if_spec (run_expr_get_value s c e) (fun s1 vi ->
let_binding (fun w ->
if_success
(if_break w (fun s2 r ->
@@ -4601,27 +4391,27 @@ let run_stat_switch runs0 s c labs e sb =
match sb with
| Coq_switchbody_nodefault scs ->
follow
- (run_stat_switch_no_default runs0 s1 c vi Coq_resvalue_empty scs)
+ (run_stat_switch_no_default s1 c vi Coq_resvalue_empty scs)
| Coq_switchbody_withdefault (scs1, ts, scs2) ->
follow
- (run_stat_switch_with_default_A runs0 s1 c false vi
+ (run_stat_switch_with_default_A s1 c false vi
Coq_resvalue_empty scs1 ts scs2)))
(** val run_stat_do_while :
- runs_type -> state -> execution_ctx -> resvalue -> label_set -> expr ->
+ state -> execution_ctx -> resvalue -> label_set -> expr ->
stat -> result **)
-let run_stat_do_while runs0 s c rv labs e1 t2 =
- if_ter (runs0.runs_type_stat s c t2) (fun s1 r ->
+and run_stat_do_while s c rv labs e1 t2 =
+ if_ter (run_stat s c t2) (fun s1 r ->
let_binding
(if resvalue_comparable r.res_value Coq_resvalue_empty
then rv
else r.res_value) (fun rv' ->
let_binding (fun x ->
- if_spec (run_expr_get_value runs0 s1 c e1) (fun s2 v1 ->
+ if_spec (run_expr_get_value s1 c e1) (fun s2 v1 ->
let_binding (convert_value_to_boolean v1) (fun b ->
if b
- then runs0.runs_type_stat_do_while s2 c rv' labs e1 t2
+ then run_stat_do_while s2 c rv' labs e1 t2
else res_ter s2 (res_normal rv')))) (fun loop ->
if and_decidable (restype_comparable r.res_type Coq_restype_continue)
(bool_decidable (res_label_in r labs))
@@ -4636,16 +4426,16 @@ let run_stat_do_while runs0 s c rv labs e1 t2 =
else loop ())))
(** val run_stat_try :
- runs_type -> state -> execution_ctx -> stat -> (prop_name * stat) option
+ state -> execution_ctx -> stat -> (prop_name * stat) option
-> stat option -> result **)
-let run_stat_try runs0 s c t1 t2o t3o =
+and run_stat_try s c t1 t2o t3o =
let_binding (fun s1 r ->
match t3o with
| Some t3 ->
- if_success (runs0.runs_type_stat s1 c t3) (fun s2 rv' -> res_ter s2 r)
+ if_success (run_stat s1 c t3) (fun s2 rv' -> res_ter s2 r)
| None -> res_ter s1 r) (fun finallycont ->
- if_any_or_throw (runs0.runs_type_stat s c t1) finallycont (fun s1 v ->
+ if_any_or_throw (run_stat s c t1) finallycont (fun s1 v ->
match t2o with
| Some y ->
let (x, t2) = y in
@@ -4659,44 +4449,44 @@ let run_stat_try runs0 s c t1 t2o t3o =
("Empty lexical environnment in [run_stat_try].")
| l :: oldlex ->
if_void
- (env_record_create_set_mutable_binding runs0 s' c l x None v
+ (env_record_create_set_mutable_binding s' c l x None v
throw_irrelevant) (fun s2 ->
let c' = execution_ctx_with_lex c lex' in
- if_ter (runs0.runs_type_stat s2 c' t2) finallycont))))
+ if_ter (run_stat s2 c' t2) finallycont))))
| None -> finallycont s1 (res_throw (Coq_resvalue_value v))))
(** val run_stat_throw :
- runs_type -> state -> execution_ctx -> expr -> result **)
+ state -> execution_ctx -> expr -> result **)
-let run_stat_throw runs0 s c e =
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
+and run_stat_throw s c e =
+ if_spec (run_expr_get_value s c e) (fun s1 v1 ->
res_ter s1 (res_throw (Coq_resvalue_value v1)))
(** val run_stat_return :
- runs_type -> state -> execution_ctx -> expr option -> result **)
+ state -> execution_ctx -> expr option -> result **)
-let run_stat_return runs0 s c _foo_ = match _foo_ with
+and run_stat_return s c _foo_ = match _foo_ with
| Some e ->
- if_spec (run_expr_get_value runs0 s c e) (fun s1 v1 ->
+ if_spec (run_expr_get_value s c e) (fun s1 v1 ->
res_ter s1 (res_return (Coq_resvalue_value v1)))
| None ->
result_out (Coq_out_ter (s,
(res_return (Coq_resvalue_value (Coq_value_prim Coq_prim_undef)))))
(** val run_stat_for_loop :
- runs_type -> state -> execution_ctx -> label_set -> resvalue -> expr
+ state -> execution_ctx -> label_set -> resvalue -> expr
option -> expr option -> stat -> result **)
-let run_stat_for_loop runs0 s c labs rv eo2 eo3 t =
+and run_stat_for_loop s c labs rv eo2 eo3 t =
let_binding (fun s0 ->
- if_ter (runs0.runs_type_stat s0 c t) (fun s1 r ->
+ if_ter (run_stat s0 c t) (fun s1 r ->
let_binding
(if not_decidable
(resvalue_comparable r.res_value Coq_resvalue_empty)
then r.res_value
else rv) (fun rv' ->
let_binding (fun s2 ->
- runs0.runs_type_stat_for_loop s2 c labs rv' eo2 eo3 t) (fun loop ->
+ run_stat_for_loop s2 c labs rv' eo2 eo3 t) (fun loop ->
if and_decidable (restype_comparable r.res_type Coq_restype_break)
(bool_decidable (res_label_in r labs))
then res_ter s1 (res_normal rv')
@@ -4707,93 +4497,93 @@ let run_stat_for_loop runs0 s c labs rv eo2 eo3 t =
(bool_decidable (res_label_in r labs)))
then (match eo3 with
| Some e3 ->
- if_spec (run_expr_get_value runs0 s1 c e3)
+ if_spec (run_expr_get_value s1 c e3)
(fun s2 v3 -> loop s2)
| None -> loop s1)
else res_ter s1 r)))) (fun follows ->
match eo2 with
| Some e2 ->
- if_spec (run_expr_get_value runs0 s c e2) (fun s0 v2 ->
+ if_spec (run_expr_get_value s c e2) (fun s0 v2 ->
let_binding (convert_value_to_boolean v2) (fun b ->
if b then follows s0 else res_ter s0 (res_normal rv)))
| None -> follows s)
(** val run_stat_for :
- runs_type -> state -> execution_ctx -> label_set -> expr option -> expr
+ state -> execution_ctx -> label_set -> expr option -> expr
option -> expr option -> stat -> result **)
-let run_stat_for runs0 s c labs eo1 eo2 eo3 t =
+and run_stat_for s c labs eo1 eo2 eo3 t =
let follows = fun s0 ->
- runs0.runs_type_stat_for_loop s0 c labs Coq_resvalue_empty eo2 eo3 t
+ run_stat_for_loop s0 c labs Coq_resvalue_empty eo2 eo3 t
in
(match eo1 with
| Some e1 ->
- if_spec (run_expr_get_value runs0 s c e1) (fun s0 v1 -> follows s0)
+ if_spec (run_expr_get_value s c e1) (fun s0 v1 -> follows s0)
| None -> follows s)
(** val run_stat_for_var :
- runs_type -> state -> execution_ctx -> label_set -> (string * expr
+ state -> execution_ctx -> label_set -> (string * expr
option) list -> expr option -> expr option -> stat -> result **)
-let run_stat_for_var runs0 s c labs ds eo2 eo3 t =
- if_ter (runs0.runs_type_stat s c (Coq_stat_var_decl ds)) (fun s0 r ->
- runs0.runs_type_stat_for_loop s0 c labs Coq_resvalue_empty eo2 eo3 t)
+and run_stat_for_var s c labs ds eo2 eo3 t =
+ if_ter (run_stat s c (Coq_stat_var_decl ds)) (fun s0 r ->
+ run_stat_for_loop s0 c labs Coq_resvalue_empty eo2 eo3 t)
-(** val run_expr : runs_type -> state -> execution_ctx -> expr -> result **)
+(** val run_expr : state -> execution_ctx -> expr -> result **)
-let run_expr runs0 s c _term_ = match _term_ with
+and run_expr s c _term_ = match _term_ with
| Coq_expr_this ->
result_out (Coq_out_ter (s, (res_val c.execution_ctx_this_binding)))
| Coq_expr_identifier x ->
- if_spec (identifier_resolution runs0 s c x) (fun s0 r ->
+ if_spec (identifier_resolution s c x) (fun s0 r ->
res_ter s0 (res_ref r))
| Coq_expr_literal i ->
result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (convert_literal_to_prim i)))))
| Coq_expr_object pds ->
- if_object (run_construct_prealloc runs0 s c Coq_prealloc_object [])
- (fun s1 l -> init_object runs0 s1 c l pds)
+ if_object (run_construct_prealloc s c Coq_prealloc_object [])
+ (fun s1 l -> init_object s1 c l pds)
| Coq_expr_array oes ->
- if_object (run_construct_prealloc runs0 s c Coq_prealloc_array [])
- (fun s1 l -> init_array runs0 s1 c l oes)
-| Coq_expr_function (fo, args, bd) -> run_expr_function runs0 s c fo args bd
-| Coq_expr_access (e1, e2) -> run_expr_access runs0 s c e1 e2
+ if_object (run_construct_prealloc s c Coq_prealloc_array [])
+ (fun s1 l -> init_array s1 c l oes)
+| Coq_expr_function (fo, args, bd) -> run_expr_function s c fo args bd
+| Coq_expr_access (e1, e2) -> run_expr_access s c e1 e2
| Coq_expr_member (e1, f) ->
- runs0.runs_type_expr s c (Coq_expr_access (e1, (Coq_expr_literal
+ run_expr s c (Coq_expr_access (e1, (Coq_expr_literal
(Coq_literal_string f))))
-| Coq_expr_new (e1, e2s) -> run_expr_new runs0 s c e1 e2s
-| Coq_expr_call (e1, e2s) -> run_expr_call runs0 s c e1 e2s
-| Coq_expr_unary_op (op, e0) -> run_unary_op runs0 s c op e0
-| Coq_expr_binary_op (e1, op, e2) -> run_expr_binary_op runs0 s c op e1 e2
+| Coq_expr_new (e1, e2s) -> run_expr_new s c e1 e2s
+| Coq_expr_call (e1, e2s) -> run_expr_call s c e1 e2s
+| Coq_expr_unary_op (op, e0) -> run_unary_op s c op e0
+| Coq_expr_binary_op (e1, op, e2) -> run_expr_binary_op s c op e1 e2
| Coq_expr_conditional (e1, e2, e3) ->
- run_expr_conditionnal runs0 s c e1 e2 e3
-| Coq_expr_assign (e1, opo, e2) -> run_expr_assign runs0 s c opo e1 e2
+ run_expr_conditionnal s c e1 e2 e3
+| Coq_expr_assign (e1, opo, e2) -> run_expr_assign s c opo e1 e2
-(** val run_stat : runs_type -> state -> execution_ctx -> stat -> result **)
+(** val run_stat : state -> execution_ctx -> stat -> result **)
-let run_stat runs0 s c _term_ = match _term_ with
+and run_stat s c _term_ = match _term_ with
| Coq_stat_expr e ->
- if_spec (run_expr_get_value runs0 s c e) (fun s0 r ->
+ if_spec (run_expr_get_value s c e) (fun s0 r ->
res_ter s0 (res_val r))
| Coq_stat_label (lab, t0) ->
- run_stat_label runs0 s c (Coq_label_string lab) t0
-| Coq_stat_block ts -> run_block runs0 s c (rev ts)
-| Coq_stat_var_decl xeos -> run_var_decl runs0 s c xeos
-| Coq_stat_if (e1, t2, to0) -> run_stat_if runs0 s c e1 t2 to0
+ run_stat_label s c (Coq_label_string lab) t0
+| Coq_stat_block ts -> run_block s c (rev ts)
+| Coq_stat_var_decl xeos -> run_var_decl s c xeos
+| Coq_stat_if (e1, t2, to0) -> run_stat_if s c e1 t2 to0
| Coq_stat_do_while (ls, t1, e2) ->
- runs0.runs_type_stat_do_while s c Coq_resvalue_empty ls e2 t1
+ run_stat_do_while s c Coq_resvalue_empty ls e2 t1
| Coq_stat_while (ls, e1, t2) ->
- runs0.runs_type_stat_while s c Coq_resvalue_empty ls e1 t2
-| Coq_stat_with (e1, t2) -> run_stat_with runs0 s c e1 t2
-| Coq_stat_throw e -> run_stat_throw runs0 s c e
-| Coq_stat_return eo -> run_stat_return runs0 s c eo
+ run_stat_while s c Coq_resvalue_empty ls e1 t2
+| Coq_stat_with (e1, t2) -> run_stat_with s c e1 t2
+| Coq_stat_throw e -> run_stat_throw s c e
+| Coq_stat_return eo -> run_stat_return s c eo
| Coq_stat_break so -> result_out (Coq_out_ter (s, (res_break so)))
| Coq_stat_continue so -> result_out (Coq_out_ter (s, (res_continue so)))
-| Coq_stat_try (t1, t2o, t3o) -> run_stat_try runs0 s c t1 t2o t3o
+| Coq_stat_try (t1, t2o, t3o) -> run_stat_try s c t1 t2o t3o
| Coq_stat_for (ls, eo1, eo2, eo3, s0) ->
- run_stat_for runs0 s c ls eo1 eo2 eo3 s0
+ run_stat_for s c ls eo1 eo2 eo3 s0
| Coq_stat_for_var (ls, ds, eo2, eo3, s0) ->
- run_stat_for_var runs0 s c ls ds eo2 eo3 s0
+ run_stat_for_var s c ls ds eo2 eo3 s0
| Coq_stat_for_in (ls, e1, e2, s0) ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
("stat_for_in")
@@ -4801,56 +4591,56 @@ let run_stat runs0 s c _term_ = match _term_ with
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
("stat_for_in_var")
| Coq_stat_debugger -> result_out (Coq_out_ter (s, res_empty))
-| Coq_stat_switch (labs, e, sb) -> run_stat_switch runs0 s c labs e sb
+| Coq_stat_switch (labs, e, sb) -> run_stat_switch s c labs e sb
(** val run_elements :
- runs_type -> state -> execution_ctx -> elements -> result **)
+ state -> execution_ctx -> elements -> result **)
-let rec run_elements runs0 s c _foo_ = match _foo_ with
+and run_elements s c _foo_ = match _foo_ with
| [] -> result_out (Coq_out_ter (s, (res_normal Coq_resvalue_empty)))
| el :: els_rev' ->
- if_success (run_elements runs0 s c els_rev') (fun s0 rv0 ->
+ if_success (run_elements s c els_rev') (fun s0 rv0 ->
match el with
| Coq_element_stat t ->
- if_ter (runs0.runs_type_stat s0 c t) (fun s1 r1 ->
+ if_ter (run_stat s0 c t) (fun s1 r1 ->
let r2 = res_overwrite_value_if_empty rv0 r1 in
res_out (Coq_out_ter (s1, r2)))
| Coq_element_func_decl (name, args, bd) -> res_ter s0 (res_normal rv0))
-(** val run_prog : runs_type -> state -> execution_ctx -> prog -> result **)
+(** val run_prog : state -> execution_ctx -> prog -> result **)
-let run_prog runs0 s c _term_ = match _term_ with
-| Coq_prog_intro (str, els) -> run_elements runs0 s c (rev els)
+and run_prog s c _term_ = match _term_ with
+| Coq_prog_intro (str, els) -> run_elements s c (rev els)
(** val push :
- runs_type -> state -> execution_ctx -> object_loc -> value list -> float
+ state -> execution_ctx -> object_loc -> value list -> float
-> result **)
-let rec push runs0 s c l args ilen =
+and push s c l args ilen =
let_binding (of_int ilen) (fun vlen ->
match args with
| [] ->
if_not_throw
- (object_put runs0 s c l ("length")
+ (object_put s c l ("length")
(Coq_value_prim (Coq_prim_number vlen)) throw_true) (fun s0 x ->
result_out (Coq_out_ter (s0,
(res_val (Coq_value_prim (Coq_prim_number vlen))))))
| v :: vs ->
- if_string (to_string runs0 s c (Coq_value_prim (Coq_prim_number vlen)))
+ if_string (to_string s c (Coq_value_prim (Coq_prim_number vlen)))
(fun s0 slen ->
- if_not_throw (object_put runs0 s0 c l slen v throw_true) (fun s1 x ->
- push runs0 s1 c l vs (ilen +. 1.))))
+ if_not_throw (object_put s0 c l slen v throw_true) (fun s1 x ->
+ push s1 c l vs (ilen +. 1.))))
(** val run_object_is_sealed :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
+ state -> execution_ctx -> object_loc -> prop_name list ->
result **)
-let rec run_object_is_sealed runs0 s c l _foo_ = match _foo_ with
+and run_object_is_sealed s c l _foo_ = match _foo_ with
| [] ->
if_some (run_object_method object_extensible_ s l) (fun ext ->
res_ter s (res_val (Coq_value_prim (Coq_prim_bool (neg ext)))))
| x :: xs' ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s0 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s0 d ->
match d with
| Coq_full_descriptor_undef ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4859,18 +4649,18 @@ let rec run_object_is_sealed runs0 s c l _foo_ = match _foo_ with
| Coq_full_descriptor_some a ->
if attributes_configurable a
then res_ter s0 (res_val (Coq_value_prim (Coq_prim_bool false)))
- else run_object_is_sealed runs0 s0 c l xs')
+ else run_object_is_sealed s0 c l xs')
(** val run_object_seal :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
+ state -> execution_ctx -> object_loc -> prop_name list ->
result **)
-let rec run_object_seal runs0 s c l _foo_ = match _foo_ with
+and run_object_seal s c l _foo_ = match _foo_ with
| [] ->
if_some (run_object_heap_set_extensible false s l) (fun s0 ->
res_ter s0 (res_val (Coq_value_object l)))
| x :: xs' ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s0 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s0 d ->
match d with
| Coq_full_descriptor_undef ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4888,19 +4678,19 @@ let rec run_object_seal runs0 s c l _foo_ = match _foo_ with
else a
in
if_bool
- (object_define_own_prop runs0 s0 c l x (descriptor_of_attributes a')
- true) (fun s1 x0 -> run_object_seal runs0 s1 c l xs'))
+ (object_define_own_prop s0 c l x (descriptor_of_attributes a')
+ true) (fun s1 x0 -> run_object_seal s1 c l xs'))
(** val run_object_freeze :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
+ state -> execution_ctx -> object_loc -> prop_name list ->
result **)
-let rec run_object_freeze runs0 s c l _foo_ = match _foo_ with
+and run_object_freeze s c l _foo_ = match _foo_ with
| [] ->
if_some (run_object_heap_set_extensible false s l) (fun s0 ->
res_ter s0 (res_val (Coq_value_object l)))
| x :: xs' ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s0 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s0 d ->
match d with
| Coq_full_descriptor_undef ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4928,23 +4718,23 @@ let rec run_object_freeze runs0 s c l _foo_ = match _foo_ with
else a'
in
if_bool
- (object_define_own_prop runs0 s0 c l x (descriptor_of_attributes a'')
- true) (fun s1 x0 -> run_object_freeze runs0 s1 c l xs'))
+ (object_define_own_prop s0 c l x (descriptor_of_attributes a'')
+ true) (fun s1 x0 -> run_object_freeze s1 c l xs'))
(** val run_object_is_frozen :
- runs_type -> state -> execution_ctx -> object_loc -> prop_name list ->
+ state -> execution_ctx -> object_loc -> prop_name list ->
result **)
-let rec run_object_is_frozen runs0 s c l _foo_ = match _foo_ with
+and run_object_is_frozen s c l _foo_ = match _foo_ with
| [] ->
if_some (run_object_method object_extensible_ s l) (fun ext ->
res_ter s (res_val (Coq_value_prim (Coq_prim_bool (neg ext)))))
| x :: xs' ->
- if_spec (runs0.runs_type_object_get_own_prop s c l x) (fun s0 d ->
+ if_spec (run_object_get_own_prop s c l x) (fun s0 d ->
let_binding (fun a ->
if attributes_configurable a
then res_ter s0 (res_val (Coq_value_prim (Coq_prim_bool false)))
- else run_object_is_frozen runs0 s0 c l xs') (fun check_configurable ->
+ else run_object_is_frozen s0 c l xs') (fun check_configurable ->
match d with
| Coq_full_descriptor_undef ->
(fun s m -> Debug.impossible_with_heap_because __LOC__ s m; Coq_result_impossible)
@@ -4960,63 +4750,63 @@ let rec run_object_is_frozen runs0 s c l _foo_ = match _foo_ with
check_configurable (Coq_attributes_accessor_of aa))))
(** val run_get_args_for_apply :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
+ state -> execution_ctx -> object_loc -> float -> float ->
value list specres **)
-let run_get_args_for_apply runs0 s c l index n =
+and run_get_args_for_apply s c l index n =
if index < n
then if_string
- (to_string runs0 s c (Coq_value_prim (Coq_prim_number
+ (to_string s c (Coq_value_prim (Coq_prim_number
(of_int index)))) (fun s0 sindex ->
- if_value (run_object_get runs0 s0 c l sindex) (fun s1 v ->
+ if_value (run_object_get s0 c l sindex) (fun s1 v ->
let_binding
- (runs0.runs_type_get_args_for_apply s1 c l (index +. 1.) n)
+ (run_get_args_for_apply s1 c l (index +. 1.) n)
(fun tail_args ->
if_spec tail_args (fun s2 tail -> res_spec s2 (v :: tail)))))
else res_spec s []
(** val valueToStringForJoin :
- runs_type -> state -> execution_ctx -> object_loc -> float -> string
+ state -> execution_ctx -> object_loc -> float -> string
specres **)
-let valueToStringForJoin runs0 s c l k =
+and valueToStringForJoin s c l k =
if_string
- (to_string runs0 s c (Coq_value_prim (Coq_prim_number (of_int k))))
+ (to_string s c (Coq_value_prim (Coq_prim_number (of_int k))))
(fun s0 prop ->
- if_value (run_object_get runs0 s0 c l prop) (fun s1 v ->
+ if_value (run_object_get s0 c l prop) (fun s1 v ->
match v with
| Coq_value_prim p ->
(match p with
| Coq_prim_undef -> res_spec s1 ""
| Coq_prim_null -> res_spec s1 ""
| Coq_prim_bool b ->
- if_string (to_string runs0 s1 c v) (fun s2 s3 -> res_spec s2 s3)
+ if_string (to_string s1 c v) (fun s2 s3 -> res_spec s2 s3)
| Coq_prim_number n ->
- if_string (to_string runs0 s1 c v) (fun s2 s3 -> res_spec s2 s3)
+ if_string (to_string s1 c v) (fun s2 s3 -> res_spec s2 s3)
| Coq_prim_string s2 ->
- if_string (to_string runs0 s1 c v) (fun s3 s4 -> res_spec s3 s4))
+ if_string (to_string s1 c v) (fun s3 s4 -> res_spec s3 s4))
| Coq_value_object o ->
- if_string (to_string runs0 s1 c v) (fun s2 s3 -> res_spec s2 s3)))
+ if_string (to_string s1 c v) (fun s2 s3 -> res_spec s2 s3)))
(** val run_array_join_elements :
- runs_type -> state -> execution_ctx -> object_loc -> float -> float ->
+ state -> execution_ctx -> object_loc -> float -> float ->
string -> string -> result **)
-let run_array_join_elements runs0 s c l k length0 sep sR =
+and run_array_join_elements s c l k length0 sep sR =
if k < length0
then let_binding (strappend sR sep) (fun ss ->
- let_binding (valueToStringForJoin runs0 s c l k) (fun sE ->
+ let_binding (valueToStringForJoin s c l k) (fun sE ->
if_spec sE (fun s0 element ->
let_binding (strappend ss element) (fun sR0 ->
- runs0.runs_type_array_join_elements s0 c l (k +. 1.)
+ run_array_join_elements s0 c l (k +. 1.)
length0 sep sR0))))
else res_ter s (res_val (Coq_value_prim (Coq_prim_string sR)))
(** val run_call_prealloc :
- runs_type -> state -> execution_ctx -> prealloc -> value -> value list ->
+ state -> execution_ctx -> prealloc -> value -> value list ->
result **)
-let run_call_prealloc runs0 s c b vthis args =
+and run_call_prealloc s c b vthis args =
match b with
| Coq_prealloc_global ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -5044,7 +4834,7 @@ let run_call_prealloc runs0 s c b vthis args =
(" not yet implemented")))
| Coq_prealloc_global_is_finite ->
let_binding (get_arg 0 args) (fun v ->
- if_number (to_number runs0 s c v) (fun s0 n ->
+ if_number (to_number s c v) (fun s0 n ->
res_ter s0
(res_val (Coq_value_prim (Coq_prim_bool
(neg
@@ -5053,7 +4843,7 @@ let run_call_prealloc runs0 s c b vthis args =
(number_comparable n JsNumber.neg_infinity)))))))))
| Coq_prealloc_global_is_nan ->
let_binding (get_arg 0 args) (fun v ->
- if_number (to_number runs0 s c v) (fun s0 n ->
+ if_number (to_number s c v) (fun s0 n ->
res_ter s0
(res_val (Coq_value_prim (Coq_prim_bool
(number_comparable n JsNumber.nan))))))
@@ -5086,8 +4876,8 @@ let run_call_prealloc runs0 s c b vthis args =
match value0 with
| Coq_value_prim p ->
(match p with
- | Coq_prim_undef -> run_construct_prealloc runs0 s c b args
- | Coq_prim_null -> run_construct_prealloc runs0 s c b args
+ | Coq_prim_undef -> run_construct_prealloc s c b args
+ | Coq_prim_null -> run_construct_prealloc s c b args
| Coq_prim_bool b0 -> to_object s value0
| Coq_prim_number n -> to_object s value0
| Coq_prim_string s0 -> to_object s value0)
@@ -5104,10 +4894,10 @@ let run_call_prealloc runs0 s c b vthis args =
match v with
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object l ->
- if_string (to_string runs0 s c (get_arg 1 args))
+ if_string (to_string s c (get_arg 1 args))
(fun s1 x ->
- if_spec (runs0.runs_type_object_get_own_prop s1 c l x) (fun s2 d ->
- from_prop_descriptor runs0 s2 c d)))
+ if_spec (run_object_get_own_prop s1 c l x) (fun s2 d ->
+ from_prop_descriptor s2 c d)))
| Coq_prealloc_object_get_own_prop_name ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
(strappend
@@ -5128,9 +4918,9 @@ let run_call_prealloc runs0 s c b vthis args =
match o with
| Coq_value_prim p0 -> run_error s Coq_native_error_type
| Coq_value_object l ->
- if_string (to_string runs0 s c p) (fun s1 name ->
- if_spec (run_to_descriptor runs0 s1 c attr) (fun s2 desc ->
- if_bool (object_define_own_prop runs0 s2 c l name desc true)
+ if_string (to_string s c p) (fun s1 name ->
+ if_spec (run_to_descriptor s1 c attr) (fun s2 desc ->
+ if_bool (object_define_own_prop s2 c l name desc true)
(fun s3 x -> res_ter s3 (res_val (Coq_value_object l))))))))
| Coq_prealloc_object_define_props ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -5144,14 +4934,14 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object l ->
if_some (object_properties_keys_as_list_pickable_option s l)
- (fun _x_ -> run_object_seal runs0 s c l _x_))
+ (fun _x_ -> run_object_seal s c l _x_))
| Coq_prealloc_object_freeze ->
let_binding (get_arg 0 args) (fun v ->
match v with
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object l ->
if_some (object_properties_keys_as_list_pickable_option s l)
- (fun _x_ -> run_object_freeze runs0 s c l _x_))
+ (fun _x_ -> run_object_freeze s c l _x_))
| Coq_prealloc_object_prevent_extensions ->
let_binding (get_arg 0 args) (fun v ->
match v with
@@ -5167,14 +4957,14 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object l ->
if_some (object_properties_keys_as_list_pickable_option s l)
- (fun _x_ -> run_object_is_sealed runs0 s c l _x_))
+ (fun _x_ -> run_object_is_sealed s c l _x_))
| Coq_prealloc_object_is_frozen ->
let_binding (get_arg 0 args) (fun v ->
match v with
| Coq_value_prim p -> run_error s Coq_native_error_type
| Coq_value_object l ->
if_some (object_properties_keys_as_list_pickable_option s l)
- (fun _x_ -> run_object_is_frozen runs0 s c l _x_))
+ (fun _x_ -> run_object_is_frozen s c l _x_))
| Coq_prealloc_object_is_extensible ->
let_binding (get_arg 0 args) (fun v ->
match v with
@@ -5247,9 +5037,9 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_prealloc_object_proto_value_of -> to_object s vthis
| Coq_prealloc_object_proto_has_own_prop ->
let_binding (get_arg 0 args) (fun v ->
- if_string (to_string runs0 s c v) (fun s1 x ->
+ if_string (to_string s c v) (fun s1 x ->
if_object (to_object s1 vthis) (fun s2 l ->
- if_spec (runs0.runs_type_object_get_own_prop s2 c l x) (fun s3 d ->
+ if_spec (run_object_get_own_prop s2 c l x) (fun s3 d ->
match d with
| Coq_full_descriptor_undef ->
res_ter s3 (res_val (Coq_value_prim (Coq_prim_bool false)))
@@ -5263,12 +5053,12 @@ let run_call_prealloc runs0 s c b vthis args =
(res_val (Coq_value_prim (Coq_prim_bool false)))))
| Coq_value_object l ->
if_object (to_object s vthis) (fun s1 lo ->
- runs0.runs_type_object_proto_is_prototype_of s1 lo l))
+ object_proto_is_prototype_of s1 lo l))
| Coq_prealloc_object_proto_prop_is_enumerable ->
let_binding (get_arg 0 args) (fun v ->
- if_string (to_string runs0 s c v) (fun s1 x ->
+ if_string (to_string s c v) (fun s1 x ->
if_object (to_object s1 vthis) (fun s2 l ->
- if_spec (runs0.runs_type_object_get_own_prop s2 c l x) (fun s3 d ->
+ if_spec (run_object_get_own_prop s2 c l x) (fun s3 d ->
match d with
| Coq_full_descriptor_undef ->
res_ter s3 (res_val (Coq_value_prim (Coq_prim_bool false)))
@@ -5303,22 +5093,22 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_value_prim p ->
(match p with
| Coq_prim_undef ->
- runs0.runs_type_call s c thisobj thisArg []
+ run_call s c thisobj thisArg []
| Coq_prim_null ->
- runs0.runs_type_call s c thisobj thisArg []
+ run_call s c thisobj thisArg []
| Coq_prim_bool b0 -> run_error s Coq_native_error_type
| Coq_prim_number n -> run_error s Coq_native_error_type
| Coq_prim_string s0 -> run_error s Coq_native_error_type)
| Coq_value_object array ->
if_value
- (run_object_get runs0 s c array
+ (run_object_get s c array
("length"))
(fun s0 v ->
- if_spec (to_uint32 runs0 s0 c v) (fun s1 ilen ->
+ if_spec (to_uint32 s0 c v) (fun s1 ilen ->
if_spec
- (run_get_args_for_apply runs0 s1 c array 0. ilen)
+ (run_get_args_for_apply s1 c array 0. ilen)
(fun s2 arguments_ ->
- runs0.runs_type_call s2 c thisobj thisArg arguments_)))))
+ run_call s2 c thisobj thisArg arguments_)))))
else run_error s Coq_native_error_type))
| Coq_prealloc_function_proto_call ->
if is_callable_dec s vthis
@@ -5329,7 +5119,7 @@ let run_call_prealloc runs0 s c b vthis args =
("Value is callable, but isn\'t an object.")
| Coq_value_object thisobj ->
let (thisArg, a) = get_arg_first_and_rest args in
- runs0.runs_type_call s c thisobj thisArg a)
+ run_call s c thisobj thisArg a)
else run_error s Coq_native_error_type
| Coq_prealloc_function_proto_bind ->
if is_callable_dec s vthis
@@ -5372,11 +5162,11 @@ let run_call_prealloc runs0 s c b vthis args =
if string_comparable class0
("Function")
then if_number
- (run_object_get runs0 s' c thisobj
+ (run_object_get s' c thisobj
("length"))
(fun s'0 n ->
if_spec
- (to_int32 runs0 s'0 c (Coq_value_prim
+ (to_int32 s'0 c (Coq_value_prim
(Coq_prim_number n)))
(fun s'1 ilen ->
if ilen <
@@ -5412,13 +5202,13 @@ let run_call_prealloc runs0 s c b vthis args =
attributes_accessor_configurable =
false } (fun a1 ->
if_bool
- (object_define_own_prop runs0 s'1 c l
+ (object_define_own_prop s'1 c l
("caller")
(descriptor_of_attributes
(Coq_attributes_accessor_of a1))
false) (fun s'2 x ->
if_bool
- (object_define_own_prop runs0 s'2 c
+ (object_define_own_prop s'2 c
l
("arguments")
(descriptor_of_attributes
@@ -5513,7 +5303,7 @@ let run_call_prealloc runs0 s c b vthis args =
if list_eq_nil_decidable args
then result_out (Coq_out_ter (s,
(res_val (Coq_value_prim (Coq_prim_number JsNumber.zero)))))
- else let v = get_arg 0 args in to_number runs0 s c v
+ else let v = get_arg 0 args in to_number s c v
| Coq_prealloc_number_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
(strappend
@@ -5577,7 +5367,7 @@ let run_call_prealloc runs0 s c b vthis args =
(strappend (string_of_prealloc b)
(" not yet implemented")))
| Coq_prealloc_array ->
- run_construct_prealloc runs0 s c Coq_prealloc_array args
+ run_construct_prealloc s c Coq_prealloc_array args
| Coq_prealloc_array_is_array ->
let_binding (get_arg 0 args) (fun arg ->
match arg with
@@ -5597,7 +5387,7 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_prealloc_array_proto_to_string ->
if_object (to_object s vthis) (fun s0 array ->
if_value
- (run_object_get runs0 s0 c array ("join"))
+ (run_object_get s0 c array ("join"))
(fun s1 vfunc ->
if is_callable_dec s1 vfunc
then (match vfunc with
@@ -5606,54 +5396,54 @@ let run_call_prealloc runs0 s c b vthis args =
s1
("Value is callable, but isn\'t an object.")
| Coq_value_object func ->
- runs0.runs_type_call s1 c func (Coq_value_object array) [])
- else runs0.runs_type_call_prealloc s1 c
+ run_call s1 c func (Coq_value_object array) [])
+ else run_call_prealloc s1 c
Coq_prealloc_object_proto_to_string (Coq_value_object array)
[]))
| Coq_prealloc_array_proto_join ->
let_binding (get_arg 0 args) (fun vsep ->
if_object (to_object s vthis) (fun s0 l ->
if_value
- (run_object_get runs0 s0 c l
+ (run_object_get s0 c l
("length")) (fun s1 vlen ->
- if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
+ if_spec (to_uint32 s1 c vlen) (fun s2 ilen ->
let_binding
(if not_decidable
(value_comparable vsep (Coq_value_prim Coq_prim_undef))
then vsep
else Coq_value_prim (Coq_prim_string (","))) (fun rsep ->
- if_string (to_string runs0 s2 c rsep) (fun s3 sep ->
+ if_string (to_string s2 c rsep) (fun s3 sep ->
if ilen = 0.0
then res_ter s3
(res_val (Coq_value_prim (Coq_prim_string "")))
- else let_binding (valueToStringForJoin runs0 s3 c l 0.)
+ else let_binding (valueToStringForJoin s3 c l 0.)
(fun sR ->
if_spec sR (fun s4 sR0 ->
- run_array_join_elements runs0 s4 c l 1. ilen sep sR0))))))))
+ run_array_join_elements s4 c l 1. ilen sep sR0))))))))
| Coq_prealloc_array_proto_pop ->
if_object (to_object s vthis) (fun s0 l ->
if_value
- (run_object_get runs0 s0 c l
+ (run_object_get s0 c l
("length")) (fun s1 vlen ->
- if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
+ if_spec (to_uint32 s1 c vlen) (fun s2 ilen ->
if ilen = 0.0
then if_not_throw
- (object_put runs0 s2 c l
+ (object_put s2 c l
("length")
(Coq_value_prim (Coq_prim_number JsNumber.zero)) throw_true)
(fun s3 x ->
result_out (Coq_out_ter (s3,
(res_val (Coq_value_prim Coq_prim_undef)))))
else if_string
- (to_string runs0 s2 c (Coq_value_prim (Coq_prim_number
+ (to_string s2 c (Coq_value_prim (Coq_prim_number
(of_int (ilen -. 1.))))) (fun s3 sindx ->
- if_value (run_object_get runs0 s3 c l sindx)
+ if_value (run_object_get s3 c l sindx)
(fun s4 velem ->
if_not_throw
- (object_delete_default runs0 s4 c l sindx throw_true)
+ (object_delete_default s4 c l sindx throw_true)
(fun s5 x ->
if_not_throw
- (object_put runs0 s5 c l
+ (object_put s5 c l
("length")
(Coq_value_prim (Coq_prim_string sindx)) throw_true)
(fun s6 x0 ->
@@ -5661,15 +5451,15 @@ let run_call_prealloc runs0 s c b vthis args =
| Coq_prealloc_array_proto_push ->
if_object (to_object s vthis) (fun s0 l ->
if_value
- (run_object_get runs0 s0 c l
+ (run_object_get s0 c l
("length")) (fun s1 vlen ->
- if_spec (to_uint32 runs0 s1 c vlen) (fun s2 ilen ->
- push runs0 s2 c l args ilen)))
+ if_spec (to_uint32 s1 c vlen) (fun s2 ilen ->
+ push s2 c l args ilen)))
| Coq_prealloc_string ->
if list_eq_nil_decidable args
then res_ter s (res_val (Coq_value_prim (Coq_prim_string "")))
else let_binding (get_arg 0 args) (fun value0 ->
- if_string (to_string runs0 s c value0) (fun s0 s1 ->
+ if_string (to_string s c value0) (fun s0 s1 ->
res_ter s0 (res_val (Coq_value_prim (Coq_prim_string s1)))))
| Coq_prealloc_string_proto ->
(fun s -> Debug.not_yet_implemented_because __LOC__ s; Coq_result_impossible)
@@ -5770,14 +5560,14 @@ let run_call_prealloc runs0 s c b vthis args =
(" not yet implemented")))
(** val run_call :
- runs_type -> state -> execution_ctx -> object_loc -> value -> value list
+ state -> execution_ctx -> object_loc -> value -> value list
-> result **)
-let run_call runs0 s c l vthis args =
+and run_call s c l vthis args =
if_some (run_object_method object_call_ s l) (fun co ->
if_some co (fun c0 ->
match c0 with
- | Coq_call_default -> entering_func_code runs0 s c l vthis args
+ | Coq_call_default -> entering_func_code s c l vthis args
| Coq_call_after_bind ->
if_some (run_object_method object_bound_args_ s l) (fun oarg ->
if_some oarg (fun boundArgs ->
@@ -5788,42 +5578,14 @@ let run_call runs0 s c l vthis args =
if_some otrg (fun target ->
let_binding (LibList.append boundArgs args)
(fun arguments_ ->
- runs0.runs_type_call s c target boundThis arguments_)))))))
- | Coq_call_prealloc b -> run_call_prealloc runs0 s c b vthis args))
+ run_call s c target boundThis arguments_)))))))
+ | Coq_call_prealloc b -> run_call_prealloc s c b vthis args))
-(** val run_javascript : runs_type -> prog -> result **)
+(** val run_javascript : prog -> result **)
-let run_javascript runs0 p =
+and run_javascript p =
let p' = add_infos_prog strictness_false p in
let c = execution_ctx_initial (prog_intro_strictness p') in
if_void
- (execution_ctx_binding_inst runs0 state_initial c Coq_codetype_global
- None p' []) (fun s' -> runs0.runs_type_prog s' c p')
-
-(** val runs : int -> runs_type **)
-
-let rec runs =
- { runs_type_expr = (fun x y z -> run_expr runs x y z);
- runs_type_stat = (fun x y z -> run_stat runs x y z);
- runs_type_prog = (fun x y z -> run_prog runs x y z);
- runs_type_call = (fun x y z r t -> run_call runs x y z r t);
- runs_type_call_prealloc = (fun x y z r t -> run_call_prealloc runs x y z r t);
- runs_type_construct = (fun x y z r t -> run_construct runs x y z r t);
- runs_type_function_has_instance = (fun x y z -> run_function_has_instance runs x y z);
- runs_type_object_has_instance = (fun x y z r t -> run_object_has_instance runs x y z r t);
- runs_type_get_args_for_apply = (fun x y z r t -> run_get_args_for_apply runs x y z r t);
- runs_type_stat_while = (fun x y z r t s -> run_stat_while runs x y z r t s);
- runs_type_stat_do_while = (fun x y z r t s -> run_stat_do_while runs x y z r t s);
- runs_type_stat_for_loop = (fun x y z r t s v -> run_stat_for_loop runs x y z r t s v);
- runs_type_object_delete = (fun x y z r t -> object_delete runs x y z r t);
- runs_type_object_get_own_prop = (fun x y z r -> run_object_get_own_prop runs x y z r);
- runs_type_object_get_prop = (fun x y z r -> run_object_get_prop runs x y z r);
- runs_type_object_get = (fun x y z r -> run_object_get runs x y z r);
- runs_type_object_proto_is_prototype_of = (fun x y z -> object_proto_is_prototype_of runs x y z);
- runs_type_object_put = (fun x y z r s t -> object_put runs x y z r s t);
- runs_type_equal = (fun x y z r -> run_equal runs x y z r);
- runs_type_to_integer = (fun x y z -> to_integer runs x y z);
- runs_type_to_string = (fun x y z -> to_string runs x y z);
- runs_type_array_join_elements = (fun x y z r s t v -> run_array_join_elements runs x y z r s t v);
- runs_type_array_element_list = (fun x y z r s -> run_array_element_list runs x y z r s);
- runs_type_object_define_own_prop_array_loop = (fun x y z r s t u v w -> run_object_define_own_prop_array_loop runs x y z r s t u v w) }
+ (execution_ctx_binding_inst state_initial c Coq_codetype_global
+ None p' []) (fun s' -> run_prog s' c p')